Metamath Proof Explorer

Theorem expm1t

Description: Exponentiation in terms of predecessor exponent. (Contributed by NM, 19-Dec-2005)

Ref Expression
Assertion expm1t 
|- ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = ( ( A ^ ( N - 1 ) ) x. A ) )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( N e. NN -> N e. CC )
2 ax-1cn 
 |-  1 e. CC
3 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
4 1 2 3 sylancl 
 |-  ( N e. NN -> ( ( N - 1 ) + 1 ) = N )
5 4 oveq2d 
 |-  ( N e. NN -> ( A ^ ( ( N - 1 ) + 1 ) ) = ( A ^ N ) )
6 5 adantl 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ ( ( N - 1 ) + 1 ) ) = ( A ^ N ) )
7 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
8 expp1 
 |-  ( ( A e. CC /\ ( N - 1 ) e. NN0 ) -> ( A ^ ( ( N - 1 ) + 1 ) ) = ( ( A ^ ( N - 1 ) ) x. A ) )
9 7 8 sylan2 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ ( ( N - 1 ) + 1 ) ) = ( ( A ^ ( N - 1 ) ) x. A ) )
10 6 9 eqtr3d 
 |-  ( ( A e. CC /\ N e. NN ) -> ( A ^ N ) = ( ( A ^ ( N - 1 ) ) x. A ) )