Description: 1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | 1ne0sr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltsosr | |
|
2 | 1sr | |
|
3 | sonr | |
|
4 | 1 2 3 | mp2an | |
5 | 0lt1sr | |
|
6 | breq1 | |
|
7 | 5 6 | mpbiri | |
8 | 4 7 | mto | |