This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ <R Or R
2 1sr ⊢ 1R ∈ R
3 sonr ⊢ ( ( <R Or R ∧ 1R ∈ R ) → ¬ 1R <R 1R )
4 1 2 3 mp2an ⊢ ¬ 1R <R 1R
5 0lt1sr ⊢ 0R <R 1R
6 breq1 ⊢ ( 1R = 0R → ( 1R <R 1R ↔ 0R <R 1R ) )
7 5 6 mpbiri ⊢ ( 1R = 0R → 1R <R 1R )
8 4 7 mto ⊢ ¬ 1R = 0R