Theorem pnfge 12971

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2106   class class class wbr 5096  +∞cpnf 11111  ℝ^*cxr 11113   < clt 11114   ≤ cle 11115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-sep 5247  ax-nul 5254  ax-pow 5312  ax-pr 5376  ax-un 7654  ax-cnex 11032  ax-resscn 11033

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3405  df-v 3444  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4274  df-if 4478  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4857  df-br 5097  df-opab 5159  df-xp 5630  df-cnv 5632  df-pnf 11116  df-mnf 11117  df-xr 11118  df-ltxr 11119  df-le 11120

This theorem is referenced by:  xnn0n0n1ge2b  12972  0lepnf  12973  nltpnft  13003  xrre2  13009  xnn0lem1lt  13083  xleadd1a  13092  xlt2add  13099  xsubge0  13100  xlesubadd  13102  xlemul1a  13127  elicore  13236  elico2  13248  iccmax  13260  elxrge0  13294  nfile  14178  hashdom  14198  hashdomi  14199  hashge1  14208  hashss  14228  hashge2el2difr  14299  pcdvdsb  16667  pc2dvds  16677  pcaddlem  16686  xrsdsreclblem  20749  leordtvallem1  22466  lecldbas  22475  isxmet2d  23585  blssec  23693  nmoix  23998  nmoleub  24000  xrtgioo  24074  xrge0tsms  24102  metdstri  24119  nmoleub2lem  24382  ovolf  24751  ovollb2  24758  ovoliun  24774  ovolre  24794  voliunlem3  24821  volsup  24825  icombl  24833  ioombl  24834  ismbfd  24908  itg2seq  25012  dvfsumrlim  25300  dvfsumrlim2  25301  radcnvcl  25681  xrlimcnp  26223  logfacbnd3  26476  log2sumbnd  26797  tgldimor  27151  xrdifh  31386  xrge0tsmsd  31602  unitssxrge0  32146  tpr2rico  32158  lmxrge0  32198  esumle  32322  esumlef  32326  esumpinfval  32337  esumpinfsum  32341  esumcvgsum  32352  ddemeas  32500  sxbrsigalem2  32551  omssubadd  32565  carsgclctunlem3  32585  signsply0  32828  ismblfin  35974  xrgepnfd  43257  supxrgelem  43263  supxrge  43264  infrpge  43277  xrlexaddrp  43278  infleinflem1  43296  infleinf  43298  infxrpnf  43373  pnfged  43401  ge0xrre  43457  iblsplit  43895  ismbl3  43915  ovolsplit  43917  sge0cl  44308  sge0less  44319  sge0pr  44321  sge0le  44334  sge0split  44336  carageniuncl  44450  ovnsubaddlem1  44497  hspmbl  44556  pimiooltgt  44637  pgrpgt2nabl  46120