ltpnf - Intuitionistic Logic Explorer

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

Theorem ltpnf 9976

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 2229	. . . 4
2		orc 717	. . . 4 $/\$ $/\$ $\/$ $/\$
3	1, 2	mpan2 425	. . 3 $/\$ $\/$ $/\$
4	3	olcd 739	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5		rexr 8192	. . 3
6		pnfxr 8199	. . 3
7		ltxr 9971	. . 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 713

wceq 1395

wcel 2200 class class class wbr 4083

cr 7998

cltrr 8003

cpnf 8178

cmnf 8179

cxr 8180

clt 8181

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 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4202 ax-pow 4258 ax-pr 4293 ax-un 4524 ax-cnex 8090

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-v 2801 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-br 4084 df-opab 4146 df-xp 4725 df-pnf 8183 df-xr 8185 df-ltxr 8186

This theorem is referenced by: ltpnfd 9977 0ltpnf 9978 xrlttr 9991 xrltso 9992 xrlttri3 9993 nltpnft 10010 npnflt 10011 xrrebnd 10015 xrre 10016 xltnegi 10031 xltadd1 10072 xposdif 10078 elioc2 10132 elicc2 10134 ioomax 10144 ioopos 10146 elioopnf 10163 elicopnf 10165 qbtwnxr 10477 dfrp2 10483 filtinf 11013 xrmaxltsup 11769 fprodge0 12148 fprodge1 12150 xblss2ps 15078