Metamath Proof Explorer

Theorem efsub

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

Ref Expression
Assertion efsub ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( 𝐴 − 𝐵 ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 efcl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ )
2 efcl ⊢ ( 𝐵 ∈ ℂ → ( exp ‘ 𝐵 ) ∈ ℂ )
3 efne0 ⊢ ( 𝐵 ∈ ℂ → ( exp ‘ 𝐵 ) ≠ 0 )
4 divrec ⊢ ( ( ( exp ‘ 𝐴 ) ∈ ℂ ∧ ( exp ‘ 𝐵 ) ∈ ℂ ∧ ( exp ‘ 𝐵 ) ≠ 0 ) → ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( 1 / ( exp ‘ 𝐵 ) ) ) )
5 1 2 3 4 syl3an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( 1 / ( exp ‘ 𝐵 ) ) ) )
6 5 3anidm23 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( 1 / ( exp ‘ 𝐵 ) ) ) )
7 efcan ⊢ ( 𝐵 ∈ ℂ → ( ( exp ‘ 𝐵 ) · ( exp ‘ - 𝐵 ) ) = 1 )
8 7 eqcomd ⊢ ( 𝐵 ∈ ℂ → 1 = ( ( exp ‘ 𝐵 ) · ( exp ‘ - 𝐵 ) ) )
9 negcl ⊢ ( 𝐵 ∈ ℂ → - 𝐵 ∈ ℂ )
10 efcl ⊢ ( - 𝐵 ∈ ℂ → ( exp ‘ - 𝐵 ) ∈ ℂ )
11 9 10 syl ⊢ ( 𝐵 ∈ ℂ → ( exp ‘ - 𝐵 ) ∈ ℂ )
12 ax-1cn ⊢ 1 ∈ ℂ
13 divmul2 ⊢ ( ( 1 ∈ ℂ ∧ ( exp ‘ - 𝐵 ) ∈ ℂ ∧ ( ( exp ‘ 𝐵 ) ∈ ℂ ∧ ( exp ‘ 𝐵 ) ≠ 0 ) ) → ( ( 1 / ( exp ‘ 𝐵 ) ) = ( exp ‘ - 𝐵 ) ↔ 1 = ( ( exp ‘ 𝐵 ) · ( exp ‘ - 𝐵 ) ) ) )
14 12 13 mp3an1 ⊢ ( ( ( exp ‘ - 𝐵 ) ∈ ℂ ∧ ( ( exp ‘ 𝐵 ) ∈ ℂ ∧ ( exp ‘ 𝐵 ) ≠ 0 ) ) → ( ( 1 / ( exp ‘ 𝐵 ) ) = ( exp ‘ - 𝐵 ) ↔ 1 = ( ( exp ‘ 𝐵 ) · ( exp ‘ - 𝐵 ) ) ) )
15 11 2 3 14 syl12anc ⊢ ( 𝐵 ∈ ℂ → ( ( 1 / ( exp ‘ 𝐵 ) ) = ( exp ‘ - 𝐵 ) ↔ 1 = ( ( exp ‘ 𝐵 ) · ( exp ‘ - 𝐵 ) ) ) )
16 8 15 mpbird ⊢ ( 𝐵 ∈ ℂ → ( 1 / ( exp ‘ 𝐵 ) ) = ( exp ‘ - 𝐵 ) )
17 16 oveq2d ⊢ ( 𝐵 ∈ ℂ → ( ( exp ‘ 𝐴 ) · ( 1 / ( exp ‘ 𝐵 ) ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐵 ) ) )
18 17 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ 𝐴 ) · ( 1 / ( exp ‘ 𝐵 ) ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐵 ) ) )
19 efadd ⊢ ( ( 𝐴 ∈ ℂ ∧ - 𝐵 ∈ ℂ ) → ( exp ‘ ( 𝐴 + - 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐵 ) ) )
20 9 19 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( 𝐴 + - 𝐵 ) ) = ( ( exp ‘ 𝐴 ) · ( exp ‘ - 𝐵 ) ) )
21 18 20 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( exp ‘ 𝐴 ) · ( 1 / ( exp ‘ 𝐵 ) ) ) = ( exp ‘ ( 𝐴 + - 𝐵 ) ) )
22 negsub ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + - 𝐵 ) = ( 𝐴 − 𝐵 ) )
23 22 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( 𝐴 + - 𝐵 ) ) = ( exp ‘ ( 𝐴 − 𝐵 ) ) )
24 6 21 23 3eqtrrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( exp ‘ ( 𝐴 − 𝐵 ) ) = ( ( exp ‘ 𝐴 ) / ( exp ‘ 𝐵 ) ) )