Theorem 0xr 11183

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 11180	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11138	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3931	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2114  ℝcr 11029  0cc0 11030  ℝ^*cxr 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11088  ax-addrcl 11091  ax-rnegex 11101  ax-cnre 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3062  df-v 3443  df-un 3907  df-ss 3919  df-xr 11174

This theorem is referenced by:  0lepnf  13051  ge0gtmnf  13091  max0sub  13115  xlt0neg1  13138  xlt0neg2  13139  xle0neg1  13140  xle0neg2  13141  xaddf  13143  xaddrid  13160  xaddlid  13161  xnn0xadd0  13166  xaddge0  13177  xsubge0  13180  xposdif  13181  xmullem  13183  xmullem2  13184  xmul01  13186  xmul02  13187  xmulneg1  13188  xmulf  13191  xmulpnf1  13193  xmulasslem2  13201  xmulge0  13203  xmulasslem  13204  xlemul1a  13207  xadddi  13214  xadddi2  13216  dfrp2  13314  ioopos  13344  ioorebas  13371  xrge0neqmnf  13372  elxrge0  13377  0e0iccpnf  13379  xov1plusxeqvd  13418  xnn0xrge0  13426  ico01fl0  13743  rpsup  13790  addmodid  13846  hashgt0  14315  hashle00  14327  hashgt0elex  14328  hashgt23el  14351  sgn0  15016  sgnp  15017  sgnn  15021  fprodge0  15920  ef01bndlem  16113  sin01bnd  16114  cos01bnd  16115  cos1bnd  16116  sinltx  16118  sin01gt0  16119  cos01gt0  16120  sin02gt0  16121  sincos1sgn  16122  sincos2sgn  16123  halfleoddlt  16293  xrsmgm  21365  leordtval2  23160  pnfnei  23168  mnfnei  23169  psmetge0  24260  isxmet2d  24275  xmetge0  24292  xmetgt0  24306  prdsdsf  24315  prdsxmetlem  24316  xpsdsval  24329  blgt0  24347  xblss2ps  24349  xblss2  24350  xbln0  24362  prdsbl  24439  stdbdxmet  24463  stdbdmopn  24466  metustto  24501  metustid  24502  metustexhalf  24504  cfilucfil  24507  blval2  24510  metuel2  24513  nmoge0  24669  nmo0  24683  cnblcld  24722  blssioo  24743  blcvx  24746  xrsxmet  24758  metdsf  24797  metds0  24799  metdseq0  24803  metnrmlem1a  24807  iccpnfcnv  24902  iccpnfhmeo  24903  xrhmeo  24904  pcoass  24984  iscfil2  25226  ovolmge0  25438  ovolge0  25442  ovolf  25443  ovolssnul  25448  ovolctb  25451  ovoliunnul  25468  ovolicopnf  25485  voliunlem3  25513  volsup  25517  ioorf  25534  volivth  25568  vitalilem4  25572  vitalilem5  25573  itg2ge0  25696  itg2const2  25702  itg2seq  25703  itg2monolem1  25711  itg2monolem2  25712  itg2monolem3  25713  itg2gt0  25721  dvne0  25976  mdegle0  26042  ply1remlem  26130  ply1rem  26131  idomrootle  26138  plypf1  26177  aaliou3lem2  26311  aaliou3lem3  26312  taylfvallem1  26324  taylfval  26326  tayl0  26329  radcnvcl  26386  radcnvle  26389  pserulm  26391  psercnlem1  26395  pilem2  26422  sinhalfpilem  26432  sincosq1lem  26466  sincosq1sgn  26467  sincosq2sgn  26468  tangtx  26474  tanabsge  26475  sinq12gt0  26476  cosq14gt0  26479  sincos4thpi  26482  pige3ALT  26489  cos02pilt1  26495  cosq34lt1  26496  cosordlem  26499  cos0pilt1  26501  tanord1  26506  tanord  26507  efifo  26516  argimgt0  26581  argimlt0  26582  logccv  26632  loglesqrt  26731  atantan  26893  rlimcnp  26935  rlimcnp2  26936  scvxcvx  26956  basellem1  27051  dchrisum0lem2a  27488  pntibndlem1  27560  pntibnd  27564  pntlemc  27566  pntlem3  27580  abvcxp  27586  padicabvf  27602  padicabvcxp  27603  ostth2  27608  ttgcontlem1  28940  elntg2  29041  nmooge0  30825  nmoo0  30849  nmlnogt0  30855  nmopge0  31969  nmopgt0  31970  nmfnge0  31985  nmop0  32044  nmfn0  32045  xraddge02  32818  xlt2addrd  32820  xrge0infss  32821  sgncl  32893  sgn3da  32896  elxrge02  32994  xrs0  33069  xrge00  33077  xrge0addass  33079  xrge0addgt0  33080  xrge0adddir  33081  fsumrp0cl  33084  ply1unit  33637  vietadeg1  33715  rtelextdg2lem  33864  metider  34032  unitssxrge0  34038  xrge0iifcnv  34071  xrge0iifcv  34072  xrge0iifiso  34073  xrge0iifhom  34075  xrge0mulc1cn  34079  pnfneige0  34089  lmxrge0  34090  esumgsum  34183  esumnul  34186  esum0  34187  esumle  34196  esumlef  34200  esumcst  34201  esumsnf  34202  esumpr2  34205  esumpinfval  34211  esumpinfsum  34215  esumpcvgval  34216  esumpmono  34217  hashf2  34222  esumcvg  34224  measle0  34346  voliune  34367  volfiniune  34368  ddemeas  34374  aean  34382  oms0  34435  prob01  34551  probmeasb  34568  dstfrvclim1  34616  signsply0  34689  chtvalz  34767  hgt750lemf  34791  cvmliftlem10  35469  cvmliftlem13  35471  sinccvglem  35847  dnizeq0  36650  iccioo01  37503  sin2h  37782  tan2h  37784  broucube  37826  mblfinlem2  37830  ovoliunnfl  37834  voliunnfl  37836  volsupnfl  37837  mbfposadd  37839  itg2addnclem2  37844  itg2gt0cn  37847  ftc1anclem5  37869  ftc1anclem8  37872  dvasin  37876  areacirc  37885  rrnequiv  38007  dvrelog2b  42357  aks6d1c5lem3  42428  aks6d1c6lem1  42461  acos1half  42649  redvmptabs  42651  readvrec2  42652  readvrec  42653  imo72b2  44449  absfico  45498  xadd0ge  45603  xrge0nemnfd  45613  xralrple2  45635  xrpnf  45765  pnfel0pnf  45810  ge0xrre  45813  sqrlearg  45835  fsumge0cl  45855  limsup10ex  46053  liminf10ex  46054  sinaover2ne0  46148  itgsin0pilem1  46230  iblsplit  46246  stoweidlem46  46326  fourierdlem43  46430  fourierdlem44  46431  fourierdlem60  46446  fourierdlem61  46447  fourierdlem87  46473  fourierdlem103  46489  fourierdlem104  46490  fourierdlem111  46497  sqwvfourb  46509  fourierswlem  46510  fouriersw  46511  etransclem23  46537  salexct2  46619  fge0npnf  46647  fge0iccico  46650  gsumge0cl  46651  sge0z  46655  sge00  46656  sge0sn  46659  sge0tsms  46660  sge0cl  46661  sge0f1o  46662  sge0ge0  46664  sge0repnf  46666  sge0fsum  46667  sge0pr  46674  sge0ssre  46677  sge0prle  46681  sge0p1  46694  sge0iunmptlemre  46695  sge0rpcpnf  46701  sge0rernmpt  46702  sge0isum  46707  sge0ad2en  46711  sge0xaddlem2  46714  sge0uzfsumgt  46724  sge0seq  46726  sge0reuz  46727  voliunsge0lem  46752  meage0  46755  meassre  46757  meale0eq0  46758  meaiuninclem  46760  omessre  46790  omeiunltfirp  46799  carageniuncllem2  46802  carageniuncl  46803  omege0  46813  omess0  46814  hoiprodcl  46827  ovnlerp  46842  ovnf  46843  ovn0lem  46845  ovnsubaddlem1  46850  hoiprodcl3  46860  hoidmvcl  46862  hoidmv1lelem3  46873  hoidmvlelem5  46879  ovnhoilem1  46881  ovolval5lem1  46932  pimrecltneg  47004  rehalfge1  47617  mod42tp1mod8  47884  eenglngeehlnmlem1  49019  eenglngeehlnmlem2  49020  rrxsphere  49030  itscnhlinecirc02p  49067  iooii  49199  io1ii  49202  sepfsepc  49209  seppcld  49211