ltpnf - Intuitionistic Logic Explorer

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

Theorem ltpnf 9350

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 2095	. . . 4
2		orc 671	. . . 4 $/\$ $/\$ $\/$ $/\$
3	1, 2	mpan2 417	. . 3 $/\$ $\/$ $/\$
4	3	olcd 691	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5		rexr 7630	. . 3
6		pnfxr 7637	. . 3
7		ltxr 9345	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
8	5, 6, 7	sylancl 405	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	4, 8	mpbird 166	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 667

wceq 1296

wcel 1445 class class class wbr 3867

cr 7446

cltrr 7451

cpnf 7616

cmnf 7617

cxr 7618

clt 7619

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-pr 4060 ax-un 4284 ax-cnex 7533

This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ral 2375 df-rex 2376 df-v 2635 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-opab 3922 df-xp 4473 df-pnf 7621 df-xr 7623 df-ltxr 7624

This theorem is referenced by: 0ltpnf 9351 xrlttr 9364 xrltso 9365 xrlttri3 9366 nltpnft 9380 npnflt 9381 xrrebnd 9385 xrre 9386 xltnegi 9401 xltadd1 9442 xposdif 9448 elioc2 9502 elicc2 9504 ioomax 9514 ioopos 9516 elioopnf 9533 elicopnf 9535 qbtwnxr 9818 filtinf 10315 xrmaxltsup 10801 xblss2ps 12190