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

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

StepHypRef Expression
1 simpr 107 . . . 4 ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R 𝐵)
2 ltrelsr 6880 . . . . . . 7 <R ⊆ (R × R)
32brel 4419 . . . . . 6 (0R <R 𝐵 → (0RR𝐵R))
43simprd 111 . . . . 5 (0R <R 𝐵𝐵R)
52brel 4419 . . . . . 6 (0R <R 𝐴 → (0RR𝐴R))
65simprd 111 . . . . 5 (0R <R 𝐴𝐴R)
7 0r 6892 . . . . . 6 0RR
8 ltasrg 6912 . . . . . 6 ((0RR𝐵R𝐴R) → (0R <R 𝐵 ↔ (𝐴 +R 0R) <R (𝐴 +R 𝐵)))
97, 8mp3an1 1230 . . . . 5 ((𝐵R𝐴R) → (0R <R 𝐵 ↔ (𝐴 +R 0R) <R (𝐴 +R 𝐵)))
104, 6, 9syl2anr 278 . . . 4 ((0R <R 𝐴 ∧ 0R <R 𝐵) → (0R <R 𝐵 ↔ (𝐴 +R 0R) <R (𝐴 +R 𝐵)))
111, 10mpbid 139 . . 3 ((0R <R 𝐴 ∧ 0R <R 𝐵) → (𝐴 +R 0R) <R (𝐴 +R 𝐵))
126adantr 265 . . . 4 ((0R <R 𝐴 ∧ 0R <R 𝐵) → 𝐴R)
13 0idsr 6909 . . . . 5 (𝐴R → (𝐴 +R 0R) = 𝐴)
1413breq1d 3801 . . . 4 (𝐴R → ((𝐴 +R 0R) <R (𝐴 +R 𝐵) ↔ 𝐴 <R (𝐴 +R 𝐵)))
1512, 14syl 14 . . 3 ((0R <R 𝐴 ∧ 0R <R 𝐵) → ((𝐴 +R 0R) <R (𝐴 +R 𝐵) ↔ 𝐴 <R (𝐴 +R 𝐵)))
1611, 15mpbid 139 . 2 ((0R <R 𝐴 ∧ 0R <R 𝐵) → 𝐴 <R (𝐴 +R 𝐵))
17 ltsosr 6906 . . 3 <R Or R
1817, 2sotri 4747 . 2 ((0R <R 𝐴𝐴 <R (𝐴 +R 𝐵)) → 0R <R (𝐴 +R 𝐵))
1916, 18syldan 270 1 ((0R <R 𝐴 ∧ 0R <R 𝐵) → 0R <R (𝐴 +R 𝐵))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 101   ↔ wb 102   ∈ wcel 1409   class class class wbr 3791  (class class class)co 5539  Rcnr 6452  0Rc0r 6453   +R cplr 6456
 Copyright terms: Public domain W3C validator