Theorem 0xr 9965

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 9962	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 9919	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3565	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 1977  ℝcr 9814  0cc0 9815  ℝ^*cxr 9952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-xr 9957

This theorem is referenced by:  0lepnf  11842  ge0gtmnf  11877  max0sub  11901  xlt0neg1  11924  xlt0neg2  11925  xle0neg1  11926  xle0neg2  11927  xaddf  11929  xaddid1  11946  xaddid2  11947  xnn0xadd0  11949  xaddge0  11960  xsubge0  11963  xposdif  11964  xmullem  11966  xmullem2  11967  xmul01  11969  xmul02  11970  xmulneg1  11971  xmulf  11974  xmulpnf1  11976  xmulasslem2  11984  xmulge0  11986  xmulasslem  11987  xlemul1a  11990  xadddi  11997  xadddi2  11999  ioopos  12121  ioorebas  12146  xrge0neqmnf  12147  elxrge0  12152  0e0iccpnf  12154  xov1plusxeqvd  12189  xnn0xrge0  12196  ico01fl0  12482  rpsup  12527  addmodid  12580  hashgt0  13038  hashle00  13049  hashgt0elex  13050  sgn0  13677  sgnp  13678  sgnn  13682  fprodge0  14563  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  cos1bnd  14756  sinltx  14758  sin01gt0  14759  cos01gt0  14760  sin02gt0  14761  sincos1sgn  14762  sincos2sgn  14763  halfleoddlt  14924  xrsmgm  19600  leordtval2  20826  pnfnei  20834  mnfnei  20835  psmetge0  21927  isxmet2d  21942  xmetge0  21959  xmetgt0  21973  prdsdsf  21982  prdsxmetlem  21983  xpsdsval  21996  blgt0  22014  xblss2ps  22016  xblss2  22017  xbln0  22029  prdsbl  22106  stdbdxmet  22130  stdbdmopn  22133  metustto  22168  metustid  22169  metustexhalf  22171  cfilucfil  22174  blval2  22177  metuel2  22180  nmoge0  22335  nmo0  22349  cnblcld  22388  blssioo  22406  blcvx  22409  xrsxmet  22420  metdsf  22459  metds0  22461  metdseq0  22465  metnrmlem1a  22469  iccpnfcnv  22551  iccpnfhmeo  22552  xrhmeo  22553  pcoass  22632  iscfil2  22872  ovolmge0  23052  ovolge0  23056  ovolf  23057  ovolssnul  23062  ovolctb  23065  ovoliunnul  23082  ovolicopnf  23099  voliunlem3  23127  volsup  23131  ioorf  23147  volivth  23181  vitalilem4  23186  vitalilem5  23187  itg2ge0  23308  itg2const2  23314  itg2seq  23315  itg2monolem1  23323  itg2monolem2  23324  itg2monolem3  23325  itg2gt0  23333  dvne0  23578  mdegle0  23641  ply1remlem  23726  ply1rem  23727  plypf1  23772  aaliou3lem2  23902  aaliou3lem3  23903  taylfvallem1  23915  taylfval  23917  tayl0  23920  radcnvcl  23975  radcnvle  23978  pserulm  23980  psercnlem1  23983  pilem2  24010  sinhalfpilem  24019  sincosq1lem  24053  sincosq1sgn  24054  sincosq2sgn  24055  tangtx  24061  tanabsge  24062  sinq12gt0  24063  cosq14gt0  24066  sincos4thpi  24069  pige3  24073  cosordlem  24081  tanord1  24087  tanord  24088  efifo  24097  argimgt0  24162  argimlt0  24163  logccv  24209  loglesqrt  24299  atantan  24450  rlimcnp  24492  rlimcnp2  24493  scvxcvx  24512  basellem1  24607  dchrisum0lem2a  25006  pntibndlem1  25078  pntibnd  25082  pntlemc  25084  pntlem3  25098  abvcxp  25104  padicabvf  25120  padicabvcxp  25121  ostth2  25126  ttgcontlem1  25565  nmooge0  27006  nmoo0  27030  nmlnogt0  27036  nmopge0  28154  nmopgt0  28155  nmfnge0  28170  nmop0  28229  nmfn0  28230  xraddge02  28911  xlt2addrd  28913  xrge0infss  28915  dfrp2  28922  elxrge02  28971  xrs0  29006  xrge00  29017  xrge0addass  29021  xrge0addgt0  29022  xrge0adddir  29023  fsumrp0cl  29026  metider  29265  unitssxrge0  29274  xrge0iifcnv  29307  xrge0iifcv  29308  xrge0iifiso  29309  xrge0iifhom  29311  xrge0mulc1cn  29315  pnfneige0  29325  lmxrge0  29326  esumgsum  29434  esumnul  29437  esum0  29438  esumle  29447  esumlef  29451  esumcst  29452  esumsnf  29453  esumpr2  29456  esumpinfval  29462  esumpinfsum  29466  esumpcvgval  29467  esumpmono  29468  hashf2  29473  esumcvg  29475  measle0  29598  voliune  29619  volfiniune  29620  ddemeas  29626  aean  29634  oms0  29686  prob01  29802  probmeasb  29819  dstfrvclim1  29866  sgncl  29927  sgn3da  29930  signsply0  29954  cvmliftlem10  30530  cvmliftlem13  30532  sinccvglem  30820  dnizeq0  31635  sin2h  32569  tan2h  32571  broucube  32613  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  mbfposadd  32627  itg2addnclem2  32632  itg2gt0cn  32635  ftc1anclem5  32659  ftc1anclem8  32662  dvasin  32666  areacirc  32675  rrnequiv  32804  idomrootle  36792  imo72b2  37497  absfico  38405  xadd0ge  38477  xrge0nemnfd  38489  xralrple2  38511  pnfel0pnf  38601  ge0nemnf2  38602  ge0xrre  38605  sqrlearg  38627  fsumge0cl  38640  sinaover2ne0  38751  itgsin0pilem1  38841  iblsplit  38858  stoweidlem46  38939  fourierdlem43  39043  fourierdlem44  39044  fourierdlem60  39059  fourierdlem61  39060  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  etransclem23  39150  salexct2  39233  fge0npnf  39260  fge0iccico  39263  gsumge0cl  39264  sge0z  39268  sge00  39269  sge0sn  39272  sge0tsms  39273  sge0cl  39274  sge0f1o  39275  sge0ge0  39277  sge0repnf  39279  sge0fsum  39280  sge0pr  39287  sge0ssre  39290  sge0prle  39294  sge0p1  39307  sge0iunmptlemre  39308  sge0rpcpnf  39314  sge0rernmpt  39315  sge0isum  39320  sge0ad2en  39324  sge0xaddlem2  39327  sge0uzfsumgt  39337  sge0seq  39339  sge0reuz  39340  voliunsge0lem  39365  meage0  39368  meassre  39370  meale0eq0  39371  meaiuninclem  39373  omessre  39400  omeiunltfirp  39409  carageniuncllem2  39412  carageniuncl  39413  omege0  39423  omess0  39424  hoiprodcl  39437  ovnlerp  39452  ovnf  39453  ovn0lem  39455  ovnsubaddlem1  39460  hoiprodcl3  39470  hoidmvcl  39472  hoidmv1lelem3  39483  hoidmvlelem5  39489  ovnhoilem1  39491  ovolval5lem1  39542  pimrecltneg  39610  mod42tp1mod8  40057