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 ) ) )