Theorem 0xr 11280

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 11277	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11235	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3955	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2108  ℝcr 11126  0cc0 11127  ℝ^*cxr 11266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-addrcl 11188  ax-rnegex 11198  ax-cnre 11200

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-v 3461  df-un 3931  df-ss 3943  df-xr 11271

This theorem is referenced by:  0lepnf  13147  ge0gtmnf  13186  max0sub  13210  xlt0neg1  13233  xlt0neg2  13234  xle0neg1  13235  xle0neg2  13236  xaddf  13238  xaddrid  13255  xaddlid  13256  xnn0xadd0  13261  xaddge0  13272  xsubge0  13275  xposdif  13276  xmullem  13278  xmullem2  13279  xmul01  13281  xmul02  13282  xmulneg1  13283  xmulf  13286  xmulpnf1  13288  xmulasslem2  13296  xmulge0  13298  xmulasslem  13299  xlemul1a  13302  xadddi  13309  xadddi2  13311  dfrp2  13409  ioopos  13439  ioorebas  13466  xrge0neqmnf  13467  elxrge0  13472  0e0iccpnf  13474  xov1plusxeqvd  13513  xnn0xrge0  13521  ico01fl0  13834  rpsup  13881  addmodid  13935  hashgt0  14404  hashle00  14416  hashgt0elex  14417  hashgt23el  14440  sgn0  15106  sgnp  15107  sgnn  15111  fprodge0  16007  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  cos1bnd  16203  sinltx  16205  sin01gt0  16206  cos01gt0  16207  sin02gt0  16208  sincos1sgn  16209  sincos2sgn  16210  halfleoddlt  16379  xrsmgm  21367  leordtval2  23148  pnfnei  23156  mnfnei  23157  psmetge0  24249  isxmet2d  24264  xmetge0  24281  xmetgt0  24295  prdsdsf  24304  prdsxmetlem  24305  xpsdsval  24318  blgt0  24336  xblss2ps  24338  xblss2  24339  xbln0  24351  prdsbl  24428  stdbdxmet  24452  stdbdmopn  24455  metustto  24490  metustid  24491  metustexhalf  24493  cfilucfil  24496  blval2  24499  metuel2  24502  nmoge0  24658  nmo0  24672  cnblcld  24711  blssioo  24732  blcvx  24735  xrsxmet  24747  metdsf  24786  metds0  24788  metdseq0  24792  metnrmlem1a  24796  iccpnfcnv  24891  iccpnfhmeo  24892  xrhmeo  24893  pcoass  24973  iscfil2  25216  ovolmge0  25428  ovolge0  25432  ovolf  25433  ovolssnul  25438  ovolctb  25441  ovoliunnul  25458  ovolicopnf  25475  voliunlem3  25503  volsup  25507  ioorf  25524  volivth  25558  vitalilem4  25562  vitalilem5  25563  itg2ge0  25686  itg2const2  25692  itg2seq  25693  itg2monolem1  25701  itg2monolem2  25702  itg2monolem3  25703  itg2gt0  25711  dvne0  25966  mdegle0  26032  ply1remlem  26120  ply1rem  26121  idomrootle  26128  plypf1  26167  aaliou3lem2  26301  aaliou3lem3  26302  taylfvallem1  26314  taylfval  26316  tayl0  26319  radcnvcl  26376  radcnvle  26379  pserulm  26381  psercnlem1  26385  pilem2  26412  sinhalfpilem  26422  sincosq1lem  26456  sincosq1sgn  26457  sincosq2sgn  26458  tangtx  26464  tanabsge  26465  sinq12gt0  26466  cosq14gt0  26469  sincos4thpi  26472  pige3ALT  26479  cos02pilt1  26485  cosq34lt1  26486  cosordlem  26489  cos0pilt1  26491  tanord1  26496  tanord  26497  efifo  26506  argimgt0  26571  argimlt0  26572  logccv  26622  loglesqrt  26721  atantan  26883  rlimcnp  26925  rlimcnp2  26926  scvxcvx  26946  basellem1  27041  dchrisum0lem2a  27478  pntibndlem1  27550  pntibnd  27554  pntlemc  27556  pntlem3  27570  abvcxp  27576  padicabvf  27592  padicabvcxp  27593  ostth2  27598  ttgcontlem1  28810  elntg2  28910  nmooge0  30694  nmoo0  30718  nmlnogt0  30724  nmopge0  31838  nmopgt0  31839  nmfnge0  31854  nmop0  31913  nmfn0  31914  xraddge02  32680  xlt2addrd  32682  xrge0infss  32683  sgncl  32756  sgn3da  32759  elxrge02  32852  xrs0  32944  xrge00  32953  xrge0addass  32957  xrge0addgt0  32958  xrge0adddir  32959  fsumrp0cl  32962  ply1unit  33534  rtelextdg2lem  33706  metider  33871  unitssxrge0  33877  xrge0iifcnv  33910  xrge0iifcv  33911  xrge0iifiso  33912  xrge0iifhom  33914  xrge0mulc1cn  33918  pnfneige0  33928  lmxrge0  33929  esumgsum  34022  esumnul  34025  esum0  34026  esumle  34035  esumlef  34039  esumcst  34040  esumsnf  34041  esumpr2  34044  esumpinfval  34050  esumpinfsum  34054  esumpcvgval  34055  esumpmono  34056  hashf2  34061  esumcvg  34063  measle0  34185  voliune  34206  volfiniune  34207  ddemeas  34213  aean  34221  oms0  34275  prob01  34391  probmeasb  34408  dstfrvclim1  34456  signsply0  34529  chtvalz  34607  hgt750lemf  34631  cvmliftlem10  35262  cvmliftlem13  35264  sinccvglem  35640  dnizeq0  36439  iccioo01  37291  sin2h  37580  tan2h  37582  broucube  37624  mblfinlem2  37628  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  mbfposadd  37637  itg2addnclem2  37642  itg2gt0cn  37645  ftc1anclem5  37667  ftc1anclem8  37670  dvasin  37674  areacirc  37683  rrnequiv  37805  dvrelog2b  42025  aks6d1c5lem3  42096  aks6d1c6lem1  42129  acos1half  42348  redvmptabs  42350  readvrec2  42351  readvrec  42352  imo72b2  44143  absfico  45190  xadd0ge  45296  xrge0nemnfd  45307  xralrple2  45329  xrpnf  45460  pnfel0pnf  45505  ge0xrre  45508  sqrlearg  45530  fsumge0cl  45550  limsup10ex  45750  liminf10ex  45751  sinaover2ne0  45845  itgsin0pilem1  45927  iblsplit  45943  stoweidlem46  46023  fourierdlem43  46127  fourierdlem44  46128  fourierdlem60  46143  fourierdlem61  46144  fourierdlem87  46170  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  sqwvfourb  46206  fourierswlem  46207  fouriersw  46208  etransclem23  46234  salexct2  46316  fge0npnf  46344  fge0iccico  46347  gsumge0cl  46348  sge0z  46352  sge00  46353  sge0sn  46356  sge0tsms  46357  sge0cl  46358  sge0f1o  46359  sge0ge0  46361  sge0repnf  46363  sge0fsum  46364  sge0pr  46371  sge0ssre  46374  sge0prle  46378  sge0p1  46391  sge0iunmptlemre  46392  sge0rpcpnf  46398  sge0rernmpt  46399  sge0isum  46404  sge0ad2en  46408  sge0xaddlem2  46411  sge0uzfsumgt  46421  sge0seq  46423  sge0reuz  46424  voliunsge0lem  46449  meage0  46452  meassre  46454  meale0eq0  46455  meaiuninclem  46457  omessre  46487  omeiunltfirp  46496  carageniuncllem2  46499  carageniuncl  46500  omege0  46510  omess0  46511  hoiprodcl  46524  ovnlerp  46539  ovnf  46540  ovn0lem  46542  ovnsubaddlem1  46547  hoiprodcl3  46557  hoidmvcl  46559  hoidmv1lelem3  46570  hoidmvlelem5  46576  ovnhoilem1  46578  ovolval5lem1  46629  pimrecltneg  46701  rehalfge1  47312  mod42tp1mod8  47564  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666  rrxsphere  48676  itscnhlinecirc02p  48713  iooii  48840  io1ii  48843  sepfsepc  48850  seppcld  48852