pnfnlt - Metamath Proof Explorer

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

Theorem pnfnlt 11333

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 9631	. . . . . . 7
2	1	neli 2802	. . . . . 6
3	2	intnanr 913	. . . . 5 $/\$
4	3	intnanr 913	. . . 4 $/\$ $/\$
5		pnfnemnf 11322	. . . . . 6
6	5	neii 2666	. . . . 5
7	6	intnanr 913	. . . 4 $/\$
8	4, 7	pm3.2ni 852	. . 3 $/\$ $/\$ $\/$ $/\$
9	2	intnanr 913	. . . 4 $/\$
10	6	intnanr 913	. . . 4 $/\$
11	9, 10	pm3.2ni 852	. . 3 $/\$ $\/$ $/\$
12	8, 11	pm3.2ni 852	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
13		pnfxr 11317	. . 3
14		ltxr 11320	. . 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 1379

wcel 1767 class class class wbr 4447

cr 9487

cltrr 9492

cpnf 9621

cmnf 9622

cxr 9623

clt 9624

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-cnex 9544 ax-resscn 9545

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-op 4034 df-uni 4246 df-br 4448 df-opab 4506 df-xp 5005 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629

This theorem is referenced by: pnfge 11335 xrltnsym 11339 xrlttr 11342 qbtwnxr 11395 xltnegi 11411 xmullem2 11453 xrinfmexpnf 11493 xrsupsslem 11494 xrinfmsslem 11495 xrub 11499 supxrpnf 11506 supxrunb1 11507 supxrunb2 11508 xrinfm0 11524 lt6abl 16688 pnfnei 19487 metdstri 21090 esumpcvgval 27724