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 
|- ( ( A e. CC /\ N e. NN0 ) -> ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 seqp1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( seq 1 ( x. , ( NN X. { A } ) ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) x. ( ( NN X. { A } ) ` ( N + 1 ) ) ) )
3 nnuz 
 |-  NN = ( ZZ>= ` 1 )
4 2 3 eleq2s 
 |-  ( N e. NN -> ( seq 1 ( x. , ( NN X. { A } ) ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) x. ( ( NN X. { A } ) ` ( N + 1 ) ) ) )
5 4 adantl 
 |-  ( ( A e. CC /\ N e. NN ) -> ( seq 1 ( x. , ( NN X. { A } ) ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) x. ( ( NN X. { A } ) ` ( N + 1 ) ) ) )
6 peano2nn 
 |-  ( N e. NN -> ( N + 1 ) e. NN )
7 fvconst2g 
 |-  ( ( A e. CC /\ ( N + 1 ) e. NN ) -> ( ( NN X. { A } ) ` ( N + 1 ) ) = A )
8 6 7 sylan2 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( NN X. { A } ) ` ( N + 1 ) ) = A )
9 8 oveq2d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) x. ( ( NN X. { A } ) ` ( N + 1 ) ) ) = ( ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) x. A ) )
10 5 9 eqtrd 
 |-  ( ( A e. CC /\ N e. NN ) -> ( seq 1 ( x. , ( NN X. { A } ) ) ` ( N + 1 ) ) = ( ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) x. A ) )
11 expnnval 
 |-  ( ( A e. CC /\ ( N + 1 ) e. NN ) -> ( A ^ ( N + 1 ) ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` ( N + 1 ) ) )
12 6 11 sylan2 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ ( N + 1 ) ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` ( N + 1 ) ) )
13 expnnval 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) )
14 13 oveq1d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( ( A ^ N ) x. A ) = ( ( seq 1 ( x. , ( NN X. { A } ) ) ` N ) x. A ) )
15 10 12 14 3eqtr4d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) )
16 exp1 
 |-  ( A e. CC -> ( A ^ 1 ) = A )
17 mullid 
 |-  ( A e. CC -> ( 1 x. A ) = A )
18 16 17 eqtr4d 
 |-  ( A e. CC -> ( A ^ 1 ) = ( 1 x. A ) )
19 18 adantr 
 |-  ( ( A e. CC /\ N = 0 ) -> ( A ^ 1 ) = ( 1 x. A ) )
20 simpr 
 |-  ( ( A e. CC /\ N = 0 ) -> N = 0 )
21 20 oveq1d 
 |-  ( ( A e. CC /\ N = 0 ) -> ( N + 1 ) = ( 0 + 1 ) )
22 0p1e1 
 |-  ( 0 + 1 ) = 1
23 21 22 eqtrdi 
 |-  ( ( A e. CC /\ N = 0 ) -> ( N + 1 ) = 1 )
24 23 oveq2d 
 |-  ( ( A e. CC /\ N = 0 ) -> ( A ^ ( N + 1 ) ) = ( A ^ 1 ) )
25 oveq2 
 |-  ( N = 0 -> ( A ^ N ) = ( A ^ 0 ) )
26 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
27 25 26 sylan9eqr 
 |-  ( ( A e. CC /\ N = 0 ) -> ( A ^ N ) = 1 )
28 27 oveq1d 
 |-  ( ( A e. CC /\ N = 0 ) -> ( ( A ^ N ) x. A ) = ( 1 x. A ) )
29 19 24 28 3eqtr4d 
 |-  ( ( A e. CC /\ N = 0 ) -> ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) )
30 15 29 jaodan 
 |-  ( ( A e. CC /\ ( N e. NN \/ N = 0 ) ) -> ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) )
31 1 30 sylan2b 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A ^ ( N + 1 ) ) = ( ( A ^ N ) x. A ) )