Theorem pnfge 13144

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2108   class class class wbr 5119  +∞cpnf 11264  ℝ^*cxr 11266   < clt 11267   ≤ cle 11268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-xp 5660  df-cnv 5662  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is referenced by:  pnfged  13145  xnn0n0n1ge2b  13146  0lepnf  13147  nltpnft  13178  xrre2  13184  xnn0lem1lt  13258  xleadd1a  13267  xlt2add  13274  xsubge0  13275  xlesubadd  13277  xlemul1a  13302  elicore  13413  elico2  13425  iccmax  13438  elxrge0  13472  nfile  14375  hashdom  14395  hashdomi  14396  hashge1  14405  hashss  14425  hashge2el2difr  14497  pcdvdsb  16887  pc2dvds  16897  pcaddlem  16906  xrsdsreclblem  21378  leordtvallem1  23146  lecldbas  23155  isxmet2d  24264  blssec  24372  nmoix  24666  nmoleub  24668  xrtgioo  24744  xrge0tsms  24772  metdstri  24789  nmoleub2lem  25063  ovolf  25433  ovollb2  25440  ovoliun  25456  ovolre  25476  voliunlem3  25503  volsup  25507  icombl  25515  ioombl  25516  ismbfd  25590  itg2seq  25693  dvfsumrlim  25988  dvfsumrlim2  25989  radcnvcl  26376  xrlimcnp  26928  logfacbnd3  27184  log2sumbnd  27505  tgldimor  28427  xrdifh  32703  xrge0tsmsd  33002  unitssxrge0  33877  tpr2rico  33889  lmxrge0  33929  esumle  34035  esumlef  34039  esumpinfval  34050  esumpinfsum  34054  esumcvgsum  34065  ddemeas  34213  sxbrsigalem2  34264  omssubadd  34278  carsgclctunlem3  34298  signsply0  34529  ismblfin  37631  xrgepnfd  45306  supxrgelem  45312  supxrge  45313  infrpge  45326  xrlexaddrp  45327  infleinflem1  45345  infleinf  45347  infxrpnf  45421  ge0xrre  45508  iblsplit  45943  ismbl3  45963  ovolsplit  45965  sge0cl  46358  sge0less  46369  sge0pr  46371  sge0le  46384  sge0split  46386  carageniuncl  46500  ovnsubaddlem1  46547  hspmbl  46606  pimiooltgt  46687  pgrpgt2nabl  48289