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

Theorem 0xr 9942
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 9939 . 2 ℝ ⊆ ℝ*
2 0re 9896 . 2 0 ∈ ℝ
31, 2sselii 3564 1 0 ∈ ℝ*
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  cr 9791  0cc0 9792  *cxr 9929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-xr 9934
This theorem is referenced by:  0lepnf  11802  ge0gtmnf  11836  max0sub  11860  xlt0neg1  11883  xlt0neg2  11884  xle0neg1  11885  xle0neg2  11886  xaddf  11888  xaddid1  11904  xaddid2  11905  xaddge0  11917  xsubge0  11920  xposdif  11921  xmullem  11923  xmullem2  11924  xmul01  11926  xmul02  11927  xmulneg1  11928  xmulf  11931  xmulpnf1  11933  xmulasslem2  11941  xmulge0  11943  xmulasslem  11944  xlemul1a  11947  xadddi  11954  xadddi2  11956  ioopos  12077  ioorebas  12102  xrge0neqmnf  12103  elxrge0  12108  0e0iccpnf  12110  xov1plusxeqvd  12145  ico01fl0  12437  rpsup  12482  addmodid  12535  hashgt0  12990  hashle00  13001  hashgt0elex  13002  sgn0  13623  sgnp  13624  sgnn  13628  fprodge0  14509  ef01bndlem  14699  sin01bnd  14700  cos01bnd  14701  cos1bnd  14702  sinltx  14704  sin01gt0  14705  cos01gt0  14706  sin02gt0  14707  sincos1sgn  14708  sincos2sgn  14709  halfleoddlt  14870  xrsmgm  19546  leordtval2  20768  pnfnei  20776  mnfnei  20777  psmetge0  21869  isxmet2d  21883  xmetge0  21900  xmetgt0  21914  prdsdsf  21923  prdsxmetlem  21924  xpsdsval  21937  blgt0  21955  xblss2ps  21957  xblss2  21958  xbln0  21970  prdsbl  22047  stdbdxmet  22071  stdbdmopn  22074  metustto  22109  metustid  22110  metustexhalf  22112  cfilucfil  22115  blval2  22118  metuel2  22121  nmoge0  22267  nmo0  22281  cnblcld  22320  blssioo  22338  blcvx  22341  xrsxmet  22352  metdsf  22390  metds0  22392  metdseq0  22396  metnrmlem1a  22400  iccpnfcnv  22482  iccpnfhmeo  22483  xrhmeo  22484  pcoass  22563  iscfil2  22790  ovolmge0  22969  ovolge0  22973  ovolf  22974  ovolssnul  22979  ovolctb  22982  ovoliunnul  22999  ovolicopnf  23016  voliunlem3  23044  volsup  23048  ioorf  23064  volivth  23098  vitalilem4  23103  vitalilem5  23104  itg2ge0  23225  itg2const2  23231  itg2seq  23232  itg2monolem1  23240  itg2monolem2  23241  itg2monolem3  23242  itg2gt0  23250  dvne0  23495  mdegle0  23558  ply1remlem  23643  ply1rem  23644  plypf1  23689  aaliou3lem2  23819  aaliou3lem3  23820  taylfvallem1  23832  taylfval  23834  tayl0  23837  radcnvcl  23892  radcnvle  23895  pserulm  23897  psercnlem1  23900  pilem2  23927  sinhalfpilem  23936  sincosq1lem  23970  sincosq1sgn  23971  sincosq2sgn  23972  tangtx  23978  tanabsge  23979  sinq12gt0  23980  cosq14gt0  23983  sincos4thpi  23986  pige3  23990  cosordlem  23998  tanord1  24004  tanord  24005  efifo  24014  argimgt0  24079  argimlt0  24080  logccv  24126  loglesqrt  24216  atantan  24367  rlimcnp  24409  rlimcnp2  24410  scvxcvx  24429  basellem1  24524  dchrisum0lem2a  24923  pntibndlem1  24995  pntibnd  24999  pntlemc  25001  pntlem3  25015  abvcxp  25021  padicabvf  25037  padicabvcxp  25038  ostth2  25043  ttgcontlem1  25483  nmooge0  26812  nmoo0  26836  nmlnogt0  26842  nmopge0  27960  nmopgt0  27961  nmfnge0  27976  nmop0  28035  nmfn0  28036  xraddge02  28717  xlt2addrd  28719  xrge0infss  28721  dfrp2  28728  elxrge02  28777  xrs0  28812  xrge00  28823  xrge0addass  28827  xrge0addgt0  28828  xrge0adddir  28829  fsumrp0cl  28832  metider  29071  unitssxrge0  29080  xrge0iifcnv  29113  xrge0iifcv  29114  xrge0iifiso  29115  xrge0iifhom  29117  xrge0mulc1cn  29121  pnfneige0  29131  lmxrge0  29132  esumgsum  29240  esumnul  29243  esum0  29244  esumle  29253  esumlef  29257  esumcst  29258  esumsnf  29259  esumpr2  29262  esumpinfval  29268  esumpinfsum  29272  esumpcvgval  29273  esumpmono  29274  hashf2  29279  esumcvg  29281  measle0  29404  voliune  29425  volfiniune  29426  ddemeas  29432  aean  29440  oms0  29492  prob01  29608  probmeasb  29625  dstfrvclim1  29672  sgncl  29733  sgn3da  29736  signsply0  29760  cvmliftlem10  30336  cvmliftlem13  30338  sinccvglem  30626  dnizeq0  31441  sin2h  32365  tan2h  32367  broucube  32409  mblfinlem2  32413  ovoliunnfl  32417  voliunnfl  32419  volsupnfl  32420  mbfposadd  32423  itg2addnclem2  32428  itg2gt0cn  32431  ftc1anclem5  32455  ftc1anclem8  32458  dvasin  32462  areacirc  32471  rrnequiv  32600  idomrootle  36588  imo72b2  37293  absfico  38201  xadd0ge  38274  xrge0nemnfd  38286  xralrple2  38308  pnfel0pnf  38398  ge0nemnf2  38399  ge0xrre  38402  sqrlearg  38424  fsumge0cl  38437  sinaover2ne0  38548  itgsin0pilem1  38638  iblsplit  38655  stoweidlem46  38736  fourierdlem43  38840  fourierdlem44  38841  fourierdlem60  38856  fourierdlem61  38857  fourierdlem87  38883  fourierdlem103  38899  fourierdlem104  38900  fourierdlem111  38907  sqwvfourb  38919  fourierswlem  38920  fouriersw  38921  etransclem23  38947  salexct2  39030  fge0npnf  39057  fge0iccico  39060  gsumge0cl  39061  sge0z  39065  sge00  39066  sge0sn  39069  sge0tsms  39070  sge0cl  39071  sge0f1o  39072  sge0ge0  39074  sge0repnf  39076  sge0fsum  39077  sge0pr  39084  sge0ssre  39087  sge0prle  39091  sge0p1  39104  sge0iunmptlemre  39105  sge0rpcpnf  39111  sge0rernmpt  39112  sge0isum  39117  sge0ad2en  39121  sge0xaddlem2  39124  sge0uzfsumgt  39134  sge0seq  39136  sge0reuz  39137  voliunsge0lem  39162  meage0  39165  meassre  39167  meale0eq0  39168  meaiuninclem  39170  omessre  39197  omeiunltfirp  39206  carageniuncllem2  39209  carageniuncl  39210  omege0  39220  omess0  39221  hoiprodcl  39234  ovnlerp  39249  ovnf  39250  ovn0lem  39252  ovnsubaddlem1  39257  hoiprodcl3  39267  hoidmvcl  39269  hoidmv1lelem3  39280  hoidmvlelem5  39286  ovnhoilem1  39288  ovolval5lem1  39339  pimrecltneg  39407  mod42tp1mod8  39855  xnn0xrge0  40198  xnn0xadd0  40210
  Copyright terms: Public domain W3C validator