Theorem 0lt1sr

Description: 0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	0lt1sr	$$⊢0_{𝑹}{<}_{𝑹}{1}_{𝑹}$$

Proof

Step	Hyp	Ref	Expression
1		1pr	$$⊢1_{𝑷}\in 𝑷$$
2		addclpr	$$⊢\left(1_{𝑷}\in 𝑷\wedge 1_{𝑷}\in 𝑷\right)\to 1_{𝑷}{+}_{𝑷}{1}_{𝑷}\in 𝑷$$
3	1 1 2	mp2an	$$⊢1_{𝑷}{+}_{𝑷}{1}_{𝑷}\in 𝑷$$
4		ltaddpr	$$⊢\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\in 𝑷\wedge 1_{𝑷}\in 𝑷\right)\to \left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}{1}_{𝑷}\right)$$
5	3 1 4	mp2an	$$⊢\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}{1}_{𝑷}\right)$$
6		addcompr	$$⊢1_{𝑷}{+}_{𝑷}\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right)=\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){+}_{𝑷}{1}_{𝑷}$$
7	5 6	breqtrri	$$⊢\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(1_{𝑷}{+}_{𝑷}\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right)\right)$$
8		ltsrpr	$$⊢\left[⟨1_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}{<}_{𝑹}\left[⟨1_{𝑷}{+}_{𝑷}{1}_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}\leftrightarrow \left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right){<}_{𝑷}\left(1_{𝑷}{+}_{𝑷}\left(1_{𝑷}{+}_{𝑷}{1}_{𝑷}\right)\right)$$
9	7 8	mpbir	$$⊢\left[⟨1_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}{<}_{𝑹}\left[⟨1_{𝑷}{+}_{𝑷}{1}_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}$$
10		df-0r	$$⊢0_{𝑹}=\left[⟨1_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}$$
11		df-1r	$$⊢1_{𝑹}=\left[⟨1_{𝑷}{+}_{𝑷}{1}_{𝑷},1_{𝑷}⟩\right]{~}_{𝑹}$$
12	9 10 11	3brtr4i	$$⊢0_{𝑹}{<}_{𝑹}{1}_{𝑹}$$