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	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge \log A=0\right)\to A=1$$

Proof

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