Theorem pnfge 13151

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2149   class class class wbr 5110  +∞cpnf 11236  ℝ^*cxr 11238   < clt 11239   ≤ cle 11240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-cnex 11152  ax-resscn 11153

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-xp 5665  df-cnv 5667  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245

This theorem is referenced by:  pnfged  13152  xnn0n0n1ge2b  13153  0lepnf  13154  nltpnft  13186  xrre2  13192  xnn0lem1lt  13266  xleadd1a  13275  xlt2add  13282  xsubge0  13283  xlesubadd  13285  xlemul1a  13310  elicore  13421  elico2  13433  iccmax  13446  elxrge0  13480  nfile  14391  hashdom  14411  hashdomi  14412  hashge1  14421  hashss  14441  hashge2el2difr  14514  pcdvdsb  16925  pc2dvds  16935  pcaddlem  16944  xrsdsreclblem  21528  leordtvallem1  23332  lecldbas  23341  isxmet2d  24449  blssec  24557  nmoix  24851  nmoleub  24853  xrtgioo  24929  xrge0tsms  24957  metdstri  24974  nmoleub2lem  25238  ovolf  25606  ovollb2  25613  ovoliun  25629  ovolre  25649  voliunlem3  25676  volsup  25680  icombl  25688  ioombl  25689  ismbfd  25763  itg2seq  25866  dvfsumrlim  26155  dvfsumrlim2  26156  radcnvcl  26542  logfacbnd3  27349  log2sumbnd  27670  tgldimor  28733  xrdifh  33062  xrge0tsmsd  33330  unitssxrge0  34231  tpr2rico  34243  lmxrge0  34283  esumle  34389  esumlef  34393  esumpinfval  34404  esumpinfsum  34408  esumcvgsum  34419  ddemeas  34567  sxbrsigalem2  34617  omssubadd  34631  carsgclctunlem3  34651  signsply0  34879  ismblfin  38195  xrgepnfd  45932  supxrgelem  45938  supxrge  45939  infrpge  45952  xrlexaddrp  45953  infleinflem1  45970  infleinf  45972  infxrpnf  46045  ge0xrre  46132  iblsplit  46565  ismbl3  46585  ovolsplit  46587  sge0cl  46980  sge0less  46991  sge0pr  46993  sge0le  47006  sge0split  47008  carageniuncl  47122  ovnsubaddlem1  47169  hspmbl  47228  pgrpgt2nabl  49024