This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem relogexp

Description: The natural logarithm of positive A raised to an integer power. Property 4 of Cohen p. 301-302, restricted to natural logarithms and integer powers N . (Contributed by Steve Rodriguez, 25-Nov-2007)

		Ref	Expression
	Assertion	relogexp	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to \log A^{N} = N \log A$

Proof

Step	Hyp	Ref	Expression
1		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
2	1	recnd	$⊢ A \in ℝ^{+} \to \log A \in ℂ$
3		efexp	$⊢ (\log A \in ℂ \land N \in ℤ) \to e^{N \log A} = {e^{\log A}}^{N}$
4	2 3	sylan	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to e^{N \log A} = {e^{\log A}}^{N}$
5		reeflog	$⊢ A \in ℝ^{+} \to e^{\log A} = A$
6	5	oveq1d	$⊢ A \in ℝ^{+} \to {e^{\log A}}^{N} = A^{N}$
7	6	adantr	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to {e^{\log A}}^{N} = A^{N}$
8	4 7	eqtrd	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to e^{N \log A} = A^{N}$
9	8	fveq2d	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to \log e^{N \log A} = \log A^{N}$
10		zre	$⊢ N \in ℤ \to N \in ℝ$
11		remulcl	$⊢ (N \in ℝ \land \log A \in ℝ) \to N \log A \in ℝ$
12	10 1 11	syl2anr	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to N \log A \in ℝ$
13		relogef	$⊢ N \log A \in ℝ \to \log e^{N \log A} = N \log A$
14	12 13	syl	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to \log e^{N \log A} = N \log A$
15	9 14	eqtr3d	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to \log A^{N} = N \log A$