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. (Contributed by NM, 20-May-2005) (Revised by Mario Carneiro, 2-Jul-2013)

Ref Expression
Assertion expp1 ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {{A}}^{{N}+1}={{A}}^{{N}}{A}$

Proof

Step Hyp Ref Expression
1 elnn0 ${⊢}{N}\in {ℕ}_{0}↔\left({N}\in ℕ\vee {N}=0\right)$
2 seqp1 ${⊢}{N}\in {ℤ}_{\ge 1}\to seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}+1\right)=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)\left(ℕ×\left\{{A}\right\}\right)\left({N}+1\right)$
3 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
4 2 3 eleq2s ${⊢}{N}\in ℕ\to seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}+1\right)=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)\left(ℕ×\left\{{A}\right\}\right)\left({N}+1\right)$
5 4 adantl ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}+1\right)=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)\left(ℕ×\left\{{A}\right\}\right)\left({N}+1\right)$
6 peano2nn ${⊢}{N}\in ℕ\to {N}+1\in ℕ$
7 fvconst2g ${⊢}\left({A}\in ℂ\wedge {N}+1\in ℕ\right)\to \left(ℕ×\left\{{A}\right\}\right)\left({N}+1\right)={A}$
8 6 7 sylan2 ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to \left(ℕ×\left\{{A}\right\}\right)\left({N}+1\right)={A}$
9 8 oveq2d ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)\left(ℕ×\left\{{A}\right\}\right)\left({N}+1\right)=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right){A}$
10 5 9 eqtrd ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}+1\right)=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right){A}$
11 expnnval ${⊢}\left({A}\in ℂ\wedge {N}+1\in ℕ\right)\to {{A}}^{{N}+1}=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}+1\right)$
12 6 11 sylan2 ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to {{A}}^{{N}+1}=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}+1\right)$
13 expnnval ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to {{A}}^{{N}}=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right)$
14 13 oveq1d ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to {{A}}^{{N}}{A}=seq1\left(×,\left(ℕ×\left\{{A}\right\}\right)\right)\left({N}\right){A}$
15 10 12 14 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {N}\in ℕ\right)\to {{A}}^{{N}+1}={{A}}^{{N}}{A}$
16 exp1 ${⊢}{A}\in ℂ\to {{A}}^{1}={A}$
17 mulid2 ${⊢}{A}\in ℂ\to 1{A}={A}$
18 16 17 eqtr4d ${⊢}{A}\in ℂ\to {{A}}^{1}=1{A}$
19 18 adantr ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {{A}}^{1}=1{A}$
20 simpr ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {N}=0$
21 20 oveq1d ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {N}+1=0+1$
22 0p1e1 ${⊢}0+1=1$
23 21 22 eqtrdi ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {N}+1=1$
24 23 oveq2d ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {{A}}^{{N}+1}={{A}}^{1}$
25 oveq2 ${⊢}{N}=0\to {{A}}^{{N}}={{A}}^{0}$
26 exp0 ${⊢}{A}\in ℂ\to {{A}}^{0}=1$
27 25 26 sylan9eqr ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {{A}}^{{N}}=1$
28 27 oveq1d ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {{A}}^{{N}}{A}=1{A}$
29 19 24 28 3eqtr4d ${⊢}\left({A}\in ℂ\wedge {N}=0\right)\to {{A}}^{{N}+1}={{A}}^{{N}}{A}$
30 15 29 jaodan ${⊢}\left({A}\in ℂ\wedge \left({N}\in ℕ\vee {N}=0\right)\right)\to {{A}}^{{N}+1}={{A}}^{{N}}{A}$
31 1 30 sylan2b ${⊢}\left({A}\in ℂ\wedge {N}\in {ℕ}_{0}\right)\to {{A}}^{{N}+1}={{A}}^{{N}}{A}$