Theorem 0xr 11184

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

Syntax hints:   ∈ wcel 2114  ℝcr 11030  0cc0 11031  ℝ^*cxr 11170

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 11089  ax-addrcl 11092  ax-rnegex 11102  ax-cnre 11104

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 11175

This theorem is referenced by:  0lepnf  13052  ge0gtmnf  13092  max0sub  13116  xlt0neg1  13139  xlt0neg2  13140  xle0neg1  13141  xle0neg2  13142  xaddf  13144  xaddrid  13161  xaddlid  13162  xnn0xadd0  13167  xaddge0  13178  xsubge0  13181  xposdif  13182  xmullem  13184  xmullem2  13185  xmul01  13187  xmul02  13188  xmulneg1  13189  xmulf  13192  xmulpnf1  13194  xmulasslem2  13202  xmulge0  13204  xmulasslem  13205  xlemul1a  13208  xadddi  13215  xadddi2  13217  dfrp2  13315  ioopos  13345  ioorebas  13372  xrge0neqmnf  13373  elxrge0  13378  0e0iccpnf  13380  xov1plusxeqvd  13419  xnn0xrge0  13427  ico01fl0  13744  rpsup  13791  addmodid  13847  hashgt0  14316  hashle00  14328  hashgt0elex  14329  hashgt23el  14352  sgn0  15017  sgnp  15018  sgnn  15022  fprodge0  15921  ef01bndlem  16114  sin01bnd  16115  cos01bnd  16116  cos1bnd  16117  sinltx  16119  sin01gt0  16120  cos01gt0  16121  sin02gt0  16122  sincos1sgn  16123  sincos2sgn  16124  halfleoddlt  16294  xrsmgm  21366  leordtval2  23161  pnfnei  23169  mnfnei  23170  psmetge0  24261  isxmet2d  24276  xmetge0  24293  xmetgt0  24307  prdsdsf  24316  prdsxmetlem  24317  xpsdsval  24330  blgt0  24348  xblss2ps  24350  xblss2  24351  xbln0  24363  prdsbl  24440  stdbdxmet  24464  stdbdmopn  24467  metustto  24502  metustid  24503  metustexhalf  24505  cfilucfil  24508  blval2  24511  metuel2  24514  nmoge0  24670  nmo0  24684  cnblcld  24723  blssioo  24744  blcvx  24747  xrsxmet  24759  metdsf  24798  metds0  24800  metdseq0  24804  metnrmlem1a  24808  iccpnfcnv  24903  iccpnfhmeo  24904  xrhmeo  24905  pcoass  24985  iscfil2  25227  ovolmge0  25439  ovolge0  25443  ovolf  25444  ovolssnul  25449  ovolctb  25452  ovoliunnul  25469  ovolicopnf  25486  voliunlem3  25514  volsup  25518  ioorf  25535  volivth  25569  vitalilem4  25573  vitalilem5  25574  itg2ge0  25697  itg2const2  25703  itg2seq  25704  itg2monolem1  25712  itg2monolem2  25713  itg2monolem3  25714  itg2gt0  25722  dvne0  25977  mdegle0  26043  ply1remlem  26131  ply1rem  26132  idomrootle  26139  plypf1  26178  aaliou3lem2  26312  aaliou3lem3  26313  taylfvallem1  26325  taylfval  26327  tayl0  26330  radcnvcl  26387  radcnvle  26390  pserulm  26392  psercnlem1  26396  pilem2  26423  sinhalfpilem  26433  sincosq1lem  26467  sincosq1sgn  26468  sincosq2sgn  26469  tangtx  26475  tanabsge  26476  sinq12gt0  26477  cosq14gt0  26480  sincos4thpi  26483  pige3ALT  26490  cos02pilt1  26496  cosq34lt1  26497  cosordlem  26500  cos0pilt1  26502  tanord1  26507  tanord  26508  efifo  26517  argimgt0  26582  argimlt0  26583  logccv  26633  loglesqrt  26732  atantan  26894  rlimcnp  26936  rlimcnp2  26937  scvxcvx  26957  basellem1  27052  dchrisum0lem2a  27489  pntibndlem1  27561  pntibnd  27565  pntlemc  27567  pntlem3  27581  abvcxp  27587  padicabvf  27603  padicabvcxp  27604  ostth2  27609  ttgcontlem1  28962  elntg2  29063  nmooge0  30847  nmoo0  30871  nmlnogt0  30877  nmopge0  31991  nmopgt0  31992  nmfnge0  32007  nmop0  32066  nmfn0  32067  xraddge02  32840  xlt2addrd  32842  xrge0infss  32843  sgncl  32915  sgn3da  32918  elxrge02  33016  xrs0  33091  xrge00  33099  xrge0addass  33101  xrge0addgt0  33102  xrge0adddir  33103  fsumrp0cl  33106  ply1unit  33660  vietadeg1  33747  rtelextdg2lem  33896  metider  34064  unitssxrge0  34070  xrge0iifcnv  34103  xrge0iifcv  34104  xrge0iifiso  34105  xrge0iifhom  34107  xrge0mulc1cn  34111  pnfneige0  34121  lmxrge0  34122  esumgsum  34215  esumnul  34218  esum0  34219  esumle  34228  esumlef  34232  esumcst  34233  esumsnf  34234  esumpr2  34237  esumpinfval  34243  esumpinfsum  34247  esumpcvgval  34248  esumpmono  34249  hashf2  34254  esumcvg  34256  measle0  34378  voliune  34399  volfiniune  34400  ddemeas  34406  aean  34414  oms0  34467  prob01  34583  probmeasb  34600  dstfrvclim1  34648  signsply0  34721  chtvalz  34799  hgt750lemf  34823  cvmliftlem10  35501  cvmliftlem13  35503  sinccvglem  35879  dnizeq0  36688  iccioo01  37545  sin2h  37824  tan2h  37826  broucube  37868  mblfinlem2  37872  ovoliunnfl  37876  voliunnfl  37878  volsupnfl  37879  mbfposadd  37881  itg2addnclem2  37886  itg2gt0cn  37889  ftc1anclem5  37911  ftc1anclem8  37914  dvasin  37918  areacirc  37927  rrnequiv  38049  dvrelog2b  42399  aks6d1c5lem3  42470  aks6d1c6lem1  42503  acos1half  42691  redvmptabs  42693  readvrec2  42694  readvrec  42695  imo72b2  44491  absfico  45539  xadd0ge  45644  xrge0nemnfd  45654  xralrple2  45676  xrpnf  45806  pnfel0pnf  45851  ge0xrre  45854  sqrlearg  45876  fsumge0cl  45896  limsup10ex  46094  liminf10ex  46095  sinaover2ne0  46189  itgsin0pilem1  46271  iblsplit  46287  stoweidlem46  46367  fourierdlem43  46471  fourierdlem44  46472  fourierdlem60  46487  fourierdlem61  46488  fourierdlem87  46514  fourierdlem103  46530  fourierdlem104  46531  fourierdlem111  46538  sqwvfourb  46550  fourierswlem  46551  fouriersw  46552  etransclem23  46578  salexct2  46660  fge0npnf  46688  fge0iccico  46691  gsumge0cl  46692  sge0z  46696  sge00  46697  sge0sn  46700  sge0tsms  46701  sge0cl  46702  sge0f1o  46703  sge0ge0  46705  sge0repnf  46707  sge0fsum  46708  sge0pr  46715  sge0ssre  46718  sge0prle  46722  sge0p1  46735  sge0iunmptlemre  46736  sge0rpcpnf  46742  sge0rernmpt  46743  sge0isum  46748  sge0ad2en  46752  sge0xaddlem2  46755  sge0uzfsumgt  46765  sge0seq  46767  sge0reuz  46768  voliunsge0lem  46793  meage0  46796  meassre  46798  meale0eq0  46799  meaiuninclem  46801  omessre  46831  omeiunltfirp  46840  carageniuncllem2  46843  carageniuncl  46844  omege0  46854  omess0  46855  hoiprodcl  46868  ovnlerp  46883  ovnf  46884  ovn0lem  46886  ovnsubaddlem1  46891  hoiprodcl3  46901  hoidmvcl  46903  hoidmv1lelem3  46914  hoidmvlelem5  46920  ovnhoilem1  46922  ovolval5lem1  46973  pimrecltneg  47045  rehalfge1  47658  mod42tp1mod8  47925  eenglngeehlnmlem1  49060  eenglngeehlnmlem2  49061  rrxsphere  49071  itscnhlinecirc02p  49108  iooii  49240  io1ii  49243  sepfsepc  49250  seppcld  49252