relog

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

		Ref	Expression
	Assertion	relog	$⊢ (A \in ℂ \land A \neq 0) \to ℜ (\log A) = \log \|A\|$

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

Metamath Proof Explorer