| 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 13170 | . 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴) | |
| 2 | pnfxr 11315 | . . 3 ⊢ +∞ ∈ ℝ* | |
| 3 | xrlenlt 11326 | . . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴)) | |
| 4 | 2, 3 | mpan2 691 | . 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴)) |
| 5 | 1, 4 | mpbird 257 | 1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∈ wcel 2108 class class class wbr 5143 +∞cpnf 11292 ℝ*cxr 11294 < clt 11295 ≤ cle 11296 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-xp 5691 df-cnv 5693 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 |
| This theorem is referenced by: pnfged 13173 xnn0n0n1ge2b 13174 0lepnf 13175 nltpnft 13206 xrre2 13212 xnn0lem1lt 13286 xleadd1a 13295 xlt2add 13302 xsubge0 13303 xlesubadd 13305 xlemul1a 13330 elicore 13439 elico2 13451 iccmax 13463 elxrge0 13497 nfile 14398 hashdom 14418 hashdomi 14419 hashge1 14428 hashss 14448 hashge2el2difr 14520 pcdvdsb 16907 pc2dvds 16917 pcaddlem 16926 xrsdsreclblem 21430 leordtvallem1 23218 lecldbas 23227 isxmet2d 24337 blssec 24445 nmoix 24750 nmoleub 24752 xrtgioo 24828 xrge0tsms 24856 metdstri 24873 nmoleub2lem 25147 ovolf 25517 ovollb2 25524 ovoliun 25540 ovolre 25560 voliunlem3 25587 volsup 25591 icombl 25599 ioombl 25600 ismbfd 25674 itg2seq 25777 dvfsumrlim 26072 dvfsumrlim2 26073 radcnvcl 26460 xrlimcnp 27011 logfacbnd3 27267 log2sumbnd 27588 tgldimor 28510 xrdifh 32782 xrge0tsmsd 33065 unitssxrge0 33899 tpr2rico 33911 lmxrge0 33951 esumle 34059 esumlef 34063 esumpinfval 34074 esumpinfsum 34078 esumcvgsum 34089 ddemeas 34237 sxbrsigalem2 34288 omssubadd 34302 carsgclctunlem3 34322 signsply0 34566 ismblfin 37668 xrgepnfd 45342 supxrgelem 45348 supxrge 45349 infrpge 45362 xrlexaddrp 45363 infleinflem1 45381 infleinf 45383 infxrpnf 45457 ge0xrre 45544 iblsplit 45981 ismbl3 46001 ovolsplit 46003 sge0cl 46396 sge0less 46407 sge0pr 46409 sge0le 46422 sge0split 46424 carageniuncl 46538 ovnsubaddlem1 46585 hspmbl 46644 pimiooltgt 46725 pgrpgt2nabl 48282 |
| Copyright terms: Public domain | W3C validator |