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

Proof

Step	Hyp	Ref	Expression
1		relogexp	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ) → ( log ‘ ( 𝐴 ↑ 𝑁 ) ) = ( 𝑁 · ( log ‘ 𝐴 ) ) )
2	1	3adant3	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( log ‘ ( 𝐴 ↑ 𝑁 ) ) = ( 𝑁 · ( log ‘ 𝐴 ) ) )
3	2	oveq1d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( ( log ‘ ( 𝐴 ↑ 𝑁 ) ) / ( log ‘ 𝐶 ) ) = ( ( 𝑁 · ( log ‘ 𝐴 ) ) / ( log ‘ 𝐶 ) ) )
4		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
5	4	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → 𝑁 ∈ ℂ )
6		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
7	6	recnd	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℂ )
8	7	3ad2ant1	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
9		relogcl	⊢ ( 𝐶 ∈ ℝ+ → ( log ‘ 𝐶 ) ∈ ℝ )
10	9	recnd	⊢ ( 𝐶 ∈ ℝ+ → ( log ‘ 𝐶 ) ∈ ℂ )
11	10	adantr	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( log ‘ 𝐶 ) ∈ ℂ )
12	11	3ad2ant3	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( log ‘ 𝐶 ) ∈ ℂ )
13		logne0	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( log ‘ 𝐶 ) ≠ 0 )
14	13	3ad2ant3	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( log ‘ 𝐶 ) ≠ 0 )
15	5 8 12 14	divassd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( ( 𝑁 · ( log ‘ 𝐴 ) ) / ( log ‘ 𝐶 ) ) = ( 𝑁 · ( ( log ‘ 𝐴 ) / ( log ‘ 𝐶 ) ) ) )
16	3 15	eqtrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) ) → ( ( log ‘ ( 𝐴 ↑ 𝑁 ) ) / ( log ‘ 𝐶 ) ) = ( 𝑁 · ( ( log ‘ 𝐴 ) / ( log ‘ 𝐶 ) ) ) )