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 
|- -. 1R = 0R

Proof

Step Hyp Ref Expression
1 ltsosr 
 |-
2 1sr 
 |-  1R e. R.
3 sonr 
 |-  ( (  -. 1R
4 1 2 3 mp2an 
 |-  -. 1R
5 0lt1sr 
 |-  0R
6 breq1 
 |-  ( 1R = 0R -> ( 1R  0R
7 5 6 mpbiri 
 |-  ( 1R = 0R -> 1R
8 4 7 mto 
 |-  -. 1R = 0R