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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( log ‘ 𝐴 ) = 0 ) → 𝐴 = 1 )

Proof

Step	Hyp	Ref	Expression
1		eflog	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
2	1	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( log ‘ 𝐴 ) = 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )
3		fveq2	⊢ ( ( log ‘ 𝐴 ) = 0 → ( exp ‘ ( log ‘ 𝐴 ) ) = ( exp ‘ 0 ) )
4		ef0	⊢ ( exp ‘ 0 ) = 1
5	3 4	eqtrdi	⊢ ( ( log ‘ 𝐴 ) = 0 → ( exp ‘ ( log ‘ 𝐴 ) ) = 1 )
6	5	3ad2ant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( log ‘ 𝐴 ) = 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 1 )
7	2 6	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ ( log ‘ 𝐴 ) = 0 ) → 𝐴 = 1 )