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 10645 | . 2 ⊢ 0 ∈ ℝ | |
2 | elicopnf 12836 | . 2 ⊢ (0 ∈ ℝ → (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∈ wcel 2114 class class class wbr 5068 (class class class)co 7158 ℝcr 10538 0cc0 10539 +∞cpnf 10674 ≤ cle 10678 [,)cico 12743 |
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 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463 ax-cnex 10595 ax-resscn 10596 ax-1cn 10597 ax-addrcl 10600 ax-rnegex 10610 ax-cnre 10612 ax-pre-lttri 10613 ax-pre-lttrn 10614 |
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 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ne 3019 df-nel 3126 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-pw 4543 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-br 5069 df-opab 5131 df-mpt 5149 df-id 5462 df-po 5476 df-so 5477 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-res 5569 df-ima 5570 df-iota 6316 df-fun 6359 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-fv 6365 df-ov 7161 df-oprab 7162 df-mpo 7163 df-er 8291 df-en 8512 df-dom 8513 df-sdom 8514 df-pnf 10679 df-mnf 10680 df-xr 10681 df-ltxr 10682 df-le 10683 df-ico 12747 |
This theorem is referenced by: nn0rp0 12846 rge0ssre 12847 0e0icopnf 12849 ge0addcl 12851 ge0mulcl 12852 fsumge0 15152 fprodge0 15349 isabvd 19593 abvge0 19598 nmolb 23328 nmoge0 23332 nmoi 23339 icopnfcnv 23548 cphsqrtcl 23790 tcphcph 23842 cphsscph 23856 ovolfsf 24074 ovolmge0 24080 ovolunlem1a 24099 ovoliunlem1 24105 ovolicc2lem4 24123 ioombl1lem4 24164 uniioombllem2 24186 uniioombllem6 24191 0plef 24275 i1fpos 24309 mbfi1fseqlem1 24318 mbfi1fseqlem3 24320 mbfi1fseqlem4 24321 mbfi1fseqlem5 24322 mbfi1fseqlem6 24323 mbfi1flimlem 24325 itg2const 24343 itg2const2 24344 itg2mulclem 24349 itg2mulc 24350 itg2monolem1 24353 itg2mono 24356 itg2addlem 24361 itg2gt0 24363 itg2cnlem1 24364 itg2cnlem2 24365 itg2cn 24366 iblconst 24420 itgconst 24421 ibladdlem 24422 itgaddlem1 24425 iblabslem 24430 iblabs 24431 iblmulc2 24433 itgmulc2lem1 24434 bddmulibl 24441 itggt0 24444 itgcn 24445 dvge0 24605 dvle 24606 dvfsumrlim 24630 cxpcn3lem 25330 cxpcn3 25331 resqrtcn 25332 loglesqrt 25341 areaf 25541 areacl 25542 areage0 25543 rlimcnp3 25547 jensenlem2 25567 jensen 25568 amgmlem 25569 amgm 25570 dchrisumlem3 26069 dchrmusumlema 26071 dchrmusum2 26072 dchrvmasumlem2 26076 dchrvmasumiflem1 26079 dchrisum0lema 26092 dchrisum0lem1b 26093 dchrisum0lem1 26094 dchrisum0lem2 26096 axcontlem2 26753 axcontlem7 26758 axcontlem8 26759 axcontlem10 26761 rge0scvg 31194 esumpcvgval 31339 hasheuni 31346 esumcvg 31347 sibfof 31600 mbfposadd 34941 itg2addnclem2 34946 itg2addnclem3 34947 itg2addnc 34948 itg2gt0cn 34949 ibladdnclem 34950 itgaddnclem1 34952 iblabsnclem 34957 iblabsnc 34958 iblmulc2nc 34959 itgmulc2nclem1 34960 bddiblnc 34964 itggt0cn 34966 ftc1anclem3 34971 ftc1anclem4 34972 ftc1anclem5 34973 ftc1anclem6 34974 ftc1anclem7 34975 ftc1anclem8 34976 areacirclem2 34985 sge0iunmptlemfi 42702 digvalnn0 44666 nn0digval 44667 dignn0fr 44668 dig2nn1st 44672 digexp 44674 2sphere 44743 itsclc0 44765 itsclc0b 44766 |
Copyright terms: Public domain | W3C validator |