Theorem ltpnf 11360

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

Assertion

Ref	Expression
ltpnf

Proof of Theorem ltpnf

Step	Hyp	Ref	Expression
1		eqid 2457	. . . 4
2		orc 385	. . . 4
3	1, 2	mpan2 671	. . 3
4	3	olcd 393	. 2
5		rexr 9660	. . 3
6		pnfxr 11350	. . 3
7		ltxr 11353	. . 3
8	5, 6, 7	sylancl 662	. 2
9	4, 8	mpbird 232	1

Syntax hints:  ->wi 4  <->wb 184  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818   class class class wbr 4452  cr 9512  cltrr 9517  cpnf 9646  cmnf 9647  cxr 9648  clt 9649

This theorem is referenced by:  0ltpnf  11361  xrlttri  11374  xrlttr  11375  xrrebnd  11398  xrre  11399  qbtwnxr  11428  xltnegi  11444  xrinfmsslem  11528  xrub  11532  supxrunb1  11540  supxrunb2  11541  elioc2  11616  elicc2  11618  ioomax  11628  ioopos  11630  elioopnf  11647  elicopnf  11649  difreicc  11681  hashbnd  12411  hashnnn0genn0  12416  hashv01gt1  12418  limsupgre  13304  pcadd  14408  ramubcl  14536  rge0srg  18487  mnfnei  19722  xblss2ps  20904  icopnfcld  21275  iocmnfcld  21276  blcvx  21303  xrtgioo  21311  reconnlem1  21331  xrge0tsms  21339  iccpnfhmeo  21445  ioombl1lem4  21971  icombl1  21973  uniioombllem1  21990  mbfmax  22056  ismbf3d  22061  mbflimsup  22073  itg2seq  22149  lhop2  22416  dvfsumlem2  22428  logccv  23044  xrlimcnp  23298  pntleme  23793  umgrafi  24322  frgrawopreglem2  25045  isblo3i  25716  htthlem  25834  xlt2addrd  27578  fsumrp0cl  27685  pnfinf  27727  xrge0tsmsd  27775  xrge0slmod  27834  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  lmxrge0  27934  esumcst  28071  voliune  28201  volfiniune  28202  sxbrsigalem0  28242  orvcgteel  28406  dstfrvclim1  28416  itg2addnclem2  30067  asindmre  30102  dvasin  30103  dvacos  30104  rfcnpre3  31408  ltpnfd  31480  fprodge0  31597  fprodge1  31598  limsupre  31647  icccncfext  31690  fourierdlem111  32000  fourierdlem113  32002  fouriersw  32014

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-cnex 9569

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-xp 5010  df-pnf 9651  df-xr 9653  df-ltxr 9654