This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem logeq0im1

Description: If the logarithm of a number is 0, the number must be 1. (Contributed by David A. Wheeler, 22-Jul-2017)

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

Step	Hyp	Ref	Expression
1		eflog	$⊢ (A \in ℂ \land A \neq 0) \to e^{\log A} = A$
2	1	3adant3	$⊢ (A \in ℂ \land A \neq 0 \land \log A = 0) \to e^{\log A} = A$
3		fveq2	$⊢ \log A = 0 \to e^{\log A} = e^{0}$
4		ef0	$⊢ e^{0} = 1$
5	3 4	eqtrdi	$⊢ \log A = 0 \to e^{\log A} = 1$
6	5	3ad2ant3	$⊢ (A \in ℂ \land A \neq 0 \land \log A = 0) \to e^{\log A} = 1$
7	2 6	eqtr3d	$⊢ (A \in ℂ \land A \neq 0 \land \log A = 0) \to A = 1$