Theorem pnfge 13169

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2105   class class class wbr 5147  +∞cpnf 11289  ℝ^*cxr 11291   < clt 11292   ≤ cle 11293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298

This theorem is referenced by:  xnn0n0n1ge2b  13170  0lepnf  13171  nltpnft  13202  xrre2  13208  xnn0lem1lt  13282  xleadd1a  13291  xlt2add  13298  xsubge0  13299  xlesubadd  13301  xlemul1a  13326  elicore  13435  elico2  13447  iccmax  13459  elxrge0  13493  nfile  14394  hashdom  14414  hashdomi  14415  hashge1  14424  hashss  14444  hashge2el2difr  14516  pcdvdsb  16902  pc2dvds  16912  pcaddlem  16921  xrsdsreclblem  21447  leordtvallem1  23233  lecldbas  23242  isxmet2d  24352  blssec  24460  nmoix  24765  nmoleub  24767  xrtgioo  24841  xrge0tsms  24869  metdstri  24886  nmoleub2lem  25160  ovolf  25530  ovollb2  25537  ovoliun  25553  ovolre  25573  voliunlem3  25600  volsup  25604  icombl  25612  ioombl  25613  ismbfd  25687  itg2seq  25791  dvfsumrlim  26086  dvfsumrlim2  26087  radcnvcl  26474  xrlimcnp  27025  logfacbnd3  27281  log2sumbnd  27602  tgldimor  28524  xrdifh  32788  xrge0tsmsd  33047  unitssxrge0  33860  tpr2rico  33872  lmxrge0  33912  esumle  34038  esumlef  34042  esumpinfval  34053  esumpinfsum  34057  esumcvgsum  34068  ddemeas  34216  sxbrsigalem2  34267  omssubadd  34281  carsgclctunlem3  34301  signsply0  34544  ismblfin  37647  xrgepnfd  45280  supxrgelem  45286  supxrge  45287  infrpge  45300  xrlexaddrp  45301  infleinflem1  45319  infleinf  45321  infxrpnf  45395  pnfged  45423  ge0xrre  45483  iblsplit  45921  ismbl3  45941  ovolsplit  45943  sge0cl  46336  sge0less  46347  sge0pr  46349  sge0le  46362  sge0split  46364  carageniuncl  46478  ovnsubaddlem1  46525  hspmbl  46584  pimiooltgt  46665  pgrpgt2nabl  48210