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

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 )