Theorem pnfge 11213

Description: Plus infinity is an upper bound for extended reals. (Contributed by NM, 30-Jan-2006.)

Assertion

Ref	Expression
pnfge	|- ( A e. RR* -> A <_ +oo )

Proof of Theorem pnfge

Step	Hyp	Ref	Expression
1		pnfnlt 11211	. 2 |- ( A e. RR* -> -. +oo < A )
2		pnfxr 11195	. . 3 |- +oo e. RR*
3		xrlenlt 9545	. . 3 |- ( ( A e. RR* /\ +oo e. RR* ) -> ( A <_ +oo <-> -. +oo < A ) )
4	2, 3	mpan2 671	. 2 |- ( A e. RR* -> ( A <_ +oo <-> -. +oo < A ) )
5	1, 4	mpbird 232	1 |- ( A e. RR* -> A <_ +oo )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   e. wcel 1758   class class class wbr 4392   +oocpnf 9518   RR*cxr 9520   < clt 9521   <_ cle 9522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4513  ax-nul 4521  ax-pow 4570  ax-pr 4631  ax-un 6474  ax-cnex 9441  ax-resscn 9442

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3072  df-dif 3431  df-un 3433  df-in 3435  df-ss 3442  df-nul 3738  df-if 3892  df-pw 3962  df-sn 3978  df-pr 3980  df-op 3984  df-uni 4192  df-br 4393  df-opab 4451  df-xp 4946  df-cnv 4948  df-pnf 9523  df-mnf 9524  df-xr 9525  df-ltxr 9526  df-le 9527

This theorem is referenced by:  0lepnf  11214  nltpnft  11241  xrre2  11245  xleadd1a  11319  xlt2add  11326  xsubge0  11327  xlesubadd  11329  xlemul1a  11354  elico2  11462  iccmax  11474  elxrge0  11497  hashdom  12246  hashdomi  12247  hashge1  12256  hashss  12270  pcdvdsb  14039  pc2dvds  14049  pcaddlem  14054  xrsdsreclblem  17970  leordtvallem1  18932  lecldbas  18941  isxmet2d  20020  blssec  20128  nmoix  20426  nmoleub  20428  xrtgioo  20501  xrge0tsms  20529  metdstri  20545  nmoleub2lem  20787  ovolf  21083  ovollb2  21090  ovoliun  21106  ovolre  21126  voliunlem3  21151  volsup  21155  icombl  21163  ioombl  21164  ismbfd  21236  itg2seq  21338  dvfsumrlim  21621  dvfsumrlim2  21622  radcnvcl  22000  xrlimcnp  22480  logfacbnd3  22680  log2sumbnd  22911  tgldimor  23075  sizeusglecusg  23531  xrge0infss  26189  xrdifh  26206  xrge0tsmsd  26389  unitssxrge0  26466  tpr2rico  26478  lmxrge0  26518  esumle  26644  esumlef  26649  esumfsupre  26656  esumpinfval  26658  esumpfinvallem  26659  esumpinfsum  26662  esumpcvgval  26663  esumcvg  26671  ddemeas  26788  sxbrsigalem2  26837  oms0  26846  signsply0  27088  ismblfin  28572  vdgfrgragt2  30760  pgrpgt2nabel  30911