Theorem efsubd

Description: Difference of exponents law for exponential function, deduction form. (Contributed by SN, 25-Apr-2025)

	Ref	Expression
Hypotheses	efsubd.a	$$⊢\phi \to A\in ℂ$$
	efsubd.b	$$⊢\phi \to B\in ℂ$$
Assertion	efsubd	$$⊢\phi \to {\mathrm{e}}^{A-B}=\frac{{\mathrm{e}}^A}{{\mathrm{e}}^B}$$

Proof

Step	Hyp	Ref	Expression
1		efsubd.a	$$⊢\phi \to A\in ℂ$$
2		efsubd.b	$$⊢\phi \to B\in ℂ$$
3		efsub	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to {\mathrm{e}}^{A-B}=\frac{{\mathrm{e}}^A}{{\mathrm{e}}^B}$$
4	1 2 3	syl2anc	$$⊢\phi \to {\mathrm{e}}^{A-B}=\frac{{\mathrm{e}}^A}{{\mathrm{e}}^B}$$