This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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