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 )