MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pnfge Structured version   Unicode version

Theorem pnfge 11342
Description: Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
Assertion
Ref Expression
pnfge  |-  ( A  e.  RR*  ->  A  <_ +oo )

Proof of Theorem pnfge
StepHypRef Expression
1 pnfnlt 11340 . 2  |-  ( A  e.  RR*  ->  -. +oo  <  A )
2 pnfxr 11324 . . 3  |- +oo  e.  RR*
3 xrlenlt 9641 . . 3  |-  ( ( A  e.  RR*  /\ +oo  e.  RR* )  ->  ( A  <_ +oo  <->  -. +oo  <  A
) )
42, 3mpan2 669 . 2  |-  ( A  e.  RR*  ->  ( A  <_ +oo  <->  -. +oo  <  A
) )
51, 4mpbird 232 1  |-  ( A  e.  RR*  ->  A  <_ +oo )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    e. wcel 1823   class class class wbr 4439   +oocpnf 9614   RR*cxr 9616    < clt 9617    <_ cle 9618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-xp 4994  df-cnv 4996  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623
This theorem is referenced by:  0lepnf  11343  nltpnft  11370  xrre2  11374  xleadd1a  11448  xlt2add  11455  xsubge0  11456  xlesubadd  11458  xlemul1a  11483  elico2  11591  iccmax  11603  elxrge0  11632  hashdom  12430  hashdomi  12431  hashge1  12440  hashss  12458  pcdvdsb  14476  pc2dvds  14486  pcaddlem  14491  xrsdsreclblem  18659  leordtvallem1  19878  lecldbas  19887  isxmet2d  20996  blssec  21104  nmoix  21402  nmoleub  21404  xrtgioo  21477  xrge0tsms  21505  metdstri  21521  nmoleub2lem  21763  ovolf  22059  ovollb2  22066  ovoliun  22082  ovolre  22102  voliunlem3  22128  volsup  22132  icombl  22140  ioombl  22141  ismbfd  22213  itg2seq  22315  dvfsumrlim  22598  dvfsumrlim2  22599  radcnvcl  22978  xrlimcnp  23496  logfacbnd3  23696  log2sumbnd  23927  tgldimor  24094  sizeusglecusg  24688  vdgfrgragt2  25229  xrdifh  27825  xrge0tsmsd  28010  unitssxrge0  28117  tpr2rico  28129  lmxrge0  28169  esumle  28287  esumlef  28291  esumpinfval  28302  esumpinfsum  28306  esumcvgsum  28317  ddemeas  28445  sxbrsigalem2  28494  oms0  28505  omssubadd  28508  carsgclctunlem3  28528  signsply0  28772  ismblfin  30295  elicore  31776  iblsplit  32004  pgrpgt2nabl  33213
  Copyright terms: Public domain W3C validator