Theorem le2addd 11807

Description: Adding both side of two inequalities. (Contributed by Mario Carneiro, 27-May-2016.) (Proof shortened by Glauco Siliprandi, 5-Apr-2020.)

Hypotheses

Ref	Expression
leidd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltnegd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
ltadd1d.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
lt2addd.4	⊢ (𝜑 → 𝐷 ∈ ℝ)
le2addd.5	⊢ (𝜑 → 𝐴 ≤ 𝐶)
le2addd.6	⊢ (𝜑 → 𝐵 ≤ 𝐷)

Assertion

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

Proof of Theorem le2addd

Step	Hyp	Ref	Expression
1		leidd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltnegd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3	1, 2	readdcld 11212	. 2 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
4		ltadd1d.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
5	4, 2	readdcld 11212	. 2 ⊢ (𝜑 → (𝐶 + 𝐵) ∈ ℝ)
6		lt2addd.4	. . 3 ⊢ (𝜑 → 𝐷 ∈ ℝ)
7	4, 6	readdcld 11212	. 2 ⊢ (𝜑 → (𝐶 + 𝐷) ∈ ℝ)
8		le2addd.5	. . 3 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
9	1, 4, 2, 8	leadd1dd 11802	. 2 ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐵))
10		le2addd.6	. . 3 ⊢ (𝜑 → 𝐵 ≤ 𝐷)
11	2, 6, 4, 10	leadd2dd 11803	. 2 ⊢ (𝜑 → (𝐶 + 𝐵) ≤ (𝐶 + 𝐷))
12	3, 5, 7, 9, 11	letrd 11341	1 ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5101  (class class class)co 7397  ℝcr 11073   + caddc 11077   ≤ cle 11218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7719  ax-resscn 11131  ax-1cn 11132  ax-icn 11133  ax-addcl 11134  ax-addrcl 11135  ax-mulcl 11136  ax-mulrcl 11137  ax-mulcom 11138  ax-addass 11139  ax-mulass 11140  ax-distr 11141  ax-i2m1 11142  ax-1ne0 11143  ax-1rid 11144  ax-rnegex 11145  ax-rrecex 11146  ax-cnre 11147  ax-pre-lttri 11148  ax-pre-lttrn 11149  ax-pre-ltadd 11150

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-po 5556  df-so 5557  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-ov 7400  df-er 8679  df-en 8929  df-dom 8930  df-sdom 8931  df-pnf 11219  df-mnf 11220  df-xr 11221  df-ltxr 11222  df-le 11223

This theorem is referenced by:  supadd  12161  o1add  15642  o1sub  15644  o1fsum  15842  sadcaddlem  16492  4sqlem11  16992  4sqlem12  16993  4sqlem15  16996  4sqlem16  16997  prdsxmetlem  24429  nrmmetd  24635  nmotri  24800  pcoass  25087  minveclem2  25489  ovollb2lem  25551  ovolunlem1a  25559  ovoliunlem1  25565  nulmbl2  25599  ioombl1lem4  25624  uniioombllem5  25650  itg2splitlem  25811  itg2addlem  25821  ibladdlem  25883  ulmbdd  26462  cxpaddle  26818  ang180lem2  26876  fsumharmonic  27077  lgamgulmlem3  27096  lgamgulmlem5  27098  ppiub  27269  lgsdirprm  27396  lgsqrlem2  27412  lgseisenlem2  27441  2sqlem8  27491  vmadivsumb  27548  dchrisumlem2  27555  dchrisum0lem1b  27580  mulog2sumlem1  27599  mulog2sumlem2  27600  selbergb  27614  selberg2b  27617  chpdifbndlem1  27618  logdivbnd  27621  selberg3lem2  27623  pntrlog2bnd  27649  pntpbnd2  27652  pntibndlem2  27656  pntlemr  27667  ostth2lem2  27699  ostth3  27703  smcnlem  30901  minvecolem2  31079  stadd3i  32452  le2halvesd  32959  wrdt2ind  33132  cos9thpiminplylem1  34080  dnibndlem9  36925  ismblfin  38161  itg2addnc  38174  ibladdnclem  38176  ftc1anclem7  38199  intlewftc  42679  aks4d1p1p2  42688  dvle2  42690  posbezout  42718  2np3bcnp1  42762  sticksstones7  42770  sticksstones12a  42775  sticksstones12  42776  pell1qrgaplem  43451  pellqrex  43457  pellfundgt1  43461  areaquad  43794  imo72b2lem0  44742  int-ineq1stprincd  44769  dvdivbd  46498  fourierdlem30  46712  sge0xaddlem1  47008  sge0xaddlem2  47009  carageniuncllem2  47097  hoidmvlelem2  47171  hspmbllem2  47202  smfmullem1  47366