Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  0lt1sr Structured version   Visualization version   GIF version

Theorem 0lt1sr 9795
 Description: 0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.)
Assertion
Ref Expression
0lt1sr 0R <R 1R

Proof of Theorem 0lt1sr
StepHypRef Expression
1 1pr 9716 . . . . . 6 1PP
2 addclpr 9719 . . . . . 6 ((1PP ∧ 1PP) → (1P +P 1P) ∈ P)
31, 1, 2mp2an 704 . . . . 5 (1P +P 1P) ∈ P
4 ltaddpr 9735 . . . . 5 (((1P +P 1P) ∈ P ∧ 1PP) → (1P +P 1P)<P ((1P +P 1P) +P 1P))
53, 1, 4mp2an 704 . . . 4 (1P +P 1P)<P ((1P +P 1P) +P 1P)
6 addcompr 9722 . . . 4 (1P +P (1P +P 1P)) = ((1P +P 1P) +P 1P)
75, 6breqtrri 4610 . . 3 (1P +P 1P)<P (1P +P (1P +P 1P))
8 ltsrpr 9777 . . 3 ([⟨1P, 1P⟩] ~R <R [⟨(1P +P 1P), 1P⟩] ~R ↔ (1P +P 1P)<P (1P +P (1P +P 1P)))
97, 8mpbir 220 . 2 [⟨1P, 1P⟩] ~R <R [⟨(1P +P 1P), 1P⟩] ~R
10 df-0r 9761 . 2 0R = [⟨1P, 1P⟩] ~R
11 df-1r 9762 . 2 1R = [⟨(1P +P 1P), 1P⟩] ~R
129, 10, 113brtr4i 4613 1 0R <R 1R
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 1977  ⟨cop 4131   class class class wbr 4583  (class class class)co 6549  [cec 7627  Pcnp 9560  1Pc1p 9561   +P cpp 9562
 Copyright terms: Public domain W3C validator