Theorem pnfge 13182

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 13180	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11288	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11299	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 704	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 260	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2145   class class class wbr 5103  +∞cpnf 11265  ℝ^*cxr 11267   < clt 11268   ≤ cle 11269

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-cnex 11181  ax-resscn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-pnf 11270  df-mnf 11271  df-xr 11272  df-ltxr 11273  df-le 11274

This theorem is used by:  pnfged  13183  xnn0n0n1ge2b  13184  0lepnf  13185  nltpnft  13217  xrre2  13223  xnn0lem1lt  13297  xleadd1a  13306  xlt2add  13313  xsubge0  13314  xlesubadd  13316  xlemul1a  13341  elicore  13452  elico2  13464  iccmax  13477  elxrge0  13511  nfile  14424  hashdom  14444  hashdomi  14445  hashge1  14454  hashss  14474  hashge2el2difr  14547  pcdvdsb  16962  pc2dvds  16972  pcaddlem  16981  xrsdsreclblem  21627  leordtvallem1  23436  lecldbas  23445  isxmet2d  24554  blssec  24662  nmoix  24956  nmoleub  24958  xrtgioo  25034  xrge0tsms  25062  metdstri  25079  nmoleub2lem  25343  ovolf  25711  ovollb2  25718  ovoliun  25734  ovolre  25754  voliunlem3  25781  volsup  25785  icombl  25793  ioombl  25794  ismbfd  25868  itg2seq  25971  dvfsumrlim  26259  dvfsumrlim2  26260  radcnvcl  26654  logfacbnd3  27460  log2sumbnd  27781  tgldimor  28845  xrdifh  33252  xrge0tsmsd  33514  unitssxrge0  34411  tpr2rico  34423  lmxrge0  34463  esumle  34569  esumlef  34573  esumpinfval  34584  esumpinfsum  34588  esumcvgsum  34599  ddemeas  34748  sxbrsigalem2  34798  omssubadd  34812  carsgclctunlem3  34832  signsply0  35060  ismblfin  38411  xrgepnfd  46162  supxrgelem  46168  supxrge  46169  infrpge  46182  xrlexaddrp  46183  infleinflem1  46200  infleinf  46202  infxrpnf  46275  ge0xrre  46362  iblsplit  46795  ismbl3  46815  ovolsplit  46817  sge0cl  47210  sge0less  47221  sge0pr  47223  sge0le  47236  sge0split  47238  carageniuncl  47352  ovnsubaddlem1  47399  hspmbl  47458  pgrpgt2nabl  49297