Theorem pnfge 11328

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 11326	. 2 |- ( A e. RR* -> -. +oo < A )
2		pnfxr 11310	. . 3 |- +oo e. RR*
3		xrlenlt 9641	. . 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 1762   class class class wbr 4440   +oocpnf 9614   RR*cxr 9616   < clt 9617   <_ cle 9618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-cnex 9537  ax-resscn 9538

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-xp 4998  df-cnv 5000  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623

This theorem is referenced by:  0lepnf  11329  nltpnft  11356  xrre2  11360  xleadd1a  11434  xlt2add  11441  xsubge0  11442  xlesubadd  11444  xlemul1a  11469  elico2  11577  iccmax  11589  elxrge0  11618  hashdom  12402  hashdomi  12403  hashge1  12412  hashss  12426  pcdvdsb  14240  pc2dvds  14250  pcaddlem  14255  xrsdsreclblem  18225  leordtvallem1  19470  lecldbas  19479  isxmet2d  20558  blssec  20666  nmoix  20964  nmoleub  20966  xrtgioo  21039  xrge0tsms  21067  metdstri  21083  nmoleub2lem  21325  ovolf  21621  ovollb2  21628  ovoliun  21644  ovolre  21664  voliunlem3  21690  volsup  21694  icombl  21702  ioombl  21703  ismbfd  21775  itg2seq  21877  dvfsumrlim  22160  dvfsumrlim2  22161  radcnvcl  22539  xrlimcnp  23019  logfacbnd3  23219  log2sumbnd  23450  tgldimor  23614  sizeusglecusg  24148  vdgfrgragt2  24690  xrge0infss  27234  xrdifh  27245  xrge0tsmsd  27424  unitssxrge0  27504  tpr2rico  27516  lmxrge0  27556  esumle  27691  esumlef  27696  esumfsupre  27703  esumpinfval  27705  esumpfinvallem  27706  esumpinfsum  27709  esumpcvgval  27710  esumcvg  27718  ddemeas  27834  sxbrsigalem2  27883  oms0  27892  signsply0  28134  ismblfin  29619  elicore  31056  iblsplit  31239  pgrpgt2nabl  31899