This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem logccne0

Description: The logarithm isn't 0 if its argument isn't 0 or 1. (Contributed by David A. Wheeler, 17-Jul-2017)

Ref Expression
Assertion logccne0 
|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) =/= 0 )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A =/= 1 )
2 1 neneqd 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> -. A = 1 )
3 logeq0im1 
 |-  ( ( A e. CC /\ A =/= 0 /\ ( log ` A ) = 0 ) -> A = 1 )
4 3 3expia 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( log ` A ) = 0 -> A = 1 ) )
5 4 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( log ` A ) = 0 -> A = 1 ) )
6 2 5 mtod 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> -. ( log ` A ) = 0 )
7 6 neqned 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) =/= 0 )