Metamath Proof Explorer

Theorem efadd

Description: Sum of exponents law for exponential function. (Contributed by NM, 10-Jan-2006) (Proof shortened by Mario Carneiro, 29-Apr-2014)

Ref Expression
Assertion efadd 
|- ( ( A e. CC /\ B e. CC ) -> ( exp ` ( A + B ) ) = ( ( exp ` A ) x. ( exp ` B ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2 eqid 
 |-  ( n e. NN0 |-> ( ( B ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( B ^ n ) / ( ! ` n ) ) )
3 eqid 
 |-  ( n e. NN0 |-> ( ( ( A + B ) ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( ( A + B ) ^ n ) / ( ! ` n ) ) )
4 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
5 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
6 1 2 3 4 5 efaddlem 
 |-  ( ( A e. CC /\ B e. CC ) -> ( exp ` ( A + B ) ) = ( ( exp ` A ) x. ( exp ` B ) ) )