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