Theorem 0xr 10690

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

Assertion

Ref	Expression
0xr	⊢ 0 ∈ ℝ*

Proof of Theorem 0xr

Step	Hyp	Ref	Expression
1		ressxr 10687	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 10645	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3966	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2114  ℝcr 10538  0cc0 10539  ℝ^*cxr 10676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-1cn 10597  ax-addrcl 10600  ax-rnegex 10610  ax-cnre 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-v 3498  df-un 3943  df-in 3945  df-ss 3954  df-xr 10681

This theorem is referenced by:  0lepnf  12530  ge0gtmnf  12568  max0sub  12592  xlt0neg1  12615  xlt0neg2  12616  xle0neg1  12617  xle0neg2  12618  xaddf  12620  xaddid1  12637  xaddid2  12638  xnn0xadd0  12643  xaddge0  12654  xsubge0  12657  xposdif  12658  xmullem  12660  xmullem2  12661  xmul01  12663  xmul02  12664  xmulneg1  12665  xmulf  12668  xmulpnf1  12670  xmulasslem2  12678  xmulge0  12680  xmulasslem  12681  xlemul1a  12684  xadddi  12691  xadddi2  12693  ioopos  12816  ioorebas  12842  xrge0neqmnf  12843  elxrge0  12848  0e0iccpnf  12850  xov1plusxeqvd  12887  xnn0xrge0  12894  ico01fl0  13192  rpsup  13237  addmodid  13290  hashgt0  13752  hashle00  13764  hashgt0elex  13765  hashgt23el  13788  sgn0  14450  sgnp  14451  sgnn  14455  fprodge0  15349  ef01bndlem  15539  sin01bnd  15540  cos01bnd  15541  cos1bnd  15542  sinltx  15544  sin01gt0  15545  cos01gt0  15546  sin02gt0  15547  sincos1sgn  15548  sincos2sgn  15549  halfleoddlt  15713  xrsmgm  20582  leordtval2  21822  pnfnei  21830  mnfnei  21831  psmetge0  22924  isxmet2d  22939  xmetge0  22956  xmetgt0  22970  prdsdsf  22979  prdsxmetlem  22980  xpsdsval  22993  blgt0  23011  xblss2ps  23013  xblss2  23014  xbln0  23026  prdsbl  23103  stdbdxmet  23127  stdbdmopn  23130  metustto  23165  metustid  23166  metustexhalf  23168  cfilucfil  23171  blval2  23174  metuel2  23177  nmoge0  23332  nmo0  23346  cnblcld  23385  blssioo  23405  blcvx  23408  xrsxmet  23419  metdsf  23458  metds0  23460  metdseq0  23464  metnrmlem1a  23468  iccpnfcnv  23550  iccpnfhmeo  23551  xrhmeo  23552  pcoass  23630  iscfil2  23871  ovolmge0  24080  ovolge0  24084  ovolf  24085  ovolssnul  24090  ovolctb  24093  ovoliunnul  24110  ovolicopnf  24127  voliunlem3  24155  volsup  24159  ioorf  24176  volivth  24210  vitalilem4  24214  vitalilem5  24215  itg2ge0  24338  itg2const2  24344  itg2seq  24345  itg2monolem1  24353  itg2monolem2  24354  itg2monolem3  24355  itg2gt0  24363  dvne0  24610  mdegle0  24673  ply1remlem  24758  ply1rem  24759  plypf1  24804  aaliou3lem2  24934  aaliou3lem3  24935  taylfvallem1  24947  taylfval  24949  tayl0  24952  radcnvcl  25007  radcnvle  25010  pserulm  25012  psercnlem1  25015  pilem2  25042  sinhalfpilem  25051  sincosq1lem  25085  sincosq1sgn  25086  sincosq2sgn  25087  tangtx  25093  tanabsge  25094  sinq12gt0  25095  cosq14gt0  25098  sincos4thpi  25101  pige3ALT  25107  cos02pilt1  25113  cosq34lt1  25114  cosordlem  25117  tanord1  25123  tanord  25124  efifo  25133  argimgt0  25197  argimlt0  25198  logccv  25248  loglesqrt  25341  atantan  25503  rlimcnp  25545  rlimcnp2  25546  scvxcvx  25565  basellem1  25660  dchrisum0lem2a  26095  pntibndlem1  26167  pntibnd  26171  pntlemc  26173  pntlem3  26187  abvcxp  26193  padicabvf  26209  padicabvcxp  26210  ostth2  26215  ttgcontlem1  26673  elntg2  26773  nmooge0  28546  nmoo0  28570  nmlnogt0  28576  nmopge0  29690  nmopgt0  29691  nmfnge0  29706  nmop0  29765  nmfn0  29766  xraddge02  30482  xlt2addrd  30484  xrge0infss  30486  dfrp2  30493  elxrge02  30610  xrs0  30664  xrge00  30675  xrge0addass  30679  xrge0addgt0  30680  xrge0adddir  30681  fsumrp0cl  30684  metider  31136  unitssxrge0  31145  xrge0iifcnv  31178  xrge0iifcv  31179  xrge0iifiso  31180  xrge0iifhom  31182  xrge0mulc1cn  31186  pnfneige0  31196  lmxrge0  31197  esumgsum  31306  esumnul  31309  esum0  31310  esumle  31319  esumlef  31323  esumcst  31324  esumsnf  31325  esumpr2  31328  esumpinfval  31334  esumpinfsum  31338  esumpcvgval  31339  esumpmono  31340  hashf2  31345  esumcvg  31347  measle0  31469  voliune  31490  volfiniune  31491  ddemeas  31497  aean  31505  oms0  31557  prob01  31673  probmeasb  31690  dstfrvclim1  31737  sgncl  31798  sgn3da  31801  signsply0  31823  chtvalz  31902  hgt750lemf  31926  cvmliftlem10  32543  cvmliftlem13  32545  sinccvglem  32917  dnizeq0  33816  sin2h  34884  tan2h  34886  broucube  34928  mblfinlem2  34932  ovoliunnfl  34936  voliunnfl  34938  volsupnfl  34939  mbfposadd  34941  itg2addnclem2  34946  itg2gt0cn  34949  ftc1anclem5  34973  ftc1anclem8  34976  dvasin  34980  areacirc  34989  rrnequiv  35115  idomrootle  39802  imo72b2  40532  absfico  41488  xadd0ge  41595  xrge0nemnfd  41607  xralrple2  41629  xrpnf  41769  pnfel0pnf  41811  ge0xrre  41814  sqrlearg  41836  fsumge0cl  41861  limsup10ex  42061  liminf10ex  42062  sinaover2ne0  42156  itgsin0pilem1  42242  iblsplit  42258  stoweidlem46  42338  fourierdlem43  42442  fourierdlem44  42443  fourierdlem60  42458  fourierdlem61  42459  fourierdlem87  42485  fourierdlem103  42501  fourierdlem104  42502  fourierdlem111  42509  sqwvfourb  42521  fourierswlem  42522  fouriersw  42523  etransclem23  42549  salexct2  42629  fge0npnf  42656  fge0iccico  42659  gsumge0cl  42660  sge0z  42664  sge00  42665  sge0sn  42668  sge0tsms  42669  sge0cl  42670  sge0f1o  42671  sge0ge0  42673  sge0repnf  42675  sge0fsum  42676  sge0pr  42683  sge0ssre  42686  sge0prle  42690  sge0p1  42703  sge0iunmptlemre  42704  sge0rpcpnf  42710  sge0rernmpt  42711  sge0isum  42716  sge0ad2en  42720  sge0xaddlem2  42723  sge0uzfsumgt  42733  sge0seq  42735  sge0reuz  42736  voliunsge0lem  42761  meage0  42764  meassre  42766  meale0eq0  42767  meaiuninclem  42769  omessre  42799  omeiunltfirp  42808  carageniuncllem2  42811  carageniuncl  42812  omege0  42822  omess0  42823  hoiprodcl  42836  ovnlerp  42851  ovnf  42852  ovn0lem  42854  ovnsubaddlem1  42859  hoiprodcl3  42869  hoidmvcl  42871  hoidmv1lelem3  42882  hoidmvlelem5  42888  ovnhoilem1  42890  ovolval5lem1  42941  pimrecltneg  43008  mod42tp1mod8  43774  eenglngeehlnmlem1  44731  eenglngeehlnmlem2  44732  rrxsphere  44742  itscnhlinecirc02p  44779