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