Theorem pnfge 12848

Description: Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)

Assertion

Ref	Expression
pnfge	⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Proof of Theorem pnfge

Step	Hyp	Ref	Expression
1		pnfnlt 12846	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11013	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11024	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 687	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 256	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2109   class class class wbr 5078  +∞cpnf 10990  ℝ^*cxr 10992   < clt 10993   ≤ cle 10994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-cnex 10911  ax-resscn 10912

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-xp 5594  df-cnv 5596  df-pnf 10995  df-mnf 10996  df-xr 10997  df-ltxr 10998  df-le 10999

This theorem is referenced by:  xnn0n0n1ge2b  12849  0lepnf  12850  nltpnft  12880  xrre2  12886  xnn0lem1lt  12960  xleadd1a  12969  xlt2add  12976  xsubge0  12977  xlesubadd  12979  xlemul1a  13004  elicore  13113  elico2  13125  iccmax  13137  elxrge0  13171  nfile  14055  hashdom  14075  hashdomi  14076  hashge1  14085  hashss  14105  hashge2el2difr  14176  pcdvdsb  16551  pc2dvds  16561  pcaddlem  16570  xrsdsreclblem  20625  leordtvallem1  22342  lecldbas  22351  isxmet2d  23461  blssec  23569  nmoix  23874  nmoleub  23876  xrtgioo  23950  xrge0tsms  23978  metdstri  23995  nmoleub2lem  24258  ovolf  24627  ovollb2  24634  ovoliun  24650  ovolre  24670  voliunlem3  24697  volsup  24701  icombl  24709  ioombl  24710  ismbfd  24784  itg2seq  24888  dvfsumrlim  25176  dvfsumrlim2  25177  radcnvcl  25557  xrlimcnp  26099  logfacbnd3  26352  log2sumbnd  26673  tgldimor  26844  xrdifh  31080  xrge0tsmsd  31296  unitssxrge0  31829  tpr2rico  31841  lmxrge0  31881  esumle  32005  esumlef  32009  esumpinfval  32020  esumpinfsum  32024  esumcvgsum  32035  ddemeas  32183  sxbrsigalem2  32232  omssubadd  32246  carsgclctunlem3  32266  signsply0  32509  ismblfin  35797  xrgepnfd  42824  supxrgelem  42830  supxrge  42831  infrpge  42844  xrlexaddrp  42845  infleinflem1  42863  infleinf  42865  infxrpnf  42940  pnfged  42968  ge0xrre  43023  iblsplit  43461  ismbl3  43481  ovolsplit  43483  sge0cl  43873  sge0less  43884  sge0pr  43886  sge0le  43899  sge0split  43901  carageniuncl  44015  ovnsubaddlem1  44062  hspmbl  44121  pimiooltgt  44199  pgrpgt2nabl  45654