Theorem pnfge 13072

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 13070	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11190	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11201	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
4	2, 3	mpan2 697	. 2 ⊢ (𝐴 ∈ ℝ* → (𝐴 ≤ +∞ ↔ ¬ +∞ < 𝐴))
5	1, 4	mpbird 258	1 ⊢ (𝐴 ∈ ℝ* → 𝐴 ≤ +∞)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∈ wcel 2119   class class class wbr 5072  +∞cpnf 11167  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  pnfged  13073  xnn0n0n1ge2b  13074  0lepnf  13075  nltpnft  13107  xrre2  13113  xnn0lem1lt  13187  xleadd1a  13196  xlt2add  13203  xsubge0  13204  xlesubadd  13206  xlemul1a  13231  elicore  13342  elico2  13354  iccmax  13367  elxrge0  13401  nfile  14312  hashdom  14332  hashdomi  14333  hashge1  14342  hashss  14362  hashge2el2difr  14434  pcdvdsb  16831  pc2dvds  16841  pcaddlem  16850  xrsdsreclblem  21388  leordtvallem1  23193  lecldbas  23202  isxmet2d  24310  blssec  24418  nmoix  24712  nmoleub  24714  xrtgioo  24790  xrge0tsms  24818  metdstri  24835  nmoleub2lem  25099  ovolf  25467  ovollb2  25474  ovoliun  25490  ovolre  25510  voliunlem3  25537  volsup  25541  icombl  25549  ioombl  25550  ismbfd  25624  itg2seq  25727  dvfsumrlim  26016  dvfsumrlim2  26017  radcnvcl  26400  logfacbnd3  27204  log2sumbnd  27525  tgldimor  28588  xrdifh  32872  xrge0tsmsd  33154  unitssxrge0  34084  tpr2rico  34096  lmxrge0  34136  esumle  34242  esumlef  34246  esumpinfval  34257  esumpinfsum  34261  esumcvgsum  34272  ddemeas  34420  sxbrsigalem2  34470  omssubadd  34484  carsgclctunlem3  34504  signsply0  34735  ismblfin  38028  xrgepnfd  45776  supxrgelem  45782  supxrge  45783  infrpge  45796  xrlexaddrp  45797  infleinflem1  45814  infleinf  45816  infxrpnf  45889  ge0xrre  45976  iblsplit  46409  ismbl3  46429  ovolsplit  46431  sge0cl  46824  sge0less  46835  sge0pr  46837  sge0le  46850  sge0split  46852  carageniuncl  46966  ovnsubaddlem1  47013  hspmbl  47072  pgrpgt2nabl  48857