Theorem pnfge 13259

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 13257	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11363	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11374	. . 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 11340  ℝ^*cxr 11342   < clt 11343   ≤ cle 11344

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 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-cnex 11256  ax-resscn 11257

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5657  df-cnv 5659  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349

This theorem is used by:  pnfged  13260  xnn0n0n1ge2b  13261  0lepnf  13262  nltpnft  13294  xrre2  13300  xnn0lem1lt  13374  xleadd1a  13383  xlt2add  13390  xsubge0  13391  xlesubadd  13393  xlemul1a  13418  elicore  13529  elico2  13541  iccmax  13554  elxrge0  13588  nfile  14503  hashdom  14523  hashdomi  14524  hashge1  14533  hashss  14553  hashge2el2difr  14626  pcdvdsb  17047  pc2dvds  17057  pcaddlem  17066  xrsdsreclblem  21719  leordtvallem1  23528  lecldbas  23537  isxmet2d  24646  blssec  24754  nmoix  25048  nmoleub  25050  xrtgioo  25126  xrge0tsms  25154  metdstri  25171  nmoleub2lem  25435  ovolf  25803  ovollb2  25810  ovoliun  25826  ovolre  25846  voliunlem3  25873  volsup  25877  icombl  25885  ioombl  25886  ismbfd  25960  itg2seq  26063  dvfsumrlim  26351  dvfsumrlim2  26352  radcnvcl  26744  logfacbnd3  27550  log2sumbnd  27871  tgldimor  28965  xrdifh  33372  xrge0tsmsd  33634  unitssxrge0  34532  tpr2rico  34544  lmxrge0  34584  esumle  34690  esumlef  34694  esumpinfval  34705  esumpinfsum  34709  esumcvgsum  34720  ddemeas  34869  sxbrsigalem2  34918  omssubadd  34932  carsgclctunlem3  34952  signsply0  35180  ismblfin  38579  xrgepnfd  46342  supxrgelem  46348  supxrge  46349  infrpge  46362  xrlexaddrp  46363  infleinflem1  46380  infleinf  46382  infxrpnf  46455  ge0xrre  46542  iblsplit  46975  ismbl3  46995  ovolsplit  46997  sge0cl  47390  sge0less  47401  sge0pr  47403  sge0le  47416  sge0split  47418  carageniuncl  47532  ovnsubaddlem1  47579  hspmbl  47638  pgrpgt2nabl  49477