![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pnfge | Structured version Visualization version Unicode 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 11419 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pnfxr 11401 |
. . 3
![]() ![]() ![]() ![]() | |
3 | xrlenlt 9685 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpan2 682 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | mpbird 240 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1672 ax-4 1685 ax-5 1761 ax-6 1808 ax-7 1854 ax-8 1892 ax-9 1899 ax-10 1918 ax-11 1923 ax-12 1936 ax-13 2091 ax-ext 2431 ax-sep 4496 ax-nul 4505 ax-pow 4553 ax-pr 4611 ax-un 6570 ax-cnex 9581 ax-resscn 9582 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 988 df-tru 1450 df-ex 1667 df-nf 1671 df-sb 1801 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-rab 2745 df-v 3014 df-dif 3374 df-un 3376 df-in 3378 df-ss 3385 df-nul 3699 df-if 3849 df-pw 3920 df-sn 3936 df-pr 3938 df-op 3942 df-uni 4168 df-br 4374 df-opab 4433 df-xp 4817 df-cnv 4819 df-pnf 9663 df-mnf 9664 df-xr 9665 df-ltxr 9666 df-le 9667 |
This theorem is referenced by: 0lepnf 11422 nltpnft 11450 xrre2 11454 xleadd1a 11528 xlt2add 11535 xsubge0 11536 xlesubadd 11538 xlemul1a 11563 elicore 11676 elico2 11687 iccmax 11699 elxrge0 11731 hashdom 12551 hashdomi 12552 hashge1 12561 hashss 12579 hashge2el2difr 12632 pcdvdsb 14828 pc2dvds 14838 pcaddlem 14843 xrsdsreclblem 19024 leordtvallem1 20236 lecldbas 20245 isxmet2d 21352 blssec 21460 nmoix 21744 nmoleub 21746 nmoixOLD 21760 nmoleubOLD 21762 xrtgioo 21834 xrge0tsms 21862 metdstri 21878 metdstriOLD 21893 nmoleub2lem 22138 ovolf 22445 ovollb2 22452 ovoliun 22468 ovolre 22489 voliunlem3 22516 volsup 22520 icombl 22528 ioombl 22529 ismbfd 22607 itg2seq 22711 dvfsumrlim 22994 dvfsumrlim2 22995 radcnvcl 23383 xrlimcnp 23905 logfacbnd3 24162 log2sumbnd 24393 tgldimor 24557 sizeusglecusg 25225 vdgfrgragt2 25766 xrdifh 28369 xrge0tsmsd 28554 unitssxrge0 28712 tpr2rico 28724 lmxrge0 28764 esumle 28885 esumlef 28889 esumpinfval 28900 esumpinfsum 28904 esumcvgsum 28915 ddemeas 29064 sxbrsigalem2 29113 omssubadd 29133 oms0OLD 29134 omssubaddOLD 29137 carsgclctunlem3 29157 signsply0 29445 ismblfin 31982 xrgepnfd 37584 supxrgelem 37590 supxrge 37591 infrpge 37604 xrlexaddrp 37605 infleinflem1 37624 infleinf 37626 ge0xrre 37673 iblsplit 37884 ismbl3 37905 ovolsplit 37907 sge0cl 38281 sge0less 38292 sge0pr 38294 sge0le 38307 sge0split 38309 carageniuncl 38407 ovnsubaddlem1 38454 hspmbl 38513 nfile 39164 pgrpgt2nabl 40475 |
Copyright terms: Public domain | W3C validator |