MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0xr Structured version   Visualization version   GIF version

Theorem 0xr 11160
Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
Assertion
Ref Expression
0xr 0 ∈ ℝ*

Proof of Theorem 0xr
StepHypRef Expression
1 ressxr 11157 . 2 ℝ ⊆ ℝ*
2 0re 11115 . 2 0 ∈ ℝ
31, 2sselii 3939 1 0 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2106  cr 11008  0cc0 11009  *cxr 11146
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-1cn 11067  ax-addrcl 11070  ax-rnegex 11080  ax-cnre 11082
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3072  df-v 3445  df-un 3913  df-in 3915  df-ss 3925  df-xr 11151
This theorem is referenced by:  0lepnf  13007  ge0gtmnf  13045  max0sub  13069  xlt0neg1  13092  xlt0neg2  13093  xle0neg1  13094  xle0neg2  13095  xaddf  13097  xaddid1  13114  xaddid2  13115  xnn0xadd0  13120  xaddge0  13131  xsubge0  13134  xposdif  13135  xmullem  13137  xmullem2  13138  xmul01  13140  xmul02  13141  xmulneg1  13142  xmulf  13145  xmulpnf1  13147  xmulasslem2  13155  xmulge0  13157  xmulasslem  13158  xlemul1a  13161  xadddi  13168  xadddi2  13170  dfrp2  13267  ioopos  13295  ioorebas  13322  xrge0neqmnf  13323  elxrge0  13328  0e0iccpnf  13330  xov1plusxeqvd  13369  xnn0xrge0  13377  ico01fl0  13678  rpsup  13725  addmodid  13778  hashgt0  14242  hashle00  14254  hashgt0elex  14255  hashgt23el  14278  sgn0  14934  sgnp  14935  sgnn  14939  fprodge0  15836  ef01bndlem  16026  sin01bnd  16027  cos01bnd  16028  cos1bnd  16029  sinltx  16031  sin01gt0  16032  cos01gt0  16033  sin02gt0  16034  sincos1sgn  16035  sincos2sgn  16036  halfleoddlt  16204  xrsmgm  20785  leordtval2  22515  pnfnei  22523  mnfnei  22524  psmetge0  23617  isxmet2d  23632  xmetge0  23649  xmetgt0  23663  prdsdsf  23672  prdsxmetlem  23673  xpsdsval  23686  blgt0  23704  xblss2ps  23706  xblss2  23707  xbln0  23719  prdsbl  23799  stdbdxmet  23823  stdbdmopn  23826  metustto  23861  metustid  23862  metustexhalf  23864  cfilucfil  23867  blval2  23870  metuel2  23873  nmoge0  24037  nmo0  24051  cnblcld  24090  blssioo  24110  blcvx  24113  xrsxmet  24124  metdsf  24163  metds0  24165  metdseq0  24169  metnrmlem1a  24173  iccpnfcnv  24259  iccpnfhmeo  24260  xrhmeo  24261  pcoass  24339  iscfil2  24582  ovolmge0  24793  ovolge0  24797  ovolf  24798  ovolssnul  24803  ovolctb  24806  ovoliunnul  24823  ovolicopnf  24840  voliunlem3  24868  volsup  24872  ioorf  24889  volivth  24923  vitalilem4  24927  vitalilem5  24928  itg2ge0  25052  itg2const2  25058  itg2seq  25059  itg2monolem1  25067  itg2monolem2  25068  itg2monolem3  25069  itg2gt0  25077  dvne0  25327  mdegle0  25394  ply1remlem  25479  ply1rem  25480  plypf1  25525  aaliou3lem2  25655  aaliou3lem3  25656  taylfvallem1  25668  taylfval  25670  tayl0  25673  radcnvcl  25728  radcnvle  25731  pserulm  25733  psercnlem1  25736  pilem2  25763  sinhalfpilem  25772  sincosq1lem  25806  sincosq1sgn  25807  sincosq2sgn  25808  tangtx  25814  tanabsge  25815  sinq12gt0  25816  cosq14gt0  25819  sincos4thpi  25822  pige3ALT  25828  cos02pilt1  25834  cosq34lt1  25835  cosordlem  25838  cos0pilt1  25840  tanord1  25845  tanord  25846  efifo  25855  argimgt0  25919  argimlt0  25920  logccv  25970  loglesqrt  26063  atantan  26225  rlimcnp  26267  rlimcnp2  26268  scvxcvx  26287  basellem1  26382  dchrisum0lem2a  26817  pntibndlem1  26889  pntibnd  26893  pntlemc  26895  pntlem3  26909  abvcxp  26915  padicabvf  26931  padicabvcxp  26932  ostth2  26937  ttgcontlem1  27662  elntg2  27763  nmooge0  29538  nmoo0  29562  nmlnogt0  29568  nmopge0  30682  nmopgt0  30683  nmfnge0  30698  nmop0  30757  nmfn0  30758  xraddge02  31487  xlt2addrd  31489  xrge0infss  31491  elxrge02  31614  xrs0  31692  xrge00  31703  xrge0addass  31707  xrge0addgt0  31708  xrge0adddir  31709  fsumrp0cl  31712  metider  32287  unitssxrge0  32293  xrge0iifcnv  32326  xrge0iifcv  32327  xrge0iifiso  32328  xrge0iifhom  32330  xrge0mulc1cn  32334  pnfneige0  32344  lmxrge0  32345  esumgsum  32456  esumnul  32459  esum0  32460  esumle  32469  esumlef  32473  esumcst  32474  esumsnf  32475  esumpr2  32478  esumpinfval  32484  esumpinfsum  32488  esumpcvgval  32489  esumpmono  32490  hashf2  32495  esumcvg  32497  measle0  32619  voliune  32640  volfiniune  32641  ddemeas  32647  aean  32655  oms0  32709  prob01  32825  probmeasb  32842  dstfrvclim1  32889  sgncl  32950  sgn3da  32953  signsply0  32975  chtvalz  33054  hgt750lemf  33078  cvmliftlem10  33700  cvmliftlem13  33702  sinccvglem  34072  dnizeq0  34876  iccioo01  35736  sin2h  36006  tan2h  36008  broucube  36050  mblfinlem2  36054  ovoliunnfl  36058  voliunnfl  36060  volsupnfl  36061  mbfposadd  36063  itg2addnclem2  36068  itg2gt0cn  36071  ftc1anclem5  36093  ftc1anclem8  36096  dvasin  36100  areacirc  36109  rrnequiv  36232  dvrelog2b  40461  acos1half  40560  idomrootle  41431  imo72b2  42356  absfico  43344  xadd0ge  43459  xrge0nemnfd  43471  xralrple2  43493  xrpnf  43626  pnfel0pnf  43667  ge0xrre  43670  sqrlearg  43692  fsumge0cl  43715  limsup10ex  43915  liminf10ex  43916  sinaover2ne0  44010  itgsin0pilem1  44092  iblsplit  44108  stoweidlem46  44188  fourierdlem43  44292  fourierdlem44  44293  fourierdlem60  44308  fourierdlem61  44309  fourierdlem87  44335  fourierdlem103  44351  fourierdlem104  44352  fourierdlem111  44359  sqwvfourb  44371  fourierswlem  44372  fouriersw  44373  etransclem23  44399  salexct2  44481  fge0npnf  44509  fge0iccico  44512  gsumge0cl  44513  sge0z  44517  sge00  44518  sge0sn  44521  sge0tsms  44522  sge0cl  44523  sge0f1o  44524  sge0ge0  44526  sge0repnf  44528  sge0fsum  44529  sge0pr  44536  sge0ssre  44539  sge0prle  44543  sge0p1  44556  sge0iunmptlemre  44557  sge0rpcpnf  44563  sge0rernmpt  44564  sge0isum  44569  sge0ad2en  44573  sge0xaddlem2  44576  sge0uzfsumgt  44586  sge0seq  44588  sge0reuz  44589  voliunsge0lem  44614  meage0  44617  meassre  44619  meale0eq0  44620  meaiuninclem  44622  omessre  44652  omeiunltfirp  44661  carageniuncllem2  44664  carageniuncl  44665  omege0  44675  omess0  44676  hoiprodcl  44689  ovnlerp  44704  ovnf  44705  ovn0lem  44707  ovnsubaddlem1  44712  hoiprodcl3  44722  hoidmvcl  44724  hoidmv1lelem3  44735  hoidmvlelem5  44741  ovnhoilem1  44743  ovolval5lem1  44794  pimrecltneg  44866  mod42tp1mod8  45695  eenglngeehlnmlem1  46724  eenglngeehlnmlem2  46725  rrxsphere  46735  itscnhlinecirc02p  46772  iooii  46851  io1ii  46854  sepfsepc  46861  seppcld  46863
  Copyright terms: Public domain W3C validator