Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  0lt1sr GIF version

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

Proof of Theorem 0lt1sr
StepHypRef Expression
1 1pr 6652 . . . . . 6 1PP
2 addclpr 6635 . . . . . 6 ((1PP ∧ 1PP) → (1P +P 1P) ∈ P)
31, 1, 2mp2an 402 . . . . 5 (1P +P 1P) ∈ P
4 ltaddpr 6695 . . . . 5 (((1P +P 1P) ∈ P ∧ 1PP) → (1P +P 1P)<P ((1P +P 1P) +P 1P))
53, 1, 4mp2an 402 . . . 4 (1P +P 1P)<P ((1P +P 1P) +P 1P)
6 addcomprg 6676 . . . . 5 ((1PP ∧ (1P +P 1P) ∈ P) → (1P +P (1P +P 1P)) = ((1P +P 1P) +P 1P))
71, 3, 6mp2an 402 . . . 4 (1P +P (1P +P 1P)) = ((1P +P 1P) +P 1P)
85, 7breqtrri 3789 . . 3 (1P +P 1P)<P (1P +P (1P +P 1P))
9 ltsrprg 6832 . . . 4 (((1PP ∧ 1PP) ∧ ((1P +P 1P) ∈ P ∧ 1PP)) → ([⟨1P, 1P⟩] ~R <R [⟨(1P +P 1P), 1P⟩] ~R ↔ (1P +P 1P)<P (1P +P (1P +P 1P))))
101, 1, 3, 1, 9mp4an 403 . . 3 ([⟨1P, 1P⟩] ~R <R [⟨(1P +P 1P), 1P⟩] ~R ↔ (1P +P 1P)<P (1P +P (1P +P 1P)))
118, 10mpbir 134 . 2 [⟨1P, 1P⟩] ~R <R [⟨(1P +P 1P), 1P⟩] ~R
12 df-0r 6816 . 2 0R = [⟨1P, 1P⟩] ~R
13 df-1r 6817 . 2 1R = [⟨(1P +P 1P), 1P⟩] ~R
1411, 12, 133brtr4i 3792 1 0R <R 1R
 Colors of variables: wff set class Syntax hints:   ↔ wb 98   = wceq 1243   ∈ wcel 1393  ⟨cop 3378   class class class wbr 3764  (class class class)co 5512  [cec 6104  Pcnp 6389  1Pc1p 6390   +P cpp 6391
 Copyright terms: Public domain W3C validator