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

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
StepHypRef Expression
1 ressxr 10674 . 2 ℝ ⊆ ℝ*
2 0re 10632 . 2 0 ∈ ℝ
31, 2sselii 3968 1 0 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  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 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-1cn 10584  ax-addrcl 10587  ax-rnegex 10597  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ral 3148  df-rex 3149  df-v 3502  df-un 3945  df-in 3947  df-ss 3956  df-xr 10668
This theorem is referenced by:  0lepnf  12517  ge0gtmnf  12555  max0sub  12579  xlt0neg1  12602  xlt0neg2  12603  xle0neg1  12604  xle0neg2  12605  xaddf  12607  xaddid1  12624  xaddid2  12625  xnn0xadd0  12630  xaddge0  12641  xsubge0  12644  xposdif  12645  xmullem  12647  xmullem2  12648  xmul01  12650  xmul02  12651  xmulneg1  12652  xmulf  12655  xmulpnf1  12657  xmulasslem2  12665  xmulge0  12667  xmulasslem  12668  xlemul1a  12671  xadddi  12678  xadddi2  12680  ioopos  12803  ioorebas  12829  xrge0neqmnf  12830  elxrge0  12835  0e0iccpnf  12837  xov1plusxeqvd  12874  xnn0xrge0  12881  ico01fl0  13179  rpsup  13224  addmodid  13277  hashgt0  13739  hashle00  13751  hashgt0elex  13752  hashgt23el  13775  sgn0  14438  sgnp  14439  sgnn  14443  fprodge0  15337  ef01bndlem  15527  sin01bnd  15528  cos01bnd  15529  cos1bnd  15530  sinltx  15532  sin01gt0  15533  cos01gt0  15534  sin02gt0  15535  sincos1sgn  15536  sincos2sgn  15537  halfleoddlt  15701  xrsmgm  20496  leordtval2  21736  pnfnei  21744  mnfnei  21745  psmetge0  22837  isxmet2d  22852  xmetge0  22869  xmetgt0  22883  prdsdsf  22892  prdsxmetlem  22893  xpsdsval  22906  blgt0  22924  xblss2ps  22926  xblss2  22927  xbln0  22939  prdsbl  23016  stdbdxmet  23040  stdbdmopn  23043  metustto  23078  metustid  23079  metustexhalf  23081  cfilucfil  23084  blval2  23087  metuel2  23090  nmoge0  23245  nmo0  23259  cnblcld  23298  blssioo  23318  blcvx  23321  xrsxmet  23332  metdsf  23371  metds0  23373  metdseq0  23377  metnrmlem1a  23381  iccpnfcnv  23463  iccpnfhmeo  23464  xrhmeo  23465  pcoass  23543  iscfil2  23784  ovolmge0  23993  ovolge0  23997  ovolf  23998  ovolssnul  24003  ovolctb  24006  ovoliunnul  24023  ovolicopnf  24040  voliunlem3  24068  volsup  24072  ioorf  24089  volivth  24123  vitalilem4  24127  vitalilem5  24128  itg2ge0  24251  itg2const2  24257  itg2seq  24258  itg2monolem1  24266  itg2monolem2  24267  itg2monolem3  24268  itg2gt0  24276  dvne0  24523  mdegle0  24586  ply1remlem  24671  ply1rem  24672  plypf1  24717  aaliou3lem2  24847  aaliou3lem3  24848  taylfvallem1  24860  taylfval  24862  tayl0  24865  radcnvcl  24920  radcnvle  24923  pserulm  24925  psercnlem1  24928  pilem2  24955  sinhalfpilem  24964  sincosq1lem  24998  sincosq1sgn  24999  sincosq2sgn  25000  tangtx  25006  tanabsge  25007  sinq12gt0  25008  cosq14gt0  25011  sincos4thpi  25014  pige3ALT  25020  cosordlem  25028  tanord1  25034  tanord  25035  efifo  25044  argimgt0  25108  argimlt0  25109  logccv  25159  loglesqrt  25252  atantan  25414  rlimcnp  25457  rlimcnp2  25458  scvxcvx  25477  basellem1  25572  dchrisum0lem2a  26007  pntibndlem1  26079  pntibnd  26083  pntlemc  26085  pntlem3  26099  abvcxp  26105  padicabvf  26121  padicabvcxp  26122  ostth2  26127  ttgcontlem1  26585  elntg2  26685  nmooge0  28458  nmoo0  28482  nmlnogt0  28488  nmopge0  29602  nmopgt0  29603  nmfnge0  29618  nmop0  29677  nmfn0  29678  xraddge02  30393  xlt2addrd  30395  xrge0infss  30397  dfrp2  30404  elxrge02  30522  xrs0  30576  xrge00  30587  xrge0addass  30591  xrge0addgt0  30592  xrge0adddir  30593  fsumrp0cl  30596  metider  31020  unitssxrge0  31029  xrge0iifcnv  31062  xrge0iifcv  31063  xrge0iifiso  31064  xrge0iifhom  31066  xrge0mulc1cn  31070  pnfneige0  31080  lmxrge0  31081  esumgsum  31190  esumnul  31193  esum0  31194  esumle  31203  esumlef  31207  esumcst  31208  esumsnf  31209  esumpr2  31212  esumpinfval  31218  esumpinfsum  31222  esumpcvgval  31223  esumpmono  31224  hashf2  31229  esumcvg  31231  measle0  31353  voliune  31374  volfiniune  31375  ddemeas  31381  aean  31389  oms0  31441  prob01  31557  probmeasb  31574  dstfrvclim1  31621  sgncl  31682  sgn3da  31685  signsply0  31707  chtvalz  31786  hgt750lemf  31810  cvmliftlem10  32425  cvmliftlem13  32427  sinccvglem  32799  dnizeq0  33698  sin2h  34749  tan2h  34751  broucube  34793  mblfinlem2  34797  ovoliunnfl  34801  voliunnfl  34803  volsupnfl  34804  mbfposadd  34806  itg2addnclem2  34811  itg2gt0cn  34814  ftc1anclem5  34838  ftc1anclem8  34841  dvasin  34845  areacirc  34854  rrnequiv  34981  idomrootle  39660  imo72b2  40391  absfico  41346  xadd0ge  41453  xrge0nemnfd  41465  xralrple2  41487  xrpnf  41627  pnfel0pnf  41669  ge0xrre  41672  sqrlearg  41694  fsumge0cl  41719  limsup10ex  41919  liminf10ex  41920  sinaover2ne0  42014  itgsin0pilem1  42100  iblsplit  42116  stoweidlem46  42197  fourierdlem43  42301  fourierdlem44  42302  fourierdlem60  42317  fourierdlem61  42318  fourierdlem87  42344  fourierdlem103  42360  fourierdlem104  42361  fourierdlem111  42368  sqwvfourb  42380  fourierswlem  42381  fouriersw  42382  etransclem23  42408  salexct2  42488  fge0npnf  42515  fge0iccico  42518  gsumge0cl  42519  sge0z  42523  sge00  42524  sge0sn  42527  sge0tsms  42528  sge0cl  42529  sge0f1o  42530  sge0ge0  42532  sge0repnf  42534  sge0fsum  42535  sge0pr  42542  sge0ssre  42545  sge0prle  42549  sge0p1  42562  sge0iunmptlemre  42563  sge0rpcpnf  42569  sge0rernmpt  42570  sge0isum  42575  sge0ad2en  42579  sge0xaddlem2  42582  sge0uzfsumgt  42592  sge0seq  42594  sge0reuz  42595  voliunsge0lem  42620  meage0  42623  meassre  42625  meale0eq0  42626  meaiuninclem  42628  omessre  42658  omeiunltfirp  42667  carageniuncllem2  42670  carageniuncl  42671  omege0  42681  omess0  42682  hoiprodcl  42695  ovnlerp  42710  ovnf  42711  ovn0lem  42713  ovnsubaddlem1  42718  hoiprodcl3  42728  hoidmvcl  42730  hoidmv1lelem3  42741  hoidmvlelem5  42747  ovnhoilem1  42749  ovolval5lem1  42800  pimrecltneg  42867  mod42tp1mod8  43599  eenglngeehlnmlem1  44556  eenglngeehlnmlem2  44557  rrxsphere  44567  itscnhlinecirc02p  44604
  Copyright terms: Public domain W3C validator