Theorem 0xr 11283

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

This proof depends on syntax axioms:   ∈ wcel 2145  ℝcr 11126  0cc0 11127  ℝ^*cxr 11269

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-1cn 11185  ax-addrcl 11188  ax-rnegex 11198  ax-cnre 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-v 3455  df-un 3907  df-ss 3919  df-xr 11274

This theorem is used by:  0lepnf  13186  ge0gtmnf  13226  max0sub  13250  xlt0neg1  13273  xlt0neg2  13274  xle0neg1  13275  xle0neg2  13276  xaddf  13278  xaddrid  13295  xaddlid  13296  xnn0xadd0  13301  xaddge0  13312  xsubge0  13315  xposdif  13316  xmullem  13318  xmullem2  13319  xmul01  13321  xmul02  13322  xmulneg1  13323  xmulf  13326  xmulpnf1  13328  xmulasslem2  13336  xmulge0  13338  xmulasslem  13339  xlemul1a  13342  xadddi  13349  xadddi2  13351  dfrp2  13449  ioopos  13479  ioorebas  13506  xrge0neqmnf  13507  elxrge0  13512  0e0iccpnf  13514  xov1plusxeqvd  13553  xnn0xrge0  13561  ico01fl0  13882  rpsup  13929  addmodid  13985  hashgt0  14454  hashle00  14466  hashgt0elex  14467  hashgt23el  14491  sgn0  15164  sgnp  15165  sgnn  15169  sgncl  15172  sgnrn  15173  sgn3da  15176  fprodge0  16084  ef01bndlem  16276  sin01bnd  16277  cos01bnd  16278  cos1bnd  16279  sinltx  16281  sin01gt0  16282  cos01gt0  16283  sin02gt0  16284  sincos1sgn  16285  sincos2sgn  16286  halfleoddlt  16456  xrsmgm  21621  leordtval2  23438  pnfnei  23446  mnfnei  23447  psmetge0  24539  isxmet2d  24554  xmetge0  24571  xmetgt0  24585  prdsdsf  24594  prdsxmetlem  24595  xpsdsval  24608  blgt0  24626  xblss2ps  24628  xblss2  24629  xbln0  24641  prdsbl  24718  stdbdxmet  24742  stdbdmopn  24745  metustto  24780  metustid  24781  metustexhalf  24783  cfilucfil  24786  blval2  24789  metuel2  24792  nmoge0  24948  nmo0  24962  cnblcld  25001  blssioo  25022  blcvx  25025  xrsxmet  25037  metdsf  25076  metds0  25078  metdseq0  25082  metnrmlem1a  25086  iccpnfcnv  25173  iccpnfhmeo  25174  xrhmeo  25175  pcoass  25253  iscfil2  25495  ovolmge0  25706  ovolge0  25710  ovolf  25711  ovolssnul  25716  ovolctb  25719  ovoliunnul  25736  ovolicopnf  25753  voliunlem3  25781  volsup  25785  ioorf  25802  volivth  25836  vitalilem4  25840  vitalilem5  25841  itg2ge0  25964  itg2const2  25970  itg2seq  25971  itg2monolem1  25979  itg2monolem2  25980  itg2monolem3  25981  itg2gt0  25989  dvne0  26240  mdegle0  26304  ply1remlem  26392  ply1rem  26393  idomrootle  26400  plypf1  26439  aaliou3lem2  26576  aaliou3lem3  26577  taylfvallem1  26590  taylfval  26592  tayl0  26595  radcnvcl  26650  radcnvle  26653  pserulm  26655  psercnlem1  26658  pilem2  26685  sinhalfpilem  26698  sincosq1lem  26732  sincosq1sgn  26733  sincosq2sgn  26734  tangtx  26740  tanabsge  26741  sinq12gt0  26742  cosq14gt0  26745  sincos4thpi  26748  pige3ALT  26755  cos02pilt1  26761  cosq34lt1  26762  cosordlem  26765  cos0pilt1  26767  tanord1  26772  tanord  26773  efifo  26782  argimgt0  26847  argimlt0  26848  logccv  26898  loglesqrt  26996  atantan  27158  rlimcnp  27200  rlimcnp2  27201  scvxcvx  27220  basellem1  27315  dchrisum0lem2a  27751  pntibndlem1  27823  pntibnd  27827  pntlemc  27829  pntlem3  27843  abvcxp  27849  padicabvf  27865  padicabvcxp  27866  ostth2  27871  ttgcontlem1  29327  elntg2  29428  nmooge0  31234  nmoo0  31258  nmlnogt0  31264  nmopge0  32378  nmopgt0  32379  nmfnge0  32394  nmop0  32453  nmfn0  32454  xraddge02  33215  xlt2addrd  33217  xrge0infss  33218  elxrge02  33364  xrs0  33433  xrge00  33441  xrge0addass  33443  xrge0addgt0  33444  xrge0adddir  33445  fsumrp0cl  33448  ply1unit  33972  vietadeg1  34075  rtelextdg2lem  34223  metider  34391  unitssxrge0  34397  xrge0iifcnv  34430  xrge0iifcv  34431  xrge0iifiso  34432  xrge0iifhom  34434  xrge0mulc1cn  34438  pnfneige0  34448  lmxrge0  34449  esumgsum  34542  esumnul  34545  esum0  34546  esumle  34555  esumlef  34559  esumcst  34560  esumsnf  34561  esumpr2  34564  esumpinfval  34570  esumpinfsum  34574  esumpcvgval  34575  esumpmono  34576  hashf2  34581  esumcvg  34583  measle0  34706  voliune  34727  volfiniune  34728  ddemeas  34734  aean  34742  oms0  34795  prob01  34911  probmeasb  34928  dstfrvclim1  34976  signsply0  35046  chtvalz  35124  hgt750lemf  35148  cvmliftlem10  35860  cvmliftlem13  35862  sinccvglem  36238  dnizeq0  37159  iccioo01  38068  sin2h  38351  tan2h  38353  broucube  38390  mblfinlem2  38394  ovoliunnfl  38398  voliunnfl  38400  volsupnfl  38401  mbfposadd  38403  itg2addnclem2  38408  itg2gt0cn  38411  ftc1anclem5  38433  ftc1anclem8  38436  dvasin  38440  areacirc  38449  rrnequiv  38572  dvrelog2b  42919  aks6d1c5lem3  42990  aks6d1c6lem1  43023  acos1half  43220  redvmptabs  43222  readvrec2  43223  readvrec  43224  imo72b2  44999  absfico  46035  xadd0ge  46139  xrge0nemnfd  46149  xralrple2  46171  xrpnf  46300  pnfel0pnf  46345  ge0xrre  46348  sqrlearg  46370  fsumge0cl  46390  limsup10ex  46588  liminf10ex  46589  sinaover2ne0  46683  itgsin0pilem1  46765  iblsplit  46781  stoweidlem46  46861  fourierdlem43  46965  fourierdlem44  46966  fourierdlem60  46981  fourierdlem61  46982  fourierdlem87  47008  fourierdlem103  47024  fourierdlem104  47025  fourierdlem111  47032  sqwvfourb  47044  fourierswlem  47045  fouriersw  47046  etransclem23  47072  salexct2  47154  fge0npnf  47182  fge0iccico  47185  gsumge0cl  47186  sge0z  47190  sge00  47191  sge0sn  47194  sge0tsms  47195  sge0cl  47196  sge0f1o  47197  sge0ge0  47199  sge0repnf  47201  sge0fsum  47202  sge0pr  47209  sge0ssre  47212  sge0prle  47216  sge0p1  47229  sge0iunmptlemre  47230  sge0rpcpnf  47236  sge0rernmpt  47237  sge0isum  47242  sge0ad2en  47246  sge0xaddlem2  47249  sge0uzfsumgt  47259  sge0seq  47261  sge0reuz  47262  voliunsge0lem  47287  meage0  47290  meassre  47292  meale0eq0  47293  meaiuninclem  47295  omessre  47325  omeiunltfirp  47334  carageniuncllem2  47337  carageniuncl  47338  omege0  47348  omess0  47349  hoiprodcl  47362  ovnlerp  47377  ovnf  47378  ovn0lem  47380  ovnsubaddlem1  47385  hoiprodcl3  47395  hoidmvcl  47397  hoidmv1lelem3  47408  hoidmvlelem5  47414  ovnhoilem1  47416  ovolval5lem1  47467  pimrecltneg  47539  rehalfge1  48214  mod42tp1mod8  48492  eenglngeehlnmlem1  49654  eenglngeehlnmlem2  49655  rrxsphere  49665  itscnhlinecirc02p  49702  iooii  49831  io1ii  49834  sepfsepc  49841  seppcld  49843