Metamath Proof Explorer

Theorem cxpadd

Description: Sum of exponents law for complex exponentiation. Proposition 10-4.2(a) of Gleason p. 135. (Contributed by Mario Carneiro, 2-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> B e. CC )
2 simp3 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> C e. CC )
3 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
4 3 3ad2ant1 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( log ` A ) e. CC )
5 1 2 4 adddird 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( ( B + C ) x. ( log ` A ) ) = ( ( B x. ( log ` A ) ) + ( C x. ( log ` A ) ) ) )
6 5 fveq2d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( exp ` ( ( B + C ) x. ( log ` A ) ) ) = ( exp ` ( ( B x. ( log ` A ) ) + ( C x. ( log ` A ) ) ) ) )
7 1 4 mulcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( B x. ( log ` A ) ) e. CC )
8 2 4 mulcld 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( C x. ( log ` A ) ) e. CC )
9 efadd 
 |-  ( ( ( B x. ( log ` A ) ) e. CC /\ ( C x. ( log ` A ) ) e. CC ) -> ( exp ` ( ( B x. ( log ` A ) ) + ( C x. ( log ` A ) ) ) ) = ( ( exp ` ( B x. ( log ` A ) ) ) x. ( exp ` ( C x. ( log ` A ) ) ) ) )
10 7 8 9 syl2anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( exp ` ( ( B x. ( log ` A ) ) + ( C x. ( log ` A ) ) ) ) = ( ( exp ` ( B x. ( log ` A ) ) ) x. ( exp ` ( C x. ( log ` A ) ) ) ) )
11 6 10 eqtrd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( exp ` ( ( B + C ) x. ( log ` A ) ) ) = ( ( exp ` ( B x. ( log ` A ) ) ) x. ( exp ` ( C x. ( log ` A ) ) ) ) )
12 simp1l 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> A e. CC )
13 simp1r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> A =/= 0 )
14 addcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B + C ) e. CC )
15 14 3adant1 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( B + C ) e. CC )
16 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( B + C ) e. CC ) -> ( A ^c ( B + C ) ) = ( exp ` ( ( B + C ) x. ( log ` A ) ) ) )
17 12 13 15 16 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B + C ) ) = ( exp ` ( ( B + C ) x. ( log ` A ) ) ) )
18 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
19 12 13 1 18 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
20 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ C e. CC ) -> ( A ^c C ) = ( exp ` ( C x. ( log ` A ) ) ) )
21 12 13 2 20 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c C ) = ( exp ` ( C x. ( log ` A ) ) ) )
22 19 21 oveq12d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( ( A ^c B ) x. ( A ^c C ) ) = ( ( exp ` ( B x. ( log ` A ) ) ) x. ( exp ` ( C x. ( log ` A ) ) ) ) )
23 11 17 22 3eqtr4d 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B + C ) ) = ( ( A ^c B ) x. ( A ^c C ) ) )