Theorem pnfge 12342

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 12340	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 10494	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 10506	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 678	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 249	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∈ wcel 2050   class class class wbr 4929  +∞cpnf 10471  ℝ^*cxr 10473   < clt 10474   ≤ cle 10475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-cnex 10391  ax-resscn 10392

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-xp 5413  df-cnv 5415  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480

This theorem is referenced by:  xnn0n0n1ge2b  12343  0lepnf  12344  nltpnft  12374  xrre2  12380  xleadd1a  12462  xlt2add  12469  xsubge0  12470  xlesubadd  12472  xlemul1a  12497  elicore  12605  elico2  12616  iccmax  12628  elxrge0  12661  nfile  13535  hashdom  13553  hashdomi  13554  hashge1  13563  hashss  13583  hashge2el2difr  13650  pcdvdsb  16061  pc2dvds  16071  pcaddlem  16080  xrsdsreclblem  20293  leordtvallem1  21522  lecldbas  21531  isxmet2d  22640  blssec  22748  nmoix  23041  nmoleub  23043  xrtgioo  23117  xrge0tsms  23145  metdstri  23162  nmoleub2lem  23421  ovolf  23786  ovollb2  23793  ovoliun  23809  ovolre  23829  voliunlem3  23856  volsup  23860  icombl  23868  ioombl  23869  ismbfd  23943  itg2seq  24046  dvfsumrlim  24331  dvfsumrlim2  24332  radcnvcl  24708  xrlimcnp  25248  logfacbnd3  25501  log2sumbnd  25822  tgldimor  25990  xnn0lem1lt  30254  xrdifh  30262  xrge0tsmsd  30536  unitssxrge0  30793  tpr2rico  30805  lmxrge0  30845  esumle  30967  esumlef  30971  esumpinfval  30982  esumpinfsum  30986  esumcvgsum  30997  ddemeas  31146  sxbrsigalem2  31195  omssubadd  31209  carsgclctunlem3  31229  signsply0  31473  ismblfin  34380  xrgepnfd  41034  supxrgelem  41040  supxrge  41041  infrpge  41054  xrlexaddrp  41055  infleinflem1  41073  infleinf  41075  infxrpnf  41158  pnfged  41187  ge0xrre  41244  iblsplit  41687  ismbl3  41708  ovolsplit  41710  sge0cl  42100  sge0less  42111  sge0pr  42113  sge0le  42126  sge0split  42128  carageniuncl  42242  ovnsubaddlem1  42289  hspmbl  42348  pimiooltgt  42426  pgrpgt2nabl  43786