Theorem 0xr 9540

Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)

Assertion

Ref	Expression
0xr	|- 0 e. RR*

Proof of Theorem 0xr

Step	Hyp	Ref	Expression
1		ressxr 9537	. 2 |- RR C_ RR*
2		0re 9496	. 2 |- 0 e. RR
3	1, 2	sselii 3460	1 |- 0 e. RR*

Syntax hints:   e. wcel 1758   RRcr 9391   0cc0 9392   RR*cxr 9527

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-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-addrcl 9453  ax-mulcl 9454  ax-mulrcl 9455  ax-i2m1 9460  ax-1ne0 9461  ax-rnegex 9463  ax-rrecex 9464  ax-cnre 9465

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-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533  df-ov 6202  df-xr 9532

This theorem is referenced by:  0lepnf  11221  ge0gtmnf  11254  max0sub  11276  xlt0neg1  11299  xlt0neg2  11300  xle0neg1  11301  xle0neg2  11302  xaddf  11304  xaddid1  11319  xaddid2  11320  xaddge0  11331  xsubge0  11334  xposdif  11335  xmullem  11337  xmullem2  11338  xmul01  11340  xmul02  11341  xmulneg1  11342  xmulf  11345  xmulpnf1  11347  xmulasslem2  11355  xmulge0  11357  xmulasslem  11358  xlemul1a  11361  xadddi  11368  xadddi2  11370  ioopos  11482  ioorebas  11507  elxrge0  11510  0e0iccpnf  11512  xov1plusxeqvd  11547  rpsup  11821  hashgt0  12268  hashle00  12275  hashgt0elex  12276  sgn0  12695  sgnp  12696  sgnn  12700  ef01bndlem  13585  sin01bnd  13586  cos01bnd  13587  cos1bnd  13588  sinltx  13590  sin01gt0  13591  cos01gt0  13592  sin02gt0  13593  sincos1sgn  13594  sincos2sgn  13595  leordtval2  18947  pnfnei  18955  mnfnei  18956  psmetge0  20019  isxmet2d  20033  xmetge0  20050  xmetgt0  20064  prdsdsf  20073  prdsxmetlem  20074  xpsdsval  20087  blgt0  20105  xblss2ps  20107  xblss2  20108  xbln0  20120  prdsbl  20197  stdbdxmet  20221  stdbdmopn  20224  metusttoOLD  20263  metustto  20264  metustidOLD  20265  metustid  20266  metustexhalfOLD  20269  metustexhalf  20270  cfilucfilOLD  20275  cfilucfil  20276  blval2  20281  metuel2  20285  nmoge0  20431  nmo0  20445  cnblcld  20485  blssioo  20503  blcvx  20506  xrsxmet  20517  metdsf  20555  metds0  20557  metdseq0  20561  metnrmlem1a  20565  iccpnfcnv  20647  iccpnfhmeo  20648  xrhmeo  20649  pcoass  20727  iscfil2  20908  ovolmge0  21091  ovolge0  21095  ovolf  21096  ovolssnul  21101  ovolctb  21104  ovoliunnul  21121  ovolicopnf  21138  voliunlem3  21165  volsup  21169  ioorf  21185  volivth  21219  vitalilem4  21223  vitalilem5  21224  itg2ge0  21345  itg2const2  21351  itg2seq  21352  itg2monolem1  21360  itg2monolem2  21361  itg2monolem3  21362  itg2gt0  21370  dvne0  21615  mdegle0  21680  ply1remlem  21766  ply1rem  21767  plypf1  21812  aaliou3lem2  21941  aaliou3lem3  21942  taylfvallem1  21954  taylfval  21956  tayl0  21959  radcnvcl  22014  radcnvle  22017  pserulm  22019  psercnlem1  22022  pilem2  22049  sinhalfpilem  22057  sincosq1lem  22091  sincosq1sgn  22092  sincosq2sgn  22093  tangtx  22099  tanabsge  22100  sinq12gt0  22101  cosq14gt0  22104  sincos4thpi  22107  pige3  22111  cosordlem  22119  tanord1  22125  tanord  22126  efifo  22135  argimgt0  22193  argimlt0  22194  logccv  22240  loglesqr  22328  atantan  22450  rlimcnp  22491  rlimcnp2  22492  scvxcvx  22511  basellem1  22550  dchrisum0lem2a  22898  pntibndlem1  22970  pntibnd  22974  pntlemc  22976  pntlem3  22990  abvcxp  22996  padicabvf  23012  padicabvcxp  23013  ostth2  23018  ttgcontlem1  23282  nmooge0  24318  nmoo0  24342  nmlnogt0  24348  nmopge0  25466  nmopgt0  25467  nmfnge0  25482  nmop0  25541  nmfn0  25542  xraddge02  26200  xlt2addrd  26201  xrge0infss  26203  elxrge02  26251  xrs0  26280  xrge00  26291  xrge0addass  26295  xrge0neqmnf  26296  xrge0addgt0  26298  xrge0adddir  26299  fsumrp0cl  26302  metider  26465  unitssxrge0  26474  xrge0iifcnv  26507  xrge0iifcv  26508  xrge0iifiso  26509  xrge0iifhom  26511  xrge0mulc1cn  26515  pnfneige0  26525  lmxrge0  26526  esumnul  26646  esum0  26647  esumle  26652  esumlef  26657  esumcst  26658  esumsn  26659  esumpr2  26661  esumpinfval  26666  esumpinfsum  26670  esumpcvgval  26671  esumpmono  26672  hashf2  26677  esumcvg  26679  measle0  26766  voliune  26788  volfiniune  26789  ddemeas  26795  aean  26803  oms0  26853  prob01  26939  probmeasb  26956  dstfrvclim1  27003  sgncl  27064  sgn3da  27067  sgn0bi  27073  cvmliftlem10  27326  cvmliftlem13  27328  sinccvglem  27460  sin2h  28569  tan2h  28571  mblfinlem2  28576  ovoliunnfl  28580  voliunnfl  28582  volsupnfl  28583  mbfposadd  28586  itg2addnclem2  28591  itg2gt0cn  28594  ftc1anclem5  28618  ftc1anclem8  28621  dvasin  28627  areacirc  28636  rrnequiv  28881  idomrootle  29707  itgsin0pilem1  29937  stoweidlem46  29988  bj-flbi3  32850