Theorem le2addd 11935

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 11338	. 2 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℝ)
4		ltadd1d.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
5	4, 2	readdcld 11338	. 2 ⊢ (𝜑 → (𝐶 + 𝐵) ∈ ℝ)
6		lt2addd.4	. . 3 ⊢ (𝜑 → 𝐷 ∈ ℝ)
7	4, 6	readdcld 11338	. 2 ⊢ (𝜑 → (𝐶 + 𝐷) ∈ ℝ)
8		le2addd.5	. . 3 ⊢ (𝜑 → 𝐴 ≤ 𝐶)
9	1, 4, 2, 8	leadd1dd 11930	. 2 ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐵))
10		le2addd.6	. . 3 ⊢ (𝜑 → 𝐵 ≤ 𝐷)
11	2, 6, 4, 10	leadd2dd 11931	. 2 ⊢ (𝜑 → (𝐶 + 𝐵) ≤ (𝐶 + 𝐷))
12	3, 5, 7, 9, 11	letrd 11467	1 ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  (class class class)co 7420  ℝcr 11199   + caddc 11203   ≤ cle 11344

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-resscn 11257  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-mulcom 11264  ax-addass 11265  ax-mulass 11266  ax-distr 11267  ax-i2m1 11268  ax-1ne0 11269  ax-1rid 11270  ax-rnegex 11271  ax-rrecex 11272  ax-cnre 11273  ax-pre-lttri 11274  ax-pre-lttrn 11275  ax-pre-ltadd 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-po 5559  df-so 5560  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349

This theorem is used by:  supadd  12285  o1add  15781  o1sub  15783  o1fsum  15980  sadcaddlem  16627  4sqlem11  17133  4sqlem12  17134  4sqlem15  17137  4sqlem16  17138  prdsxmetlem  24687  nrmmetd  24893  nmotri  25058  pcoass  25345  minveclem2  25747  ovollb2lem  25809  ovolunlem1a  25817  ovoliunlem1  25823  nulmbl2  25857  ioombl1lem4  25882  uniioombllem5  25908  itg2splitlem  26069  itg2addlem  26079  ibladdlem  26140  ulmbdd  26725  cxpaddle  27080  ang180lem2  27138  fsumharmonic  27339  lgamgulmlem3  27358  lgamgulmlem5  27360  ppiub  27531  lgsdirprm  27658  lgsqrlem2  27674  lgseisenlem2  27703  2sqlem8  27753  vmadivsumb  27810  dchrisumlem2  27817  dchrisum0lem1b  27842  mulog2sumlem1  27861  mulog2sumlem2  27862  selbergb  27876  selberg2b  27879  chpdifbndlem1  27880  logdivbnd  27883  selberg3lem2  27885  pntrlog2bnd  27911  pntpbnd2  27914  pntibndlem2  27918  pntlemr  27929  ostth2lem2  27961  ostth3  27965  smcnlem  31299  minvecolem2  31477  stadd3i  32850  le2halvesd  33348  wrdt2ind  33516  cos9thpiminplylem1  34414  dnibndlem9  37352  ismblfin  38579  itg2addnc  38592  ibladdnclem  38594  ftc1anclem7  38617  intlewftc  43111  aks4d1p1p2  43120  dvle2  43122  posbezout  43150  2np3bcnp1  43194  sticksstones7  43202  sticksstones12a  43207  sticksstones12  43208  pell1qrgaplem  43879  pellqrex  43885  pellfundgt1  43889  areaquad  44217  imo72b2lem0  45164  int-ineq1stprincd  45191  dvdivbd  46932  fourierdlem30  47146  sge0xaddlem1  47442  sge0xaddlem2  47443  carageniuncllem2  47531  hoidmvlelem2  47605  hspmbllem2  47636  smfmullem1  47800