Theorem 0xr 11255

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 11252	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11209	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3933	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2141  ℝcr 11098  0cc0 11099  ℝ^*cxr 11241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11157  ax-addrcl 11160  ax-rnegex 11170  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-v 3455  df-un 3909  df-ss 3921  df-xr 11246

This theorem is referenced by:  0lepnf  13157  ge0gtmnf  13197  max0sub  13221  xlt0neg1  13244  xlt0neg2  13245  xle0neg1  13246  xle0neg2  13247  xaddf  13249  xaddrid  13266  xaddlid  13267  xnn0xadd0  13272  xaddge0  13283  xsubge0  13286  xposdif  13287  xmullem  13289  xmullem2  13290  xmul01  13292  xmul02  13293  xmulneg1  13294  xmulf  13297  xmulpnf1  13299  xmulasslem2  13307  xmulge0  13309  xmulasslem  13310  xlemul1a  13313  xadddi  13320  xadddi2  13322  dfrp2  13420  ioopos  13450  ioorebas  13477  xrge0neqmnf  13478  elxrge0  13483  0e0iccpnf  13485  xov1plusxeqvd  13524  xnn0xrge0  13532  ico01fl0  13851  rpsup  13898  addmodid  13954  hashgt0  14423  hashle00  14435  hashgt0elex  14436  hashgt23el  14460  sgn0  15125  sgnp  15126  sgnn  15130  sgncl  15133  sgnrn  15134  sgn3da  15137  fprodge0  16046  ef01bndlem  16239  sin01bnd  16240  cos01bnd  16241  cos1bnd  16242  sinltx  16244  sin01gt0  16245  cos01gt0  16246  sin02gt0  16247  sincos1sgn  16248  sincos2sgn  16249  halfleoddlt  16419  xrsmgm  21536  leordtval2  23348  pnfnei  23356  mnfnei  23357  psmetge0  24448  isxmet2d  24463  xmetge0  24480  xmetgt0  24494  prdsdsf  24503  prdsxmetlem  24504  xpsdsval  24517  blgt0  24535  xblss2ps  24537  xblss2  24538  xbln0  24550  prdsbl  24627  stdbdxmet  24651  stdbdmopn  24654  metustto  24689  metustid  24690  metustexhalf  24692  cfilucfil  24695  blval2  24698  metuel2  24701  nmoge0  24857  nmo0  24871  cnblcld  24910  blssioo  24931  blcvx  24934  xrsxmet  24946  metdsf  24985  metds0  24987  metdseq0  24991  metnrmlem1a  24995  iccpnfcnv  25082  iccpnfhmeo  25083  xrhmeo  25084  pcoass  25162  iscfil2  25404  ovolmge0  25615  ovolge0  25619  ovolf  25620  ovolssnul  25625  ovolctb  25628  ovoliunnul  25645  ovolicopnf  25662  voliunlem3  25690  volsup  25694  ioorf  25711  volivth  25745  vitalilem4  25749  vitalilem5  25750  itg2ge0  25873  itg2const2  25879  itg2seq  25880  itg2monolem1  25888  itg2monolem2  25889  itg2monolem3  25890  itg2gt0  25898  dvne0  26149  mdegle0  26213  ply1remlem  26301  ply1rem  26302  idomrootle  26309  plypf1  26348  aaliou3lem2  26483  aaliou3lem3  26484  taylfvallem1  26496  taylfval  26498  tayl0  26501  radcnvcl  26556  radcnvle  26559  pserulm  26561  psercnlem1  26564  pilem2  26591  sinhalfpilem  26604  sincosq1lem  26638  sincosq1sgn  26639  sincosq2sgn  26640  tangtx  26646  tanabsge  26647  sinq12gt0  26648  cosq14gt0  26651  sincos4thpi  26654  pige3ALT  26661  cos02pilt1  26667  cosq34lt1  26668  cosordlem  26671  cos0pilt1  26673  tanord1  26678  tanord  26679  efifo  26688  argimgt0  26753  argimlt0  26754  logccv  26804  loglesqrt  26902  atantan  27064  rlimcnp  27106  rlimcnp2  27107  scvxcvx  27126  basellem1  27221  dchrisum0lem2a  27657  pntibndlem1  27729  pntibnd  27733  pntlemc  27735  pntlem3  27749  abvcxp  27755  padicabvf  27771  padicabvcxp  27772  ostth2  27777  ttgcontlem1  29200  elntg2  29301  nmooge0  31085  nmoo0  31109  nmlnogt0  31115  nmopge0  32229  nmopgt0  32230  nmfnge0  32245  nmop0  32304  nmfn0  32305  xraddge02  33068  xlt2addrd  33070  xrge0infss  33071  elxrge02  33217  xrs0  33292  xrge00  33300  xrge0addass  33302  xrge0addgt0  33303  xrge0adddir  33304  fsumrp0cl  33307  ply1unit  33831  vietadeg1  33934  rtelextdg2lem  34082  metider  34250  unitssxrge0  34256  xrge0iifcnv  34289  xrge0iifcv  34290  xrge0iifiso  34291  xrge0iifhom  34293  xrge0mulc1cn  34297  pnfneige0  34307  lmxrge0  34308  esumgsum  34401  esumnul  34404  esum0  34405  esumle  34414  esumlef  34418  esumcst  34419  esumsnf  34420  esumpr2  34423  esumpinfval  34429  esumpinfsum  34433  esumpcvgval  34434  esumpmono  34435  hashf2  34440  esumcvg  34442  measle0  34564  voliune  34585  volfiniune  34586  ddemeas  34592  aean  34600  oms0  34653  prob01  34769  probmeasb  34786  dstfrvclim1  34834  signsply0  34904  chtvalz  34982  hgt750lemf  35006  cvmliftlem10  35740  cvmliftlem13  35742  sinccvglem  36118  dnizeq0  37008  iccioo01  37917  sin2h  38205  tan2h  38207  broucube  38249  mblfinlem2  38253  ovoliunnfl  38257  voliunnfl  38259  volsupnfl  38260  mbfposadd  38262  itg2addnclem2  38267  itg2gt0cn  38270  ftc1anclem5  38292  ftc1anclem8  38295  dvasin  38299  areacirc  38308  rrnequiv  38430  dvrelog2b  42779  aks6d1c5lem3  42850  aks6d1c6lem1  42883  acos1half  43065  redvmptabs  43067  readvrec2  43068  readvrec  43069  imo72b2  44846  absfico  45882  xadd0ge  45986  xrge0nemnfd  45996  xralrple2  46018  xrpnf  46147  pnfel0pnf  46192  ge0xrre  46195  sqrlearg  46217  fsumge0cl  46237  limsup10ex  46435  liminf10ex  46436  sinaover2ne0  46530  itgsin0pilem1  46612  iblsplit  46628  stoweidlem46  46708  fourierdlem43  46812  fourierdlem44  46813  fourierdlem60  46828  fourierdlem61  46829  fourierdlem87  46855  fourierdlem103  46871  fourierdlem104  46872  fourierdlem111  46879  sqwvfourb  46891  fourierswlem  46892  fouriersw  46893  etransclem23  46919  salexct2  47001  fge0npnf  47029  fge0iccico  47032  gsumge0cl  47033  sge0z  47037  sge00  47038  sge0sn  47041  sge0tsms  47042  sge0cl  47043  sge0f1o  47044  sge0ge0  47046  sge0repnf  47048  sge0fsum  47049  sge0pr  47056  sge0ssre  47059  sge0prle  47063  sge0p1  47076  sge0iunmptlemre  47077  sge0rpcpnf  47083  sge0rernmpt  47084  sge0isum  47089  sge0ad2en  47093  sge0xaddlem2  47096  sge0uzfsumgt  47106  sge0seq  47108  sge0reuz  47109  voliunsge0lem  47134  meage0  47137  meassre  47139  meale0eq0  47140  meaiuninclem  47142  omessre  47172  omeiunltfirp  47181  carageniuncllem2  47184  carageniuncl  47185  omege0  47195  omess0  47196  hoiprodcl  47209  ovnlerp  47224  ovnf  47225  ovn0lem  47227  ovnsubaddlem1  47232  hoiprodcl3  47242  hoidmvcl  47244  hoidmv1lelem3  47255  hoidmvlelem5  47261  ovnhoilem1  47263  ovolval5lem1  47314  pimrecltneg  47386  rehalfge1  48021  mod42tp1mod8  48299  eenglngeehlnmlem1  49462  eenglngeehlnmlem2  49463  rrxsphere  49473  itscnhlinecirc02p  49510  iooii  49641  io1ii  49644  sepfsepc  49651  seppcld  49653