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

 Description: The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
Assertion
Ref Expression
addgt0sr ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 +R 𝐵))

StepHypRef Expression
1 ltrelsr 10483 . . . . 5 <R ⊆ (R × R)
21brel 5585 . . . 4 (0R <R 𝐴 → (0RR𝐴R))
3 ltasr 10515 . . . . 5 (𝐴R → (0R <R 𝐵 ↔ (𝐴 +R 0R) <R (𝐴 +R 𝐵)))
4 0idsr 10512 . . . . . 6 (𝐴R → (𝐴 +R 0R) = 𝐴)
54breq1d 5043 . . . . 5 (𝐴R → ((𝐴 +R 0R) <R (𝐴 +R 𝐵) ↔ 𝐴 <R (𝐴 +R 𝐵)))
63, 5bitrd 282 . . . 4 (𝐴R → (0R <R 𝐵𝐴 <R (𝐴 +R 𝐵)))
72, 6simpl2im 507 . . 3 (0R <R 𝐴 → (0R <R 𝐵𝐴 <R (𝐴 +R 𝐵)))
87biimpa 480 . 2 ((0R <R 𝐴 ∧ 0R <R 𝐵) → 𝐴 <R (𝐴 +R 𝐵))
9 ltsosr 10509 . . 3 <R Or R
109, 1sotri 5958 . 2 ((0R <R 𝐴𝐴 <R (𝐴 +R 𝐵)) → 0R <R (𝐴 +R 𝐵))
118, 10syldan 594 1 ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 +R 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∈ wcel 2112   class class class wbr 5033  (class class class)co 7139  Rcnr 10280  0Rc0r 10281   +R cplr 10284
 Copyright terms: Public domain W3C validator