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 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 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 )