Theorem pnfge 13075

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 13073	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11193	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11204	. . 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 5086  +∞cpnf 11170  ℝ^*cxr 11172   < clt 11173   ≤ cle 11174

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 5232  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-xp 5631  df-cnv 5633  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179

This theorem is referenced by:  pnfged  13076  xnn0n0n1ge2b  13077  0lepnf  13078  nltpnft  13110  xrre2  13116  xnn0lem1lt  13190  xleadd1a  13199  xlt2add  13206  xsubge0  13207  xlesubadd  13209  xlemul1a  13234  elicore  13345  elico2  13357  iccmax  13370  elxrge0  13404  nfile  14315  hashdom  14335  hashdomi  14336  hashge1  14345  hashss  14365  hashge2el2difr  14437  pcdvdsb  16834  pc2dvds  16844  pcaddlem  16853  xrsdsreclblem  21405  leordtvallem1  23188  lecldbas  23197  isxmet2d  24305  blssec  24413  nmoix  24707  nmoleub  24709  xrtgioo  24785  xrge0tsms  24813  metdstri  24830  nmoleub2lem  25094  ovolf  25462  ovollb2  25469  ovoliun  25485  ovolre  25505  voliunlem3  25532  volsup  25536  icombl  25544  ioombl  25545  ismbfd  25619  itg2seq  25722  dvfsumrlim  26011  dvfsumrlim2  26012  radcnvcl  26398  logfacbnd3  27203  log2sumbnd  27524  tgldimor  28587  xrdifh  32871  xrge0tsmsd  33152  unitssxrge0  34063  tpr2rico  34075  lmxrge0  34115  esumle  34221  esumlef  34225  esumpinfval  34236  esumpinfsum  34240  esumcvgsum  34251  ddemeas  34399  sxbrsigalem2  34449  omssubadd  34463  carsgclctunlem3  34483  signsply0  34714  ismblfin  37999  xrgepnfd  45782  supxrgelem  45788  supxrge  45789  infrpge  45802  xrlexaddrp  45803  infleinflem1  45820  infleinf  45822  infxrpnf  45895  ge0xrre  45982  iblsplit  46415  ismbl3  46435  ovolsplit  46437  sge0cl  46830  sge0less  46841  sge0pr  46843  sge0le  46856  sge0split  46858  carageniuncl  46972  ovnsubaddlem1  47019  hspmbl  47078  pgrpgt2nabl  48857