Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elxrge0 | Structured version Visualization version GIF version |
Description: Elementhood in the set of nonnegative extended reals. (Contributed by Mario Carneiro, 28-Jun-2014.) |
Ref | Expression |
---|---|
elxrge0 | ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1085 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞)) | |
2 | 0xr 10688 | . . 3 ⊢ 0 ∈ ℝ* | |
3 | pnfxr 10695 | . . 3 ⊢ +∞ ∈ ℝ* | |
4 | elicc1 12783 | . . 3 ⊢ ((0 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞))) | |
5 | 2, 3, 4 | mp2an 690 | . 2 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 ≤ +∞)) |
6 | pnfge 12526 | . . . 4 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞) | |
7 | 6 | adantr 483 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) → 𝐴 ≤ +∞) |
8 | 7 | pm4.71i 562 | . 2 ⊢ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ↔ ((𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴) ∧ 𝐴 ≤ +∞)) |
9 | 1, 5, 8 | 3bitr4i 305 | 1 ⊢ (𝐴 ∈ (0[,]+∞) ↔ (𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∧ w3a 1083 ∈ wcel 2114 class class class wbr 5066 (class class class)co 7156 0cc0 10537 +∞cpnf 10672 ℝ*cxr 10674 ≤ cle 10676 [,]cicc 12742 |
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 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-addrcl 10598 ax-rnegex 10608 ax-cnre 10610 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 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-rab 3147 df-v 3496 df-sbc 3773 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4839 df-br 5067 df-opab 5129 df-id 5460 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-iota 6314 df-fun 6357 df-fv 6363 df-ov 7159 df-oprab 7160 df-mpo 7161 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-icc 12746 |
This theorem is referenced by: 0e0iccpnf 12848 ge0xaddcl 12851 ge0xmulcl 12852 xnn0xrge0 12892 xrge0subm 20586 psmetxrge0 22923 isxmet2d 22937 prdsdsf 22977 prdsxmetlem 22978 comet 23123 stdbdxmet 23125 xrge0gsumle 23441 xrge0tsms 23442 metdsf 23456 metds0 23458 metdstri 23459 metdsre 23461 metdseq0 23462 metdscnlem 23463 metnrmlem1a 23466 xrhmeo 23550 lebnumlem1 23565 xrge0f 24332 itg2const2 24342 itg2uba 24344 itg2mono 24354 itg2gt0 24361 itg2cnlem2 24363 itg2cn 24364 iblss 24405 itgle 24410 itgeqa 24414 ibladdlem 24420 iblabs 24429 iblabsr 24430 iblmulc2 24431 itgsplit 24436 bddmulibl 24439 xrge0addge 30481 xrge0infss 30484 xrge0addcld 30486 xrge0subcld 30487 xrge00 30673 xrge0tsmsd 30692 esummono 31313 gsumesum 31318 esumsnf 31323 esumrnmpt2 31327 esumpmono 31338 hashf2 31343 measge0 31466 measle0 31467 measssd 31474 measunl 31475 omssubaddlem 31557 omssubadd 31558 carsgsigalem 31573 pmeasmono 31582 sibfinima 31597 prob01 31671 dstrvprob 31729 itg2addnclem 34958 ibladdnclem 34963 iblabsnc 34971 iblmulc2nc 34972 bddiblnc 34977 ftc1anclem4 34985 ftc1anclem5 34986 ftc1anclem6 34987 ftc1anclem7 34988 ftc1anclem8 34989 ftc1anc 34990 xrge0ge0 41635 rrxsphere 44755 |
Copyright terms: Public domain | W3C validator |