Theorem pnfge 13032

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5092  +∞cpnf 11146  ℝ^*cxr 11148   < clt 11149   ≤ cle 11150

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155

This theorem is referenced by:  pnfged  13033  xnn0n0n1ge2b  13034  0lepnf  13035  nltpnft  13066  xrre2  13072  xnn0lem1lt  13146  xleadd1a  13155  xlt2add  13162  xsubge0  13163  xlesubadd  13165  xlemul1a  13190  elicore  13301  elico2  13313  iccmax  13326  elxrge0  13360  nfile  14266  hashdom  14286  hashdomi  14287  hashge1  14296  hashss  14316  hashge2el2difr  14388  pcdvdsb  16781  pc2dvds  16791  pcaddlem  16800  xrsdsreclblem  21319  leordtvallem1  23095  lecldbas  23104  isxmet2d  24213  blssec  24321  nmoix  24615  nmoleub  24617  xrtgioo  24693  xrge0tsms  24721  metdstri  24738  nmoleub2lem  25012  ovolf  25381  ovollb2  25388  ovoliun  25404  ovolre  25424  voliunlem3  25451  volsup  25455  icombl  25463  ioombl  25464  ismbfd  25538  itg2seq  25641  dvfsumrlim  25936  dvfsumrlim2  25937  radcnvcl  26324  xrlimcnp  26876  logfacbnd3  27132  log2sumbnd  27453  tgldimor  28447  xrdifh  32723  xrge0tsmsd  33015  unitssxrge0  33867  tpr2rico  33879  lmxrge0  33919  esumle  34025  esumlef  34029  esumpinfval  34040  esumpinfsum  34044  esumcvgsum  34055  ddemeas  34203  sxbrsigalem2  34254  omssubadd  34268  carsgclctunlem3  34288  signsply0  34519  ismblfin  37641  xrgepnfd  45311  supxrgelem  45317  supxrge  45318  infrpge  45331  xrlexaddrp  45332  infleinflem1  45349  infleinf  45351  infxrpnf  45425  ge0xrre  45512  iblsplit  45947  ismbl3  45967  ovolsplit  45969  sge0cl  46362  sge0less  46373  sge0pr  46375  sge0le  46388  sge0split  46390  carageniuncl  46504  ovnsubaddlem1  46551  hspmbl  46610  pimiooltgt  46691  pgrpgt2nabl  48350