Theorem pnfge 13090

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5107  +∞cpnf 11205  ℝ^*cxr 11207   < clt 11208   ≤ cle 11209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214

This theorem is referenced by:  pnfged  13091  xnn0n0n1ge2b  13092  0lepnf  13093  nltpnft  13124  xrre2  13130  xnn0lem1lt  13204  xleadd1a  13213  xlt2add  13220  xsubge0  13221  xlesubadd  13223  xlemul1a  13248  elicore  13359  elico2  13371  iccmax  13384  elxrge0  13418  nfile  14324  hashdom  14344  hashdomi  14345  hashge1  14354  hashss  14374  hashge2el2difr  14446  pcdvdsb  16840  pc2dvds  16850  pcaddlem  16859  xrsdsreclblem  21329  leordtvallem1  23097  lecldbas  23106  isxmet2d  24215  blssec  24323  nmoix  24617  nmoleub  24619  xrtgioo  24695  xrge0tsms  24723  metdstri  24740  nmoleub2lem  25014  ovolf  25383  ovollb2  25390  ovoliun  25406  ovolre  25426  voliunlem3  25453  volsup  25457  icombl  25465  ioombl  25466  ismbfd  25540  itg2seq  25643  dvfsumrlim  25938  dvfsumrlim2  25939  radcnvcl  26326  xrlimcnp  26878  logfacbnd3  27134  log2sumbnd  27455  tgldimor  28429  xrdifh  32703  xrge0tsmsd  33002  unitssxrge0  33890  tpr2rico  33902  lmxrge0  33942  esumle  34048  esumlef  34052  esumpinfval  34063  esumpinfsum  34067  esumcvgsum  34078  ddemeas  34226  sxbrsigalem2  34277  omssubadd  34291  carsgclctunlem3  34311  signsply0  34542  ismblfin  37655  xrgepnfd  45327  supxrgelem  45333  supxrge  45334  infrpge  45347  xrlexaddrp  45348  infleinflem1  45366  infleinf  45368  infxrpnf  45442  ge0xrre  45529  iblsplit  45964  ismbl3  45984  ovolsplit  45986  sge0cl  46379  sge0less  46390  sge0pr  46392  sge0le  46405  sge0split  46407  carageniuncl  46521  ovnsubaddlem1  46568  hspmbl  46627  pimiooltgt  46708  pgrpgt2nabl  48354