ltpnf - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > ltpnf		Unicode version

Theorem ltpnf 9902

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 2205	. . . 4
2		orc 714	. . . 4 $/\$ $/\$ $\/$ $/\$
3	1, 2	mpan2 425	. . 3 $/\$ $\/$ $/\$
4	3	olcd 736	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5		rexr 8118	. . 3
6		pnfxr 8125	. . 3
7		ltxr 9897	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
8	5, 6, 7	sylancl 413	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	4, 8	mpbird 167	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 104

wb 105 $\/$ wo 710

wceq 1373

wcel 2176 class class class wbr 4044

cr 7924

cltrr 7929

cpnf 8104

cmnf 8105

cxr 8106

clt 8107

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-13 2178 ax-14 2179 ax-ext 2187 ax-sep 4162 ax-pow 4218 ax-pr 4253 ax-un 4480 ax-cnex 8016

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1484 df-sb 1786 df-eu 2057 df-mo 2058 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ral 2489 df-rex 2490 df-v 2774 df-un 3170 df-in 3172 df-ss 3179 df-pw 3618 df-sn 3639 df-pr 3640 df-op 3642 df-uni 3851 df-br 4045 df-opab 4106 df-xp 4681 df-pnf 8109 df-xr 8111 df-ltxr 8112

This theorem is referenced by: ltpnfd 9903 0ltpnf 9904 xrlttr 9917 xrltso 9918 xrlttri3 9919 nltpnft 9936 npnflt 9937 xrrebnd 9941 xrre 9942 xltnegi 9957 xltadd1 9998 xposdif 10004 elioc2 10058 elicc2 10060 ioomax 10070 ioopos 10072 elioopnf 10089 elicopnf 10091 qbtwnxr 10400 dfrp2 10406 filtinf 10936 xrmaxltsup 11569 fprodge0 11948 fprodge1 11950 xblss2ps 14876