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

Theorem leadd1dd 10260
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 10240 . 2  |-  ( ph  ->  ( A  <_  B  <->  ( A  +  C )  <_  ( B  +  C ) ) )
61, 5mpbid 215 1  |-  ( ph  ->  ( A  +  C
)  <_  ( B  +  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   class class class wbr 4418  (class class class)co 6320   RRcr 9569    + caddc 9573    <_ cle 9707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-resscn 9627  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-addrcl 9631  ax-mulcl 9632  ax-mulrcl 9633  ax-mulcom 9634  ax-addass 9635  ax-mulass 9636  ax-distr 9637  ax-i2m1 9638  ax-1ne0 9639  ax-1rid 9640  ax-rnegex 9641  ax-rrecex 9642  ax-cnre 9643  ax-pre-lttri 9644  ax-pre-lttrn 9645  ax-pre-ltadd 9646
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-mpt 4479  df-id 4771  df-po 4777  df-so 4778  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-ov 6323  df-er 7394  df-en 7601  df-dom 7602  df-sdom 7603  df-pnf 9708  df-mnf 9709  df-xr 9710  df-ltxr 9711  df-le 9712
This theorem is referenced by:  lesub3d  10264  supaddc  10607  rpnnen1lem5  11328  xleadd1a  11573  fzoaddel  12004  fladdz  12096  ltdifltdiv  12104  bernneq3  12438  caucvgrlem  13791  caucvgrlemOLD  13792  eirrlem  14311  vdwlem3  14988  vdwlem9  14994  vdwlem10  14995  2expltfac  15118  pcoass  22110  trirn  22409  minveclem2  22423  minveclem2OLD  22435  ovolfiniun  22509  ovolshftlem1  22517  unmbl  22546  uniioombllem5  22601  opnmbllem  22615  vitalilem2  22623  itg2split  22763  dvfsumlem2  23035  dvfsumlem4  23037  dvfsum2  23042  fta1glem2  23173  coemullem  23260  fta1lem  23316  leibpi  23924  log2tlbnd  23927  jensenlem2  23969  harmonicubnd  23991  harmonicbnd4  23992  lgamgulmlem5  24014  lgambdd  24018  ppiub  24188  bcmono  24261  bposlem5  24272  mulog2sumlem2  24429  selberg2lem  24444  chpdifbndlem1  24447  pntrlog2bndlem2  24472  pntpbnd2  24481  pntibndlem2  24485  pntlemg  24492  pntlemk  24500  pntlemo  24501  qabvle  24519  ostth2lem3  24529  minvecolem2  26573  minvecolem2OLD  26583  nndiffz1  28418  reofld  28654  dya2icoseg  29149  rescon  30019  poimirlem15  32001  opnmbllem0  32022  itg2addnclem3  32041  bfplem2  32201  pellexlem2  35720  rmygeid  35860  jm3.1lem2  35919  fzisoeu  37593  absnpncan2d  37595  absnpncan3d  37600  leadd12dd  37613  iccshift  37704  fsumnncl  37735  climsuselem1  37772  sumnnodd  37796  dvbdfbdioolem2  37887  ioodvbdlimc1lem1  37889  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem1OLD  37891  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  dvnmul  37904  iblspltprt  37936  itgspltprt  37942  itgiccshift  37943  itgperiod  37944  stoweidlem1  37962  stoweidlem11  37972  stoweidlem14  37975  stoweidlem26  37987  stoweidlem44  38006  stirlinglem11  38047  fourierdlem10  38080  fourierdlem11  38081  fourierdlem15  38085  fourierdlem30  38100  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem68  38139  fourierdlem79  38150  fourierdlem92  38163  sge0xaddlem1  38378  carageniuncllem2  38451  hoidmv1lelem1  38520  ovolval5lem1  38581
  Copyright terms: Public domain W3C validator