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	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( ( log ‘ ( 𝐶 ↑ 𝑁 ) ) / ( log ‘ 𝐶 ) ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		simprl	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → 𝐶 ∈ ℝ+ )
2		simpl	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → 𝑁 ∈ ℤ )
3		simpr	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) )
4		reglogexp	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( ( log ‘ ( 𝐶 ↑ 𝑁 ) ) / ( log ‘ 𝐶 ) ) = ( 𝑁 · ( ( log ‘ 𝐶 ) / ( log ‘ 𝐶 ) ) ) )
5	1 2 3 4	syl3anc	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( ( log ‘ ( 𝐶 ↑ 𝑁 ) ) / ( log ‘ 𝐶 ) ) = ( 𝑁 · ( ( log ‘ 𝐶 ) / ( log ‘ 𝐶 ) ) ) )
6		reglogbas	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( ( log ‘ 𝐶 ) / ( log ‘ 𝐶 ) ) = 1 )
7	6	adantl	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( ( log ‘ 𝐶 ) / ( log ‘ 𝐶 ) ) = 1 )
8	7	oveq2d	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( 𝑁 · ( ( log ‘ 𝐶 ) / ( log ‘ 𝐶 ) ) ) = ( 𝑁 · 1 ) )
9		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
10	9	adantr	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → 𝑁 ∈ ℂ )
11	10	mulid1d	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( 𝑁 · 1 ) = 𝑁 )
12	5 8 11	3eqtrd	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( ( log ‘ ( 𝐶 ↑ 𝑁 ) ) / ( log ‘ 𝐶 ) ) = 𝑁 )