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