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_{𝑹}$

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

Metamath Proof Explorer