![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > le2addd | Structured version Visualization version GIF version |
Description: Adding both side of two inequalities. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
leidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltnegd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
ltadd1d.3 | ⊢ (𝜑 → 𝐶 ∈ ℝ) |
lt2addd.4 | ⊢ (𝜑 → 𝐷 ∈ ℝ) |
le2addd.5 | ⊢ (𝜑 → 𝐴 ≤ 𝐶) |
le2addd.6 | ⊢ (𝜑 → 𝐵 ≤ 𝐷) |
Ref | Expression |
---|---|
le2addd | ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | le2addd.5 | . 2 ⊢ (𝜑 → 𝐴 ≤ 𝐶) | |
2 | le2addd.6 | . 2 ⊢ (𝜑 → 𝐵 ≤ 𝐷) | |
3 | leidd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
4 | ltnegd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
5 | ltadd1d.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ) | |
6 | lt2addd.4 | . . 3 ⊢ (𝜑 → 𝐷 ∈ ℝ) | |
7 | le2add 10976 | . . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))) | |
8 | 3, 4, 5, 6, 7 | syl22anc 835 | . 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐶 ∧ 𝐵 ≤ 𝐷) → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷))) |
9 | 1, 2, 8 | mp2and 695 | 1 ⊢ (𝜑 → (𝐴 + 𝐵) ≤ (𝐶 + 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∈ wcel 2083 class class class wbr 4968 (class class class)co 7023 ℝcr 10389 + caddc 10393 ≤ cle 10529 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 ax-resscn 10447 ax-1cn 10448 ax-icn 10449 ax-addcl 10450 ax-addrcl 10451 ax-mulcl 10452 ax-mulrcl 10453 ax-mulcom 10454 ax-addass 10455 ax-mulass 10456 ax-distr 10457 ax-i2m1 10458 ax-1ne0 10459 ax-1rid 10460 ax-rnegex 10461 ax-rrecex 10462 ax-cnre 10463 ax-pre-lttri 10464 ax-pre-lttrn 10465 ax-pre-ltadd 10466 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-nel 3093 df-ral 3112 df-rex 3113 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-po 5369 df-so 5370 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-ov 7026 df-er 8146 df-en 8365 df-dom 8366 df-sdom 8367 df-pnf 10530 df-mnf 10531 df-xr 10532 df-ltxr 10533 df-le 10534 |
This theorem is referenced by: supadd 11463 o1add 14808 o1sub 14810 o1fsum 15005 sadcaddlem 15643 4sqlem11 16124 4sqlem12 16125 4sqlem15 16128 4sqlem16 16129 prdsxmetlem 22665 nrmmetd 22871 nmotri 23035 pcoass 23315 minveclem2 23716 ovollb2lem 23776 ovolunlem1a 23784 ovoliunlem1 23790 nulmbl2 23824 ioombl1lem4 23849 uniioombllem5 23875 itg2splitlem 24036 itg2addlem 24046 ibladdlem 24107 ulmbdd 24673 cxpaddle 25018 ang180lem2 25073 fsumharmonic 25275 lgamgulmlem3 25294 lgamgulmlem5 25296 ppiub 25466 lgsdirprm 25593 lgsqrlem2 25609 lgseisenlem2 25638 2sqlem8 25688 vmadivsumb 25745 dchrisumlem2 25752 dchrisum0lem1b 25777 mulog2sumlem1 25796 mulog2sumlem2 25797 selbergb 25811 selberg2b 25814 chpdifbndlem1 25815 logdivbnd 25818 selberg3lem2 25820 pntrlog2bnd 25846 pntpbnd2 25849 pntibndlem2 25853 pntlemr 25864 ostth2lem2 25896 ostth3 25900 smcnlem 28161 minvecolem2 28339 stadd3i 29712 le2halvesd 30163 wrdt2ind 30302 dnibndlem9 33436 ismblfin 34485 itg2addnc 34498 ibladdnclem 34500 ftc1anclem7 34525 pell1qrgaplem 38976 pellqrex 38982 pellfundgt1 38986 areaquad 39329 imo72b2lem0 40022 int-ineq1stprincd 40052 dvdivbd 41771 fourierdlem30 41986 sge0xaddlem2 42280 carageniuncllem2 42368 |
Copyright terms: Public domain | W3C validator |