Theorem logdiv2

Description: Generalization of relogdiv to a complex left argument. (Contributed by Mario Carneiro, 8-Jul-2017)

	Ref	Expression
Assertion	logdiv2	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log \left(\frac{A}{B}\right)=\log A-\log B$$

Proof

Step	Hyp	Ref	Expression
1		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
2	1	3adant3	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log A\in ℂ$$
3		relogcl	$$⊢B\in {ℝ}^{+}\to \log B\in ℝ$$
4	3	3ad2ant3	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log B\in ℝ$$
5	4	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log B\in ℂ$$
6		efsub	$$⊢\left(\log A\in ℂ\wedge \log B\in ℂ\right)\to {\mathrm{e}}^{\log A-\log B}=\frac{{\mathrm{e}}^{\log A}}{{\mathrm{e}}^{\log B}}$$
7	2 5 6	syl2anc	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to {\mathrm{e}}^{\log A-\log B}=\frac{{\mathrm{e}}^{\log A}}{{\mathrm{e}}^{\log B}}$$
8		eflog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$
9	8	3adant3	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to {\mathrm{e}}^{\log A}=A$$
10		reeflog	$$⊢B\in {ℝ}^{+}\to {\mathrm{e}}^{\log B}=B$$
11	10	3ad2ant3	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to {\mathrm{e}}^{\log B}=B$$
12	9 11	oveq12d	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \frac{{\mathrm{e}}^{\log A}}{{\mathrm{e}}^{\log B}}=\frac{A}{B}$$
13	7 12	eqtrd	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to {\mathrm{e}}^{\log A-\log B}=\frac{A}{B}$$
14	13	fveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log {\mathrm{e}}^{\log A-\log B}=\log \left(\frac{A}{B}\right)$$
15	2 5	negsubd	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log A+\left(-\log B\right)=\log A-\log B$$
16		logrncl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in \mathrm{ran}log$$
17	16	3adant3	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log A\in \mathrm{ran}log$$
18	4	renegcld	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to -\log B\in ℝ$$
19		logrnaddcl	$$⊢\left(\log A\in \mathrm{ran}log\wedge -\log B\in ℝ\right)\to \log A+\left(-\log B\right)\in \mathrm{ran}log$$
20	17 18 19	syl2anc	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log A+\left(-\log B\right)\in \mathrm{ran}log$$
21	15 20	eqeltrrd	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log A-\log B\in \mathrm{ran}log$$
22		logef	$$⊢\log A-\log B\in \mathrm{ran}log\to \log {\mathrm{e}}^{\log A-\log B}=\log A-\log B$$
23	21 22	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log {\mathrm{e}}^{\log A-\log B}=\log A-\log B$$
24	14 23	eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in {ℝ}^{+}\right)\to \log \left(\frac{A}{B}\right)=\log A-\log B$$