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 ∈ ℂ ∧ B ∈ ℂ → e A − B = e A e B

Proof

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