Theorem pnfge 13044

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 13042	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11186	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11197	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 691	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 257	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2113   class class class wbr 5098  +∞cpnf 11163  ℝ^*cxr 11165   < clt 11166   ≤ cle 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-cnex 11082  ax-resscn 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172

This theorem is referenced by:  pnfged  13045  xnn0n0n1ge2b  13046  0lepnf  13047  nltpnft  13079  xrre2  13085  xnn0lem1lt  13159  xleadd1a  13168  xlt2add  13175  xsubge0  13176  xlesubadd  13178  xlemul1a  13203  elicore  13314  elico2  13326  iccmax  13339  elxrge0  13373  nfile  14282  hashdom  14302  hashdomi  14303  hashge1  14312  hashss  14332  hashge2el2difr  14404  pcdvdsb  16797  pc2dvds  16807  pcaddlem  16816  xrsdsreclblem  21367  leordtvallem1  23154  lecldbas  23163  isxmet2d  24271  blssec  24379  nmoix  24673  nmoleub  24675  xrtgioo  24751  xrge0tsms  24779  metdstri  24796  nmoleub2lem  25070  ovolf  25439  ovollb2  25446  ovoliun  25462  ovolre  25482  voliunlem3  25509  volsup  25513  icombl  25521  ioombl  25522  ismbfd  25596  itg2seq  25699  dvfsumrlim  25994  dvfsumrlim2  25995  radcnvcl  26382  logfacbnd3  27190  log2sumbnd  27511  tgldimor  28574  xrdifh  32860  xrge0tsmsd  33155  unitssxrge0  34057  tpr2rico  34069  lmxrge0  34109  esumle  34215  esumlef  34219  esumpinfval  34230  esumpinfsum  34234  esumcvgsum  34245  ddemeas  34393  sxbrsigalem2  34443  omssubadd  34457  carsgclctunlem3  34477  signsply0  34708  ismblfin  37862  xrgepnfd  45576  supxrgelem  45582  supxrge  45583  infrpge  45596  xrlexaddrp  45597  infleinflem1  45614  infleinf  45616  infxrpnf  45690  ge0xrre  45777  iblsplit  46210  ismbl3  46230  ovolsplit  46232  sge0cl  46625  sge0less  46636  sge0pr  46638  sge0le  46651  sge0split  46653  carageniuncl  46767  ovnsubaddlem1  46814  hspmbl  46873  pgrpgt2nabl  48612