Metamath Proof Explorer


Theorem 1ne0sr

Description: 1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion 1ne0sr ¬1𝑹=0𝑹

Proof

Step Hyp Ref Expression
1 ltsosr <𝑹Or𝑹
2 1sr 1𝑹𝑹
3 sonr <𝑹Or𝑹1𝑹𝑹¬1𝑹<𝑹1𝑹
4 1 2 3 mp2an ¬1𝑹<𝑹1𝑹
5 0lt1sr 0𝑹<𝑹1𝑹
6 breq1 1𝑹=0𝑹1𝑹<𝑹1𝑹0𝑹<𝑹1𝑹
7 5 6 mpbiri 1𝑹=0𝑹1𝑹<𝑹1𝑹
8 4 7 mto ¬1𝑹=0𝑹