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 ( 𝜑𝐴 ∈ ℂ )
logccne0d.0 ( 𝜑𝐴 ≠ 0 )
logccne0d.1 ( 𝜑𝐴 ≠ 1 )
Assertion logccne0d ( 𝜑 → ( log ‘ 𝐴 ) ≠ 0 )

Proof

Step Hyp Ref Expression
1 logccne0d.a ( 𝜑𝐴 ∈ ℂ )
2 logccne0d.0 ( 𝜑𝐴 ≠ 0 )
3 logccne0d.1 ( 𝜑𝐴 ≠ 1 )
4 logccne0 ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐴 ≠ 1 ) → ( log ‘ 𝐴 ) ≠ 0 )
5 1 2 3 4 syl3anc ( 𝜑 → ( log ‘ 𝐴 ) ≠ 0 )