ltpnf - Intuitionistic Logic Explorer

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

Theorem ltpnf 10116

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 2234	. . . 4
2		orc 720	. . . 4 $/\$ $/\$ $\/$ $/\$
3	1, 2	mpan2 425	. . 3 $/\$ $\/$ $/\$
4	3	olcd 742	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5		rexr 8321	. . 3
6		pnfxr 8328	. . 3
7		ltxr 10111	. . 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 716

wceq 1398

wcel 2205 class class class wbr 4111

cr 8128

cltrr 8133

cpnf 8307

cmnf 8308

cxr 8309

clt 8310

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 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2207 ax-14 2208 ax-ext 2216 ax-sep 4230 ax-pow 4289 ax-pr 4324 ax-un 4556 ax-cnex 8220

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-nf 1510 df-sb 1812 df-eu 2085 df-mo 2086 df-clab 2221 df-cleq 2227 df-clel 2230 df-nfc 2375 df-ral 2527 df-rex 2528 df-v 2817 df-un 3217 df-in 3219 df-ss 3226 df-pw 3673 df-sn 3697 df-pr 3698 df-op 3700 df-uni 3917 df-br 4112 df-opab 4174 df-xp 4757 df-pnf 8312 df-xr 8314 df-ltxr 8315

This theorem is referenced by: ltpnfd 10117 0ltpnf 10118 xrlttr 10131 xrltso 10132 xrlttri3 10133 nltpnft 10150 npnflt 10151 xrrebnd 10155 xrre 10156 xltnegi 10171 xltadd1 10212 xposdif 10218 elioc2 10272 elicc2 10274 ioomax 10284 ioopos 10286 elioopnf 10303 elicopnf 10305 qbtwnxr 10621 dfrp2 10627 filtinf 11158 xrmaxltsup 11947 fprodge0 12327 fprodge1 12329 xblss2ps 15286