efsub

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

		Ref	Expression
	Assertion	efsub	$⊢ (A \in ℂ \land B \in ℂ) \to e^{A - B} = \frac{e^{A}}{e^{B}}$

Proof

Step	Hyp	Ref	Expression
1		efcl	$⊢ A \in ℂ \to e^{A} \in ℂ$
2		efcl	$⊢ B \in ℂ \to e^{B} \in ℂ$
3		efne0	$⊢ B \in ℂ \to e^{B} \neq 0$
4		divrec	$⊢ (e^{A} \in ℂ \land e^{B} \in ℂ \land e^{B} \neq 0) \to \frac{e^{A}}{e^{B}} = e^{A} (\frac{1}{e^{B}})$
5	1 2 3 4	syl3an	$⊢ (A \in ℂ \land B \in ℂ \land B \in ℂ) \to \frac{e^{A}}{e^{B}} = e^{A} (\frac{1}{e^{B}})$
6	5	3anidm23	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{e^{A}}{e^{B}} = e^{A} (\frac{1}{e^{B}})$
7		efcan	$⊢ B \in ℂ \to e^{B} e^{- B} = 1$
8	7	eqcomd	$⊢ B \in ℂ \to 1 = e^{B} e^{- B}$
9		negcl	$⊢ B \in ℂ \to - B \in ℂ$
10		efcl	$⊢ - B \in ℂ \to e^{- B} \in ℂ$
11	9 10	syl	$⊢ B \in ℂ \to e^{- B} \in ℂ$
12		ax-1cn	$⊢ 1 \in ℂ$
13		divmul2	$⊢ (1 \in ℂ \land e^{- B} \in ℂ \land (e^{B} \in ℂ \land e^{B} \neq 0)) \to (\frac{1}{e^{B}} = e^{- B} \leftrightarrow 1 = e^{B} e^{- B})$
14	12 13	mp3an1	$⊢ (e^{- B} \in ℂ \land (e^{B} \in ℂ \land e^{B} \neq 0)) \to (\frac{1}{e^{B}} = e^{- B} \leftrightarrow 1 = e^{B} e^{- B})$
15	11 2 3 14	syl12anc	$⊢ B \in ℂ \to (\frac{1}{e^{B}} = e^{- B} \leftrightarrow 1 = e^{B} e^{- B})$
16	8 15	mpbird	$⊢ B \in ℂ \to \frac{1}{e^{B}} = e^{- B}$
17	16	oveq2d	$⊢ B \in ℂ \to e^{A} (\frac{1}{e^{B}}) = e^{A} e^{- B}$
18	17	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to e^{A} (\frac{1}{e^{B}}) = e^{A} e^{- B}$
19		efadd	$⊢ (A \in ℂ \land - B \in ℂ) \to e^{A + (- B)} = e^{A} e^{- B}$
20	9 19	sylan2	$⊢ (A \in ℂ \land B \in ℂ) \to e^{A + (- B)} = e^{A} e^{- B}$
21	18 20	eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{A} (\frac{1}{e^{B}}) = e^{A + (- B)}$
22		negsub	$⊢ (A \in ℂ \land B \in ℂ) \to A + (- B) = A - B$
23	22	fveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{A + (- B)} = e^{A - B}$
24	6 21 23	3eqtrrd	$⊢ (A \in ℂ \land B \in ℂ) \to e^{A - B} = \frac{e^{A}}{e^{B}}$

Metamath Proof Explorer

Theorem efsub

Proof