Theorem reglogbas

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

	Ref	Expression
Assertion	reglogbas	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( ( log ‘ 𝐶 ) / ( log ‘ 𝐶 ) ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		relogcl	⊢ ( 𝐶 ∈ ℝ+ → ( log ‘ 𝐶 ) ∈ ℝ )
2	1	recnd	⊢ ( 𝐶 ∈ ℝ+ → ( log ‘ 𝐶 ) ∈ ℂ )
3	2	adantr	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( log ‘ 𝐶 ) ∈ ℂ )
4		logne0	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( log ‘ 𝐶 ) ≠ 0 )
5	3 4	dividd	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( ( log ‘ 𝐶 ) / ( log ‘ 𝐶 ) ) = 1 )