Theorem pnfge 13132

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 13130	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11236	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11247	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 701	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 259	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∈ wcel 2142   class class class wbr 5100  +∞cpnf 11213  ℝ^*cxr 11215   < clt 11216   ≤ cle 11217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pow 5322  ax-pr 5390  ax-un 7718  ax-cnex 11129  ax-resscn 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5653  df-cnv 5655  df-pnf 11218  df-mnf 11219  df-xr 11220  df-ltxr 11221  df-le 11222

This theorem is referenced by:  pnfged  13133  xnn0n0n1ge2b  13134  0lepnf  13135  nltpnft  13167  xrre2  13173  xnn0lem1lt  13247  xleadd1a  13256  xlt2add  13263  xsubge0  13264  xlesubadd  13266  xlemul1a  13291  elicore  13402  elico2  13414  iccmax  13427  elxrge0  13461  nfile  14372  hashdom  14392  hashdomi  14393  hashge1  14402  hashss  14422  hashge2el2difr  14494  pcdvdsb  16905  pc2dvds  16915  pcaddlem  16924  xrsdsreclblem  21465  leordtvallem1  23270  lecldbas  23279  isxmet2d  24387  blssec  24495  nmoix  24789  nmoleub  24791  xrtgioo  24867  xrge0tsms  24895  metdstri  24912  nmoleub2lem  25176  ovolf  25544  ovollb2  25551  ovoliun  25567  ovolre  25587  voliunlem3  25614  volsup  25618  icombl  25626  ioombl  25627  ismbfd  25701  itg2seq  25804  dvfsumrlim  26093  dvfsumrlim2  26094  radcnvcl  26480  logfacbnd3  27287  log2sumbnd  27608  tgldimor  28671  xrdifh  32982  xrge0tsmsd  33253  unitssxrge0  34197  tpr2rico  34209  lmxrge0  34249  esumle  34355  esumlef  34359  esumpinfval  34370  esumpinfsum  34374  esumcvgsum  34385  ddemeas  34533  sxbrsigalem2  34583  omssubadd  34597  carsgclctunlem3  34617  signsply0  34845  ismblfin  38160  xrgepnfd  45907  supxrgelem  45913  supxrge  45914  infrpge  45927  xrlexaddrp  45928  infleinflem1  45945  infleinf  45947  infxrpnf  46020  ge0xrre  46107  iblsplit  46540  ismbl3  46560  ovolsplit  46562  sge0cl  46955  sge0less  46966  sge0pr  46968  sge0le  46981  sge0split  46983  carageniuncl  47097  ovnsubaddlem1  47144  hspmbl  47203  pgrpgt2nabl  48988