pnfnlt - Metamath Proof Explorer

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

Theorem pnfnlt 11211

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 9528	. . . . . . 7
2	1	neli 2783	. . . . . 6
3	2	intnanr 906	. . . . 5 $/\$
4	3	intnanr 906	. . . 4 $/\$ $/\$
5		pnfnemnf 11200	. . . . . 6
6	5	neii 2648	. . . . 5
7	6	intnanr 906	. . . 4 $/\$
8	4, 7	pm3.2ni 850	. . 3 $/\$ $/\$ $\/$ $/\$
9	2	intnanr 906	. . . 4 $/\$
10	6	intnanr 906	. . . 4 $/\$
11	9, 10	pm3.2ni 850	. . 3 $/\$ $\/$ $/\$
12	8, 11	pm3.2ni 850	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
13		pnfxr 11195	. . 3
14		ltxr 11198	. . 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 1370

wcel 1758 class class class wbr 4392

cr 9384

cltrr 9389

cpnf 9518

cmnf 9519

cxr 9520

clt 9521

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4513 ax-nul 4521 ax-pow 4570 ax-pr 4631 ax-un 6474 ax-cnex 9441 ax-resscn 9442

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-rab 2804 df-v 3072 df-dif 3431 df-un 3433 df-in 3435 df-ss 3442 df-nul 3738 df-if 3892 df-pw 3962 df-sn 3978 df-pr 3980 df-op 3984 df-uni 4192 df-br 4393 df-opab 4451 df-xp 4946 df-pnf 9523 df-mnf 9524 df-xr 9525 df-ltxr 9526

This theorem is referenced by: pnfge 11213 xrltnsym 11217 xrlttr 11220 qbtwnxr 11273 xltnegi 11289 xmullem2 11331 xrinfmexpnf 11371 xrsupsslem 11372 xrinfmsslem 11373 xrub 11377 supxrpnf 11384 supxrunb1 11385 supxrunb2 11386 xrinfm0 11402 lt6abl 16477 pnfnei 18942 metdstri 20545 esumpcvgval 26663