ltpnf - Intuitionistic Logic Explorer

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

Theorem ltpnf 9904

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 8120	. . 3
6		pnfxr 8127	. . 3
7		ltxr 9899	. . 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 4045

cr 7926

cltrr 7931

cpnf 8106

cmnf 8107

cxr 8108

clt 8109

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 4163 ax-pow 4219 ax-pr 4254 ax-un 4481 ax-cnex 8018

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 4046 df-opab 4107 df-xp 4682 df-pnf 8111 df-xr 8113 df-ltxr 8114

This theorem is referenced by: ltpnfd 9905 0ltpnf 9906 xrlttr 9919 xrltso 9920 xrlttri3 9921 nltpnft 9938 npnflt 9939 xrrebnd 9943 xrre 9944 xltnegi 9959 xltadd1 10000 xposdif 10006 elioc2 10060 elicc2 10062 ioomax 10072 ioopos 10074 elioopnf 10091 elicopnf 10093 qbtwnxr 10402 dfrp2 10408 filtinf 10938 xrmaxltsup 11602 fprodge0 11981 fprodge1 11983 xblss2ps 14909