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	⊢ 0R <R 1R

Proof

Step	Hyp	Ref	Expression
1		1pr	⊢ 1P ∈ P
2		addclpr	⊢ ( ( 1P ∈ P ∧ 1P ∈ P ) → ( 1P +P 1P ) ∈ P )
3	1 1 2	mp2an	⊢ ( 1P +P 1P ) ∈ P
4		ltaddpr	⊢ ( ( ( 1P +P 1P ) ∈ P ∧ 1P ∈ P ) → ( 1P +P 1P ) <P ( ( 1P +P 1P ) +P 1P ) )
5	3 1 4	mp2an	⊢ ( 1P +P 1P ) <P ( ( 1P +P 1P ) +P 1P )
6		addcompr	⊢ ( 1P +P ( 1P +P 1P ) ) = ( ( 1P +P 1P ) +P 1P )
7	5 6	breqtrri	⊢ ( 1P +P 1P ) <P ( 1P +P ( 1P +P 1P ) )
8		ltsrpr	⊢ ( [ ⟨ 1P , 1P ⟩ ] ~R <R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R ↔ ( 1P +P 1P ) <P ( 1P +P ( 1P +P 1P ) ) )
9	7 8	mpbir	⊢ [ ⟨ 1P , 1P ⟩ ] ~R <R [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R
10		df-0r	⊢ 0R = [ ⟨ 1P , 1P ⟩ ] ~R
11		df-1r	⊢ 1R = [ ⟨ ( 1P +P 1P ) , 1P ⟩ ] ~R
12	9 10 11	3brtr4i	⊢ 0R <R 1R