Theorem 0xr 11240

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 11237	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11194	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3934	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2143  ℝcr 11083  0cc0 11084  ℝ^*cxr 11226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11142  ax-addrcl 11145  ax-rnegex 11155  ax-cnre 11157

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1564  df-ex 1801  df-sb 2092  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3088  df-v 3457  df-un 3910  df-ss 3922  df-xr 11231

This theorem is referenced by:  0lepnf  13145  ge0gtmnf  13185  max0sub  13209  xlt0neg1  13232  xlt0neg2  13233  xle0neg1  13234  xle0neg2  13235  xaddf  13237  xaddrid  13254  xaddlid  13255  xnn0xadd0  13260  xaddge0  13271  xsubge0  13274  xposdif  13275  xmullem  13277  xmullem2  13278  xmul01  13280  xmul02  13281  xmulneg1  13282  xmulf  13285  xmulpnf1  13287  xmulasslem2  13295  xmulge0  13297  xmulasslem  13298  xlemul1a  13301  xadddi  13308  xadddi2  13310  dfrp2  13408  ioopos  13438  ioorebas  13465  xrge0neqmnf  13466  elxrge0  13471  0e0iccpnf  13473  xov1plusxeqvd  13512  xnn0xrge0  13520  ico01fl0  13839  rpsup  13886  addmodid  13942  hashgt0  14411  hashle00  14423  hashgt0elex  14424  hashgt23el  14447  sgn0  15112  sgnp  15113  sgnn  15117  sgncl  15120  sgnrn  15121  sgn3da  15124  fprodge0  16033  ef01bndlem  16226  sin01bnd  16227  cos01bnd  16228  cos1bnd  16229  sinltx  16231  sin01gt0  16232  cos01gt0  16233  sin02gt0  16234  sincos1sgn  16235  sincos2sgn  16236  halfleoddlt  16406  xrsmgm  21466  leordtval2  23279  pnfnei  23287  mnfnei  23288  psmetge0  24379  isxmet2d  24394  xmetge0  24411  xmetgt0  24425  prdsdsf  24434  prdsxmetlem  24435  xpsdsval  24448  blgt0  24466  xblss2ps  24468  xblss2  24469  xbln0  24481  prdsbl  24558  stdbdxmet  24582  stdbdmopn  24585  metustto  24620  metustid  24621  metustexhalf  24623  cfilucfil  24626  blval2  24629  metuel2  24632  nmoge0  24788  nmo0  24802  cnblcld  24841  blssioo  24862  blcvx  24865  xrsxmet  24877  metdsf  24916  metds0  24918  metdseq0  24922  metnrmlem1a  24926  iccpnfcnv  25013  iccpnfhmeo  25014  xrhmeo  25015  pcoass  25093  iscfil2  25335  ovolmge0  25546  ovolge0  25550  ovolf  25551  ovolssnul  25556  ovolctb  25559  ovoliunnul  25576  ovolicopnf  25593  voliunlem3  25621  volsup  25625  ioorf  25642  volivth  25676  vitalilem4  25680  vitalilem5  25681  itg2ge0  25804  itg2const2  25810  itg2seq  25811  itg2monolem1  25819  itg2monolem2  25820  itg2monolem3  25821  itg2gt0  25829  dvne0  26080  mdegle0  26144  ply1remlem  26232  ply1rem  26233  idomrootle  26240  plypf1  26279  aaliou3lem2  26414  aaliou3lem3  26415  taylfvallem1  26427  taylfval  26429  tayl0  26432  radcnvcl  26487  radcnvle  26490  pserulm  26492  psercnlem1  26495  pilem2  26522  sinhalfpilem  26535  sincosq1lem  26569  sincosq1sgn  26570  sincosq2sgn  26571  tangtx  26577  tanabsge  26578  sinq12gt0  26579  cosq14gt0  26582  sincos4thpi  26585  pige3ALT  26592  cos02pilt1  26598  cosq34lt1  26599  cosordlem  26602  cos0pilt1  26604  tanord1  26609  tanord  26610  efifo  26619  argimgt0  26684  argimlt0  26685  logccv  26735  loglesqrt  26833  atantan  26995  rlimcnp  27037  rlimcnp2  27038  scvxcvx  27057  basellem1  27152  dchrisum0lem2a  27588  pntibndlem1  27660  pntibnd  27664  pntlemc  27666  pntlem3  27680  abvcxp  27686  padicabvf  27702  padicabvcxp  27703  ostth2  27708  ttgcontlem1  29092  elntg2  29193  nmooge0  30977  nmoo0  31001  nmlnogt0  31007  nmopge0  32121  nmopgt0  32122  nmfnge0  32137  nmop0  32196  nmfn0  32197  xraddge02  32965  xlt2addrd  32967  xrge0infss  32968  elxrge02  33115  xrs0  33190  xrge00  33198  xrge0addass  33200  xrge0addgt0  33201  xrge0adddir  33202  fsumrp0cl  33205  ply1unit  33774  vietadeg1  33877  rtelextdg2lem  34025  metider  34193  unitssxrge0  34199  xrge0iifcnv  34232  xrge0iifcv  34233  xrge0iifiso  34234  xrge0iifhom  34236  xrge0mulc1cn  34240  pnfneige0  34250  lmxrge0  34251  esumgsum  34344  esumnul  34347  esum0  34348  esumle  34357  esumlef  34361  esumcst  34362  esumsnf  34363  esumpr2  34366  esumpinfval  34372  esumpinfsum  34376  esumpcvgval  34377  esumpmono  34378  hashf2  34383  esumcvg  34385  measle0  34507  voliune  34528  volfiniune  34529  ddemeas  34535  aean  34543  oms0  34596  prob01  34712  probmeasb  34729  dstfrvclim1  34777  signsply0  34847  chtvalz  34925  hgt750lemf  34949  cvmliftlem10  35649  cvmliftlem13  35651  sinccvglem  36027  dnizeq0  36918  iccioo01  37826  sin2h  38114  tan2h  38116  broucube  38158  mblfinlem2  38162  ovoliunnfl  38166  voliunnfl  38168  volsupnfl  38169  mbfposadd  38171  itg2addnclem2  38176  itg2gt0cn  38179  ftc1anclem5  38201  ftc1anclem8  38204  dvasin  38208  areacirc  38217  rrnequiv  38339  dvrelog2b  42688  aks6d1c5lem3  42759  aks6d1c6lem1  42792  acos1half  42972  redvmptabs  42974  readvrec2  42975  readvrec  42976  imo72b2  44753  absfico  45785  xadd0ge  45889  xrge0nemnfd  45899  xralrple2  45921  xrpnf  46050  pnfel0pnf  46095  ge0xrre  46098  sqrlearg  46120  fsumge0cl  46140  limsup10ex  46338  liminf10ex  46339  sinaover2ne0  46433  itgsin0pilem1  46515  iblsplit  46531  stoweidlem46  46611  fourierdlem43  46715  fourierdlem44  46716  fourierdlem60  46731  fourierdlem61  46732  fourierdlem87  46758  fourierdlem103  46774  fourierdlem104  46775  fourierdlem111  46782  sqwvfourb  46794  fourierswlem  46795  fouriersw  46796  etransclem23  46822  salexct2  46904  fge0npnf  46932  fge0iccico  46935  gsumge0cl  46936  sge0z  46940  sge00  46941  sge0sn  46944  sge0tsms  46945  sge0cl  46946  sge0f1o  46947  sge0ge0  46949  sge0repnf  46951  sge0fsum  46952  sge0pr  46959  sge0ssre  46962  sge0prle  46966  sge0p1  46979  sge0iunmptlemre  46980  sge0rpcpnf  46986  sge0rernmpt  46987  sge0isum  46992  sge0ad2en  46996  sge0xaddlem2  46999  sge0uzfsumgt  47009  sge0seq  47011  sge0reuz  47012  voliunsge0lem  47037  meage0  47040  meassre  47042  meale0eq0  47043  meaiuninclem  47045  omessre  47075  omeiunltfirp  47084  carageniuncllem2  47087  carageniuncl  47088  omege0  47098  omess0  47099  hoiprodcl  47112  ovnlerp  47127  ovnf  47128  ovn0lem  47130  ovnsubaddlem1  47135  hoiprodcl3  47145  hoidmvcl  47147  hoidmv1lelem3  47158  hoidmvlelem5  47164  ovnhoilem1  47166  ovolval5lem1  47217  pimrecltneg  47289  rehalfge1  47924  mod42tp1mod8  48202  eenglngeehlnmlem1  49350  eenglngeehlnmlem2  49351  rrxsphere  49361  itscnhlinecirc02p  49398  iooii  49530  io1ii  49533  sepfsepc  49540  seppcld  49542