Theorem pnfge 13097

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 13095	. 2 ⊢ (𝐴 ∈ ℝ* → ¬ +∞ < 𝐴)
2		pnfxr 11235	. . 3 ⊢ +∞ ∈ ℝ*
3		xrlenlt 11246	. . 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 5110  +∞cpnf 11212  ℝ^*cxr 11214   < clt 11215   ≤ cle 11216

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221

This theorem is referenced by:  pnfged  13098  xnn0n0n1ge2b  13099  0lepnf  13100  nltpnft  13131  xrre2  13137  xnn0lem1lt  13211  xleadd1a  13220  xlt2add  13227  xsubge0  13228  xlesubadd  13230  xlemul1a  13255  elicore  13366  elico2  13378  iccmax  13391  elxrge0  13425  nfile  14331  hashdom  14351  hashdomi  14352  hashge1  14361  hashss  14381  hashge2el2difr  14453  pcdvdsb  16847  pc2dvds  16857  pcaddlem  16866  xrsdsreclblem  21336  leordtvallem1  23104  lecldbas  23113  isxmet2d  24222  blssec  24330  nmoix  24624  nmoleub  24626  xrtgioo  24702  xrge0tsms  24730  metdstri  24747  nmoleub2lem  25021  ovolf  25390  ovollb2  25397  ovoliun  25413  ovolre  25433  voliunlem3  25460  volsup  25464  icombl  25472  ioombl  25473  ismbfd  25547  itg2seq  25650  dvfsumrlim  25945  dvfsumrlim2  25946  radcnvcl  26333  xrlimcnp  26885  logfacbnd3  27141  log2sumbnd  27462  tgldimor  28436  xrdifh  32710  xrge0tsmsd  33009  unitssxrge0  33897  tpr2rico  33909  lmxrge0  33949  esumle  34055  esumlef  34059  esumpinfval  34070  esumpinfsum  34074  esumcvgsum  34085  ddemeas  34233  sxbrsigalem2  34284  omssubadd  34298  carsgclctunlem3  34318  signsply0  34549  ismblfin  37662  xrgepnfd  45334  supxrgelem  45340  supxrge  45341  infrpge  45354  xrlexaddrp  45355  infleinflem1  45373  infleinf  45375  infxrpnf  45449  ge0xrre  45536  iblsplit  45971  ismbl3  45991  ovolsplit  45993  sge0cl  46386  sge0less  46397  sge0pr  46399  sge0le  46412  sge0split  46414  carageniuncl  46528  ovnsubaddlem1  46575  hspmbl  46634  pimiooltgt  46715  pgrpgt2nabl  48358