Metamath Proof Explorer


Theorem logccne0d

Description: The logarithm isn't 0 if its argument isn't 0 or 1, deduction form. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses logccne0d.a
|- ( ph -> A e. CC )
logccne0d.0
|- ( ph -> A =/= 0 )
logccne0d.1
|- ( ph -> A =/= 1 )
Assertion logccne0d
|- ( ph -> ( log ` A ) =/= 0 )

Proof

Step Hyp Ref Expression
1 logccne0d.a
 |-  ( ph -> A e. CC )
2 logccne0d.0
 |-  ( ph -> A =/= 0 )
3 logccne0d.1
 |-  ( ph -> A =/= 1 )
4 logccne0
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) =/= 0 )
5 1 2 3 4 syl3anc
 |-  ( ph -> ( log ` A ) =/= 0 )