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

Theorem addgt0sr 9410
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  A  /\  0R  <R  B )  ->  0R  <R  ( A  +R  B ) )

Proof of Theorem addgt0sr
StepHypRef Expression
1 ltrelsr 9374 . . . . . 6  |-  <R  C_  ( R.  X.  R. )
21brel 4975 . . . . 5  |-  ( 0R 
<R  A  ->  ( 0R  e.  R.  /\  A  e.  R. ) )
32simprd 461 . . . 4  |-  ( 0R 
<R  A  ->  A  e. 
R. )
4 ltasr 9406 . . . . 5  |-  ( A  e.  R.  ->  ( 0R  <R  B  <->  ( A  +R  0R )  <R  ( A  +R  B ) ) )
5 0idsr 9403 . . . . . 6  |-  ( A  e.  R.  ->  ( A  +R  0R )  =  A )
65breq1d 4390 . . . . 5  |-  ( A  e.  R.  ->  (
( A  +R  0R )  <R  ( A  +R  B )  <->  A  <R  ( A  +R  B ) ) )
74, 6bitrd 253 . . . 4  |-  ( A  e.  R.  ->  ( 0R  <R  B  <->  A  <R  ( A  +R  B ) ) )
83, 7syl 16 . . 3  |-  ( 0R 
<R  A  ->  ( 0R 
<R  B  <->  A  <R  ( A  +R  B ) ) )
98biimpa 482 . 2  |-  ( ( 0R  <R  A  /\  0R  <R  B )  ->  A  <R  ( A  +R  B ) )
10 ltsosr 9400 . . 3  |-  <R  Or  R.
1110, 1sotri 5320 . 2  |-  ( ( 0R  <R  A  /\  A  <R  ( A  +R  B ) )  ->  0R  <R  ( A  +R  B ) )
129, 11syldan 468 1  |-  ( ( 0R  <R  A  /\  0R  <R  B )  ->  0R  <R  ( A  +R  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    e. wcel 1836   class class class wbr 4380  (class class class)co 6214   R.cnr 9172   0Rc0r 9173    +R cplr 9176    <R cltr 9178
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509  ax-inf2 7990
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-reu 2749  df-rmo 2750  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-pss 3418  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-tp 3962  df-op 3964  df-uni 4177  df-int 4213  df-iun 4258  df-br 4381  df-opab 4439  df-mpt 4440  df-tr 4474  df-eprel 4718  df-id 4722  df-po 4727  df-so 4728  df-fr 4765  df-we 4767  df-ord 4808  df-on 4809  df-lim 4810  df-suc 4811  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-om 6618  df-1st 6717  df-2nd 6718  df-recs 6978  df-rdg 7012  df-1o 7066  df-oadd 7070  df-omul 7071  df-er 7247  df-ec 7249  df-qs 7253  df-ni 9179  df-pli 9180  df-mi 9181  df-lti 9182  df-plpq 9215  df-mpq 9216  df-ltpq 9217  df-enq 9218  df-nq 9219  df-erq 9220  df-plq 9221  df-mq 9222  df-1nq 9223  df-rq 9224  df-ltnq 9225  df-np 9288  df-1p 9289  df-plp 9290  df-ltp 9292  df-enr 9362  df-nr 9363  df-plr 9364  df-ltr 9366  df-0r 9367
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator