Theorem ltpnf 11342

Description: Any (finite) real is less than plus infinity. (Contributed by NM, 14-Oct-2005.)

Assertion

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

Proof of Theorem ltpnf

Step	Hyp	Ref	Expression
1		eqid 2443	. . . 4 |- +oo = +oo
2		orc 385	. . . 4 |- ( ( A e. RR /\ +oo = +oo ) -> ( ( A e. RR /\ +oo = +oo ) \/ ( A = -oo /\ +oo e. RR ) ) )
3	1, 2	mpan2 671	. . 3 |- ( A e. RR -> ( ( A e. RR /\ +oo = +oo ) \/ ( A = -oo /\ +oo e. RR ) ) )
4	3	olcd 393	. 2 |- ( A e. RR -> ( ( ( ( A e. RR /\ +oo e. RR ) /\ A <RR +oo ) \/ ( A = -oo /\ +oo = +oo ) ) \/ ( ( A e. RR /\ +oo = +oo ) \/ ( A = -oo /\ +oo e. RR ) ) ) )
5		rexr 9642	. . 3 |- ( A e. RR -> A e. RR* )
6		pnfxr 11332	. . 3 |- +oo e. RR*
7		ltxr 11335	. . 3 |- ( ( A e. RR* /\ +oo e. RR* ) -> ( A < +oo <-> ( ( ( ( A e. RR /\ +oo e. RR ) /\ A <RR +oo ) \/ ( A = -oo /\ +oo = +oo ) ) \/ ( ( A e. RR /\ +oo = +oo ) \/ ( A = -oo /\ +oo e. RR ) ) ) ) )
8	5, 6, 7	sylancl 662	. 2 |- ( A e. RR -> ( A < +oo <-> ( ( ( ( A e. RR /\ +oo e. RR ) /\ A <RR +oo ) \/ ( A = -oo /\ +oo = +oo ) ) \/ ( ( A e. RR /\ +oo = +oo ) \/ ( A = -oo /\ +oo e. RR ) ) ) ) )
9	4, 8	mpbird 232	1 |- ( A e. RR -> A < +oo )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   = wceq 1383   e. wcel 1804   class class class wbr 4437   RRcr 9494   <RR cltrr 9499   +oocpnf 9628   -oocmnf 9629   RR*cxr 9630   < clt 9631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-xp 4995  df-pnf 9633  df-xr 9635  df-ltxr 9636

This theorem is referenced by:  0ltpnf  11343  xrlttri  11356  xrlttr  11357  xrrebnd  11380  xrre  11381  qbtwnxr  11410  xltnegi  11426  xrinfmsslem  11510  xrub  11514  supxrunb1  11522  supxrunb2  11523  elioc2  11598  elicc2  11600  ioomax  11610  ioopos  11612  elioopnf  11629  elicopnf  11631  difreicc  11663  hashbnd  12393  hashnnn0genn0  12398  hashv01gt1  12400  limsupgre  13286  pcadd  14390  ramubcl  14518  rge0srg  18466  mnfnei  19700  xblss2ps  20882  icopnfcld  21253  iocmnfcld  21254  blcvx  21281  xrtgioo  21289  reconnlem1  21309  xrge0tsms  21317  iccpnfhmeo  21423  ioombl1lem4  21949  icombl1  21951  uniioombllem1  21968  mbfmax  22034  ismbf3d  22039  mbflimsup  22051  itg2seq  22127  lhop2  22394  dvfsumlem2  22406  logccv  23022  xrlimcnp  23276  pntleme  23771  umgrafi  24300  frgrawopreglem2  25023  isblo3i  25694  htthlem  25812  xlt2addrd  27556  fsumrp0cl  27663  pnfinf  27705  xrge0tsmsd  27753  xrge0slmod  27812  xrge0iifcnv  27893  xrge0iifiso  27895  xrge0iifhom  27897  lmxrge0  27912  esumcst  28049  voliune  28179  volfiniune  28180  sxbrsigalem0  28220  orvcgteel  28384  dstfrvclim1  28394  itg2addnclem2  30043  asindmre  30078  dvasin  30079  dvacos  30080  rfcnpre3  31362  ltpnfd  31434  fprodge0  31551  fprodge1  31552  limsupre  31601  icccncfext  31644  fourierdlem111  31954  fourierdlem113  31956  fouriersw  31968