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	$$⊢\neg 1_{𝑹}=0_{𝑹}$$

Proof

Step	Hyp	Ref	Expression
1		ltsosr	$$⊢{<}_{𝑹}\mathrm{Or}𝑹$$
2		1sr	$$⊢1_{𝑹}\in 𝑹$$
3		sonr	$$⊢\left({<}_{𝑹}\mathrm{Or}𝑹\wedge 1_{𝑹}\in 𝑹\right)\to \neg 1_{𝑹}{<}_{𝑹}{1}_{𝑹}$$
4	1 2 3	mp2an	$$⊢\neg 1_{𝑹}{<}_{𝑹}{1}_{𝑹}$$
5		0lt1sr	$$⊢0_{𝑹}{<}_{𝑹}{1}_{𝑹}$$
6		breq1	$$⊢1_{𝑹}=0_{𝑹}\to \left(1_{𝑹}{<}_{𝑹}{1}_{𝑹}\leftrightarrow 0_{𝑹}{<}_{𝑹}{1}_{𝑹}\right)$$
7	5 6	mpbiri	$$⊢1_{𝑹}=0_{𝑹}\to 1_{𝑹}{<}_{𝑹}{1}_{𝑹}$$
8	4 7	mto	$$⊢\neg 1_{𝑹}=0_{𝑹}$$