Theorem ltpnf 11422

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 2451	. . . 4 |- +oo = +oo
2		orc 387	. . . 4 |- ( ( A e. RR /\ +oo = +oo ) -> ( ( A e. RR /\ +oo = +oo ) \/ ( A = -oo /\ +oo e. RR ) ) )
3	1, 2	mpan2 677	. . 3 |- ( A e. RR -> ( ( A e. RR /\ +oo = +oo ) \/ ( A = -oo /\ +oo e. RR ) ) )
4	3	olcd 395	. 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 9686	. . 3 |- ( A e. RR -> A e. RR* )
6		pnfxr 11412	. . 3 |- +oo e. RR*
7		ltxr 11415	. . 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 668	. 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 236	1 |- ( A e. RR -> A < +oo )

Syntax hints:   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   = wceq 1444   e. wcel 1887   class class class wbr 4402   RRcr 9538   <RR cltrr 9543   +oocpnf 9672   -oocmnf 9673   RR*cxr 9674   < clt 9675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-xp 4840  df-pnf 9677  df-xr 9679  df-ltxr 9680

This theorem is referenced by:  ltpnfd  11423  0ltpnf  11424  xrlttri  11438  xrlttr  11439  xrrebnd  11463  xrre  11464  qbtwnxr  11493  xltnegi  11509  xrinfmsslem  11593  xrub  11597  supxrunb1  11605  supxrunb2  11606  elioc2  11697  elicc2  11699  ioomax  11709  ioopos  11711  elioopnf  11728  elicopnf  11730  difreicc  11764  hashbnd  12521  hashnnn0genn0  12526  hashv01gt1  12528  limsupgreOLD  13543  fprodge0  14047  fprodge1  14049  pcadd  14834  ramubcl  14976  rge0srg  19038  mnfnei  20237  xblss2ps  21416  icopnfcld  21788  iocmnfcld  21789  blcvx  21816  xrtgioo  21824  reconnlem1  21844  xrge0tsms  21852  iccpnfhmeo  21973  ioombl1lem4  22514  icombl1  22516  uniioombllem1  22538  mbfmax  22605  ismbf3d  22610  mbflimsupOLD  22624  itg2seq  22700  lhop2  22967  dvfsumlem2  22979  logccv  23608  xrlimcnp  23894  pntleme  24446  umgrafi  25049  frgrawopreglem2  25773  topnfbey  25906  isblo3i  26442  htthlem  26570  xlt2addrd  28338  dfrp2  28352  fsumrp0cl  28458  pnfinf  28500  xrge0tsmsd  28548  xrge0slmod  28607  xrge0iifcnv  28739  xrge0iifiso  28741  xrge0iifhom  28743  lmxrge0  28758  esumcst  28884  esumcvgre  28912  voliune  29052  volfiniune  29053  sxbrsigalem0  29093  orvcgteel  29300  dstfrvclim1  29310  itg2addnclem2  31994  asindmre  32027  dvasin  32028  dvacos  32029  rfcnpre3  37354  supxrgere  37556  supxrgelem  37560  xrlexaddrp  37575  limsupre  37721  limsupreOLD  37722  icccncfext  37765  fourierdlem111  38081  fourierdlem113  38083  fouriersw  38095  sge0iunmptlemre  38257  sge0rpcpnf  38263  sge0xaddlem1  38275  hoidmvlelem5  38421  iccpartiltu  38736  upgrfi  39183