Theorem reglog1

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

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

Proof

Step	Hyp	Ref	Expression
1		log1	⊢ ( log ‘ 1 ) = 0
2	1	oveq1i	⊢ ( ( log ‘ 1 ) / ( log ‘ 𝐶 ) ) = ( 0 / ( log ‘ 𝐶 ) )
3		relogcl	⊢ ( 𝐶 ∈ ℝ+ → ( log ‘ 𝐶 ) ∈ ℝ )
4	3	recnd	⊢ ( 𝐶 ∈ ℝ+ → ( log ‘ 𝐶 ) ∈ ℂ )
5	4	adantr	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( log ‘ 𝐶 ) ∈ ℂ )
6		logne0	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( log ‘ 𝐶 ) ≠ 0 )
7	5 6	div0d	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( 0 / ( log ‘ 𝐶 ) ) = 0 )
8	2 7	eqtrid	⊢ ( ( 𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1 ) → ( ( log ‘ 1 ) / ( log ‘ 𝐶 ) ) = 0 )