Theorem 0xr 11260

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

This proof depends on syntax axioms:   ∈ wcel 2143  ℝcr 11103  0cc0 11104  ℝ^*cxr 11246

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11162  ax-addrcl 11165  ax-rnegex 11175  ax-cnre 11177

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-v 3457  df-un 3910  df-ss 3922  df-xr 11251

This theorem is used by:  0lepnf  13162  ge0gtmnf  13202  max0sub  13226  xlt0neg1  13249  xlt0neg2  13250  xle0neg1  13251  xle0neg2  13252  xaddf  13254  xaddrid  13271  xaddlid  13272  xnn0xadd0  13277  xaddge0  13288  xsubge0  13291  xposdif  13292  xmullem  13294  xmullem2  13295  xmul01  13297  xmul02  13298  xmulneg1  13299  xmulf  13302  xmulpnf1  13304  xmulasslem2  13312  xmulge0  13314  xmulasslem  13315  xlemul1a  13318  xadddi  13325  xadddi2  13327  dfrp2  13425  ioopos  13455  ioorebas  13482  xrge0neqmnf  13483  elxrge0  13488  0e0iccpnf  13490  xov1plusxeqvd  13529  xnn0xrge0  13537  ico01fl0  13857  rpsup  13904  addmodid  13960  hashgt0  14429  hashle00  14441  hashgt0elex  14442  hashgt23el  14466  sgn0  15131  sgnp  15132  sgnn  15136  sgncl  15139  sgnrn  15140  sgn3da  15143  fprodge0  16052  ef01bndlem  16244  sin01bnd  16245  cos01bnd  16246  cos1bnd  16247  sinltx  16249  sin01gt0  16250  cos01gt0  16251  sin02gt0  16252  sincos1sgn  16253  sincos2sgn  16254  halfleoddlt  16424  xrsmgm  21566  leordtval2  23378  pnfnei  23386  mnfnei  23387  psmetge0  24478  isxmet2d  24493  xmetge0  24510  xmetgt0  24524  prdsdsf  24533  prdsxmetlem  24534  xpsdsval  24547  blgt0  24565  xblss2ps  24567  xblss2  24568  xbln0  24580  prdsbl  24657  stdbdxmet  24681  stdbdmopn  24684  metustto  24719  metustid  24720  metustexhalf  24722  cfilucfil  24725  blval2  24728  metuel2  24731  nmoge0  24887  nmo0  24901  cnblcld  24940  blssioo  24961  blcvx  24964  xrsxmet  24976  metdsf  25015  metds0  25017  metdseq0  25021  metnrmlem1a  25025  iccpnfcnv  25112  iccpnfhmeo  25113  xrhmeo  25114  pcoass  25192  iscfil2  25434  ovolmge0  25645  ovolge0  25649  ovolf  25650  ovolssnul  25655  ovolctb  25658  ovoliunnul  25675  ovolicopnf  25692  voliunlem3  25720  volsup  25724  ioorf  25741  volivth  25775  vitalilem4  25779  vitalilem5  25780  itg2ge0  25903  itg2const2  25909  itg2seq  25910  itg2monolem1  25918  itg2monolem2  25919  itg2monolem3  25920  itg2gt0  25928  dvne0  26179  mdegle0  26243  ply1remlem  26331  ply1rem  26332  idomrootle  26339  plypf1  26378  aaliou3lem2  26515  aaliou3lem3  26516  taylfvallem1  26529  taylfval  26531  tayl0  26534  radcnvcl  26589  radcnvle  26592  pserulm  26594  psercnlem1  26597  pilem2  26624  sinhalfpilem  26637  sincosq1lem  26671  sincosq1sgn  26672  sincosq2sgn  26673  tangtx  26679  tanabsge  26680  sinq12gt0  26681  cosq14gt0  26684  sincos4thpi  26687  pige3ALT  26694  cos02pilt1  26700  cosq34lt1  26701  cosordlem  26704  cos0pilt1  26706  tanord1  26711  tanord  26712  efifo  26721  argimgt0  26786  argimlt0  26787  logccv  26837  loglesqrt  26935  atantan  27097  rlimcnp  27139  rlimcnp2  27140  scvxcvx  27159  basellem1  27254  dchrisum0lem2a  27690  pntibndlem1  27762  pntibnd  27766  pntlemc  27768  pntlem3  27782  abvcxp  27788  padicabvf  27804  padicabvcxp  27805  ostth2  27810  ttgcontlem1  29243  elntg2  29344  nmooge0  31128  nmoo0  31152  nmlnogt0  31158  nmopge0  32272  nmopgt0  32273  nmfnge0  32288  nmop0  32347  nmfn0  32348  xraddge02  33111  xlt2addrd  33113  xrge0infss  33114  elxrge02  33260  xrs0  33335  xrge00  33343  xrge0addass  33345  xrge0addgt0  33346  xrge0adddir  33347  fsumrp0cl  33350  ply1unit  33874  vietadeg1  33977  rtelextdg2lem  34125  metider  34293  unitssxrge0  34299  xrge0iifcnv  34332  xrge0iifcv  34333  xrge0iifiso  34334  xrge0iifhom  34336  xrge0mulc1cn  34340  pnfneige0  34350  lmxrge0  34351  esumgsum  34444  esumnul  34447  esum0  34448  esumle  34457  esumlef  34461  esumcst  34462  esumsnf  34463  esumpr2  34466  esumpinfval  34472  esumpinfsum  34476  esumpcvgval  34477  esumpmono  34478  hashf2  34483  esumcvg  34485  measle0  34607  voliune  34628  volfiniune  34629  ddemeas  34635  aean  34643  oms0  34696  prob01  34812  probmeasb  34829  dstfrvclim1  34877  signsply0  34947  chtvalz  35025  hgt750lemf  35049  cvmliftlem10  35794  cvmliftlem13  35796  sinccvglem  36172  dnizeq0  37092  iccioo01  38001  sin2h  38289  tan2h  38291  broucube  38333  mblfinlem2  38337  ovoliunnfl  38341  voliunnfl  38343  volsupnfl  38344  mbfposadd  38346  itg2addnclem2  38351  itg2gt0cn  38354  ftc1anclem5  38376  ftc1anclem8  38379  dvasin  38383  areacirc  38392  rrnequiv  38514  dvrelog2b  42861  aks6d1c5lem3  42932  aks6d1c6lem1  42965  acos1half  43147  redvmptabs  43149  readvrec2  43150  readvrec  43151  imo72b2  44926  absfico  45962  xadd0ge  46066  xrge0nemnfd  46076  xralrple2  46098  xrpnf  46227  pnfel0pnf  46272  ge0xrre  46275  sqrlearg  46297  fsumge0cl  46317  limsup10ex  46515  liminf10ex  46516  sinaover2ne0  46610  itgsin0pilem1  46692  iblsplit  46708  stoweidlem46  46788  fourierdlem43  46892  fourierdlem44  46893  fourierdlem60  46908  fourierdlem61  46909  fourierdlem87  46935  fourierdlem103  46951  fourierdlem104  46952  fourierdlem111  46959  sqwvfourb  46971  fourierswlem  46972  fouriersw  46973  etransclem23  46999  salexct2  47081  fge0npnf  47109  fge0iccico  47112  gsumge0cl  47113  sge0z  47117  sge00  47118  sge0sn  47121  sge0tsms  47122  sge0cl  47123  sge0f1o  47124  sge0ge0  47126  sge0repnf  47128  sge0fsum  47129  sge0pr  47136  sge0ssre  47139  sge0prle  47143  sge0p1  47156  sge0iunmptlemre  47157  sge0rpcpnf  47163  sge0rernmpt  47164  sge0isum  47169  sge0ad2en  47173  sge0xaddlem2  47176  sge0uzfsumgt  47186  sge0seq  47188  sge0reuz  47189  voliunsge0lem  47214  meage0  47217  meassre  47219  meale0eq0  47220  meaiuninclem  47222  omessre  47252  omeiunltfirp  47261  carageniuncllem2  47264  carageniuncl  47265  omege0  47275  omess0  47276  hoiprodcl  47289  ovnlerp  47304  ovnf  47305  ovn0lem  47307  ovnsubaddlem1  47312  hoiprodcl3  47322  hoidmvcl  47324  hoidmv1lelem3  47335  hoidmvlelem5  47341  ovnhoilem1  47343  ovolval5lem1  47394  pimrecltneg  47466  rehalfge1  48104  mod42tp1mod8  48382  eenglngeehlnmlem1  49545  eenglngeehlnmlem2  49546  rrxsphere  49556  itscnhlinecirc02p  49593  iooii  49724  io1ii  49727  sepfsepc  49734  seppcld  49736