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