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 e. CC /\ A =/= 0 /\ ( log ` A ) = 0 ) -> A = 1 )

Proof

Step Hyp Ref Expression
1 eflog
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
2 1 3adant3
 |-  ( ( A e. CC /\ A =/= 0 /\ ( log ` A ) = 0 ) -> ( exp ` ( log ` A ) ) = A )
3 fveq2
 |-  ( ( log ` A ) = 0 -> ( exp ` ( log ` A ) ) = ( exp ` 0 ) )
4 ef0
 |-  ( exp ` 0 ) = 1
5 3 4 eqtrdi
 |-  ( ( log ` A ) = 0 -> ( exp ` ( log ` A ) ) = 1 )
6 5 3ad2ant3
 |-  ( ( A e. CC /\ A =/= 0 /\ ( log ` A ) = 0 ) -> ( exp ` ( log ` A ) ) = 1 )
7 2 6 eqtr3d
 |-  ( ( A e. CC /\ A =/= 0 /\ ( log ` A ) = 0 ) -> A = 1 )