Theorem 0xr 11383

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 11380	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11337	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3910	1 ⊢ 0 ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2147  ℝcr 11226  0cc0 11227  ℝ^*cxr 11369

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11285  ax-addrcl 11288  ax-rnegex 11298  ax-cnre 11300

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-v 3456  df-ss 3901  df-un 4154  df-xr 11374

This theorem is used by:  0lepnf  13289  ge0gtmnf  13329  max0sub  13353  xlt0neg1  13376  xlt0neg2  13377  xle0neg1  13378  xle0neg2  13379  xaddf  13381  xaddrid  13398  xaddlid  13399  xnn0xadd0  13404  xaddge0  13415  xsubge0  13418  xposdif  13419  xmullem  13421  xmullem2  13422  xmul01  13424  xmul02  13425  xmulneg1  13426  xmulf  13429  xmulpnf1  13431  xmulasslem2  13439  xmulge0  13441  xmulasslem  13442  xlemul1a  13445  xadddi  13452  xadddi2  13454  dfrp2  13552  ioopos  13582  ioorebas  13609  xrge0neqmnf  13610  elxrge0  13615  0e0iccpnf  13617  xov1plusxeqvd  13656  xnn0xrge0  13664  ico01fl0  13986  rpsup  14033  addmodid  14089  hashgt0  14559  hashle00  14571  hashgt0elex  14572  hashgt23el  14596  sgn0  15271  sgnp  15272  sgnn  15276  sgncl  15279  sgnrn  15280  sgn3da  15283  fprodge0  16189  ef01bndlem  16381  sin01bnd  16382  cos01bnd  16383  cos1bnd  16384  sinltx  16386  sin01gt0  16387  cos01gt0  16388  sin02gt0  16389  sincos1sgn  16390  sincos2sgn  16391  halfleoddlt  16561  xrsmgm  21743  leordtval2  23560  pnfnei  23568  mnfnei  23569  psmetge0  24661  isxmet2d  24676  xmetge0  24693  xmetgt0  24707  prdsdsf  24716  prdsxmetlem  24717  xpsdsval  24730  blgt0  24748  xblss2ps  24750  xblss2  24751  xbln0  24763  prdsbl  24840  stdbdxmet  24864  stdbdmopn  24867  metustto  24902  metustid  24903  metustexhalf  24905  cfilucfil  24908  blval2  24911  metuel2  24914  nmoge0  25070  nmo0  25084  cnblcld  25123  blssioo  25144  blcvx  25147  xrsxmet  25159  metdsf  25198  metds0  25200  metdseq0  25204  metnrmlem1a  25208  iccpnfcnv  25295  iccpnfhmeo  25296  xrhmeo  25297  pcoass  25375  iscfil2  25617  ovolmge0  25828  ovolge0  25832  ovolf  25833  ovolssnul  25838  ovolctb  25841  ovoliunnul  25858  ovolicopnf  25875  voliunlem3  25903  volsup  25907  ioorf  25924  volivth  25958  vitalilem4  25962  vitalilem5  25963  itg2ge0  26086  itg2const2  26092  itg2seq  26093  itg2monolem1  26101  itg2monolem2  26102  itg2monolem3  26103  itg2gt0  26111  dvne0  26361  mdegle0  26425  ply1remlem  26513  ply1rem  26514  idomrootle  26521  plypf1  26561  aaliou3lem2  26700  aaliou3lem3  26701  taylfvallem1  26714  taylfval  26716  tayl0  26719  radcnvcl  26774  radcnvle  26777  pserulm  26779  psercnlem1  26782  pilem2  26809  sinhalfpilem  26822  sincosq1lem  26856  sincosq1sgn  26857  sincosq2sgn  26858  tangtx  26864  tanabsge  26865  sinq12gt0  26866  cosq14gt0  26869  sincos4thpi  26872  pige3ALT  26878  cos02pilt1  26884  cosq34lt1  26885  cosordlem  26888  cos0pilt1  26890  tanord1  26895  tanord  26896  efifo  26905  argimgt0  26970  argimlt0  26971  logccv  27021  loglesqrt  27119  atantan  27281  rlimcnp  27323  rlimcnp2  27324  scvxcvx  27343  basellem1  27438  dchrisum0lem2a  27874  pntibndlem1  27946  pntibnd  27950  pntlemc  27952  pntlem3  27966  abvcxp  27972  padicabvf  27988  padicabvcxp  27989  ostth2  27994  ttgcontlem1  29492  elntg2  29593  nmooge0  31399  nmoo0  31423  nmlnogt0  31429  nmopge0  32543  nmopgt0  32544  nmfnge0  32559  nmop0  32618  nmfn0  32619  xraddge02  33419  xlt2addrd  33421  xrge0infss  33422  elxrge02  33568  xrs0  33637  xrge00  33645  xrge0addass  33647  xrge0addgt0  33648  xrge0adddir  33649  fsumrp0cl  33652  ply1unit  34177  vietadeg1  34280  rtelextdg2lem  34428  metider  34596  unitssxrge0  34602  xrge0iifcnv  34635  xrge0iifcv  34636  xrge0iifiso  34637  xrge0iifhom  34639  xrge0mulc1cn  34643  pnfneige0  34653  lmxrge0  34654  esumgsum  34747  esumnul  34750  esum0  34751  esumle  34760  esumlef  34764  esumcst  34765  esumsnf  34766  esumpr2  34769  esumpinfval  34775  esumpinfsum  34779  esumpcvgval  34780  esumpmono  34781  hashf2  34786  esumcvg  34788  measle0  34911  voliune  34932  volfiniune  34933  ddemeas  34939  aean  34947  oms0  34999  prob01  35115  probmeasb  35132  dstfrvclim1  35180  signsply0  35250  chtvalz  35328  hgt750lemf  35352  cvmliftlem10  36226  cvmliftlem13  36228  sinccvglem  36604  dnizeq0  37519  iccioo01  38442  sin2h  38725  tan2h  38727  broucube  38764  mblfinlem2  38768  ovoliunnfl  38772  voliunnfl  38774  volsupnfl  38775  mbfposadd  38777  itg2addnclem2  38782  itg2gt0cn  38785  ftc1anclem5  38807  ftc1anclem8  38810  dvasin  38814  areacirc  38823  rrnequiv  38961  dvrelog2b  43308  aks6d1c5lem3  43379  aks6d1c6lem1  43412  acos1half  43602  redvmptabs  43604  readvrec2  43605  readvrec  43606  imo72b2  45364  absfico  46436  xadd0ge  46539  xrge0nemnfd  46549  xralrple2  46571  xrpnf  46700  pnfel0pnf  46745  ge0xrre  46748  sqrlearg  46770  fsumge0cl  46790  limsup10ex  46988  liminf10ex  46989  sinaover2ne0  47083  itgsin0pilem1  47165  iblsplit  47181  stoweidlem46  47261  fourierdlem43  47365  fourierdlem44  47366  fourierdlem60  47381  fourierdlem61  47382  fourierdlem87  47408  fourierdlem103  47424  fourierdlem104  47425  fourierdlem111  47432  sqwvfourb  47444  fourierswlem  47445  fouriersw  47446  etransclem23  47472  salexct2  47554  fge0npnf  47582  fge0iccico  47585  gsumge0cl  47586  sge0z  47590  sge00  47591  sge0sn  47594  sge0tsms  47595  sge0cl  47596  sge0f1o  47597  sge0ge0  47599  sge0repnf  47601  sge0fsum  47602  sge0pr  47609  sge0ssre  47612  sge0prle  47616  sge0p1  47629  sge0iunmptlemre  47630  sge0rpcpnf  47636  sge0rernmpt  47637  sge0isum  47642  sge0ad2en  47646  sge0xaddlem2  47649  sge0uzfsumgt  47659  sge0seq  47661  sge0reuz  47662  voliunsge0lem  47687  meage0  47690  meassre  47692  meale0eq0  47693  meaiuninclem  47695  omessre  47725  omeiunltfirp  47734  carageniuncllem2  47737  carageniuncl  47738  omege0  47748  omess0  47749  hoiprodcl  47762  ovnlerp  47777  ovnf  47778  ovn0lem  47780  ovnsubaddlem1  47785  hoiprodcl3  47795  hoidmvcl  47797  hoidmv1lelem3  47808  hoidmvlelem5  47814  ovnhoilem1  47816  ovolval5lem1  47867  pimrecltneg  47939  rehalfge1  48614  mod42tp1mod8  48892  eenglngeehlnmlem1  50055  eenglngeehlnmlem2  50056  rrxsphere  50065  itscnhlinecirc02p  50102  iooii  50237  io1ii  50240  sepfsepc  50247  seppcld  50249