Theorem 0xr 11311

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 11308	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11266	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3976	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2099  ℝcr 11157  0cc0 11158  ℝ^*cxr 11297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-1cn 11216  ax-addrcl 11219  ax-rnegex 11229  ax-cnre 11231

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rex 3061  df-v 3464  df-un 3952  df-ss 3964  df-xr 11302

This theorem is referenced by:  0lepnf  13166  ge0gtmnf  13205  max0sub  13229  xlt0neg1  13252  xlt0neg2  13253  xle0neg1  13254  xle0neg2  13255  xaddf  13257  xaddrid  13274  xaddlid  13275  xnn0xadd0  13280  xaddge0  13291  xsubge0  13294  xposdif  13295  xmullem  13297  xmullem2  13298  xmul01  13300  xmul02  13301  xmulneg1  13302  xmulf  13305  xmulpnf1  13307  xmulasslem2  13315  xmulge0  13317  xmulasslem  13318  xlemul1a  13321  xadddi  13328  xadddi2  13330  dfrp2  13427  ioopos  13455  ioorebas  13482  xrge0neqmnf  13483  elxrge0  13488  0e0iccpnf  13490  xov1plusxeqvd  13529  xnn0xrge0  13537  ico01fl0  13839  rpsup  13886  addmodid  13939  hashgt0  14405  hashle00  14417  hashgt0elex  14418  hashgt23el  14441  sgn0  15094  sgnp  15095  sgnn  15099  fprodge0  15995  ef01bndlem  16186  sin01bnd  16187  cos01bnd  16188  cos1bnd  16189  sinltx  16191  sin01gt0  16192  cos01gt0  16193  sin02gt0  16194  sincos1sgn  16195  sincos2sgn  16196  halfleoddlt  16364  xrsmgm  21398  leordtval2  23207  pnfnei  23215  mnfnei  23216  psmetge0  24309  isxmet2d  24324  xmetge0  24341  xmetgt0  24355  prdsdsf  24364  prdsxmetlem  24365  xpsdsval  24378  blgt0  24396  xblss2ps  24398  xblss2  24399  xbln0  24411  prdsbl  24491  stdbdxmet  24515  stdbdmopn  24518  metustto  24553  metustid  24554  metustexhalf  24556  cfilucfil  24559  blval2  24562  metuel2  24565  nmoge0  24729  nmo0  24743  cnblcld  24782  blssioo  24802  blcvx  24805  xrsxmet  24816  metdsf  24855  metds0  24857  metdseq0  24861  metnrmlem1a  24865  iccpnfcnv  24960  iccpnfhmeo  24961  xrhmeo  24962  pcoass  25042  iscfil2  25285  ovolmge0  25497  ovolge0  25501  ovolf  25502  ovolssnul  25507  ovolctb  25510  ovoliunnul  25527  ovolicopnf  25544  voliunlem3  25572  volsup  25576  ioorf  25593  volivth  25627  vitalilem4  25631  vitalilem5  25632  itg2ge0  25756  itg2const2  25762  itg2seq  25763  itg2monolem1  25771  itg2monolem2  25772  itg2monolem3  25773  itg2gt0  25781  dvne0  26035  mdegle0  26104  ply1remlem  26192  ply1rem  26193  idomrootle  26200  plypf1  26239  aaliou3lem2  26371  aaliou3lem3  26372  taylfvallem1  26384  taylfval  26386  tayl0  26389  radcnvcl  26446  radcnvle  26449  pserulm  26451  psercnlem1  26455  pilem2  26482  sinhalfpilem  26491  sincosq1lem  26525  sincosq1sgn  26526  sincosq2sgn  26527  tangtx  26533  tanabsge  26534  sinq12gt0  26535  cosq14gt0  26538  sincos4thpi  26541  pige3ALT  26547  cos02pilt1  26553  cosq34lt1  26554  cosordlem  26557  cos0pilt1  26559  tanord1  26564  tanord  26565  efifo  26574  argimgt0  26639  argimlt0  26640  logccv  26690  loglesqrt  26789  atantan  26951  rlimcnp  26993  rlimcnp2  26994  scvxcvx  27014  basellem1  27109  dchrisum0lem2a  27546  pntibndlem1  27618  pntibnd  27622  pntlemc  27624  pntlem3  27638  abvcxp  27644  padicabvf  27660  padicabvcxp  27661  ostth2  27666  ttgcontlem1  28818  elntg2  28919  nmooge0  30700  nmoo0  30724  nmlnogt0  30730  nmopge0  31844  nmopgt0  31845  nmfnge0  31860  nmop0  31919  nmfn0  31920  xraddge02  32660  xlt2addrd  32662  xrge0infss  32664  elxrge02  32793  xrs0  32886  xrge00  32895  xrge0addass  32899  xrge0addgt0  32900  xrge0adddir  32901  fsumrp0cl  32904  ply1unit  33447  rtelextdg2lem  33604  metider  33709  unitssxrge0  33715  xrge0iifcnv  33748  xrge0iifcv  33749  xrge0iifiso  33750  xrge0iifhom  33752  xrge0mulc1cn  33756  pnfneige0  33766  lmxrge0  33767  esumgsum  33878  esumnul  33881  esum0  33882  esumle  33891  esumlef  33895  esumcst  33896  esumsnf  33897  esumpr2  33900  esumpinfval  33906  esumpinfsum  33910  esumpcvgval  33911  esumpmono  33912  hashf2  33917  esumcvg  33919  measle0  34041  voliune  34062  volfiniune  34063  ddemeas  34069  aean  34077  oms0  34131  prob01  34247  probmeasb  34264  dstfrvclim1  34311  sgncl  34372  sgn3da  34375  signsply0  34397  chtvalz  34475  hgt750lemf  34499  cvmliftlem10  35122  cvmliftlem13  35124  sinccvglem  35500  dnizeq0  36178  iccioo01  37034  sin2h  37311  tan2h  37313  broucube  37355  mblfinlem2  37359  ovoliunnfl  37363  voliunnfl  37365  volsupnfl  37366  mbfposadd  37368  itg2addnclem2  37373  itg2gt0cn  37376  ftc1anclem5  37398  ftc1anclem8  37401  dvasin  37405  areacirc  37414  rrnequiv  37536  dvrelog2b  41765  aks6d1c5lem3  41835  aks6d1c6lem1  41868  acos1half  42328  imo72b2  43839  absfico  44825  xadd0ge  44935  xrge0nemnfd  44947  xralrple2  44969  xrpnf  45101  pnfel0pnf  45146  ge0xrre  45149  sqrlearg  45171  fsumge0cl  45194  limsup10ex  45394  liminf10ex  45395  sinaover2ne0  45489  itgsin0pilem1  45571  iblsplit  45587  stoweidlem46  45667  fourierdlem43  45771  fourierdlem44  45772  fourierdlem60  45787  fourierdlem61  45788  fourierdlem87  45814  fourierdlem103  45830  fourierdlem104  45831  fourierdlem111  45838  sqwvfourb  45850  fourierswlem  45851  fouriersw  45852  etransclem23  45878  salexct2  45960  fge0npnf  45988  fge0iccico  45991  gsumge0cl  45992  sge0z  45996  sge00  45997  sge0sn  46000  sge0tsms  46001  sge0cl  46002  sge0f1o  46003  sge0ge0  46005  sge0repnf  46007  sge0fsum  46008  sge0pr  46015  sge0ssre  46018  sge0prle  46022  sge0p1  46035  sge0iunmptlemre  46036  sge0rpcpnf  46042  sge0rernmpt  46043  sge0isum  46048  sge0ad2en  46052  sge0xaddlem2  46055  sge0uzfsumgt  46065  sge0seq  46067  sge0reuz  46068  voliunsge0lem  46093  meage0  46096  meassre  46098  meale0eq0  46099  meaiuninclem  46101  omessre  46131  omeiunltfirp  46140  carageniuncllem2  46143  carageniuncl  46144  omege0  46154  omess0  46155  hoiprodcl  46168  ovnlerp  46183  ovnf  46184  ovn0lem  46186  ovnsubaddlem1  46191  hoiprodcl3  46201  hoidmvcl  46203  hoidmv1lelem3  46214  hoidmvlelem5  46220  ovnhoilem1  46222  ovolval5lem1  46273  pimrecltneg  46345  mod42tp1mod8  47174  eenglngeehlnmlem1  48125  eenglngeehlnmlem2  48126  rrxsphere  48136  itscnhlinecirc02p  48173  iooii  48251  io1ii  48254  sepfsepc  48261  seppcld  48263