Theorem pnfge 11964

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 11962	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 10092	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 10103	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 707	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 247	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∈ wcel 1990   class class class wbr 4653  +∞cpnf 10071  ℝ^*cxr 10073   < clt 10074   ≤ cle 10075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080

This theorem is referenced by:  xnn0n0n1ge2b  11965  0lepnf  11966  nltpnft  11995  xrre2  12001  xleadd1a  12083  xlt2add  12090  xsubge0  12091  xlesubadd  12093  xlemul1a  12118  elicore  12226  elico2  12237  iccmax  12249  elxrge0  12281  nfile  13150  hashdom  13168  hashdomi  13169  hashge1  13178  hashss  13197  hashge2el2difr  13263  pcdvdsb  15573  pc2dvds  15583  pcaddlem  15592  xrsdsreclblem  19792  leordtvallem1  21014  lecldbas  21023  isxmet2d  22132  blssec  22240  nmoix  22533  nmoleub  22535  xrtgioo  22609  xrge0tsms  22637  metdstri  22654  nmoleub2lem  22914  ovolf  23250  ovollb2  23257  ovoliun  23273  ovolre  23293  voliunlem3  23320  volsup  23324  icombl  23332  ioombl  23333  ismbfd  23407  itg2seq  23509  dvfsumrlim  23794  dvfsumrlim2  23795  radcnvcl  24171  xrlimcnp  24695  logfacbnd3  24948  log2sumbnd  25233  tgldimor  25397  xrdifh  29542  xrge0tsmsd  29785  unitssxrge0  29946  tpr2rico  29958  lmxrge0  29998  esumle  30120  esumlef  30124  esumpinfval  30135  esumpinfsum  30139  esumcvgsum  30150  ddemeas  30299  sxbrsigalem2  30348  omssubadd  30362  carsgclctunlem3  30382  signsply0  30628  ismblfin  33450  xrgepnfd  39547  supxrgelem  39553  supxrge  39554  infrpge  39567  xrlexaddrp  39568  infleinflem1  39586  infleinf  39588  infxrpnf  39674  pnfged  39704  ge0xrre  39758  iblsplit  40182  ismbl3  40203  ovolsplit  40205  sge0cl  40598  sge0less  40609  sge0pr  40611  sge0le  40624  sge0split  40626  carageniuncl  40737  ovnsubaddlem1  40784  hspmbl  40843  pimiooltgt  40921  pgrpgt2nabl  42147