Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pnfge | Structured version Visualization version GIF version |
Description: Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.) |
Ref | Expression |
---|---|
pnfge | ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pnfnlt 12685 | . 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴) | |
2 | pnfxr 10852 | . . 3 ⊢ +∞ ∈ ℝ* | |
3 | xrlenlt 10863 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴)) | |
4 | 2, 3 | mpan2 691 | . 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴)) |
5 | 1, 4 | mpbird 260 | 1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∈ wcel 2112 class class class wbr 5039 +∞cpnf 10829 ℝ*cxr 10831 < clt 10832 ≤ cle 10833 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pow 5243 ax-pr 5307 ax-un 7501 ax-cnex 10750 ax-resscn 10751 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ne 2933 df-nel 3037 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-pw 4501 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-opab 5102 df-xp 5542 df-cnv 5544 df-pnf 10834 df-mnf 10835 df-xr 10836 df-ltxr 10837 df-le 10838 |
This theorem is referenced by: xnn0n0n1ge2b 12688 0lepnf 12689 nltpnft 12719 xrre2 12725 xnn0lem1lt 12799 xleadd1a 12808 xlt2add 12815 xsubge0 12816 xlesubadd 12818 xlemul1a 12843 elicore 12952 elico2 12964 iccmax 12976 elxrge0 13010 nfile 13891 hashdom 13911 hashdomi 13912 hashge1 13921 hashss 13941 hashge2el2difr 14012 pcdvdsb 16385 pc2dvds 16395 pcaddlem 16404 xrsdsreclblem 20363 leordtvallem1 22061 lecldbas 22070 isxmet2d 23179 blssec 23287 nmoix 23581 nmoleub 23583 xrtgioo 23657 xrge0tsms 23685 metdstri 23702 nmoleub2lem 23965 ovolf 24333 ovollb2 24340 ovoliun 24356 ovolre 24376 voliunlem3 24403 volsup 24407 icombl 24415 ioombl 24416 ismbfd 24490 itg2seq 24594 dvfsumrlim 24882 dvfsumrlim2 24883 radcnvcl 25263 xrlimcnp 25805 logfacbnd3 26058 log2sumbnd 26379 tgldimor 26547 xrdifh 30775 xrge0tsmsd 30990 unitssxrge0 31518 tpr2rico 31530 lmxrge0 31570 esumle 31692 esumlef 31696 esumpinfval 31707 esumpinfsum 31711 esumcvgsum 31722 ddemeas 31870 sxbrsigalem2 31919 omssubadd 31933 carsgclctunlem3 31953 signsply0 32196 ismblfin 35504 xrgepnfd 42484 supxrgelem 42490 supxrge 42491 infrpge 42504 xrlexaddrp 42505 infleinflem1 42523 infleinf 42525 infxrpnf 42601 pnfged 42630 ge0xrre 42685 iblsplit 43125 ismbl3 43145 ovolsplit 43147 sge0cl 43537 sge0less 43548 sge0pr 43550 sge0le 43563 sge0split 43565 carageniuncl 43679 ovnsubaddlem1 43726 hspmbl 43785 pimiooltgt 43863 pgrpgt2nabl 45318 |
Copyright terms: Public domain | W3C validator |