Theorem relog

Description: Real part of a logarithm. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	relog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)=\log \left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
2	1	recld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)\in ℝ$$
3		relogef	$$⊢\Re \left(\log A\right)\in ℝ\to \log {\mathrm{e}}^{\Re \left(\log A\right)}=\Re \left(\log A\right)$$
4	2 3	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log {\mathrm{e}}^{\Re \left(\log A\right)}=\Re \left(\log A\right)$$
5		absef	$$⊢\log A\in ℂ\to \left|{\mathrm{e}}^{\log A}\right|={\mathrm{e}}^{\Re \left(\log A\right)}$$
6	1 5	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|{\mathrm{e}}^{\log A}\right|={\mathrm{e}}^{\Re \left(\log A\right)}$$
7		eflog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\log A}=A$$
8	7	fveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|{\mathrm{e}}^{\log A}\right|=\left|A\right|$$
9	6 8	eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to {\mathrm{e}}^{\Re \left(\log A\right)}=\left|A\right|$$
10	9	fveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log {\mathrm{e}}^{\Re \left(\log A\right)}=\log \left|A\right|$$
11	4 10	eqtr3d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)=\log \left|A\right|$$