Theorem 0xr 11356

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 11353	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11310	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3905	1 ⊢ 0 ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2144  ℝcr 11199  0cc0 11200  ℝ^*cxr 11342

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11258  ax-addrcl 11261  ax-rnegex 11271  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-ss 3896  df-un 4151  df-xr 11347

This theorem is used by:  0lepnf  13262  ge0gtmnf  13302  max0sub  13326  xlt0neg1  13349  xlt0neg2  13350  xle0neg1  13351  xle0neg2  13352  xaddf  13354  xaddrid  13371  xaddlid  13372  xnn0xadd0  13377  xaddge0  13388  xsubge0  13391  xposdif  13392  xmullem  13394  xmullem2  13395  xmul01  13397  xmul02  13398  xmulneg1  13399  xmulf  13402  xmulpnf1  13404  xmulasslem2  13412  xmulge0  13414  xmulasslem  13415  xlemul1a  13418  xadddi  13425  xadddi2  13427  dfrp2  13525  ioopos  13555  ioorebas  13582  xrge0neqmnf  13583  elxrge0  13588  0e0iccpnf  13590  xov1plusxeqvd  13629  xnn0xrge0  13637  ico01fl0  13959  rpsup  14006  addmodid  14062  hashgt0  14532  hashle00  14544  hashgt0elex  14545  hashgt23el  14569  sgn0  15242  sgnp  15243  sgnn  15247  sgncl  15250  sgnrn  15251  sgn3da  15254  fprodge0  16160  ef01bndlem  16352  sin01bnd  16353  cos01bnd  16354  cos1bnd  16355  sinltx  16357  sin01gt0  16358  cos01gt0  16359  sin02gt0  16360  sincos1sgn  16361  sincos2sgn  16362  halfleoddlt  16532  xrsmgm  21713  leordtval2  23530  pnfnei  23538  mnfnei  23539  psmetge0  24631  isxmet2d  24646  xmetge0  24663  xmetgt0  24677  prdsdsf  24686  prdsxmetlem  24687  xpsdsval  24700  blgt0  24718  xblss2ps  24720  xblss2  24721  xbln0  24733  prdsbl  24810  stdbdxmet  24834  stdbdmopn  24837  metustto  24872  metustid  24873  metustexhalf  24875  cfilucfil  24878  blval2  24881  metuel2  24884  nmoge0  25040  nmo0  25054  cnblcld  25093  blssioo  25114  blcvx  25117  xrsxmet  25129  metdsf  25168  metds0  25170  metdseq0  25174  metnrmlem1a  25178  iccpnfcnv  25265  iccpnfhmeo  25266  xrhmeo  25267  pcoass  25345  iscfil2  25587  ovolmge0  25798  ovolge0  25802  ovolf  25803  ovolssnul  25808  ovolctb  25811  ovoliunnul  25828  ovolicopnf  25845  voliunlem3  25873  volsup  25877  ioorf  25894  volivth  25928  vitalilem4  25932  vitalilem5  25933  itg2ge0  26056  itg2const2  26062  itg2seq  26063  itg2monolem1  26071  itg2monolem2  26072  itg2monolem3  26073  itg2gt0  26081  dvne0  26331  mdegle0  26395  ply1remlem  26483  ply1rem  26484  idomrootle  26491  plypf1  26531  aaliou3lem2  26670  aaliou3lem3  26671  taylfvallem1  26684  taylfval  26686  tayl0  26689  radcnvcl  26744  radcnvle  26747  pserulm  26749  psercnlem1  26752  pilem2  26779  sinhalfpilem  26792  sincosq1lem  26826  sincosq1sgn  26827  sincosq2sgn  26828  tangtx  26834  tanabsge  26835  sinq12gt0  26836  cosq14gt0  26839  sincos4thpi  26842  pige3ALT  26848  cos02pilt1  26854  cosq34lt1  26855  cosordlem  26858  cos0pilt1  26860  tanord1  26865  tanord  26866  efifo  26875  argimgt0  26940  argimlt0  26941  logccv  26991  loglesqrt  27089  atantan  27251  rlimcnp  27293  rlimcnp2  27294  scvxcvx  27313  basellem1  27408  dchrisum0lem2a  27844  pntibndlem1  27916  pntibnd  27920  pntlemc  27922  pntlem3  27936  abvcxp  27942  padicabvf  27958  padicabvcxp  27959  ostth2  27964  ttgcontlem1  29462  elntg2  29563  nmooge0  31369  nmoo0  31393  nmlnogt0  31399  nmopge0  32513  nmopgt0  32514  nmfnge0  32529  nmop0  32588  nmfn0  32589  xraddge02  33391  xlt2addrd  33393  xrge0infss  33394  elxrge02  33540  xrs0  33609  xrge00  33617  xrge0addass  33619  xrge0addgt0  33620  xrge0adddir  33621  fsumrp0cl  33624  ply1unit  34149  vietadeg1  34252  rtelextdg2lem  34400  metider  34568  unitssxrge0  34574  xrge0iifcnv  34607  xrge0iifcv  34608  xrge0iifiso  34609  xrge0iifhom  34611  xrge0mulc1cn  34615  pnfneige0  34625  lmxrge0  34626  esumgsum  34719  esumnul  34722  esum0  34723  esumle  34732  esumlef  34736  esumcst  34737  esumsnf  34738  esumpr2  34741  esumpinfval  34747  esumpinfsum  34751  esumpcvgval  34752  esumpmono  34753  hashf2  34758  esumcvg  34760  measle0  34883  voliune  34904  volfiniune  34905  ddemeas  34911  aean  34919  oms0  34971  prob01  35087  probmeasb  35104  dstfrvclim1  35152  signsply0  35222  chtvalz  35300  hgt750lemf  35324  cvmliftlem10  36101  cvmliftlem13  36103  sinccvglem  36479  dnizeq0  37383  iccioo01  38293  sin2h  38576  tan2h  38578  broucube  38615  mblfinlem2  38619  ovoliunnfl  38623  voliunnfl  38625  volsupnfl  38626  mbfposadd  38628  itg2addnclem2  38633  itg2gt0cn  38636  ftc1anclem5  38658  ftc1anclem8  38661  dvasin  38665  areacirc  38674  rrnequiv  38812  dvrelog2b  43159  aks6d1c5lem3  43230  aks6d1c6lem1  43263  acos1half  43452  redvmptabs  43454  readvrec2  43455  readvrec  43456  imo72b2  45215  absfico  46274  xadd0ge  46377  xrge0nemnfd  46387  xralrple2  46409  xrpnf  46538  pnfel0pnf  46583  ge0xrre  46586  sqrlearg  46608  fsumge0cl  46628  limsup10ex  46826  liminf10ex  46827  sinaover2ne0  46921  itgsin0pilem1  47003  iblsplit  47019  stoweidlem46  47099  fourierdlem43  47203  fourierdlem44  47204  fourierdlem60  47219  fourierdlem61  47220  fourierdlem87  47246  fourierdlem103  47262  fourierdlem104  47263  fourierdlem111  47270  sqwvfourb  47282  fourierswlem  47283  fouriersw  47284  etransclem23  47310  salexct2  47392  fge0npnf  47420  fge0iccico  47423  gsumge0cl  47424  sge0z  47428  sge00  47429  sge0sn  47432  sge0tsms  47433  sge0cl  47434  sge0f1o  47435  sge0ge0  47437  sge0repnf  47439  sge0fsum  47440  sge0pr  47447  sge0ssre  47450  sge0prle  47454  sge0p1  47467  sge0iunmptlemre  47468  sge0rpcpnf  47474  sge0rernmpt  47475  sge0isum  47480  sge0ad2en  47484  sge0xaddlem2  47487  sge0uzfsumgt  47497  sge0seq  47499  sge0reuz  47500  voliunsge0lem  47525  meage0  47528  meassre  47530  meale0eq0  47531  meaiuninclem  47533  omessre  47563  omeiunltfirp  47572  carageniuncllem2  47575  carageniuncl  47576  omege0  47586  omess0  47587  hoiprodcl  47600  ovnlerp  47615  ovnf  47616  ovn0lem  47618  ovnsubaddlem1  47623  hoiprodcl3  47633  hoidmvcl  47635  hoidmv1lelem3  47646  hoidmvlelem5  47652  ovnhoilem1  47654  ovolval5lem1  47705  pimrecltneg  47777  rehalfge1  48452  mod42tp1mod8  48730  eenglngeehlnmlem1  49892  eenglngeehlnmlem2  49893  rrxsphere  49903  itscnhlinecirc02p  49940  iooii  50069  io1ii  50072  sepfsepc  50079  seppcld  50081