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

Proof

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