ltpnf - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ltpnf		Structured version Unicode version

Theorem ltpnf 11102

Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)

**Assertion**
Ref	Expression
ltpnf

**Proof of Theorem ltpnf**
Step	Hyp	Ref	Expression
1		eqid 2443	. . . 4
2		orc 385	. . . 4 $/\$ $/\$ $\/$ $/\$
3	1, 2	mpan2 671	. . 3 $/\$ $\/$ $/\$
4	3	olcd 393	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5		rexr 9429	. . 3
6		pnfxr 11092	. . 3
7		ltxr 11095	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
8	5, 6, 7	sylancl 662	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	4, 8	mpbird 232	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1369

wcel 1756 class class class wbr 4292

cr 9281

cltrr 9286

cpnf 9415

cmnf 9416

cxr 9417

clt 9418

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372 ax-cnex 9338

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-rab 2724 df-v 2974 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-op 3884 df-uni 4092 df-br 4293 df-opab 4351 df-xp 4846 df-pnf 9420 df-xr 9422 df-ltxr 9423

This theorem is referenced by: 0ltpnf 11103 xrlttri 11116 xrlttr 11117 xrrebnd 11140 xrre 11141 qbtwnxr 11170 xltnegi 11186 xrinfmsslem 11270 xrub 11274 supxrunb1 11282 supxrunb2 11283 elioc2 11358 elicc2 11360 ioomax 11370 ioopos 11372 elioopnf 11383 elicopnf 11385 difreicc 11417 hashbnd 12109 hashnnn0genn0 12114 hashv01gt1 12116 limsupgre 12959 pcadd 13951 ramubcl 14079 rge0srg 17882 mnfnei 18825 xblss2ps 19976 icopnfcld 20347 iocmnfcld 20348 blcvx 20375 xrtgioo 20383 reconnlem1 20403 xrge0tsms 20411 iccpnfhmeo 20517 ioombl1lem4 21042 icombl1 21044 uniioombllem1 21061 mbfmax 21127 ismbf3d 21132 mbflimsup 21144 itg2seq 21220 lhop2 21487 dvfsumlem2 21499 logccv 22108 xrlimcnp 22362 pntleme 22857 umgrafi 23256 isblo3i 24201 htthlem 24319 xlt2addrd 26051 fsumrp0cl 26158 pnfinf 26200 xrge0tsmsd 26253 xrge0slmod 26312 xrge0iifcnv 26363 xrge0iifiso 26365 xrge0iifhom 26367 lmxrge0 26382 esumcst 26514 voliune 26645 volfiniune 26646 sxbrsigalem0 26686 orvcgteel 26850 dstfrvclim1 26860 itg2addnclem2 28444 asindmre 28479 dvasin 28480 dvacos 28481 rfcnpre3 29755 frgrawopreglem2 30638