Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lesub2dd | Structured version Visualization version GIF version |
Description: Subtraction of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.) |
Ref | Expression |
---|---|
leidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltnegd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
ltadd1d.3 | ⊢ (𝜑 → 𝐶 ∈ ℝ) |
leadd1dd.4 | ⊢ (𝜑 → 𝐴 ≤ 𝐵) |
Ref | Expression |
---|---|
lesub2dd | ⊢ (𝜑 → (𝐶 − 𝐵) ≤ (𝐶 − 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leadd1dd.4 | . 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵) | |
2 | leidd.1 | . . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
3 | ltnegd.2 | . . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
4 | ltadd1d.3 | . . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ) | |
5 | 2, 3, 4 | lesub2d 11234 | . 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ (𝐶 − 𝐵) ≤ (𝐶 − 𝐴))) |
6 | 1, 5 | mpbid 234 | 1 ⊢ (𝜑 → (𝐶 − 𝐵) ≤ (𝐶 − 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 class class class wbr 5052 (class class class)co 7142 ℝcr 10522 ≤ cle 10662 − cmin 10856 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5189 ax-nul 5196 ax-pow 5252 ax-pr 5316 ax-un 7447 ax-resscn 10580 ax-1cn 10581 ax-icn 10582 ax-addcl 10583 ax-addrcl 10584 ax-mulcl 10585 ax-mulrcl 10586 ax-mulcom 10587 ax-addass 10588 ax-mulass 10589 ax-distr 10590 ax-i2m1 10591 ax-1ne0 10592 ax-1rid 10593 ax-rnegex 10594 ax-rrecex 10595 ax-cnre 10596 ax-pre-lttri 10597 ax-pre-lttrn 10598 ax-pre-ltadd 10599 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3488 df-sbc 3764 df-csb 3872 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-nul 4280 df-if 4454 df-pw 4527 df-sn 4554 df-pr 4556 df-op 4560 df-uni 4825 df-br 5053 df-opab 5115 df-mpt 5133 df-id 5446 df-po 5460 df-so 5461 df-xp 5547 df-rel 5548 df-cnv 5549 df-co 5550 df-dm 5551 df-rn 5552 df-res 5553 df-ima 5554 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-riota 7100 df-ov 7145 df-oprab 7146 df-mpo 7147 df-er 8275 df-en 8496 df-dom 8497 df-sdom 8498 df-pnf 10663 df-mnf 10664 df-xr 10665 df-ltxr 10666 df-le 10667 df-sub 10858 df-neg 10859 |
This theorem is referenced by: subeluzsub 12262 fzomaxdiflem 14687 icodiamlt 14780 climsqz 14982 rlimsqz 14991 climsup 15011 dvlog2lem 25221 atans2 25495 harmonicbnd4 25574 lgamgulmlem3 25594 gausslemma2dlem1a 25927 pntrlog2bndlem1 26139 pntrlog2bndlem5 26143 pntpbnd1 26148 pntlemj 26165 clwlkclwwlklem2fv1 27758 dnibndlem7 33830 dnibndlem8 33831 unbdqndv2lem2 33856 iccbnd 35150 irrapxlem3 39513 jm2.17a 39649 fzmaxdif 39670 ioodvbdlimc2lem 42309 dvnmul 42318 stoweidlem24 42399 stoweidlem41 42416 stoweidlem45 42420 fourierdlem7 42489 fourierdlem19 42501 fourierdlem42 42524 fourierdlem63 42544 fourierdlem65 42546 etransclem24 42633 etransclem27 42636 |
Copyright terms: Public domain | W3C validator |