Theorem leadd1dd 11285

Description: Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.)

Hypotheses

Ref	Expression
leidd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltnegd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
ltadd1d.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
leadd1dd.4	⊢ (𝜑 → 𝐴 ≤ 𝐵)

Assertion

Ref	Expression
leadd1dd	⊢ (𝜑 → (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))

Proof of Theorem leadd1dd

Step	Hyp	Ref	Expression
1		leadd1dd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		leidd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		ltnegd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4		ltadd1d.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
5	2, 3, 4	leadd1d 11265	. 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)))
6	1, 5	mpbid 235	1 ⊢ (𝜑 → (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))

Syntax hints:   → wi 4   ∈ wcel 2112   class class class wbr 5033  (class class class)co 7151  ℝcr 10567   + caddc 10571   ≤ cle 10707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-op 4530  df-uni 4800  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5431  df-po 5444  df-so 5445  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7154  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10708  df-mnf 10709  df-xr 10710  df-ltxr 10711  df-le 10712

This theorem is referenced by:  lesub3d  11289  supaddc  11637  rpnnen1lem5  12414  xleadd1a  12680  fzoaddel  13132  fladdz  13237  ltdifltdiv  13246  bernneq3  13635  caucvgrlem  15070  eirrlem  15598  vdwlem3  16367  vdwlem9  16373  vdwlem10  16374  2expltfac  16477  pcoass  23718  trirn  24093  minveclem2  24119  ovolfiniun  24194  ovolshftlem1  24202  unmbl  24230  uniioombllem5  24280  opnmbllem  24294  vitalilem2  24302  itg2split  24442  dvfsumlem2  24719  dvfsumlem4  24721  dvfsum2  24726  fta1glem2  24859  coemullem  24939  fta1lem  24995  leibpi  25620  log2tlbnd  25623  jensenlem2  25665  harmonicubnd  25687  harmonicbnd4  25688  lgamgulmlem5  25710  lgambdd  25714  ppiub  25880  bposlem5  25964  mulog2sumlem2  26211  selberg2lem  26226  chpdifbndlem1  26229  pntrlog2bndlem2  26254  pntpbnd2  26263  pntibndlem2  26267  pntlemg  26274  pntlemk  26282  pntlemo  26283  qabvle  26301  ostth2lem3  26311  minvecolem2  28750  nndiffz1  30624  wrdt2ind  30742  cycpmco2lem6  30917  reofld  31058  dya2icoseg  31756  resconn  32717  poimirlem15  35345  opnmbllem0  35366  itg2addnclem3  35383  bfplem2  35534  lcmineqlem19  39607  aks4d1p1p4  39630  aks4d1p1p7  39633  metakunt2  39641  pellexlem2  40137  rmygeid  40271  jm3.1lem2  40325  fzisoeu  42293  absnpncan2d  42295  absnpncan3d  42300  leadd12dd  42309  iccshift  42514  fsumnncl  42572  climsuselem1  42608  sumnnodd  42631  climleltrp  42677  dvbdfbdioolem2  42930  ioodvbdlimc1lem1  42932  ioodvbdlimc1lem2  42933  ioodvbdlimc2lem  42935  dvnmul  42944  iblspltprt  42974  itgspltprt  42980  itgiccshift  42981  itgperiod  42982  stoweidlem1  43002  stoweidlem11  43012  stoweidlem14  43015  stoweidlem26  43027  stoweidlem44  43045  stirlinglem11  43085  fourierdlem10  43118  fourierdlem11  43119  fourierdlem15  43123  fourierdlem30  43138  fourierdlem42  43150  fourierdlem68  43175  fourierdlem79  43186  fourierdlem92  43199  sge0xaddlem1  43431  carageniuncllem2  43520  hoidmv1lelem1  43589  ovolval5lem1  43650  smfmullem1  43782