pnfnlt - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > pnfnlt		Structured version Unicode version

Theorem pnfnlt 11362

Description: No extended real is greater than plus infinity. (Contributed by NM, 15-Oct-2005.)

**Assertion**
Ref	Expression
pnfnlt

**Proof of Theorem pnfnlt**
Step	Hyp	Ref	Expression
1		pnfnre 9652	. . . . . . 7
2	1	neli 2792	. . . . . 6
3	2	intnanr 915	. . . . 5 $/\$
4	3	intnanr 915	. . . 4 $/\$ $/\$
5		pnfnemnf 11351	. . . . . 6
6	5	neii 2656	. . . . 5
7	6	intnanr 915	. . . 4 $/\$
8	4, 7	pm3.2ni 854	. . 3 $/\$ $/\$ $\/$ $/\$
9	2	intnanr 915	. . . 4 $/\$
10	6	intnanr 915	. . . 4 $/\$
11	9, 10	pm3.2ni 854	. . 3 $/\$ $\/$ $/\$
12	8, 11	pm3.2ni 854	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
13		pnfxr 11346	. . 3
14		ltxr 11349	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
15	13, 14	mpan 670	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
16	12, 15	mtbiri 303	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1395

wcel 1819 class class class wbr 4456

cr 9508

cltrr 9513

cpnf 9642

cmnf 9643

cxr 9644

clt 9645

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-cnex 9565 ax-resscn 9566

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3111 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-op 4039 df-uni 4252 df-br 4457 df-opab 4516 df-xp 5014 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650

This theorem is referenced by: pnfge 11364 xrltnsym 11368 xrlttr 11371 qbtwnxr 11424 xltnegi 11440 xmullem2 11482 xrinfmexpnf 11522 xrsupsslem 11523 xrinfmsslem 11524 xrub 11528 supxrpnf 11535 supxrunb1 11536 supxrunb2 11537 xrinfm0 11553 lt6abl 17023 pnfnei 19847 metdstri 21480 esumpcvgval 28240