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	$$⊢\left(C\in {ℝ}^{+}\wedge C\ne 1\right)\to \frac{\log 1}{\log C}=0$$

Proof

Step	Hyp	Ref	Expression
1		log1	$$⊢\log 1=0$$
2	1	oveq1i	$$⊢\frac{\log 1}{\log C}=\frac{0}{\log C}$$
3		relogcl	$$⊢C\in {ℝ}^{+}\to \log C\in ℝ$$
4	3	recnd	$$⊢C\in {ℝ}^{+}\to \log C\in ℂ$$
5	4	adantr	$$⊢\left(C\in {ℝ}^{+}\wedge C\ne 1\right)\to \log C\in ℂ$$
6		logne0	$$⊢\left(C\in {ℝ}^{+}\wedge C\ne 1\right)\to \log C\ne 0$$
7	5 6	div0d	$$⊢\left(C\in {ℝ}^{+}\wedge C\ne 1\right)\to \frac{0}{\log C}=0$$
8	2 7	syl5eq	$$⊢\left(C\in {ℝ}^{+}\wedge C\ne 1\right)\to \frac{\log 1}{\log C}=0$$