Theorem pnfge 13134

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 13132	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11290	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11301	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 690	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 257	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2099   class class class wbr 5142  +∞cpnf 11267  ℝ^*cxr 11269   < clt 11270   ≤ cle 11271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-cnex 11186  ax-resscn 11187

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-xp 5678  df-cnv 5680  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276

This theorem is referenced by:  xnn0n0n1ge2b  13135  0lepnf  13136  nltpnft  13167  xrre2  13173  xnn0lem1lt  13247  xleadd1a  13256  xlt2add  13263  xsubge0  13264  xlesubadd  13266  xlemul1a  13291  elicore  13400  elico2  13412  iccmax  13424  elxrge0  13458  nfile  14342  hashdom  14362  hashdomi  14363  hashge1  14372  hashss  14392  hashge2el2difr  14466  pcdvdsb  16829  pc2dvds  16839  pcaddlem  16848  xrsdsreclblem  21332  leordtvallem1  23101  lecldbas  23110  isxmet2d  24220  blssec  24328  nmoix  24633  nmoleub  24635  xrtgioo  24709  xrge0tsms  24737  metdstri  24754  nmoleub2lem  25028  ovolf  25398  ovollb2  25405  ovoliun  25421  ovolre  25441  voliunlem3  25468  volsup  25472  icombl  25480  ioombl  25481  ismbfd  25555  itg2seq  25659  dvfsumrlim  25953  dvfsumrlim2  25954  radcnvcl  26340  xrlimcnp  26887  logfacbnd3  27143  log2sumbnd  27464  tgldimor  28293  xrdifh  32532  xrge0tsmsd  32749  unitssxrge0  33437  tpr2rico  33449  lmxrge0  33489  esumle  33613  esumlef  33617  esumpinfval  33628  esumpinfsum  33632  esumcvgsum  33643  ddemeas  33791  sxbrsigalem2  33842  omssubadd  33856  carsgclctunlem3  33876  signsply0  34119  ismblfin  37069  xrgepnfd  44636  supxrgelem  44642  supxrge  44643  infrpge  44656  xrlexaddrp  44657  infleinflem1  44675  infleinf  44677  infxrpnf  44751  pnfged  44779  ge0xrre  44839  iblsplit  45277  ismbl3  45297  ovolsplit  45299  sge0cl  45692  sge0less  45703  sge0pr  45705  sge0le  45718  sge0split  45720  carageniuncl  45834  ovnsubaddlem1  45881  hspmbl  45940  pimiooltgt  46021  pgrpgt2nabl  47353