Theorem 0xr 10677

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 10674	. 2 ⊢ ℝ ⊆ ℝ*
2		0re 10632	. 2 ⊢ 0 ∈ ℝ
3	1, 2	sselii 3912	1 ⊢ 0 ∈ ℝ*

Syntax hints:   ∈ wcel 2111  ℝcr 10525  0cc0 10526  ℝ^*cxr 10663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-addrcl 10587  ax-rnegex 10597  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-xr 10668

This theorem is referenced by:  0lepnf  12515  ge0gtmnf  12553  max0sub  12577  xlt0neg1  12600  xlt0neg2  12601  xle0neg1  12602  xle0neg2  12603  xaddf  12605  xaddid1  12622  xaddid2  12623  xnn0xadd0  12628  xaddge0  12639  xsubge0  12642  xposdif  12643  xmullem  12645  xmullem2  12646  xmul01  12648  xmul02  12649  xmulneg1  12650  xmulf  12653  xmulpnf1  12655  xmulasslem2  12663  xmulge0  12665  xmulasslem  12666  xlemul1a  12669  xadddi  12676  xadddi2  12678  ioopos  12802  ioorebas  12829  xrge0neqmnf  12830  elxrge0  12835  0e0iccpnf  12837  xov1plusxeqvd  12876  xnn0xrge0  12884  ico01fl0  13184  rpsup  13229  addmodid  13282  hashgt0  13745  hashle00  13757  hashgt0elex  13758  hashgt23el  13781  sgn0  14440  sgnp  14441  sgnn  14445  fprodge0  15339  ef01bndlem  15529  sin01bnd  15530  cos01bnd  15531  cos1bnd  15532  sinltx  15534  sin01gt0  15535  cos01gt0  15536  sin02gt0  15537  sincos1sgn  15538  sincos2sgn  15539  halfleoddlt  15703  xrsmgm  20126  leordtval2  21817  pnfnei  21825  mnfnei  21826  psmetge0  22919  isxmet2d  22934  xmetge0  22951  xmetgt0  22965  prdsdsf  22974  prdsxmetlem  22975  xpsdsval  22988  blgt0  23006  xblss2ps  23008  xblss2  23009  xbln0  23021  prdsbl  23098  stdbdxmet  23122  stdbdmopn  23125  metustto  23160  metustid  23161  metustexhalf  23163  cfilucfil  23166  blval2  23169  metuel2  23172  nmoge0  23327  nmo0  23341  cnblcld  23380  blssioo  23400  blcvx  23403  xrsxmet  23414  metdsf  23453  metds0  23455  metdseq0  23459  metnrmlem1a  23463  iccpnfcnv  23549  iccpnfhmeo  23550  xrhmeo  23551  pcoass  23629  iscfil2  23870  ovolmge0  24081  ovolge0  24085  ovolf  24086  ovolssnul  24091  ovolctb  24094  ovoliunnul  24111  ovolicopnf  24128  voliunlem3  24156  volsup  24160  ioorf  24177  volivth  24211  vitalilem4  24215  vitalilem5  24216  itg2ge0  24339  itg2const2  24345  itg2seq  24346  itg2monolem1  24354  itg2monolem2  24355  itg2monolem3  24356  itg2gt0  24364  dvne0  24614  mdegle0  24678  ply1remlem  24763  ply1rem  24764  plypf1  24809  aaliou3lem2  24939  aaliou3lem3  24940  taylfvallem1  24952  taylfval  24954  tayl0  24957  radcnvcl  25012  radcnvle  25015  pserulm  25017  psercnlem1  25020  pilem2  25047  sinhalfpilem  25056  sincosq1lem  25090  sincosq1sgn  25091  sincosq2sgn  25092  tangtx  25098  tanabsge  25099  sinq12gt0  25100  cosq14gt0  25103  sincos4thpi  25106  pige3ALT  25112  cos02pilt1  25118  cosq34lt1  25119  cosordlem  25122  cos0pilt1  25124  tanord1  25129  tanord  25130  efifo  25139  argimgt0  25203  argimlt0  25204  logccv  25254  loglesqrt  25347  atantan  25509  rlimcnp  25551  rlimcnp2  25552  scvxcvx  25571  basellem1  25666  dchrisum0lem2a  26101  pntibndlem1  26173  pntibnd  26177  pntlemc  26179  pntlem3  26193  abvcxp  26199  padicabvf  26215  padicabvcxp  26216  ostth2  26221  ttgcontlem1  26679  elntg2  26779  nmooge0  28550  nmoo0  28574  nmlnogt0  28580  nmopge0  29694  nmopgt0  29695  nmfnge0  29710  nmop0  29769  nmfn0  29770  xraddge02  30506  xlt2addrd  30508  xrge0infss  30510  dfrp2  30517  elxrge02  30634  xrs0  30709  xrge00  30720  xrge0addass  30724  xrge0addgt0  30725  xrge0adddir  30726  fsumrp0cl  30729  metider  31247  unitssxrge0  31253  xrge0iifcnv  31286  xrge0iifcv  31287  xrge0iifiso  31288  xrge0iifhom  31290  xrge0mulc1cn  31294  pnfneige0  31304  lmxrge0  31305  esumgsum  31414  esumnul  31417  esum0  31418  esumle  31427  esumlef  31431  esumcst  31432  esumsnf  31433  esumpr2  31436  esumpinfval  31442  esumpinfsum  31446  esumpcvgval  31447  esumpmono  31448  hashf2  31453  esumcvg  31455  measle0  31577  voliune  31598  volfiniune  31599  ddemeas  31605  aean  31613  oms0  31665  prob01  31781  probmeasb  31798  dstfrvclim1  31845  sgncl  31906  sgn3da  31909  signsply0  31931  chtvalz  32010  hgt750lemf  32034  cvmliftlem10  32654  cvmliftlem13  32656  sinccvglem  33028  dnizeq0  33927  iccioo01  34741  sin2h  35047  tan2h  35049  broucube  35091  mblfinlem2  35095  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  mbfposadd  35104  itg2addnclem2  35109  itg2gt0cn  35112  ftc1anclem5  35134  ftc1anclem8  35137  dvasin  35141  areacirc  35150  rrnequiv  35273  idomrootle  40139  imo72b2  40878  absfico  41847  xadd0ge  41952  xrge0nemnfd  41964  xralrple2  41986  xrpnf  42125  pnfel0pnf  42165  ge0xrre  42168  sqrlearg  42190  fsumge0cl  42215  limsup10ex  42415  liminf10ex  42416  sinaover2ne0  42510  itgsin0pilem1  42592  iblsplit  42608  stoweidlem46  42688  fourierdlem43  42792  fourierdlem44  42793  fourierdlem60  42808  fourierdlem61  42809  fourierdlem87  42835  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  sqwvfourb  42871  fourierswlem  42872  fouriersw  42873  etransclem23  42899  salexct2  42979  fge0npnf  43006  fge0iccico  43009  gsumge0cl  43010  sge0z  43014  sge00  43015  sge0sn  43018  sge0tsms  43019  sge0cl  43020  sge0f1o  43021  sge0ge0  43023  sge0repnf  43025  sge0fsum  43026  sge0pr  43033  sge0ssre  43036  sge0prle  43040  sge0p1  43053  sge0iunmptlemre  43054  sge0rpcpnf  43060  sge0rernmpt  43061  sge0isum  43066  sge0ad2en  43070  sge0xaddlem2  43073  sge0uzfsumgt  43083  sge0seq  43085  sge0reuz  43086  voliunsge0lem  43111  meage0  43114  meassre  43116  meale0eq0  43117  meaiuninclem  43119  omessre  43149  omeiunltfirp  43158  carageniuncllem2  43161  carageniuncl  43162  omege0  43172  omess0  43173  hoiprodcl  43186  ovnlerp  43201  ovnf  43202  ovn0lem  43204  ovnsubaddlem1  43209  hoiprodcl3  43219  hoidmvcl  43221  hoidmv1lelem3  43232  hoidmvlelem5  43238  ovnhoilem1  43240  ovolval5lem1  43291  pimrecltneg  43358  mod42tp1mod8  44120  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  rrxsphere  45162  itscnhlinecirc02p  45199