Theorem pnfge 13150

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2143   class class class wbr 5109  +∞cpnf 11235  ℝ^*cxr 11237   < clt 11238   ≤ cle 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-xp 5667  df-cnv 5669  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244

This theorem is referenced by:  pnfged  13151  xnn0n0n1ge2b  13152  0lepnf  13153  nltpnft  13185  xrre2  13191  xnn0lem1lt  13265  xleadd1a  13274  xlt2add  13281  xsubge0  13282  xlesubadd  13284  xlemul1a  13309  elicore  13420  elico2  13432  iccmax  13445  elxrge0  13479  nfile  14391  hashdom  14411  hashdomi  14412  hashge1  14421  hashss  14441  hashge2el2difr  14514  pcdvdsb  16924  pc2dvds  16934  pcaddlem  16943  xrsdsreclblem  21563  leordtvallem1  23367  lecldbas  23376  isxmet2d  24484  blssec  24592  nmoix  24886  nmoleub  24888  xrtgioo  24964  xrge0tsms  24992  metdstri  25009  nmoleub2lem  25273  ovolf  25641  ovollb2  25648  ovoliun  25664  ovolre  25684  voliunlem3  25711  volsup  25715  icombl  25723  ioombl  25724  ismbfd  25798  itg2seq  25901  dvfsumrlim  26190  dvfsumrlim2  26191  radcnvcl  26580  logfacbnd3  27387  log2sumbnd  27708  tgldimor  28771  xrdifh  33125  xrge0tsmsd  33393  unitssxrge0  34290  tpr2rico  34302  lmxrge0  34342  esumle  34448  esumlef  34452  esumpinfval  34463  esumpinfsum  34467  esumcvgsum  34478  ddemeas  34626  sxbrsigalem2  34676  omssubadd  34690  carsgclctunlem3  34710  signsply0  34938  ismblfin  38332  xrgepnfd  46067  supxrgelem  46073  supxrge  46074  infrpge  46087  xrlexaddrp  46088  infleinflem1  46105  infleinf  46107  infxrpnf  46180  ge0xrre  46267  iblsplit  46700  ismbl3  46720  ovolsplit  46722  sge0cl  47115  sge0less  47126  sge0pr  47128  sge0le  47141  sge0split  47143  carageniuncl  47257  ovnsubaddlem1  47304  hspmbl  47363  pgrpgt2nabl  49166