Theorem pnfge 13299

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 13297	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11402	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11413	. . 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 2147   class class class wbr 5108  +∞cpnf 11379  ℝ^*cxr 11381   < clt 11382   ≤ cle 11383

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-xp 5664  df-cnv 5666  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388

This theorem is used by:  pnfged  13300  xnn0n0n1ge2b  13301  0lepnf  13302  nltpnft  13334  xrre2  13340  xnn0lem1lt  13414  xleadd1a  13423  xlt2add  13430  xsubge0  13431  xlesubadd  13433  xlemul1a  13458  elicore  13569  elico2  13581  iccmax  13594  elxrge0  13628  nfile  14544  hashdom  14564  hashdomi  14565  hashge1  14574  hashss  14594  hashge2el2difr  14667  pcdvdsb  17091  pc2dvds  17101  pcaddlem  17110  xrsdsreclblem  21771  leordtvallem1  23583  lecldbas  23592  isxmet2d  24701  blssec  24809  nmoix  25103  nmoleub  25105  xrtgioo  25181  xrge0tsms  25209  metdstri  25226  nmoleub2lem  25490  ovolf  25858  ovollb2  25865  ovoliun  25881  ovolre  25901  voliunlem3  25928  volsup  25932  icombl  25940  ioombl  25941  ismbfd  26015  itg2seq  26118  dvfsumrlim  26406  dvfsumrlim2  26407  radcnvcl  26801  logfacbnd3  27607  log2sumbnd  27928  tgldimor  29022  xrdifh  33468  xrge0tsmsd  33733  unitssxrge0  34643  tpr2rico  34655  lmxrge0  34695  esumle  34801  esumlef  34805  esumpinfval  34816  esumpinfsum  34820  esumcvgsum  34831  ddemeas  34980  sxbrsigalem2  35029  carsgclctunlem3  35063  signsply0  35291  ismblfin  38847  xrgepnfd  46616  supxrgelem  46622  supxrge  46623  infrpge  46636  xrlexaddrp  46637  infleinflem1  46654  infleinf  46656  infxrpnf  46729  ge0xrre  46816  iblsplit  47249  ismbl3  47269  ovolsplit  47271  sge0cl  47664  sge0less  47675  sge0pr  47677  sge0le  47690  sge0split  47692  carageniuncl  47806  ovnsubaddlem1  47853  hspmbl  47912  pgrpgt2nabl  49809