nltmnf - Intuitionistic Logic Explorer

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

Theorem nltmnf 8928

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

**Assertion**
Ref	Expression
nltmnf

**Proof of Theorem nltmnf**
Step	Hyp	Ref	Expression
1		mnfnre 7212	. . . . . . 7
2	1	neli 2342	. . . . . 6
3	2	intnan 872	. . . . 5 $/\$
4	3	intnanr 873	. . . 4 $/\$ $/\$
5		pnfnemnf 7224	. . . . . 6
6	5	nesymi 2292	. . . . 5
7	6	intnan 872	. . . 4 $/\$
8	4, 7	pm3.2ni 760	. . 3 $/\$ $/\$ $\/$ $/\$
9	6	intnan 872	. . . 4 $/\$
10	2	intnan 872	. . . 4 $/\$
11	9, 10	pm3.2ni 760	. . 3 $/\$ $\/$ $/\$
12	8, 11	pm3.2ni 760	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
13		mnfxr 7226	. . 3
14		ltxr 8916	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
15	13, 14	mpan2 416	. 2 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
16	12, 15	mtbiri 633	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 102

wb 103 $\/$ wo 662

wceq 1285

wcel 1434 class class class wbr 3787

cr 7031

cltrr 7036

cpnf 7201

cmnf 7202

cxr 7203

clt 7204

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-sep 3898 ax-pow 3950 ax-pr 3966 ax-un 4190 ax-setind 4282 ax-cnex 7118 ax-resscn 7119

This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-nel 2341 df-ral 2354 df-rex 2355 df-rab 2358 df-v 2604 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-pw 3386 df-sn 3406 df-pr 3407 df-op 3409 df-uni 3604 df-br 3788 df-opab 3842 df-xp 4371 df-pnf 7206 df-mnf 7207 df-xr 7208 df-ltxr 7209

This theorem is referenced by: mnfle 8932 xrltnsym 8933 xrlttr 8935 xrltso 8936 xltnegi 8967 qbtwnxr 9333