Theorem pnfge 11348

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 11346	. 2 |- ( A e. RR* -> -. +oo < A )
2		pnfxr 11330	. . 3 |- +oo e. RR*
3		xrlenlt 9655	. . 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 1804   class class class wbr 4437   +oocpnf 9628   RR*cxr 9630   < clt 9631   <_ cle 9632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-cnex 9551  ax-resscn 9552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-nel 2641  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-xp 4995  df-cnv 4997  df-pnf 9633  df-mnf 9634  df-xr 9635  df-ltxr 9636  df-le 9637

This theorem is referenced by:  0lepnf  11349  nltpnft  11376  xrre2  11380  xleadd1a  11454  xlt2add  11461  xsubge0  11462  xlesubadd  11464  xlemul1a  11489  elico2  11597  iccmax  11609  elxrge0  11638  hashdom  12426  hashdomi  12427  hashge1  12436  hashss  12453  pcdvdsb  14269  pc2dvds  14279  pcaddlem  14284  xrsdsreclblem  18338  leordtvallem1  19584  lecldbas  19593  isxmet2d  20703  blssec  20811  nmoix  21109  nmoleub  21111  xrtgioo  21184  xrge0tsms  21212  metdstri  21228  nmoleub2lem  21470  ovolf  21766  ovollb2  21773  ovoliun  21789  ovolre  21809  voliunlem3  21835  volsup  21839  icombl  21847  ioombl  21848  ismbfd  21920  itg2seq  22022  dvfsumrlim  22305  dvfsumrlim2  22306  radcnvcl  22684  xrlimcnp  23170  logfacbnd3  23370  log2sumbnd  23601  tgldimor  23765  sizeusglecusg  24358  vdgfrgragt2  24899  xrdifh  27463  xrge0tsmsd  27648  unitssxrge0  27755  tpr2rico  27767  lmxrge0  27807  esumle  27938  esumlef  27943  esumpinfval  27952  esumpinfsum  27956  ddemeas  28081  sxbrsigalem2  28130  signsply0  28381  ismblfin  30030  elicore  31473  iblsplit  31655  pgrpgt2nabl  32692