Theorem 0xr 10374

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 10371	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 10330	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3802	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2157  ℝcr 10223  0cc0 10224  ℝ^*cxr 10361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-i2m1 10292  ax-1ne0 10293  ax-rnegex 10295  ax-rrecex 10296  ax-cnre 10297

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-iota 6067  df-fv 6112  df-ov 6880  df-xr 10366

This theorem is referenced by:  0lepnf  12185  ge0gtmnf  12224  max0sub  12248  xlt0neg1  12271  xlt0neg2  12272  xle0neg1  12273  xle0neg2  12274  xaddf  12276  xaddid1  12293  xaddid2  12294  xnn0xadd0  12298  xaddge0  12309  xsubge0  12312  xposdif  12313  xmullem  12315  xmullem2  12316  xmul01  12318  xmul02  12319  xmulneg1  12320  xmulf  12323  xmulpnf1  12325  xmulasslem2  12333  xmulge0  12335  xmulasslem  12336  xlemul1a  12339  xadddi  12346  xadddi2  12348  ioopos  12471  ioorebas  12497  xrge0neqmnf  12498  xrge0neqmnfOLD  12499  elxrge0  12504  0e0iccpnf  12506  xov1plusxeqvd  12544  xnn0xrge0  12551  ico01fl0  12847  rpsup  12892  addmodid  12945  hashgt0  13398  hashle00  13408  hashgt0elex  13409  sgn0  14055  sgnp  14056  sgnn  14060  fprodge0  14947  ef01bndlem  15137  sin01bnd  15138  cos01bnd  15139  cos1bnd  15140  sinltx  15142  sin01gt0  15143  cos01gt0  15144  sin02gt0  15145  sincos1sgn  15146  sincos2sgn  15147  halfleoddlt  15309  xrsmgm  19992  leordtval2  21234  pnfnei  21242  mnfnei  21243  psmetge0  22334  isxmet2d  22349  xmetge0  22366  xmetgt0  22380  prdsdsf  22389  prdsxmetlem  22390  xpsdsval  22403  blgt0  22421  xblss2ps  22423  xblss2  22424  xbln0  22436  prdsbl  22513  stdbdxmet  22537  stdbdmopn  22540  metustto  22575  metustid  22576  metustexhalf  22578  cfilucfil  22581  blval2  22584  metuel2  22587  nmoge0  22742  nmo0  22756  cnblcld  22795  blssioo  22815  blcvx  22818  xrsxmet  22829  metdsf  22868  metds0  22870  metdseq0  22874  metnrmlem1a  22878  iccpnfcnv  22960  iccpnfhmeo  22961  xrhmeo  22962  pcoass  23040  iscfil2  23281  ovolmge0  23464  ovolge0  23468  ovolf  23469  ovolssnul  23474  ovolctb  23477  ovoliunnul  23494  ovolicopnf  23511  voliunlem3  23539  volsup  23543  ioorf  23560  volivth  23594  vitalilem4  23598  vitalilem5  23599  itg2ge0  23722  itg2const2  23728  itg2seq  23729  itg2monolem1  23737  itg2monolem2  23738  itg2monolem3  23739  itg2gt0  23747  dvne0  23994  mdegle0  24057  ply1remlem  24142  ply1rem  24143  plypf1  24188  aaliou3lem2  24318  aaliou3lem3  24319  taylfvallem1  24331  taylfval  24333  tayl0  24336  radcnvcl  24391  radcnvle  24394  pserulm  24396  psercnlem1  24399  pilem2  24426  sinhalfpilem  24436  sincosq1lem  24470  sincosq1sgn  24471  sincosq2sgn  24472  tangtx  24478  tanabsge  24479  sinq12gt0  24480  cosq14gt0  24483  sincos4thpi  24486  pige3  24490  cosordlem  24498  tanord1  24504  tanord  24505  efifo  24514  argimgt0  24578  argimlt0  24579  logccv  24629  loglesqrt  24719  atantan  24870  rlimcnp  24912  rlimcnp2  24913  scvxcvx  24932  basellem1  25027  dchrisum0lem2a  25426  pntibndlem1  25498  pntibnd  25502  pntlemc  25504  pntlem3  25518  abvcxp  25524  padicabvf  25540  padicabvcxp  25541  ostth2  25546  ttgcontlem1  25985  nmooge0  27956  nmoo0  27980  nmlnogt0  27986  nmopge0  29104  nmopgt0  29105  nmfnge0  29120  nmop0  29179  nmfn0  29180  xraddge02  29854  xlt2addrd  29856  xrge0infss  29858  dfrp2  29865  elxrge02  29971  xrs0  30006  xrge00  30017  xrge0addass  30021  xrge0addgt0  30022  xrge0adddir  30023  fsumrp0cl  30026  metider  30268  unitssxrge0  30277  xrge0iifcnv  30310  xrge0iifcv  30311  xrge0iifiso  30312  xrge0iifhom  30314  xrge0mulc1cn  30318  pnfneige0  30328  lmxrge0  30329  esumgsum  30438  esumnul  30441  esum0  30442  esumle  30451  esumlef  30455  esumcst  30456  esumsnf  30457  esumpr2  30460  esumpinfval  30466  esumpinfsum  30470  esumpcvgval  30471  esumpmono  30472  hashf2  30477  esumcvg  30479  measle0  30602  voliune  30623  volfiniune  30624  ddemeas  30630  aean  30638  oms0  30690  prob01  30806  probmeasb  30823  dstfrvclim1  30870  sgncl  30931  sgn3da  30934  signsply0  30959  chtvalz  31038  hgt750lemf  31062  cvmliftlem10  31604  cvmliftlem13  31606  sinccvglem  31893  dnizeq0  32787  sin2h  33714  tan2h  33716  broucube  33758  mblfinlem2  33762  ovoliunnfl  33766  voliunnfl  33768  volsupnfl  33769  mbfposadd  33771  itg2addnclem2  33776  itg2gt0cn  33779  ftc1anclem5  33803  ftc1anclem8  33806  dvasin  33810  areacirc  33819  rrnequiv  33947  idomrootle  38275  imo72b2  38976  absfico  39898  xadd0ge  40017  xrge0nemnfd  40029  xralrple2  40051  xrpnf  40196  pnfel0pnf  40236  ge0xrre  40239  sqrlearg  40261  fsumge0cl  40286  limsup10ex  40486  liminf10ex  40487  sinaover2ne0  40560  itgsin0pilem1  40646  iblsplit  40662  stoweidlem46  40743  fourierdlem43  40847  fourierdlem44  40848  fourierdlem60  40863  fourierdlem61  40864  fourierdlem87  40890  fourierdlem103  40906  fourierdlem104  40907  fourierdlem111  40914  sqwvfourb  40926  fourierswlem  40927  fouriersw  40928  etransclem23  40954  salexct2  41037  fge0npnf  41064  fge0iccico  41067  gsumge0cl  41068  sge0z  41072  sge00  41073  sge0sn  41076  sge0tsms  41077  sge0cl  41078  sge0f1o  41079  sge0ge0  41081  sge0repnf  41083  sge0fsum  41084  sge0pr  41091  sge0ssre  41094  sge0prle  41098  sge0p1  41111  sge0iunmptlemre  41112  sge0rpcpnf  41118  sge0rernmpt  41119  sge0isum  41124  sge0ad2en  41128  sge0xaddlem2  41131  sge0uzfsumgt  41141  sge0seq  41143  sge0reuz  41144  voliunsge0lem  41169  meage0  41172  meassre  41174  meale0eq0  41175  meaiuninclem  41177  omessre  41207  omeiunltfirp  41216  carageniuncllem2  41219  carageniuncl  41220  omege0  41230  omess0  41231  hoiprodcl  41244  ovnlerp  41259  ovnf  41260  ovn0lem  41262  ovnsubaddlem1  41267  hoiprodcl3  41277  hoidmvcl  41279  hoidmv1lelem3  41290  hoidmvlelem5  41296  ovnhoilem1  41298  ovolval5lem1  41349  pimrecltneg  41416  mod42tp1mod8  42095