Theorem 0xr 11262

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

This proof depends on syntax axioms:   ∈ wcel 2142  ℝcr 11105  0cc0 11106  ℝ^*cxr 11248

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11164  ax-addrcl 11167  ax-rnegex 11177  ax-cnre 11179

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-v 3456  df-un 3909  df-ss 3921  df-xr 11253

This theorem is used by:  0lepnf  13164  ge0gtmnf  13204  max0sub  13228  xlt0neg1  13251  xlt0neg2  13252  xle0neg1  13253  xle0neg2  13254  xaddf  13256  xaddrid  13273  xaddlid  13274  xnn0xadd0  13279  xaddge0  13290  xsubge0  13293  xposdif  13294  xmullem  13296  xmullem2  13297  xmul01  13299  xmul02  13300  xmulneg1  13301  xmulf  13304  xmulpnf1  13306  xmulasslem2  13314  xmulge0  13316  xmulasslem  13317  xlemul1a  13320  xadddi  13327  xadddi2  13329  dfrp2  13427  ioopos  13457  ioorebas  13484  xrge0neqmnf  13485  elxrge0  13490  0e0iccpnf  13492  xov1plusxeqvd  13531  xnn0xrge0  13539  ico01fl0  13859  rpsup  13906  addmodid  13962  hashgt0  14431  hashle00  14443  hashgt0elex  14444  hashgt23el  14468  sgn0  15133  sgnp  15134  sgnn  15138  sgncl  15141  sgnrn  15142  sgn3da  15145  fprodge0  16054  ef01bndlem  16246  sin01bnd  16247  cos01bnd  16248  cos1bnd  16249  sinltx  16251  sin01gt0  16252  cos01gt0  16253  sin02gt0  16254  sincos1sgn  16255  sincos2sgn  16256  halfleoddlt  16426  xrsmgm  21568  leordtval2  23380  pnfnei  23388  mnfnei  23389  psmetge0  24480  isxmet2d  24495  xmetge0  24512  xmetgt0  24526  prdsdsf  24535  prdsxmetlem  24536  xpsdsval  24549  blgt0  24567  xblss2ps  24569  xblss2  24570  xbln0  24582  prdsbl  24659  stdbdxmet  24683  stdbdmopn  24686  metustto  24721  metustid  24722  metustexhalf  24724  cfilucfil  24727  blval2  24730  metuel2  24733  nmoge0  24889  nmo0  24903  cnblcld  24942  blssioo  24963  blcvx  24966  xrsxmet  24978  metdsf  25017  metds0  25019  metdseq0  25023  metnrmlem1a  25027  iccpnfcnv  25114  iccpnfhmeo  25115  xrhmeo  25116  pcoass  25194  iscfil2  25436  ovolmge0  25647  ovolge0  25651  ovolf  25652  ovolssnul  25657  ovolctb  25660  ovoliunnul  25677  ovolicopnf  25694  voliunlem3  25722  volsup  25726  ioorf  25743  volivth  25777  vitalilem4  25781  vitalilem5  25782  itg2ge0  25905  itg2const2  25911  itg2seq  25912  itg2monolem1  25920  itg2monolem2  25921  itg2monolem3  25922  itg2gt0  25930  dvne0  26181  mdegle0  26245  ply1remlem  26333  ply1rem  26334  idomrootle  26341  plypf1  26380  aaliou3lem2  26517  aaliou3lem3  26518  taylfvallem1  26531  taylfval  26533  tayl0  26536  radcnvcl  26591  radcnvle  26594  pserulm  26596  psercnlem1  26599  pilem2  26626  sinhalfpilem  26639  sincosq1lem  26673  sincosq1sgn  26674  sincosq2sgn  26675  tangtx  26681  tanabsge  26682  sinq12gt0  26683  cosq14gt0  26686  sincos4thpi  26689  pige3ALT  26696  cos02pilt1  26702  cosq34lt1  26703  cosordlem  26706  cos0pilt1  26708  tanord1  26713  tanord  26714  efifo  26723  argimgt0  26788  argimlt0  26789  logccv  26839  loglesqrt  26937  atantan  27099  rlimcnp  27141  rlimcnp2  27142  scvxcvx  27161  basellem1  27256  dchrisum0lem2a  27692  pntibndlem1  27764  pntibnd  27768  pntlemc  27770  pntlem3  27784  abvcxp  27790  padicabvf  27806  padicabvcxp  27807  ostth2  27812  ttgcontlem1  29245  elntg2  29346  nmooge0  31130  nmoo0  31154  nmlnogt0  31160  nmopge0  32274  nmopgt0  32275  nmfnge0  32290  nmop0  32349  nmfn0  32350  xraddge02  33113  xlt2addrd  33115  xrge0infss  33116  elxrge02  33262  xrs0  33335  xrge00  33343  xrge0addass  33345  xrge0addgt0  33346  xrge0adddir  33347  fsumrp0cl  33350  ply1unit  33874  vietadeg1  33977  rtelextdg2lem  34125  metider  34293  unitssxrge0  34299  xrge0iifcnv  34332  xrge0iifcv  34333  xrge0iifiso  34334  xrge0iifhom  34336  xrge0mulc1cn  34340  pnfneige0  34350  lmxrge0  34351  esumgsum  34444  esumnul  34447  esum0  34448  esumle  34457  esumlef  34461  esumcst  34462  esumsnf  34463  esumpr2  34466  esumpinfval  34472  esumpinfsum  34476  esumpcvgval  34477  esumpmono  34478  hashf2  34483  esumcvg  34485  measle0  34607  voliune  34628  volfiniune  34629  ddemeas  34635  aean  34643  oms0  34696  prob01  34812  probmeasb  34829  dstfrvclim1  34877  signsply0  34947  chtvalz  35025  hgt750lemf  35049  cvmliftlem10  35794  cvmliftlem13  35796  sinccvglem  36172  dnizeq0  37092  iccioo01  38001  sin2h  38289  tan2h  38291  broucube  38333  mblfinlem2  38337  ovoliunnfl  38341  voliunnfl  38343  volsupnfl  38344  mbfposadd  38346  itg2addnclem2  38351  itg2gt0cn  38354  ftc1anclem5  38376  ftc1anclem8  38379  dvasin  38383  areacirc  38392  rrnequiv  38514  dvrelog2b  42861  aks6d1c5lem3  42932  aks6d1c6lem1  42965  acos1half  43147  redvmptabs  43149  readvrec2  43150  readvrec  43151  imo72b2  44926  absfico  45962  xadd0ge  46066  xrge0nemnfd  46076  xralrple2  46098  xrpnf  46227  pnfel0pnf  46272  ge0xrre  46275  sqrlearg  46297  fsumge0cl  46317  limsup10ex  46515  liminf10ex  46516  sinaover2ne0  46610  itgsin0pilem1  46692  iblsplit  46708  stoweidlem46  46788  fourierdlem43  46892  fourierdlem44  46893  fourierdlem60  46908  fourierdlem61  46909  fourierdlem87  46935  fourierdlem103  46951  fourierdlem104  46952  fourierdlem111  46959  sqwvfourb  46971  fourierswlem  46972  fouriersw  46973  etransclem23  46999  salexct2  47081  fge0npnf  47109  fge0iccico  47112  gsumge0cl  47113  sge0z  47117  sge00  47118  sge0sn  47121  sge0tsms  47122  sge0cl  47123  sge0f1o  47124  sge0ge0  47126  sge0repnf  47128  sge0fsum  47129  sge0pr  47136  sge0ssre  47139  sge0prle  47143  sge0p1  47156  sge0iunmptlemre  47157  sge0rpcpnf  47163  sge0rernmpt  47164  sge0isum  47169  sge0ad2en  47173  sge0xaddlem2  47176  sge0uzfsumgt  47186  sge0seq  47188  sge0reuz  47189  voliunsge0lem  47214  meage0  47217  meassre  47219  meale0eq0  47220  meaiuninclem  47222  omessre  47252  omeiunltfirp  47261  carageniuncllem2  47264  carageniuncl  47265  omege0  47275  omess0  47276  hoiprodcl  47289  ovnlerp  47304  ovnf  47305  ovn0lem  47307  ovnsubaddlem1  47312  hoiprodcl3  47322  hoidmvcl  47324  hoidmv1lelem3  47335  hoidmvlelem5  47341  ovnhoilem1  47343  ovolval5lem1  47394  pimrecltneg  47466  rehalfge1  48104  mod42tp1mod8  48382  eenglngeehlnmlem1  49545  eenglngeehlnmlem2  49546  rrxsphere  49556  itscnhlinecirc02p  49593  iooii  49724  io1ii  49727  sepfsepc  49734  seppcld  49736