logccne0

Description: The logarithm isn't 0 if its argument isn't 0 or 1. (Contributed by David A. Wheeler, 17-Jul-2017)

		Ref	Expression
	Assertion	logccne0	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \neq 0$

Step	Hyp	Ref	Expression
1		simp3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to A \neq 1$
2	1	neneqd	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \neg A = 1$
3		logeq0im1	$⊢ (A \in ℂ \land A \neq 0 \land \log A = 0) \to A = 1$
4	3	3expia	$⊢ (A \in ℂ \land A \neq 0) \to (\log A = 0 \to A = 1)$
5	4	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to (\log A = 0 \to A = 1)$
6	2 5	mtod	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \neg \log A = 0$
7	6	neqned	$⊢ (A \in ℂ \land A \neq 0 \land A \neq 1) \to \log A \neq 0$

Metamath Proof Explorer