ltpnf - Intuitionistic Logic Explorer

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

Theorem ltpnf 9567

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 2139	. . . 4
2		orc 701	. . . 4 $/\$ $/\$ $\/$ $/\$
3	1, 2	mpan2 421	. . 3 $/\$ $\/$ $/\$
4	3	olcd 723	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5		rexr 7811	. . 3
6		pnfxr 7818	. . 3
7		ltxr 9562	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
8	5, 6, 7	sylancl 409	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
9	4, 8	mpbird 166	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104 $\/$ wo 697

wceq 1331

wcel 1480 class class class wbr 3929

cr 7619

cltrr 7624

cpnf 7797

cmnf 7798

cxr 7799

clt 7800

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-13 1491 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-pr 4131 ax-un 4355 ax-cnex 7711

This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-ral 2421 df-rex 2422 df-v 2688 df-un 3075 df-in 3077 df-ss 3084 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-uni 3737 df-br 3930 df-opab 3990 df-xp 4545 df-pnf 7802 df-xr 7804 df-ltxr 7805

This theorem is referenced by: 0ltpnf 9568 xrlttr 9581 xrltso 9582 xrlttri3 9583 nltpnft 9597 npnflt 9598 xrrebnd 9602 xrre 9603 xltnegi 9618 xltadd1 9659 xposdif 9665 elioc2 9719 elicc2 9721 ioomax 9731 ioopos 9733 elioopnf 9750 elicopnf 9752 qbtwnxr 10035 filtinf 10538 xrmaxltsup 11027 xblss2ps 12573