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

Theorem leadd1dd 10216
Description: Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.)
Hypotheses
Ref Expression
leidd.1  |-  ( ph  ->  A  e.  RR )
ltnegd.2  |-  ( ph  ->  B  e.  RR )
ltadd1d.3  |-  ( ph  ->  C  e.  RR )
leadd1dd.4  |-  ( ph  ->  A  <_  B )
Assertion
Ref Expression
leadd1dd  |-  ( ph  ->  ( A  +  C
)  <_  ( B  +  C ) )

Proof of Theorem leadd1dd
StepHypRef Expression
1 leadd1dd.4 . 2  |-  ( ph  ->  A  <_  B )
2 leidd.1 . . 3  |-  ( ph  ->  A  e.  RR )
3 ltnegd.2 . . 3  |-  ( ph  ->  B  e.  RR )
4 ltadd1d.3 . . 3  |-  ( ph  ->  C  e.  RR )
52, 3, 4leadd1d 10196 . 2  |-  ( ph  ->  ( A  <_  B  <->  ( A  +  C )  <_  ( B  +  C ) ) )
61, 5mpbid 213 1  |-  ( ph  ->  ( A  +  C
)  <_  ( B  +  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   class class class wbr 4417  (class class class)co 6296   RRcr 9527    + caddc 9531    <_ cle 9665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-addrcl 9589  ax-mulcl 9590  ax-mulrcl 9591  ax-mulcom 9592  ax-addass 9593  ax-mulass 9594  ax-distr 9595  ax-i2m1 9596  ax-1ne0 9597  ax-1rid 9598  ax-rnegex 9599  ax-rrecex 9600  ax-cnre 9601  ax-pre-lttri 9602  ax-pre-lttrn 9603  ax-pre-ltadd 9604
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-po 4766  df-so 4767  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-ov 6299  df-er 7362  df-en 7569  df-dom 7570  df-sdom 7571  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670
This theorem is referenced by:  lesub3d  10220  supaddc  10563  rpnnen1lem5  11283  xleadd1a  11528  fzoaddel  11953  fladdz  12044  ltdifltdiv  12052  bernneq3  12386  caucvgrlem  13703  caucvgrlemOLD  13704  eirrlem  14223  vdwlem3  14885  vdwlem9  14891  vdwlem10  14892  2expltfac  15015  pcoass  21941  trirn  22240  minveclem2  22254  ovolfiniun  22328  ovolshftlem1  22336  unmbl  22365  uniioombllem5  22419  opnmbllem  22433  vitalilem2  22441  itg2split  22581  dvfsumlem2  22853  dvfsumlem4  22855  dvfsum2  22860  fta1glem2  22989  coemullem  23069  fta1lem  23125  leibpi  23730  log2tlbnd  23733  jensenlem2  23775  harmonicubnd  23797  harmonicbnd4  23798  lgamgulmlem5  23820  lgambdd  23824  ppiub  23992  bcmono  24065  bposlem5  24076  mulog2sumlem2  24233  selberg2lem  24248  chpdifbndlem1  24251  pntrlog2bndlem2  24276  pntpbnd2  24285  pntibndlem2  24289  pntlemg  24296  pntlemk  24304  pntlemo  24305  qabvle  24323  ostth2lem3  24333  minvecolem2  26359  nndiffz1  28199  reofld  28439  dya2icoseg  28935  rescon  29754  poimirlem15  31659  opnmbllem0  31680  itg2addnclem3  31699  bfplem2  31859  pellexlem2  35384  rmygeid  35524  jm3.1lem2  35583  fzisoeu  37131  absnpncan2d  37133  absnpncan3d  37138  leadd12dd  37151  iccshift  37208  fsumnncl  37229  climsuselem1  37262  sumnnodd  37286  dvbdfbdioolem2  37377  ioodvbdlimc1lem1  37379  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  dvnmul  37391  iblspltprt  37423  itgspltprt  37429  itgiccshift  37430  itgperiod  37431  stoweidlem1  37434  stoweidlem11  37444  stoweidlem14  37447  stoweidlem26  37459  stoweidlem44  37478  stirlinglem11  37519  fourierdlem10  37552  fourierdlem11  37553  fourierdlem15  37557  fourierdlem30  37572  fourierdlem42  37584  fourierdlem68  37610  fourierdlem79  37621  fourierdlem92  37634  carageniuncllem2  37856
  Copyright terms: Public domain W3C validator