![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ltpnf | Structured version Visualization version Unicode version |
Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.) |
Ref | Expression |
---|---|
ltpnf |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2451 |
. . . 4
![]() ![]() ![]() ![]() | |
2 | orc 387 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpan2 677 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | olcd 395 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | rexr 9686 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | pnfxr 11412 |
. . 3
![]() ![]() ![]() ![]() | |
7 | ltxr 11415 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
8 | 5, 6, 7 | sylancl 668 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 4, 8 | mpbird 236 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-op 3975 df-uni 4199 df-br 4403 df-opab 4462 df-xp 4840 df-pnf 9677 df-xr 9679 df-ltxr 9680 |
This theorem is referenced by: ltpnfd 11423 0ltpnf 11424 xrlttri 11438 xrlttr 11439 xrrebnd 11463 xrre 11464 qbtwnxr 11493 xltnegi 11509 xrinfmsslem 11593 xrub 11597 supxrunb1 11605 supxrunb2 11606 elioc2 11697 elicc2 11699 ioomax 11709 ioopos 11711 elioopnf 11728 elicopnf 11730 difreicc 11764 hashbnd 12521 hashnnn0genn0 12526 hashv01gt1 12528 limsupgreOLD 13543 fprodge0 14047 fprodge1 14049 pcadd 14834 ramubcl 14976 rge0srg 19038 mnfnei 20237 xblss2ps 21416 icopnfcld 21788 iocmnfcld 21789 blcvx 21816 xrtgioo 21824 reconnlem1 21844 xrge0tsms 21852 iccpnfhmeo 21973 ioombl1lem4 22514 icombl1 22516 uniioombllem1 22538 mbfmax 22605 ismbf3d 22610 mbflimsupOLD 22624 itg2seq 22700 lhop2 22967 dvfsumlem2 22979 logccv 23608 xrlimcnp 23894 pntleme 24446 umgrafi 25049 frgrawopreglem2 25773 topnfbey 25906 isblo3i 26442 htthlem 26570 xlt2addrd 28338 dfrp2 28352 fsumrp0cl 28458 pnfinf 28500 xrge0tsmsd 28548 xrge0slmod 28607 xrge0iifcnv 28739 xrge0iifiso 28741 xrge0iifhom 28743 lmxrge0 28758 esumcst 28884 esumcvgre 28912 voliune 29052 volfiniune 29053 sxbrsigalem0 29093 orvcgteel 29300 dstfrvclim1 29310 itg2addnclem2 31994 asindmre 32027 dvasin 32028 dvacos 32029 rfcnpre3 37354 supxrgere 37556 supxrgelem 37560 xrlexaddrp 37575 limsupre 37721 limsupreOLD 37722 icccncfext 37765 fourierdlem111 38081 fourierdlem113 38083 fouriersw 38095 sge0iunmptlemre 38257 sge0rpcpnf 38263 sge0xaddlem1 38275 hoidmvlelem5 38421 iccpartiltu 38736 upgrfi 39183 |
Copyright terms: Public domain | W3C validator |