Theorem 0xr 11327

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 11324	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 11281	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3927	1 ⊢ 0 ∈ ℝ*

This proof depends on syntax axioms:   ∈ wcel 2145  ℝcr 11170  0cc0 11171  ℝ^*cxr 11313

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 2732  ax-1cn 11229  ax-addrcl 11232  ax-rnegex 11242  ax-cnre 11244

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 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-un 3903  df-ss 3915  df-xr 11318

This theorem is used by:  0lepnf  13231  ge0gtmnf  13271  max0sub  13295  xlt0neg1  13318  xlt0neg2  13319  xle0neg1  13320  xle0neg2  13321  xaddf  13323  xaddrid  13340  xaddlid  13341  xnn0xadd0  13346  xaddge0  13357  xsubge0  13360  xposdif  13361  xmullem  13363  xmullem2  13364  xmul01  13366  xmul02  13367  xmulneg1  13368  xmulf  13371  xmulpnf1  13373  xmulasslem2  13381  xmulge0  13383  xmulasslem  13384  xlemul1a  13387  xadddi  13394  xadddi2  13396  dfrp2  13494  ioopos  13524  ioorebas  13551  xrge0neqmnf  13552  elxrge0  13557  0e0iccpnf  13559  xov1plusxeqvd  13598  xnn0xrge0  13606  ico01fl0  13927  rpsup  13974  addmodid  14030  hashgt0  14499  hashle00  14511  hashgt0elex  14512  hashgt23el  14536  sgn0  15209  sgnp  15210  sgnn  15214  sgncl  15217  sgnrn  15218  sgn3da  15221  fprodge0  16127  ef01bndlem  16319  sin01bnd  16320  cos01bnd  16321  cos1bnd  16322  sinltx  16324  sin01gt0  16325  cos01gt0  16326  sin02gt0  16327  sincos1sgn  16328  sincos2sgn  16329  halfleoddlt  16499  xrsmgm  21674  leordtval2  23491  pnfnei  23499  mnfnei  23500  psmetge0  24592  isxmet2d  24607  xmetge0  24624  xmetgt0  24638  prdsdsf  24647  prdsxmetlem  24648  xpsdsval  24661  blgt0  24679  xblss2ps  24681  xblss2  24682  xbln0  24694  prdsbl  24771  stdbdxmet  24795  stdbdmopn  24798  metustto  24833  metustid  24834  metustexhalf  24836  cfilucfil  24839  blval2  24842  metuel2  24845  nmoge0  25001  nmo0  25015  cnblcld  25054  blssioo  25075  blcvx  25078  xrsxmet  25090  metdsf  25129  metds0  25131  metdseq0  25135  metnrmlem1a  25139  iccpnfcnv  25226  iccpnfhmeo  25227  xrhmeo  25228  pcoass  25306  iscfil2  25548  ovolmge0  25759  ovolge0  25763  ovolf  25764  ovolssnul  25769  ovolctb  25772  ovoliunnul  25789  ovolicopnf  25806  voliunlem3  25834  volsup  25838  ioorf  25855  volivth  25889  vitalilem4  25893  vitalilem5  25894  itg2ge0  26017  itg2const2  26023  itg2seq  26024  itg2monolem1  26032  itg2monolem2  26033  itg2monolem3  26034  itg2gt0  26042  dvne0  26292  mdegle0  26356  ply1remlem  26444  ply1rem  26445  idomrootle  26452  plypf1  26492  aaliou3lem2  26633  aaliou3lem3  26634  taylfvallem1  26647  taylfval  26649  tayl0  26652  radcnvcl  26707  radcnvle  26710  pserulm  26712  psercnlem1  26715  pilem2  26742  sinhalfpilem  26755  sincosq1lem  26789  sincosq1sgn  26790  sincosq2sgn  26791  tangtx  26797  tanabsge  26798  sinq12gt0  26799  cosq14gt0  26802  sincos4thpi  26805  pige3ALT  26811  cos02pilt1  26817  cosq34lt1  26818  cosordlem  26821  cos0pilt1  26823  tanord1  26828  tanord  26829  efifo  26838  argimgt0  26903  argimlt0  26904  logccv  26954  loglesqrt  27052  atantan  27214  rlimcnp  27256  rlimcnp2  27257  scvxcvx  27276  basellem1  27371  dchrisum0lem2a  27807  pntibndlem1  27879  pntibnd  27883  pntlemc  27885  pntlem3  27899  abvcxp  27905  padicabvf  27921  padicabvcxp  27922  ostth2  27927  ttgcontlem1  29395  elntg2  29496  nmooge0  31302  nmoo0  31326  nmlnogt0  31332  nmopge0  32446  nmopgt0  32447  nmfnge0  32462  nmop0  32521  nmfn0  32522  xraddge02  33282  xlt2addrd  33284  xrge0infss  33285  elxrge02  33431  xrs0  33500  xrge00  33508  xrge0addass  33510  xrge0addgt0  33511  xrge0adddir  33512  fsumrp0cl  33515  ply1unit  34040  vietadeg1  34143  rtelextdg2lem  34291  metider  34459  unitssxrge0  34465  xrge0iifcnv  34498  xrge0iifcv  34499  xrge0iifiso  34500  xrge0iifhom  34502  xrge0mulc1cn  34506  pnfneige0  34516  lmxrge0  34517  esumgsum  34610  esumnul  34613  esum0  34614  esumle  34623  esumlef  34627  esumcst  34628  esumsnf  34629  esumpr2  34632  esumpinfval  34638  esumpinfsum  34642  esumpcvgval  34643  esumpmono  34644  hashf2  34649  esumcvg  34651  measle0  34774  voliune  34795  volfiniune  34796  ddemeas  34802  aean  34810  oms0  34863  prob01  34979  probmeasb  34996  dstfrvclim1  35044  signsply0  35114  chtvalz  35192  hgt750lemf  35216  cvmliftlem10  35980  cvmliftlem13  35982  sinccvglem  36358  dnizeq0  37263  iccioo01  38170  sin2h  38453  tan2h  38455  broucube  38492  mblfinlem2  38496  ovoliunnfl  38500  voliunnfl  38502  volsupnfl  38503  mbfposadd  38505  itg2addnclem2  38510  itg2gt0cn  38513  ftc1anclem5  38535  ftc1anclem8  38538  dvasin  38542  areacirc  38551  rrnequiv  38689  dvrelog2b  43036  aks6d1c5lem3  43107  aks6d1c6lem1  43140  acos1half  43337  redvmptabs  43339  readvrec2  43340  readvrec  43341  imo72b2  45116  absfico  46152  xadd0ge  46256  xrge0nemnfd  46266  xralrple2  46288  xrpnf  46417  pnfel0pnf  46462  ge0xrre  46465  sqrlearg  46487  fsumge0cl  46507  limsup10ex  46705  liminf10ex  46706  sinaover2ne0  46800  itgsin0pilem1  46882  iblsplit  46898  stoweidlem46  46978  fourierdlem43  47082  fourierdlem44  47083  fourierdlem60  47098  fourierdlem61  47099  fourierdlem87  47125  fourierdlem103  47141  fourierdlem104  47142  fourierdlem111  47149  sqwvfourb  47161  fourierswlem  47162  fouriersw  47163  etransclem23  47189  salexct2  47271  fge0npnf  47299  fge0iccico  47302  gsumge0cl  47303  sge0z  47307  sge00  47308  sge0sn  47311  sge0tsms  47312  sge0cl  47313  sge0f1o  47314  sge0ge0  47316  sge0repnf  47318  sge0fsum  47319  sge0pr  47326  sge0ssre  47329  sge0prle  47333  sge0p1  47346  sge0iunmptlemre  47347  sge0rpcpnf  47353  sge0rernmpt  47354  sge0isum  47359  sge0ad2en  47363  sge0xaddlem2  47366  sge0uzfsumgt  47376  sge0seq  47378  sge0reuz  47379  voliunsge0lem  47404  meage0  47407  meassre  47409  meale0eq0  47410  meaiuninclem  47412  omessre  47442  omeiunltfirp  47451  carageniuncllem2  47454  carageniuncl  47455  omege0  47465  omess0  47466  hoiprodcl  47479  ovnlerp  47494  ovnf  47495  ovn0lem  47497  ovnsubaddlem1  47502  hoiprodcl3  47512  hoidmvcl  47514  hoidmv1lelem3  47525  hoidmvlelem5  47531  ovnhoilem1  47533  ovolval5lem1  47584  pimrecltneg  47656  rehalfge1  48331  mod42tp1mod8  48609  eenglngeehlnmlem1  49771  eenglngeehlnmlem2  49772  rrxsphere  49782  itscnhlinecirc02p  49819  iooii  49948  io1ii  49951  sepfsepc  49958  seppcld  49960