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

Metamath Proof Explorer

Theorem ine1

Description: _i is not 1. (Contributed by SN, 25-Apr-2025)

Ref Expression
Assertion ine1 i ≠ 1

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 inelr ⊢ ¬ i ∈ ℝ
3 nelne2 ⊢ ( ( 1 ∈ ℝ ∧ ¬ i ∈ ℝ ) → 1 ≠ i )
4 1 2 3 mp2an ⊢ 1 ≠ i
5 4 necomi ⊢ i ≠ 1