reglogexp

Description: Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use relogbzexp instead.

		Ref	Expression
	Assertion	reglogexp	$⊢ (A \in ℝ^{+} \land N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log A^{N}}{\log C} = N (\frac{\log A}{\log C})$

Step	Hyp	Ref	Expression
1		relogexp	$⊢ (A \in ℝ^{+} \land N \in ℤ) \to \log A^{N} = N \log A$
2	1	3adant3	$⊢ (A \in ℝ^{+} \land N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \log A^{N} = N \log A$
3	2	oveq1d	$⊢ (A \in ℝ^{+} \land N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log A^{N}}{\log C} = \frac{N \log A}{\log C}$
4		zcn	$⊢ N \in ℤ \to N \in ℂ$
5	4	3ad2ant2	$⊢ (A \in ℝ^{+} \land N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to N \in ℂ$
6		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
7	6	recnd	$⊢ A \in ℝ^{+} \to \log A \in ℂ$
8	7	3ad2ant1	$⊢ (A \in ℝ^{+} \land N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \log A \in ℂ$
9		relogcl	$⊢ C \in ℝ^{+} \to \log C \in ℝ$
10	9	recnd	$⊢ C \in ℝ^{+} \to \log C \in ℂ$
11	10	adantr	$⊢ (C \in ℝ^{+} \land C \neq 1) \to \log C \in ℂ$
12	11	3ad2ant3	$⊢ (A \in ℝ^{+} \land N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \log C \in ℂ$
13		logne0	$⊢ (C \in ℝ^{+} \land C \neq 1) \to \log C \neq 0$
14	13	3ad2ant3	$⊢ (A \in ℝ^{+} \land N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \log C \neq 0$
15	5 8 12 14	divassd	$⊢ (A \in ℝ^{+} \land N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{N \log A}{\log C} = N (\frac{\log A}{\log C})$
16	3 15	eqtrd	$⊢ (A \in ℝ^{+} \land N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log A^{N}}{\log C} = N (\frac{\log A}{\log C})$

Metamath Proof Explorer