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

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

Metamath Proof Explorer