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

Theorem 0xr 9064
Description: Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.)
Assertion
Ref Expression
0xr  |-  0  e.  RR*

Proof of Theorem 0xr
StepHypRef Expression
1 ressxr 9062 . 2  |-  RR  C_  RR*
2 0re 9024 . 2  |-  0  e.  RR
31, 2sselii 3288 1  |-  0  e.  RR*
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   RRcr 8922   0cc0 8923   RR*cxr 9052
This theorem is referenced by:  nn0pnfge0  10660  ge0gtmnf  10692  max0sub  10714  xlt0neg1  10737  xlt0neg2  10738  xle0neg1  10739  xle0neg2  10740  xaddf  10742  xaddid1  10757  xaddid2  10758  xaddge0  10769  xsubge0  10772  xposdif  10773  xmullem  10775  xmullem2  10776  xmul01  10778  xmul02  10779  xmulneg1  10780  xmulf  10783  xmulpnf1  10785  xmulasslem2  10793  xmulge0  10795  xmulasslem  10796  xlemul1a  10799  xadddi  10806  xadddi2  10808  ioopos  10919  ioorebas  10938  elxrge0  10940  xov1plusxeqvd  10973  rpsup  11174  hashgt0  11589  hashle00  11596  hashgt0elex  11597  ef01bndlem  12712  sin01bnd  12713  cos01bnd  12714  cos1bnd  12715  sinltx  12717  sin01gt0  12718  cos01gt0  12719  sin02gt0  12720  sincos1sgn  12721  sincos2sgn  12722  pcge0  13162  xrge0subm  16662  leordtval2  17198  pnfnei  17206  mnfnei  17207  isxmet2d  18266  xmetge0  18283  xmetgt0  18296  prdsdsf  18305  prdsxmetlem  18306  xpsdsval  18319  blgt0  18330  xblss2  18332  xbln0  18339  prdsbl  18411  stdbdxmet  18435  stdbdmopn  18438  metustto  18473  metustid  18474  metustexhalf  18476  cfilucfil  18479  blval2  18482  metuel2  18485  nmoge0  18626  nmo0  18640  cnblcld  18680  blssioo  18697  blcvx  18700  xrsxmet  18711  metdsf  18749  metds0  18751  metdseq0  18755  metnrmlem1a  18759  iccpnfcnv  18840  iccpnfhmeo  18841  xrhmeo  18842  pcoass  18920  iscfil2  19090  ovolmge0  19240  ovolge0  19244  ovolf  19245  ovolssnul  19250  ovolctb  19253  ovoliunnul  19270  ovolicopnf  19287  voliunlem3  19313  volsup  19317  ioorf  19332  volivth  19366  vitalilem4  19370  vitalilem5  19371  itg2ge0  19494  itg2const2  19500  itg2seq  19501  itg2splitlem  19507  itg2split  19508  itg2monolem1  19509  itg2monolem2  19510  itg2monolem3  19511  itg2gt0  19519  itg2cnlem2  19521  itg2cn  19522  iblss  19563  itgle  19568  itgeqa  19572  ibladdlem  19578  iblabs  19587  iblabsr  19588  iblmulc2  19589  bddmulibl  19597  dvne0  19762  mdegle0  19867  ply1remlem  19952  ply1rem  19953  plypf1  19998  aaliou3lem2  20127  aaliou3lem3  20128  taylfvallem1  20140  taylfval  20142  tayl0  20145  radcnvcl  20200  radcnvle  20203  pserulm  20205  psercnlem1  20208  pilem2  20235  sinhalfpilem  20241  sincosq1lem  20272  sincosq1sgn  20273  sincosq2sgn  20274  tangtx  20280  tanabsge  20281  sinq12gt0  20282  cosq14gt0  20285  sincos4thpi  20288  pige3  20292  cosordlem  20300  tanord1  20306  tanord  20307  efifo  20316  argimgt0  20374  argimlt0  20375  logccv  20421  loglesqr  20509  atantan  20630  rlimcnp  20671  rlimcnp2  20672  rlimcnp3  20673  scvxcvx  20691  basellem1  20730  dchrisum0lem2a  21078  pntibndlem1  21150  pntibnd  21154  pntlemc  21156  pntlem3  21170  abvcxp  21176  padicabvf  21192  padicabvcxp  21193  ostth2  21198  nmooge0  22116  nmoo0  22140  nmlnogt0  22146  nmopge0  23262  nmopgt0  23263  nmfnge0  23278  nmop0  23337  nmfn0  23338  xraddge02  23959  xlt2addrd  23960  elxrge02  24017  xrs0  24031  xrge00  24037  xrge0addass  24040  xrge0neqmnf  24041  xrge0addgt0  24043  xrge0adddir  24044  fsumrp0cl  24046  unitssxrge0  24102  xrge0iifcnv  24123  xrge0iifcv  24124  xrge0iifiso  24125  xrge0iifhom  24127  xrge0mulc1cn  24131  pnfneige0  24140  lmxrge0  24141  esumnul  24239  esum0  24240  esumle  24245  esumlef  24250  esumcst  24251  esumsn  24252  esumpr2  24254  esumpinfval  24259  esumpfinvallem  24260  esumpinfsum  24263  esumpcvgval  24264  esumpmono  24265  esummulc1  24267  hashf2  24270  esumcvg  24272  measle0  24356  voliune  24379  volfiniune  24380  aean  24389  prob01  24450  probmeasb  24467  dstfrvclim1  24514  cvmliftlem10  24760  cvmliftlem13  24762  sinccvglem  24888  ovoliunnfl  25953  voliunnfl  25955  volsupnfl  25956  itg2addnclem  25957  itg2addnclem2  25958  itg2gt0cn  25960  ibladdnclem  25961  itgaddnclem2  25964  iblabsnc  25969  iblmulc2nc  25970  bddiblnc  25975  dvreasin  25980  areacirc  25988  rrnequiv  26235  idomrootle  27180  itgsin0pilem1  27412  stoweidlem46  27463  sgn0  27865  sgnp  27866  sgnn  27870
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-1cn 8981  ax-icn 8982  ax-addcl 8983  ax-addrcl 8984  ax-mulcl 8985  ax-mulrcl 8986  ax-i2m1 8991  ax-1ne0 8992  ax-rnegex 8994  ax-rrecex 8995  ax-cnre 8996
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023  df-xr 9057
  Copyright terms: Public domain W3C validator