Theorem pnfge 12912

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2104   class class class wbr 5081  +∞cpnf 11052  ℝ^*cxr 11054   < clt 11055   ≤ cle 11056

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-cnex 10973  ax-resscn 10974

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-xp 5606  df-cnv 5608  df-pnf 11057  df-mnf 11058  df-xr 11059  df-ltxr 11060  df-le 11061

This theorem is referenced by:  xnn0n0n1ge2b  12913  0lepnf  12914  nltpnft  12944  xrre2  12950  xnn0lem1lt  13024  xleadd1a  13033  xlt2add  13040  xsubge0  13041  xlesubadd  13043  xlemul1a  13068  elicore  13177  elico2  13189  iccmax  13201  elxrge0  13235  nfile  14119  hashdom  14139  hashdomi  14140  hashge1  14149  hashss  14169  hashge2el2difr  14240  pcdvdsb  16615  pc2dvds  16625  pcaddlem  16634  xrsdsreclblem  20689  leordtvallem1  22406  lecldbas  22415  isxmet2d  23525  blssec  23633  nmoix  23938  nmoleub  23940  xrtgioo  24014  xrge0tsms  24042  metdstri  24059  nmoleub2lem  24322  ovolf  24691  ovollb2  24698  ovoliun  24714  ovolre  24734  voliunlem3  24761  volsup  24765  icombl  24773  ioombl  24774  ismbfd  24848  itg2seq  24952  dvfsumrlim  25240  dvfsumrlim2  25241  radcnvcl  25621  xrlimcnp  26163  logfacbnd3  26416  log2sumbnd  26737  tgldimor  26908  xrdifh  31146  xrge0tsmsd  31362  unitssxrge0  31895  tpr2rico  31907  lmxrge0  31947  esumle  32071  esumlef  32075  esumpinfval  32086  esumpinfsum  32090  esumcvgsum  32101  ddemeas  32249  sxbrsigalem2  32298  omssubadd  32312  carsgclctunlem3  32332  signsply0  32575  ismblfin  35862  xrgepnfd  42918  supxrgelem  42924  supxrge  42925  infrpge  42938  xrlexaddrp  42939  infleinflem1  42957  infleinf  42959  infxrpnf  43034  pnfged  43062  ge0xrre  43118  iblsplit  43556  ismbl3  43576  ovolsplit  43578  sge0cl  43969  sge0less  43980  sge0pr  43982  sge0le  43995  sge0split  43997  carageniuncl  44111  ovnsubaddlem1  44158  hspmbl  44217  pimiooltgt  44298  pgrpgt2nabl  45760