Metamath Proof Explorer

Theorem reglogexpbas

Description: General log of a power of the base is the exponent. (Contributed by Stefan O'Rear, 19-Sep-2014) (New usage is discouraged.) Use relogbexp instead.

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

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ (N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to C \in ℝ^{+}$
2		simpl	$⊢ (N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to N \in ℤ$
3		simpr	$⊢ (N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to (C \in ℝ^{+} \land C \neq 1)$
4		reglogexp	$⊢ (C \in ℝ^{+} \land N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log C^{N}}{\log C} = N (\frac{\log C}{\log C})$
5	1 2 3 4	syl3anc	$⊢ (N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log C^{N}}{\log C} = N (\frac{\log C}{\log C})$
6		reglogbas	$⊢ (C \in ℝ^{+} \land C \neq 1) \to \frac{\log C}{\log C} = 1$
7	6	adantl	$⊢ (N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log C}{\log C} = 1$
8	7	oveq2d	$⊢ (N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to N (\frac{\log C}{\log C}) = N \cdot 1$
9		zcn	$⊢ N \in ℤ \to N \in ℂ$
10	9	adantr	$⊢ (N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to N \in ℂ$
11	10	mulid1d	$⊢ (N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to N \cdot 1 = N$
12	5 8 11	3eqtrd	$⊢ (N \in ℤ \land (C \in ℝ^{+} \land C \neq 1)) \to \frac{\log C^{N}}{\log C} = N$