Metamath Proof Explorer

Theorem efsub

Description: Difference of exponents law for exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007)

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

Proof

Step Hyp Ref Expression
1 efcl 
 |-  ( A e. CC -> ( exp ` A ) e. CC )
2 efcl 
 |-  ( B e. CC -> ( exp ` B ) e. CC )
3 efne0 
 |-  ( B e. CC -> ( exp ` B ) =/= 0 )
4 divrec 
 |-  ( ( ( exp ` A ) e. CC /\ ( exp ` B ) e. CC /\ ( exp ` B ) =/= 0 ) -> ( ( exp ` A ) / ( exp ` B ) ) = ( ( exp ` A ) x. ( 1 / ( exp ` B ) ) ) )
5 1 2 3 4 syl3an 
 |-  ( ( A e. CC /\ B e. CC /\ B e. CC ) -> ( ( exp ` A ) / ( exp ` B ) ) = ( ( exp ` A ) x. ( 1 / ( exp ` B ) ) ) )
6 5 3anidm23 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( exp ` A ) / ( exp ` B ) ) = ( ( exp ` A ) x. ( 1 / ( exp ` B ) ) ) )
7 efcan 
 |-  ( B e. CC -> ( ( exp ` B ) x. ( exp ` -u B ) ) = 1 )
8 7 eqcomd 
 |-  ( B e. CC -> 1 = ( ( exp ` B ) x. ( exp ` -u B ) ) )
9 negcl 
 |-  ( B e. CC -> -u B e. CC )
10 efcl 
 |-  ( -u B e. CC -> ( exp ` -u B ) e. CC )
11 9 10 syl 
 |-  ( B e. CC -> ( exp ` -u B ) e. CC )
12 ax-1cn 
 |-  1 e. CC
13 divmul2 
 |-  ( ( 1 e. CC /\ ( exp ` -u B ) e. CC /\ ( ( exp ` B ) e. CC /\ ( exp ` B ) =/= 0 ) ) -> ( ( 1 / ( exp ` B ) ) = ( exp ` -u B ) <-> 1 = ( ( exp ` B ) x. ( exp ` -u B ) ) ) )
14 12 13 mp3an1 
 |-  ( ( ( exp ` -u B ) e. CC /\ ( ( exp ` B ) e. CC /\ ( exp ` B ) =/= 0 ) ) -> ( ( 1 / ( exp ` B ) ) = ( exp ` -u B ) <-> 1 = ( ( exp ` B ) x. ( exp ` -u B ) ) ) )
15 11 2 3 14 syl12anc 
 |-  ( B e. CC -> ( ( 1 / ( exp ` B ) ) = ( exp ` -u B ) <-> 1 = ( ( exp ` B ) x. ( exp ` -u B ) ) ) )
16 8 15 mpbird 
 |-  ( B e. CC -> ( 1 / ( exp ` B ) ) = ( exp ` -u B ) )
17 16 oveq2d 
 |-  ( B e. CC -> ( ( exp ` A ) x. ( 1 / ( exp ` B ) ) ) = ( ( exp ` A ) x. ( exp ` -u B ) ) )
18 17 adantl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( exp ` A ) x. ( 1 / ( exp ` B ) ) ) = ( ( exp ` A ) x. ( exp ` -u B ) ) )
19 efadd 
 |-  ( ( A e. CC /\ -u B e. CC ) -> ( exp ` ( A + -u B ) ) = ( ( exp ` A ) x. ( exp ` -u B ) ) )
20 9 19 sylan2 
 |-  ( ( A e. CC /\ B e. CC ) -> ( exp ` ( A + -u B ) ) = ( ( exp ` A ) x. ( exp ` -u B ) ) )
21 18 20 eqtr4d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( exp ` A ) x. ( 1 / ( exp ` B ) ) ) = ( exp ` ( A + -u B ) ) )
22 negsub 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + -u B ) = ( A - B ) )
23 22 fveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( exp ` ( A + -u B ) ) = ( exp ` ( A - B ) ) )
24 6 21 23 3eqtrrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( exp ` ( A - B ) ) = ( ( exp ` A ) / ( exp ` B ) ) )