Theorem pnfge 13056

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2114   class class class wbr 5100  +∞cpnf 11175  ℝ^*cxr 11177   < clt 11178   ≤ cle 11179

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184

This theorem is referenced by:  pnfged  13057  xnn0n0n1ge2b  13058  0lepnf  13059  nltpnft  13091  xrre2  13097  xnn0lem1lt  13171  xleadd1a  13180  xlt2add  13187  xsubge0  13188  xlesubadd  13190  xlemul1a  13215  elicore  13326  elico2  13338  iccmax  13351  elxrge0  13385  nfile  14294  hashdom  14314  hashdomi  14315  hashge1  14324  hashss  14344  hashge2el2difr  14416  pcdvdsb  16809  pc2dvds  16819  pcaddlem  16828  xrsdsreclblem  21379  leordtvallem1  23166  lecldbas  23175  isxmet2d  24283  blssec  24391  nmoix  24685  nmoleub  24687  xrtgioo  24763  xrge0tsms  24791  metdstri  24808  nmoleub2lem  25082  ovolf  25451  ovollb2  25458  ovoliun  25474  ovolre  25494  voliunlem3  25521  volsup  25525  icombl  25533  ioombl  25534  ismbfd  25608  itg2seq  25711  dvfsumrlim  26006  dvfsumrlim2  26007  radcnvcl  26394  logfacbnd3  27202  log2sumbnd  27523  tgldimor  28586  xrdifh  32871  xrge0tsmsd  33167  unitssxrge0  34078  tpr2rico  34090  lmxrge0  34130  esumle  34236  esumlef  34240  esumpinfval  34251  esumpinfsum  34255  esumcvgsum  34266  ddemeas  34414  sxbrsigalem2  34464  omssubadd  34478  carsgclctunlem3  34498  signsply0  34729  ismblfin  37912  xrgepnfd  45690  supxrgelem  45696  supxrge  45697  infrpge  45710  xrlexaddrp  45711  infleinflem1  45728  infleinf  45730  infxrpnf  45804  ge0xrre  45891  iblsplit  46324  ismbl3  46344  ovolsplit  46346  sge0cl  46739  sge0less  46750  sge0pr  46752  sge0le  46765  sge0split  46767  carageniuncl  46881  ovnsubaddlem1  46928  hspmbl  46987  pgrpgt2nabl  48726