Theorem leadd1dd 11102

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 11082	. 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐴 + 𝐶) ≤ (𝐵 + 𝐶)))
6	1, 5	mpbid 233	1 ⊢ (𝜑 → (𝐴 + 𝐶) ≤ (𝐵 + 𝐶))

Syntax hints:   → wi 4   ∈ wcel 2081   class class class wbr 4962  (class class class)co 7016  ℝcr 10382   + caddc 10386   ≤ cle 10522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-resscn 10440  ax-1cn 10441  ax-icn 10442  ax-addcl 10443  ax-addrcl 10444  ax-mulcl 10445  ax-mulrcl 10446  ax-mulcom 10447  ax-addass 10448  ax-mulass 10449  ax-distr 10450  ax-i2m1 10451  ax-1ne0 10452  ax-1rid 10453  ax-rnegex 10454  ax-rrecex 10455  ax-cnre 10456  ax-pre-lttri 10457  ax-pre-lttrn 10458  ax-pre-ltadd 10459

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-po 5362  df-so 5363  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-ov 7019  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527

This theorem is referenced by:  lesub3d  11106  supaddc  11456  rpnnen1lem5  12230  xleadd1a  12496  fzoaddel  12940  fladdz  13045  ltdifltdiv  13054  bernneq3  13442  caucvgrlem  14863  eirrlem  15390  vdwlem3  16148  vdwlem9  16154  vdwlem10  16155  2expltfac  16255  pcoass  23311  trirn  23686  minveclem2  23712  ovolfiniun  23785  ovolshftlem1  23793  unmbl  23821  uniioombllem5  23871  opnmbllem  23885  vitalilem2  23893  itg2split  24033  dvfsumlem2  24307  dvfsumlem4  24309  dvfsum2  24314  fta1glem2  24443  coemullem  24523  fta1lem  24579  leibpi  25202  log2tlbnd  25205  jensenlem2  25247  harmonicubnd  25269  harmonicbnd4  25270  lgamgulmlem5  25292  lgambdd  25296  ppiub  25462  bposlem5  25546  mulog2sumlem2  25793  selberg2lem  25808  chpdifbndlem1  25811  pntrlog2bndlem2  25836  pntpbnd2  25845  pntibndlem2  25849  pntlemg  25856  pntlemk  25864  pntlemo  25865  qabvle  25883  ostth2lem3  25893  minvecolem2  28343  nndiffz1  30197  wrdt2ind  30306  reofld  30567  dya2icoseg  31152  resconn  32101  poimirlem15  34438  opnmbllem0  34459  itg2addnclem3  34476  bfplem2  34633  pellexlem2  38912  rmygeid  39046  jm3.1lem2  39100  fzisoeu  41108  absnpncan2d  41110  absnpncan3d  41115  leadd12dd  41125  iccshift  41336  fsumnncl  41394  climsuselem1  41430  sumnnodd  41453  climleltrp  41499  dvbdfbdioolem2  41755  ioodvbdlimc1lem1  41757  ioodvbdlimc1lem2  41758  ioodvbdlimc2lem  41760  dvnmul  41769  iblspltprt  41799  itgspltprt  41805  itgiccshift  41806  itgperiod  41807  stoweidlem1  41828  stoweidlem11  41838  stoweidlem14  41841  stoweidlem26  41853  stoweidlem44  41871  stirlinglem11  41911  fourierdlem10  41944  fourierdlem11  41945  fourierdlem15  41949  fourierdlem30  41964  fourierdlem42  41976  fourierdlem68  42001  fourierdlem79  42012  fourierdlem92  42025  sge0xaddlem1  42257  carageniuncllem2  42346  hoidmv1lelem1  42415  ovolval5lem1  42476  smfmullem1  42608