Metamath Proof Explorer

Theorem cxpp1

Description: Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion cxpp1 
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c ( B + 1 ) ) = ( ( A ^c B ) x. A ) )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 cxpadd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ 1 e. CC ) -> ( A ^c ( B + 1 ) ) = ( ( A ^c B ) x. ( A ^c 1 ) ) )
3 1 2 mp3an3 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC ) -> ( A ^c ( B + 1 ) ) = ( ( A ^c B ) x. ( A ^c 1 ) ) )
4 3 3impa 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c ( B + 1 ) ) = ( ( A ^c B ) x. ( A ^c 1 ) ) )
5 cxp1 
 |-  ( A e. CC -> ( A ^c 1 ) = A )
6 5 3ad2ant1 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c 1 ) = A )
7 6 oveq2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( ( A ^c B ) x. ( A ^c 1 ) ) = ( ( A ^c B ) x. A ) )
8 4 7 eqtrd 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c ( B + 1 ) ) = ( ( A ^c B ) x. A ) )