This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem expp1

Description: Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of Gleason p. 134. When A is nonzero, this holds for all integers N , see expneg . (Contributed by NM, 20-May-2005) (Revised by Mario Carneiro, 2-Jul-2013)

Ref Expression
Assertion expp1 ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 elnn0 ⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 seqp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) · ( ( ℕ × { 𝐴 } ) ‘ ( 𝑁 + 1 ) ) ) )
3 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
4 2 3 eleq2s ⊢ ( 𝑁 ∈ ℕ → ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) · ( ( ℕ × { 𝐴 } ) ‘ ( 𝑁 + 1 ) ) ) )
5 4 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) · ( ( ℕ × { 𝐴 } ) ‘ ( 𝑁 + 1 ) ) ) )
6 peano2nn ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 + 1 ) ∈ ℕ )
7 fvconst2g ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℕ ) → ( ( ℕ × { 𝐴 } ) ‘ ( 𝑁 + 1 ) ) = 𝐴 )
8 6 7 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( ℕ × { 𝐴 } ) ‘ ( 𝑁 + 1 ) ) = 𝐴 )
9 8 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) · ( ( ℕ × { 𝐴 } ) ‘ ( 𝑁 + 1 ) ) ) = ( ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) · 𝐴 ) )
10 5 9 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑁 + 1 ) ) = ( ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) · 𝐴 ) )
11 expnnval ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 + 1 ) ∈ ℕ ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑁 + 1 ) ) )
12 6 11 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ ( 𝑁 + 1 ) ) )
13 expnnval ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ 𝑁 ) = ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) )
14 13 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) = ( ( seq 1 ( · , ( ℕ × { 𝐴 } ) ) ‘ 𝑁 ) · 𝐴 ) )
15 10 12 14 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) )
16 exp1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
17 mullid ⊢ ( 𝐴 ∈ ℂ → ( 1 · 𝐴 ) = 𝐴 )
18 16 17 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = ( 1 · 𝐴 ) )
19 18 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 1 ) = ( 1 · 𝐴 ) )
20 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → 𝑁 = 0 )
21 20 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝑁 + 1 ) = ( 0 + 1 ) )
22 0p1e1 ⊢ ( 0 + 1 ) = 1
23 21 22 eqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝑁 + 1 ) = 1 )
24 23 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( 𝐴 ↑ 1 ) )
25 oveq2 ⊢ ( 𝑁 = 0 → ( 𝐴 ↑ 𝑁 ) = ( 𝐴 ↑ 0 ) )
26 exp0 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
27 25 26 sylan9eqr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ 𝑁 ) = 1 )
28 27 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) = ( 1 · 𝐴 ) )
29 19 24 28 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 = 0 ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) )
30 15 29 jaodan ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) )
31 1 30 sylan2b ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 ↑ ( 𝑁 + 1 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) )