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 ) ) = ( ( 𝐴 ↑ 𝑁 ) · 𝐴 ) )