Theorem logne0

Description: Logarithm of a non-1 positive real number is not zero and thus suitable as a divisor. (Contributed by Stefan O'Rear, 19-Sep-2014) (Proof shortened by AV, 14-Jun-2020)

	Ref	Expression
Assertion	logne0	$$⊢\left(A\in {ℝ}^{+}\wedge A\ne 1\right)\to \log A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
2	1	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge A\ne 1\right)\to A\in ℂ$$
3		rpne0	$$⊢A\in {ℝ}^{+}\to A\ne 0$$
4	3	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge A\ne 1\right)\to A\ne 0$$
5		simpr	$$⊢\left(A\in {ℝ}^{+}\wedge A\ne 1\right)\to A\ne 1$$
6		logccne0	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge A\ne 1\right)\to \log A\ne 0$$
7	2 4 5 6	syl3anc	$$⊢\left(A\in {ℝ}^{+}\wedge A\ne 1\right)\to \log A\ne 0$$