Theorem pnfnltt 5559

Description: No extended real is greater than plus infinity.

Assertion

Ref	Expression
pnfnltt	|- (A e. RR* -> -. +oo < A)

Proof of Theorem pnfnltt

Step	Hyp	Ref	Expression
1		pnfnre 5509	. . . . . . 7 |- +oo e/ RR
2		df-nel 1595	. . . . . . 7 |- ( +oo e/ RR <-> -. +oo e. RR)
3	1, 2	mpbi 189	. . . . . 6 |- -. +oo e. RR
4	3	intnanr 696	. . . . 5 |- -. ( +oo e. RR /\ A e. RR)
5	4	intnanr 696	. . . 4 |- -. (( +oo e. RR /\ A e. RR) /\ +oo <R A)
6		pnfnemnf 5549	. . . . . 6 |- +oo =/= -oo
7		df-ne 1594	. . . . . 6 |- ( +oo =/= -oo <-> -. +oo = -oo)
8	6, 7	mpbi 189	. . . . 5 |- -. +oo = -oo
9	8	intnanr 696	. . . 4 |- -. ( +oo = -oo /\ A = +oo)
10	5, 9	pm3.2ni 583	. . 3 |- -. ((( +oo e. RR /\ A e. RR) /\ +oo <R A) \/ ( +oo = -oo /\ A = +oo))
11	3	intnanr 696	. . . 4 |- -. ( +oo e. RR /\ A = +oo)
12	8	intnanr 696	. . . 4 |- -. ( +oo = -oo /\ A e. RR)
13	11, 12	pm3.2ni 583	. . 3 |- -. (( +oo e. RR /\ A = +oo) \/ ( +oo = -oo /\ A e. RR))
14	10, 13	pm3.2ni 583	. 2 |- -. (((( +oo e. RR /\ A e. RR) /\ +oo <R A) \/ ( +oo = -oo /\ A = +oo)) \/ (( +oo e. RR /\ A = +oo) \/ ( +oo = -oo /\ A e. RR)))
15		pnfxr 5506	. . 3 |- +oo e. RR*
16		ltxrt 5508	. . 3 |- (( +oo e. RR* /\ A e. RR*) -> ( +oo < A <-> (((( +oo e. RR /\ A e. RR) /\ +oo <R A) \/ ( +oo = -oo /\ A = +oo)) \/ (( +oo e. RR /\ A = +oo) \/ ( +oo = -oo /\ A e. RR)))))
17	15, 16	mpan 699	. 2 |- (A e. RR* -> ( +oo < A <-> (((( +oo e. RR /\ A e. RR) /\ +oo <R A) \/ ( +oo = -oo /\ A = +oo)) \/ (( +oo e. RR /\ A = +oo) \/ ( +oo = -oo /\ A e. RR)))))
18	14, 17	mtbiri 721	1 |- (A e. RR* -> -. +oo < A)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   = wceq 960   e. wcel 962   =/= wne 1592   e/ wnel 1593   class class class wbr 2632  RRcr 5246   <R cltrr 5251   +oocpnf 5496   -oocmnf 5497  RR*cxr 5498   < clt 5499

This theorem is referenced by:  pnfget 5561  xrltnsymt 5563  xrlttrt 5566  xrinfmexpnf 6081  xrsupsslem 6082  xrinfmsslem 6083  xrub 6086  supxrre 6089  supxrpnf 6094  supxrunb1 6095  supxrunb2 6096  qbtwnxr 6290  tgioolem 7923

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466  ax-rep 2706  ax-sep 2716  ax-nul 2723  ax-pow 2756  ax-pr 2793  ax-un 2880  ax-inf2 4637

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1178  df-eu 1388  df-mo 1389  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-nel 1595  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2010  df-dif 2058  df-un 2059  df-in 2060  df-ss 2062  df-pss 2064  df-nul 2290  df-if 2372  df-pw 2412  df-sn 2422  df-pr 2423  df-tp 2425  df-op 2426  df-uni 2516  df-int 2546  df-iun 2580  df-br 2633  df-opab 2680  df-tr 2694  df-eprel 2846  df-id 2849  df-po 2854  df-so 2864  df-fr 2931  df-we 2948  df-ord 2965  df-on 2966  df-lim 2967  df-suc 2968  df-om 3146  df-xp 3198  df-rel 3199  df-cnv 3200  df-co 3201  df-dm 3202  df-rn 3203  df-res 3204  df-ima 3205  df-fun 3206  df-fn 3207  df-f 3208  df-f1 3209  df-fo 3210  df-f1o 3211  df-fv 3212  df-rdg 3946  df-opr 3979  df-oprab 3980  df-1st 4093  df-2nd 4094  df-1o 4147  df-oadd 4149  df-omul 4150  df-er 4275  df-ec 4277  df-qs 4280  df-en 4382  df-dom 4383  df-sdom 4384  df-ni 5013  df-pli 5014  df-mi 5015  df-lti 5016  df-plpq 5048  df-mpq 5049  df-enq 5050  df-nq 5051  df-plq 5052  df-mq 5053  df-rq 5054  df-ltq 5055  df-1q 5056  df-np 5099  df-1p 5100  df-enr 5179  df-nr 5180  df-0r 5184  df-c 5253  df-r 5257  df-pnf 5500  df-mnf 5501  df-xr 5502  df-ltxr 5503

Copyright terms: Public domain