![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 0e0icopnf | Structured version Visualization version GIF version |
Description: 0 is a member of (0[,)+∞). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
0e0icopnf | ⊢ 0 ∈ (0[,)+∞) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 10328 | . 2 ⊢ 0 ∈ ℝ | |
2 | 0le0 11417 | . 2 ⊢ 0 ≤ 0 | |
3 | elrege0 12525 | . 2 ⊢ (0 ∈ (0[,)+∞) ↔ (0 ∈ ℝ ∧ 0 ≤ 0)) | |
4 | 1, 2, 3 | mpbir2an 703 | 1 ⊢ 0 ∈ (0[,)+∞) |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2157 class class class wbr 4841 (class class class)co 6876 ℝcr 10221 0cc0 10222 +∞cpnf 10358 ≤ cle 10362 [,)cico 12422 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 ax-un 7181 ax-cnex 10278 ax-resscn 10279 ax-1cn 10280 ax-addrcl 10283 ax-rnegex 10293 ax-cnre 10295 ax-pre-lttri 10296 ax-pre-lttrn 10297 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-nel 3073 df-ral 3092 df-rex 3093 df-rab 3096 df-v 3385 df-sbc 3632 df-csb 3727 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-pw 4349 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-br 4842 df-opab 4904 df-mpt 4921 df-id 5218 df-po 5231 df-so 5232 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 df-iota 6062 df-fun 6101 df-fn 6102 df-f 6103 df-f1 6104 df-fo 6105 df-f1o 6106 df-fv 6107 df-ov 6879 df-oprab 6880 df-mpt2 6881 df-er 7980 df-en 8194 df-dom 8195 df-sdom 8196 df-pnf 10363 df-mnf 10364 df-xr 10365 df-ltxr 10366 df-le 10367 df-ico 12426 |
This theorem is referenced by: fsumge0 14862 fprodge0 15057 rege0subm 20121 rge0srg 20136 itg2cnlem1 23866 ibladdlem 23924 itgaddlem1 23927 iblabslem 23932 iblabs 23933 iblmulc2 23935 itgmulc2lem1 23936 bddmulibl 23943 itggt0 23946 itgcn 23947 cxpcn3 24830 rlimcnp3 25043 efrlim 25045 fsumrp0cl 30203 xrge0slmod 30352 esumpfinvallem 30644 ibladdnclem 33946 itgaddnclem1 33948 iblabsnclem 33953 iblabsnc 33954 iblmulc2nc 33955 itgmulc2nclem1 33956 itggt0cn 33962 ftc1anclem8 33972 sge0z 41323 sge0tsms 41328 hoidmvcl 41530 dig0 43187 |
Copyright terms: Public domain | W3C validator |