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

Theorem pnfge 11961
Description: Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)
Assertion
Ref Expression
pnfge (𝐴 ∈ ℝ*𝐴 ≤ +∞)

Proof of Theorem pnfge
StepHypRef Expression
1 pnfnlt 11959 . 2 (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2 pnfxr 10089 . . 3 +∞ ∈ ℝ*
3 xrlenlt 10100 . . 3 ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
42, 3mpan2 707 . 2 (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
51, 4mpbird 247 1 (𝐴 ∈ ℝ*𝐴 ≤ +∞)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wcel 1989   class class class wbr 4651  +∞cpnf 10068  *cxr 10070   < clt 10071  cle 10072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946  ax-cnex 9989  ax-resscn 9990
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-nel 2897  df-ral 2916  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-xp 5118  df-cnv 5120  df-pnf 10073  df-mnf 10074  df-xr 10075  df-ltxr 10076  df-le 10077
This theorem is referenced by:  xnn0n0n1ge2b  11962  0lepnf  11963  nltpnft  11992  xrre2  11998  xleadd1a  12080  xlt2add  12087  xsubge0  12088  xlesubadd  12090  xlemul1a  12115  elicore  12223  elico2  12234  iccmax  12246  elxrge0  12278  nfile  13145  hashdom  13163  hashdomi  13164  hashge1  13173  hashss  13192  hashge2el2difr  13258  pcdvdsb  15567  pc2dvds  15577  pcaddlem  15586  xrsdsreclblem  19786  leordtvallem1  21008  lecldbas  21017  isxmet2d  22126  blssec  22234  nmoix  22527  nmoleub  22529  xrtgioo  22603  xrge0tsms  22631  metdstri  22648  nmoleub2lem  22908  ovolf  23244  ovollb2  23251  ovoliun  23267  ovolre  23287  voliunlem3  23314  volsup  23318  icombl  23326  ioombl  23327  ismbfd  23401  itg2seq  23503  dvfsumrlim  23788  dvfsumrlim2  23789  radcnvcl  24165  xrlimcnp  24689  logfacbnd3  24942  log2sumbnd  25227  tgldimor  25391  xrdifh  29527  xrge0tsmsd  29770  unitssxrge0  29931  tpr2rico  29943  lmxrge0  29983  esumle  30105  esumlef  30109  esumpinfval  30120  esumpinfsum  30124  esumcvgsum  30135  ddemeas  30284  sxbrsigalem2  30333  omssubadd  30347  carsgclctunlem3  30367  signsply0  30613  ismblfin  33430  xrgepnfd  39366  supxrgelem  39372  supxrge  39373  infrpge  39386  xrlexaddrp  39387  infleinflem1  39405  infleinf  39407  infxrpnf  39493  ge0xrre  39567  iblsplit  39951  ismbl3  39972  ovolsplit  39974  sge0cl  40367  sge0less  40378  sge0pr  40380  sge0le  40393  sge0split  40395  carageniuncl  40506  ovnsubaddlem1  40553  hspmbl  40612  pimiooltgt  40690  pgrpgt2nabl  41918
  Copyright terms: Public domain W3C validator