![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elrege0 | Structured version Visualization version GIF version |
Description: The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) |
Ref | Expression |
---|---|
elrege0 | ⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 10632 | . 2 ⊢ 0 ∈ ℝ | |
2 | elicopnf 12823 | . 2 ⊢ (0 ∈ ℝ → (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∈ wcel 2111 class class class wbr 5030 (class class class)co 7135 ℝcr 10525 0cc0 10526 +∞cpnf 10661 ≤ cle 10665 [,)cico 12728 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pow 5231 ax-pr 5295 ax-un 7441 ax-cnex 10582 ax-resscn 10583 ax-1cn 10584 ax-addrcl 10587 ax-rnegex 10597 ax-cnre 10599 ax-pre-lttri 10600 ax-pre-lttrn 10601 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-nel 3092 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-csb 3829 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-pw 4499 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-po 5438 df-so 5439 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-rn 5530 df-res 5531 df-ima 5532 df-iota 6283 df-fun 6326 df-fn 6327 df-f 6328 df-f1 6329 df-fo 6330 df-f1o 6331 df-fv 6332 df-ov 7138 df-oprab 7139 df-mpo 7140 df-er 8272 df-en 8493 df-dom 8494 df-sdom 8495 df-pnf 10666 df-mnf 10667 df-xr 10668 df-ltxr 10669 df-le 10670 df-ico 12732 |
This theorem is referenced by: nn0rp0 12833 rge0ssre 12834 0e0icopnf 12836 ge0addcl 12838 ge0mulcl 12839 fsumge0 15142 fprodge0 15339 isabvd 19584 abvge0 19589 nmolb 23323 nmoge0 23327 nmoi 23334 icopnfcnv 23547 cphsqrtcl 23789 tcphcph 23841 cphsscph 23855 ovolfsf 24075 ovolmge0 24081 ovolunlem1a 24100 ovoliunlem1 24106 ovolicc2lem4 24124 ioombl1lem4 24165 uniioombllem2 24187 uniioombllem6 24192 0plef 24276 i1fpos 24310 mbfi1fseqlem1 24319 mbfi1fseqlem3 24321 mbfi1fseqlem4 24322 mbfi1fseqlem5 24323 mbfi1fseqlem6 24324 mbfi1flimlem 24326 itg2const 24344 itg2const2 24345 itg2mulclem 24350 itg2mulc 24351 itg2monolem1 24354 itg2mono 24357 itg2addlem 24362 itg2gt0 24364 itg2cnlem1 24365 itg2cnlem2 24366 itg2cn 24367 iblconst 24421 itgconst 24422 ibladdlem 24423 itgaddlem1 24426 iblabslem 24431 iblabs 24432 iblmulc2 24434 itgmulc2lem1 24435 bddmulibl 24442 bddiblnc 24445 itggt0 24447 itgcn 24448 dvge0 24609 dvle 24610 dvfsumrlim 24634 cxpcn3lem 25336 cxpcn3 25337 resqrtcn 25338 loglesqrt 25347 areaf 25547 areacl 25548 areage0 25549 rlimcnp3 25553 jensenlem2 25573 jensen 25574 amgmlem 25575 amgm 25576 dchrisumlem3 26075 dchrmusumlema 26077 dchrmusum2 26078 dchrvmasumlem2 26082 dchrvmasumiflem1 26085 dchrisum0lema 26098 dchrisum0lem1b 26099 dchrisum0lem1 26100 dchrisum0lem2 26102 axcontlem2 26759 axcontlem7 26764 axcontlem8 26765 axcontlem10 26767 rge0scvg 31302 esumpcvgval 31447 hasheuni 31454 esumcvg 31455 sibfof 31708 mbfposadd 35104 itg2addnclem2 35109 itg2addnclem3 35110 itg2addnc 35111 itg2gt0cn 35112 ibladdnclem 35113 itgaddnclem1 35115 iblabsnclem 35120 iblabsnc 35121 iblmulc2nc 35122 itgmulc2nclem1 35123 itggt0cn 35127 ftc1anclem3 35132 ftc1anclem4 35133 ftc1anclem5 35134 ftc1anclem6 35135 ftc1anclem7 35136 ftc1anclem8 35137 areacirclem2 35146 sge0iunmptlemfi 43052 digvalnn0 45013 nn0digval 45014 dignn0fr 45015 dig2nn1st 45019 digexp 45021 2sphere 45163 itsclc0 45185 itsclc0b 45186 |
Copyright terms: Public domain | W3C validator |