Theorem pnfge 11421

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 11419	. 2 |- ( A e. RR* -> -. +oo < A )
2		pnfxr 11401	. . 3 |- +oo e. RR*
3		xrlenlt 9685	. . 3 |- ( ( A e. RR* /\ +oo e. RR* ) -> ( A <_ +oo <-> -. +oo < A ) )
4	2, 3	mpan2 682	. 2 |- ( A e. RR* -> ( A <_ +oo <-> -. +oo < A ) )
5	1, 4	mpbird 240	1 |- ( A e. RR* -> A <_ +oo )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   e. wcel 1890   class class class wbr 4373   +oocpnf 9658   RR*cxr 9660   < clt 9661   <_ cle 9662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-cnex 9581  ax-resscn 9582

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3014  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-op 3942  df-uni 4168  df-br 4374  df-opab 4433  df-xp 4817  df-cnv 4819  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667

This theorem is referenced by:  0lepnf  11422  nltpnft  11450  xrre2  11454  xleadd1a  11528  xlt2add  11535  xsubge0  11536  xlesubadd  11538  xlemul1a  11563  elicore  11676  elico2  11687  iccmax  11699  elxrge0  11731  hashdom  12551  hashdomi  12552  hashge1  12561  hashss  12579  hashge2el2difr  12632  pcdvdsb  14828  pc2dvds  14838  pcaddlem  14843  xrsdsreclblem  19024  leordtvallem1  20236  lecldbas  20245  isxmet2d  21352  blssec  21460  nmoix  21744  nmoleub  21746  nmoixOLD  21760  nmoleubOLD  21762  xrtgioo  21834  xrge0tsms  21862  metdstri  21878  metdstriOLD  21893  nmoleub2lem  22138  ovolf  22445  ovollb2  22452  ovoliun  22468  ovolre  22489  voliunlem3  22516  volsup  22520  icombl  22528  ioombl  22529  ismbfd  22607  itg2seq  22711  dvfsumrlim  22994  dvfsumrlim2  22995  radcnvcl  23383  xrlimcnp  23905  logfacbnd3  24162  log2sumbnd  24393  tgldimor  24557  sizeusglecusg  25225  vdgfrgragt2  25766  xrdifh  28369  xrge0tsmsd  28554  unitssxrge0  28712  tpr2rico  28724  lmxrge0  28764  esumle  28885  esumlef  28889  esumpinfval  28900  esumpinfsum  28904  esumcvgsum  28915  ddemeas  29064  sxbrsigalem2  29113  omssubadd  29133  oms0OLD  29134  omssubaddOLD  29137  carsgclctunlem3  29157  signsply0  29445  ismblfin  31982  xrgepnfd  37584  supxrgelem  37590  supxrge  37591  infrpge  37604  xrlexaddrp  37605  infleinflem1  37624  infleinf  37626  ge0xrre  37673  iblsplit  37884  ismbl3  37905  ovolsplit  37907  sge0cl  38281  sge0less  38292  sge0pr  38294  sge0le  38307  sge0split  38309  carageniuncl  38407  ovnsubaddlem1  38454  hspmbl  38513  nfile  39164  pgrpgt2nabl  40475