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

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

StepHypRef Expression
1 simpr 103 . . . 4 ((0R <R A 0R <R B) → 0R <R B)
2 ltrelsr 6646 . . . . . . 7 <R ⊆ (R × R)
32brel 4335 . . . . . 6 (0R <R B → (0R R B R))
43simprd 107 . . . . 5 (0R <R BB R)
52brel 4335 . . . . . 6 (0R <R A → (0R R A R))
65simprd 107 . . . . 5 (0R <R AA R)
7 0r 6658 . . . . . 6 0R R
8 ltasrg 6678 . . . . . 6 ((0R R B R A R) → (0R <R B ↔ (A +R 0R) <R (A +R B)))
97, 8mp3an1 1218 . . . . 5 ((B R A R) → (0R <R B ↔ (A +R 0R) <R (A +R B)))
104, 6, 9syl2anr 274 . . . 4 ((0R <R A 0R <R B) → (0R <R B ↔ (A +R 0R) <R (A +R B)))
111, 10mpbid 135 . . 3 ((0R <R A 0R <R B) → (A +R 0R) <R (A +R B))
126adantr 261 . . . 4 ((0R <R A 0R <R B) → A R)
13 0idsr 6675 . . . . 5 (A R → (A +R 0R) = A)
1413breq1d 3765 . . . 4 (A R → ((A +R 0R) <R (A +R B) ↔ A <R (A +R B)))
1512, 14syl 14 . . 3 ((0R <R A 0R <R B) → ((A +R 0R) <R (A +R B) ↔ A <R (A +R B)))
1611, 15mpbid 135 . 2 ((0R <R A 0R <R B) → A <R (A +R B))
17 ltsosr 6672 . . 3 <R Or R
1817, 2sotri 4663 . 2 ((0R <R A A <R (A +R B)) → 0R <R (A +R B))
1916, 18syldan 266 1 ((0R <R A 0R <R B) → 0R <R (A +R B))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∈ wcel 1390   class class class wbr 3755  (class class class)co 5455  Rcnr 6281  0Rc0r 6282   +R cplr 6285
 Copyright terms: Public domain W3C validator