![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > subge0d | Structured version Visualization version GIF version |
Description: Nonnegative subtraction. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
leidd.1 | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
ltnegd.2 | ⊢ (𝜑 → 𝐵 ∈ ℝ) |
Ref | Expression |
---|---|
subge0d | ⊢ (𝜑 → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leidd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℝ) | |
2 | ltnegd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ ℝ) | |
3 | subge0 11006 | . 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → (0 ≤ (𝐴 − 𝐵) ↔ 𝐵 ≤ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∈ wcel 2081 class class class wbr 4966 (class class class)co 7021 ℝcr 10387 0cc0 10388 ≤ cle 10527 − cmin 10722 |
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 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 ax-resscn 10445 ax-1cn 10446 ax-icn 10447 ax-addcl 10448 ax-addrcl 10449 ax-mulcl 10450 ax-mulrcl 10451 ax-mulcom 10452 ax-addass 10453 ax-mulass 10454 ax-distr 10455 ax-i2m1 10456 ax-1ne0 10457 ax-1rid 10458 ax-rnegex 10459 ax-rrecex 10460 ax-cnre 10461 ax-pre-lttri 10462 ax-pre-lttrn 10463 ax-pre-ltadd 10464 |
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-reu 3112 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-br 4967 df-opab 5029 df-mpt 5046 df-id 5353 df-po 5367 df-so 5368 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-riota 6982 df-ov 7024 df-oprab 7025 df-mpo 7026 df-er 8144 df-en 8363 df-dom 8364 df-sdom 8365 df-pnf 10528 df-mnf 10529 df-xr 10530 df-ltxr 10531 df-le 10532 df-sub 10724 df-neg 10725 |
This theorem is referenced by: ofsubge0 11490 uzsubsubfz 12784 modsubdir 13163 modsumfzodifsn 13167 serle 13280 discr 13456 bcval5 13533 fzomaxdiflem 14541 sqreulem 14558 amgm2 14568 climle 14835 rlimle 14843 iseralt 14880 fsumle 14992 cvgcmp 15009 binomrisefac 15234 smuval2 15669 pcz 16051 4sqlem15 16129 mndodconglem 18405 ipcau2 23525 pjthlem1 23728 ovolicc2lem4 23809 vitalilem2 23898 itg1lea 24001 dvlip 24278 dvge0 24291 dvle 24292 dvivthlem1 24293 dvfsumlem2 24312 dvfsumlem4 24314 loglesqrt 25025 emcllem6 25265 harmoniclbnd 25273 basellem9 25353 gausslemma2dlem0h 25626 lgseisenlem1 25638 2sqmod 25699 vmadivsum 25745 rplogsumlem1 25747 dchrisumlem2 25753 rplogsum 25790 vmalogdivsum2 25801 selberg2lem 25813 logdivbnd 25819 pntpbnd2 25850 pntibndlem2 25854 pntlemg 25861 pntlemn 25863 ttgcontlem1 26359 brbtwn2 26379 axpaschlem 26414 axcontlem8 26445 crctcsh 27294 clwlkclwwlklem2a1 27462 clwlkclwwlklem2fv2 27466 pjhthlem1 28864 leop2 29597 pjssposi 29645 fdvposle 31494 rddif2 33432 dnibndlem4 33436 broucube 34483 areacirclem2 34540 areacirclem4 34542 areacirclem5 34543 areacirc 34544 acongrep 39088 lptre2pt 41489 dvnmul 41796 dvnprodlem1 41799 dvnprodlem2 41800 stoweidlem1 41855 stoweidlem26 41880 stoweidlem62 41916 wallispilem4 41922 fourierdlem26 41987 fourierdlem42 42003 fourierdlem65 42025 fourierdlem75 42035 elaa2lem 42087 etransclem3 42091 etransclem7 42095 etransclem10 42098 etransclem20 42108 etransclem21 42109 etransclem22 42110 etransclem24 42112 etransclem27 42115 hoidmvlelem1 42446 nnpw2pmod 44151 2itscp 44276 |
Copyright terms: Public domain | W3C validator |