Theorem 0xr 11151

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 11148	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11106	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3929	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2110  ℝcr 10997  0cc0 10998  ℝ^*cxr 11137

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-1cn 11056  ax-addrcl 11059  ax-rnegex 11069  ax-cnre 11071

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-v 3436  df-un 3905  df-ss 3917  df-xr 11142

This theorem is referenced by:  0lepnf  13024  ge0gtmnf  13063  max0sub  13087  xlt0neg1  13110  xlt0neg2  13111  xle0neg1  13112  xle0neg2  13113  xaddf  13115  xaddrid  13132  xaddlid  13133  xnn0xadd0  13138  xaddge0  13149  xsubge0  13152  xposdif  13153  xmullem  13155  xmullem2  13156  xmul01  13158  xmul02  13159  xmulneg1  13160  xmulf  13163  xmulpnf1  13165  xmulasslem2  13173  xmulge0  13175  xmulasslem  13176  xlemul1a  13179  xadddi  13186  xadddi2  13188  dfrp2  13286  ioopos  13316  ioorebas  13343  xrge0neqmnf  13344  elxrge0  13349  0e0iccpnf  13351  xov1plusxeqvd  13390  xnn0xrge0  13398  ico01fl0  13715  rpsup  13762  addmodid  13818  hashgt0  14287  hashle00  14299  hashgt0elex  14300  hashgt23el  14323  sgn0  14988  sgnp  14989  sgnn  14993  fprodge0  15892  ef01bndlem  16085  sin01bnd  16086  cos01bnd  16087  cos1bnd  16088  sinltx  16090  sin01gt0  16091  cos01gt0  16092  sin02gt0  16093  sincos1sgn  16094  sincos2sgn  16095  halfleoddlt  16265  xrsmgm  21336  leordtval2  23120  pnfnei  23128  mnfnei  23129  psmetge0  24220  isxmet2d  24235  xmetge0  24252  xmetgt0  24266  prdsdsf  24275  prdsxmetlem  24276  xpsdsval  24289  blgt0  24307  xblss2ps  24309  xblss2  24310  xbln0  24322  prdsbl  24399  stdbdxmet  24423  stdbdmopn  24426  metustto  24461  metustid  24462  metustexhalf  24464  cfilucfil  24467  blval2  24470  metuel2  24473  nmoge0  24629  nmo0  24643  cnblcld  24682  blssioo  24703  blcvx  24706  xrsxmet  24718  metdsf  24757  metds0  24759  metdseq0  24763  metnrmlem1a  24767  iccpnfcnv  24862  iccpnfhmeo  24863  xrhmeo  24864  pcoass  24944  iscfil2  25186  ovolmge0  25398  ovolge0  25402  ovolf  25403  ovolssnul  25408  ovolctb  25411  ovoliunnul  25428  ovolicopnf  25445  voliunlem3  25473  volsup  25477  ioorf  25494  volivth  25528  vitalilem4  25532  vitalilem5  25533  itg2ge0  25656  itg2const2  25662  itg2seq  25663  itg2monolem1  25671  itg2monolem2  25672  itg2monolem3  25673  itg2gt0  25681  dvne0  25936  mdegle0  26002  ply1remlem  26090  ply1rem  26091  idomrootle  26098  plypf1  26137  aaliou3lem2  26271  aaliou3lem3  26272  taylfvallem1  26284  taylfval  26286  tayl0  26289  radcnvcl  26346  radcnvle  26349  pserulm  26351  psercnlem1  26355  pilem2  26382  sinhalfpilem  26392  sincosq1lem  26426  sincosq1sgn  26427  sincosq2sgn  26428  tangtx  26434  tanabsge  26435  sinq12gt0  26436  cosq14gt0  26439  sincos4thpi  26442  pige3ALT  26449  cos02pilt1  26455  cosq34lt1  26456  cosordlem  26459  cos0pilt1  26461  tanord1  26466  tanord  26467  efifo  26476  argimgt0  26541  argimlt0  26542  logccv  26592  loglesqrt  26691  atantan  26853  rlimcnp  26895  rlimcnp2  26896  scvxcvx  26916  basellem1  27011  dchrisum0lem2a  27448  pntibndlem1  27520  pntibnd  27524  pntlemc  27526  pntlem3  27540  abvcxp  27546  padicabvf  27562  padicabvcxp  27563  ostth2  27568  ttgcontlem1  28856  elntg2  28956  nmooge0  30737  nmoo0  30761  nmlnogt0  30767  nmopge0  31881  nmopgt0  31882  nmfnge0  31897  nmop0  31956  nmfn0  31957  xraddge02  32730  xlt2addrd  32732  xrge0infss  32733  sgncl  32804  sgn3da  32807  elxrge02  32902  xrs0  32977  xrge00  32985  xrge0addass  32987  xrge0addgt0  32988  xrge0adddir  32989  fsumrp0cl  32992  ply1unit  33528  rtelextdg2lem  33729  metider  33897  unitssxrge0  33903  xrge0iifcnv  33936  xrge0iifcv  33937  xrge0iifiso  33938  xrge0iifhom  33940  xrge0mulc1cn  33944  pnfneige0  33954  lmxrge0  33955  esumgsum  34048  esumnul  34051  esum0  34052  esumle  34061  esumlef  34065  esumcst  34066  esumsnf  34067  esumpr2  34070  esumpinfval  34076  esumpinfsum  34080  esumpcvgval  34081  esumpmono  34082  hashf2  34087  esumcvg  34089  measle0  34211  voliune  34232  volfiniune  34233  ddemeas  34239  aean  34247  oms0  34300  prob01  34416  probmeasb  34433  dstfrvclim1  34481  signsply0  34554  chtvalz  34632  hgt750lemf  34656  cvmliftlem10  35306  cvmliftlem13  35308  sinccvglem  35684  dnizeq0  36488  iccioo01  37340  sin2h  37629  tan2h  37631  broucube  37673  mblfinlem2  37677  ovoliunnfl  37681  voliunnfl  37683  volsupnfl  37684  mbfposadd  37686  itg2addnclem2  37691  itg2gt0cn  37694  ftc1anclem5  37716  ftc1anclem8  37719  dvasin  37723  areacirc  37732  rrnequiv  37854  dvrelog2b  42078  aks6d1c5lem3  42149  aks6d1c6lem1  42182  acos1half  42370  redvmptabs  42372  readvrec2  42373  readvrec  42374  imo72b2  44184  absfico  45234  xadd0ge  45339  xrge0nemnfd  45350  xralrple2  45372  xrpnf  45502  pnfel0pnf  45547  ge0xrre  45550  sqrlearg  45572  fsumge0cl  45592  limsup10ex  45790  liminf10ex  45791  sinaover2ne0  45885  itgsin0pilem1  45967  iblsplit  45983  stoweidlem46  46063  fourierdlem43  46167  fourierdlem44  46168  fourierdlem60  46183  fourierdlem61  46184  fourierdlem87  46210  fourierdlem103  46226  fourierdlem104  46227  fourierdlem111  46234  sqwvfourb  46246  fourierswlem  46247  fouriersw  46248  etransclem23  46274  salexct2  46356  fge0npnf  46384  fge0iccico  46387  gsumge0cl  46388  sge0z  46392  sge00  46393  sge0sn  46396  sge0tsms  46397  sge0cl  46398  sge0f1o  46399  sge0ge0  46401  sge0repnf  46403  sge0fsum  46404  sge0pr  46411  sge0ssre  46414  sge0prle  46418  sge0p1  46431  sge0iunmptlemre  46432  sge0rpcpnf  46438  sge0rernmpt  46439  sge0isum  46444  sge0ad2en  46448  sge0xaddlem2  46451  sge0uzfsumgt  46461  sge0seq  46463  sge0reuz  46464  voliunsge0lem  46489  meage0  46492  meassre  46494  meale0eq0  46495  meaiuninclem  46497  omessre  46527  omeiunltfirp  46536  carageniuncllem2  46539  carageniuncl  46540  omege0  46550  omess0  46551  hoiprodcl  46564  ovnlerp  46579  ovnf  46580  ovn0lem  46582  ovnsubaddlem1  46587  hoiprodcl3  46597  hoidmvcl  46599  hoidmv1lelem3  46610  hoidmvlelem5  46616  ovnhoilem1  46618  ovolval5lem1  46669  pimrecltneg  46741  rehalfge1  47345  mod42tp1mod8  47612  eenglngeehlnmlem1  48748  eenglngeehlnmlem2  48749  rrxsphere  48759  itscnhlinecirc02p  48796  iooii  48928  io1ii  48931  sepfsepc  48938  seppcld  48940