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

Theorem 0re 8883
Description:  0 is a real number. See also 0reALT 9188. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
0re  |-  0  e.  RR

Proof of Theorem 0re
StepHypRef Expression
1 1re 8882 . 2  |-  1  e.  RR
2 ax-rnegex 8853 . 2  |-  ( 1  e.  RR  ->  E. x  e.  RR  ( 1  +  x )  =  0 )
3 readdcl 8865 . . . . 5  |-  ( ( 1  e.  RR  /\  x  e.  RR )  ->  ( 1  +  x
)  e.  RR )
41, 3mpan 651 . . . 4  |-  ( x  e.  RR  ->  (
1  +  x )  e.  RR )
5 eleq1 2376 . . . 4  |-  ( ( 1  +  x )  =  0  ->  (
( 1  +  x
)  e.  RR  <->  0  e.  RR ) )
64, 5syl5ibcom 211 . . 3  |-  ( x  e.  RR  ->  (
( 1  +  x
)  =  0  -> 
0  e.  RR ) )
76rexlimiv 2695 . 2  |-  ( E. x  e.  RR  (
1  +  x )  =  0  ->  0  e.  RR )
81, 2, 7mp2b 9 1  |-  0  e.  RR
Colors of variables: wff set class
Syntax hints:    = wceq 1633    e. wcel 1701   E.wrex 2578  (class class class)co 5900   RRcr 8781   0cc0 8782   1c1 8783    + caddc 8785
This theorem is referenced by:  0xr  8923  axmulgt0  8942  ne0gt0  8970  00id  9032  mul02lem1  9033  mul02lem2  9034  mul02  9035  addid1  9037  gt0ne0  9284  addgt0  9305  addgegt0  9306  addgtge0  9307  addge0  9308  ltaddpos  9309  ltneg  9319  leneg  9322  lt0neg1  9325  lt0neg2  9326  le0neg1  9327  le0neg2  9328  addge01  9329  add20  9331  subge0  9332  suble0  9333  lesub0  9335  mulge0  9336  msqgt0  9339  msqge0  9340  0le1  9342  gt0ne0i  9353  gt0ne0d  9382  lt0ne0d  9383  addgt0d  9392  elimge0  9638  ltm1  9641  recgt0  9645  prodgt0  9646  prodge0  9648  lemul1a  9655  ltmul12a  9657  lemul12a  9659  mulgt1  9660  gt0div  9667  ge0div  9668  lt2msq1  9684  lediv12a  9694  recgt1i  9698  recreclt  9700  ledivp1  9703  squeeze0  9704  recgt0ii  9707  ledivp1i  9727  ltdivp1i  9728  fimaxre2  9747  supmul1  9764  supmul  9767  inelr  9781  crne0  9784  nnge1  9817  nngt0  9820  nnrecgt0  9828  0le0  9872  nn0ssre  10016  nn0ge0  10038  nn0nlt0  10039  nn0le0eq0  10041  elnnnn0b  10055  elnnnn0c  10056  nn0sub  10061  elnnz  10081  0z  10082  elnn0z  10083  elnnz1  10096  nn0lt10b  10125  recnz  10134  gtndiv  10136  uzindOLD  10153  fnn0ind  10158  rpge0  10413  rpgecl  10426  ge0p1rp  10429  rpneg  10430  0nrp  10431  ge0gtmnf  10548  max0sub  10570  qsqueeze  10575  xneg0  10586  xaddid1  10613  xsubge0  10628  xmulpnf1  10641  xmulgt0  10650  xlemul1a  10655  xadddi  10662  xrsupsslem  10672  xrinfmsslem  10673  elrege0  10793  0elunit  10801  1elunit  10802  lincmb01cmp  10824  iccf1o  10825  xov1plusxeqvd  10827  unitssre  10828  rpsup  11017  0mod  11042  1mod  11043  expgt1  11187  ltexp2a  11200  expcan  11201  ltexp2  11202  leexp2  11203  leexp2a  11204  expubnd  11209  le2sq2  11226  sqlecan  11256  bernneq2  11275  expnbnd  11277  expnlbnd  11278  expnlbnd2  11279  expmulnbnd  11280  discr1  11284  discr  11285  facdiv  11347  faclbnd  11350  faclbnd3  11352  faclbnd6  11359  bcval4  11367  bcval5  11377  bcpasc  11380  hasheq0  11400  reim0  11650  re0  11684  im0  11685  rei  11688  imi  11689  cj0  11690  sqeqd  11698  rennim  11771  cnpart  11772  sqr0lem  11773  sqrlem4  11778  resqrex  11783  sqrgt0  11791  sqr00  11796  sqrneglem  11799  sqr4  11805  sqr9  11806  sqr2gt1lt2  11807  leabs  11831  absor  11832  max0add  11842  absgt0  11855  sqreulem  11890  eqsqr2d  11899  amgm2  11900  sqrpclii  11913  rlimconst  12065  rlimrege0  12100  lo1mul  12148  iserge0  12181  iseraltlem2  12202  fsumrecl  12254  fsumge0  12300  fsum00  12303  o1fsum  12318  cvgcmp  12321  cvgcmpce  12323  isumless  12351  arisum2  12366  georeclim  12375  geo2sum  12376  geo2lim  12378  geomulcvg  12379  geoisumr  12381  0.999...  12384  cvgrat  12386  mertenslem2  12388  efcllem  12406  ege2le3  12418  cos0  12477  ef01bndlem  12511  sin01bnd  12512  cos01bnd  12513  cos2bnd  12515  sin01gt0  12517  cos01gt0  12518  sincos2sgn  12521  sin4lt0  12522  absef  12524  absefib  12525  efieq1re  12526  epos  12532  znnenlem  12537  rpnnen2lem2  12541  rpnnen2lem3  12542  rpnnen2lem4  12543  rpnnen2lem9  12548  rpnnen2  12551  rpnnen  12552  ruclem6  12560  nthruz  12577  moddvds  12585  dvdslelem  12620  divalglem1  12640  divalglem5  12643  divalglem6  12644  bitsp1o  12671  bitsinv1lem  12679  sadcaddlem  12695  sadcadd  12696  gcdn0gt0  12748  nn0seqcvgd  12787  algcvgblem  12794  algcvga  12796  qnumgt0  12868  pythagtriplem12  12926  pythagtriplem13  12927  pythagtriplem14  12928  pythagtriplem16  12930  qexpz  12996  prmreclem4  13013  prmreclem5  13014  prmreclem6  13015  1arith  13021  4sqlem6  13037  vdwap0  13070  ramz  13119  mulgnegnn  14626  subgmulg  14684  isabvd  15634  abvf  15637  abvtrivd  15654  psrbaglesupp  16163  xrs1mnd  16465  xrs10  16466  rege0subm  16484  gzrngunit  16493  leordtval2  16998  pnfnei  17006  mnfnei  17007  prdsmet  17986  imasdsf1olem  17989  ssbl  18023  xmeter  18031  dscmet  18147  dscopn  18148  nlmvscnlem2  18248  nlmvscnlem1  18249  nmoi  18289  nmo0  18296  nmoeq0  18297  0nghm  18302  idnghm  18304  cnbl0  18335  blcvx  18356  xrsxmet  18367  metdseq0  18410  iitopon  18435  dfii2  18438  dfii3  18439  dfii5  18441  iicmp  18442  iicon  18443  iirev  18480  iirevcn  18481  iihalf1  18482  iihalf1cn  18483  iihalf2  18484  iihalf2cn  18485  elii1  18486  elii2  18487  iimulcl  18488  iimulcn  18489  icchmeo  18492  icopnfcnv  18493  icopnfhmeo  18494  iccpnfcnv  18495  iccpnfhmeo  18496  xrhmeo  18497  xrhmph  18498  icccvx  18501  evth  18510  lebnumlem1  18512  lebnumii  18517  htpycc  18531  reparphti  18548  pcoval1  18564  pco0  18565  pcoval2  18567  pcocn  18568  pcohtpylem  18570  pcopt  18573  pcopt2  18574  pcoass  18575  pcorevlem  18577  pcorev2  18579  pi1xfrcnv  18608  nmoleub2lem3  18649  cphsqrcl  18673  ipcnlem2  18724  ipcnlem1  18725  minveclem4c  18842  minveclem2  18843  minveclem3b  18845  minveclem4  18849  minveclem6  18851  minveclem7  18852  pjthlem1  18854  cniccbdd  18874  ovollb2lem  18900  ovollb2  18901  ovolunlem1a  18908  ovolunlem1  18909  ovolunnul  18912  ovoliunlem1  18914  ovoliunnul  18919  ovolicc1  18928  ovolicc2lem4  18932  ovolicopnf  18936  ovolre  18937  voliunlem3  18962  volsup  18966  ioombl1lem2  18969  ioombl1lem4  18971  iccvolcl  18977  ovolioo  18978  ioorcl2  18980  ioorcl  18985  uniioombllem1  18989  uniioombllem2  18991  uniioombllem3  18993  uniioombllem6  18996  volivth  19015  vitalilem1  19016  vitalilem2  19017  vitalilem4  19019  vitalilem5  19020  vitali  19021  ismbf  19038  mbfmulc2lem  19055  mbfpos  19059  mbfposr  19060  0plef  19080  i1f0  19095  i1f1  19098  itg1addlem2  19105  itg1addlem4  19107  itg1addlem5  19108  i1fmulc  19111  itg1mulc  19112  itg1ge0a  19119  mbfi1fseqlem3  19125  mbfi1fseqlem4  19126  mbfi1fseqlem5  19127  mbfi1fseqlem6  19128  mbfi1flimlem  19130  mbfi1flim  19131  xrge0f  19139  itg2ge0  19143  itg2const  19148  itg2seq  19150  itg2mulclem  19154  itg2mulc  19155  itg2splitlem  19156  itg2split  19157  itg2monolem1  19158  itg2monolem2  19159  itg2monolem3  19160  itg2mono  19161  itg2i1fseq  19163  itg2gt0  19168  itg2cnlem1  19169  itg2cnlem2  19170  ibl0  19194  iblrelem  19198  iblposlem  19199  iblpos  19200  iblre  19201  itgreval  19204  itgneg  19211  iblss  19212  i1fibl  19215  itgitg1  19216  itgle  19217  itgge0  19218  itgeqa  19221  itgless  19224  iblconst  19225  itgconst  19226  ibladdlem  19227  itgaddlem1  19230  itgaddlem2  19231  iblabslem  19235  iblabs  19236  iblabsr  19237  iblmulc2  19238  itgmulc2lem1  19239  itgmulc2lem2  19240  itgabs  19242  itgsplit  19243  bddmulibl  19246  itggt0  19249  itgcn  19250  dvferm1  19385  dvferm2  19387  dvferm  19388  dvlip  19393  dvlipcn  19394  c1lip1  19397  dveq0  19400  dv11cn  19401  dvlt0  19405  dvne0  19411  dvfsumge  19422  ftc1lem4  19439  deg1lt0  19530  ply1divex  19575  plypf1  19647  dgradd2  19702  dgrco  19709  plyrecj  19713  plydivlem3  19728  vieta1lem2  19744  aalioulem2  19766  aalioulem3  19767  mtest  19834  radcnvlem1  19842  radcnv0  19845  radcnvlt1  19847  radcnvle  19849  pserulm  19851  psercnlem2  19853  psercnlem1  19854  psercn  19855  pserdvlem1  19856  pserdv  19858  abelthlem2  19861  abelthlem6  19865  abelthlem7  19867  abelth  19870  abelth2  19871  reeff1olem  19875  reeff1o  19876  pilem2  19881  pilem3  19882  pipos  19886  sinhalfpilem  19887  sincosq1sgn  19919  sincosq2sgn  19920  coseq00topi  19923  coseq0negpitopi  19924  tangtx  19926  tanabsge  19927  sinq12ge0  19929  sinq34lt0t  19930  cosq14ge0  19932  sincos4thpi  19934  tan4thpi  19935  sincos6thpi  19936  pige3  19938  sineq0  19942  cosordlem  19946  cosord  19947  cos11  19948  sinord  19949  recosf1o  19950  resinf1o  19951  tanord1  19952  tanord  19953  tanregt0  19954  efif1olem4  19960  efifo  19962  relogrn  19972  log1  19992  logneg  19994  logne0  20009  rplogcl  20011  argregt0  20017  argrege0  20018  argimgt0  20019  logneg2  20022  logdivlti  20024  logdivlt  20025  logdivle  20026  ellogdm  20039  logdmn0  20040  logdmnrp  20041  logcnlem3  20044  logcnlem4  20045  dvloglem  20048  logdmopn  20049  logf1o2  20050  dvlog2lem  20052  efopnlem1  20056  logtayl  20060  recxpcl  20075  cxpge0  20083  abscxp2  20093  cxplt  20094  cxple  20095  cxple2  20097  cxple2a  20099  cxpsqrlem  20102  cxpcn3lem  20140  cxpcn3  20141  cxpaddlelem  20144  cxpaddle  20145  abscxpbnd  20146  loglesqr  20151  ang180lem3  20162  ang180lem4  20163  chordthmlem4  20185  chordthmlem5  20186  asinlem3  20220  atanre  20234  asinneg  20235  asin1  20243  reasinsin  20245  acosbnd  20249  atan0  20257  atanrecl  20260  atanlogaddlem  20262  atanlogadd  20263  atanlogsublem  20264  atanlogsub  20265  atantan  20272  atanbnd  20275  atan1  20277  atans2  20280  ressatans  20283  leibpi  20291  log2cnv  20293  log2tlbnd  20294  log2ublem3  20297  log2ub  20298  rlimcnp  20313  rlimcnp2  20314  rlimcnp3  20315  efrlim  20317  o1cxp  20322  cxp2limlem  20323  cxp2lim  20324  cxploglim2  20326  divsqrsumlem  20327  cvxcl  20332  scvxcvx  20333  jensenlem1  20334  jensenlem2  20335  jensen  20336  amgm  20338  emgt0  20353  harmonicbnd3  20354  harmoniclbnd  20355  harmonicubnd  20356  harmonicbnd4  20357  fsumharmonic  20358  ftalem1  20363  ftalem2  20364  ftalem5  20367  basellem3  20373  basellem8  20378  efnnfsumcl  20393  ppisval  20394  vmacl  20409  vmage0  20412  chpge0  20417  chtwordi  20447  efchtdvds  20450  ppiwordi  20453  chtrpcl  20466  ppiltx  20468  fsumfldivdiaglem  20482  ppiub  20496  chpeq0  20500  chteq0  20501  chtleppi  20502  fsumvma2  20506  chpval2  20510  chpchtsum  20511  chpub  20512  logfacbnd3  20515  logexprlim  20517  mersenne  20519  dchr1re  20555  bcmono  20569  efexple  20573  bposlem1  20576  bposlem4  20579  bposlem5  20580  bposlem7  20582  bposlem8  20583  bposlem9  20584  lgslem4  20591  lgsval2lem  20598  lgsval4a  20610  lgsneg  20611  lgsdilem  20614  lgsdir2lem1  20615  lgsne0  20625  lgseisen  20645  lgsquadlem1  20646  lgsquadlem2  20647  m1lgs  20654  2sqlem11  20667  chebbnd1lem2  20672  chebbnd1lem3  20673  chebbnd1  20674  chtppilimlem1  20675  chtppilimlem2  20676  chtppilim  20677  chebbnd2  20679  chto1lb  20680  chpchtlim  20681  chpo1ub  20682  rplogsumlem2  20687  rpvmasumlem  20689  dchrisumlema  20690  dchrisumlem2  20692  dchrisumlem3  20693  dchrmusumlema  20695  dchrvmasumlem2  20700  dchrvmasumiflem1  20703  dchrisum0flblem1  20710  dchrisum0flblem2  20711  dchrisum0fno1  20713  dchrisum0re  20715  dchrisum0lema  20716  dchrisum0  20722  rplogsum  20729  dirith2  20730  logdivsum  20735  mulog2sumlem1  20736  mulog2sumlem2  20737  vmalogdivsum2  20740  log2sumbnd  20746  selberg2lem  20752  chpdifbndlem1  20755  chpdifbndlem2  20756  chpdifbnd  20757  logdivbnd  20758  selberg3lem1  20759  pntrmax  20766  pntrsumo1  20767  pntrlog2bndlem4  20782  pntrlog2bndlem5  20783  pntpbnd1a  20787  pntpbnd1  20788  pntpbnd2  20789  pntlemg  20800  pntlemj  20805  pntlemk  20808  pntlem3  20811  pntleml  20813  pnt2  20815  pnt  20816  ostth2lem1  20820  padicabv  20832  padicabvcxp  20834  ostth2lem3  20837  ostth2lem4  20838  ostth2  20839  ostth3  20840  ex-po  20875  gxnval  20980  readdsubgo  21073  nvz0  21289  ipidsq  21341  0blo  21425  nmlno0lem  21426  nmblolbii  21432  siilem2  21485  minvecolem2  21509  minvecolem3  21510  minvecolem4c  21513  minvecolem4  21514  minvecolem5  21515  minvecolem6  21516  minvecolem7  21517  htthlem  21552  hiidge0  21732  normlem6  21749  normgt0  21761  norm-i  21763  normpyc  21780  normpar2i  21790  bcsiALT  21813  pjhthlem1  22025  pjneli  22357  0bdop  22628  nmlnop0iALT  22630  unopbd  22650  nmbdoplbi  22659  nmcoplbi  22663  nmbdfnlbi  22684  nmbdfnlb  22685  nmcfnlbi  22687  cnlnadjlem7  22708  nmopcoi  22730  branmfn  22740  leopmul  22769  nmopleid  22774  pjbdlni  22784  pjnormssi  22803  stcl  22851  stge0  22859  stle1  22860  stle0i  22874  strlem3a  22887  cdj3lem1  23069  xlt2addrd  23270  bcm1n  23298  xdiv0  23327  xaddeq0  23339  xrge00  23346  xrge0neqmnf  23350  xrge0adddir  23353  fsumrp0cl  23355  unitsscn  23363  elunitrn  23364  elunitge0  23366  unitdivcld  23368  sqsscirc1  23375  xrge0iifcnv  23388  xrge0iifiso  23390  xrge0iifhom  23392  xrge0mulc1cn  23396  lmlimxrge0  23403  rge0scvg  23404  pnfneige0  23405  lmxrge0  23406  lmdvg  23407  metustexhalf  23498  re0g  23530  recusp  23535  rnlogblem  23591  logbrec  23597  log2le1  23599  esumfsupre  23637  esumpfinvallem  23640  esumpfinval  23641  esumpfinvalf  23642  esumpcvgval  23644  esumcvg  23652  measinb  23749  voliune  23759  volfiniune  23760  indf  23828  indfval  23829  pr01ssre  23830  indf1o  23836  probvalrnd  23856  probmeasb  23862  cndprobprob  23870  0rrv  23883  coinfliprv  23914  ballotlem2  23920  ballotlemfc0  23924  ballotlemfcc  23925  ballotlemodife  23929  ballotlem4  23930  ballotlemi1  23934  ballotlemic  23938  zetacvg  23973  eldmgm  23978  cvxpcon  24057  cvxscon  24058  rescon  24061  iiscon  24067  iillyscon  24068  cvmliftlem2  24101  cvmliftlem8  24107  cvmliftlem10  24109  konigsberg  24195  snmlff  24196  divelunit  24366  mulge0b  24372  relin01  24375  fz0n  24383  4bc2eq6  24385  brbtwn2  24919  axsegconlem7  24937  axsegconlem10  24940  ax5seglem1  24942  ax5seglem2  24943  ax5seglem3  24945  ax5seglem5  24947  ax5seglem6  24948  ax5seglem9  24951  ax5seg  24952  axbtwnid  24953  axpaschlem  24954  axpasch  24955  axlowdimlem1  24956  axlowdimlem6  24961  axlowdimlem7  24962  axlowdimlem10  24965  axlowdim1  24973  axlowdim2  24974  axlowdim  24975  axeuclidlem  24976  axcontlem2  24979  axcontlem4  24981  axcontlem7  24984  axcontlem10  24987  bpoly0  25171  bpoly4  25180  ovoliunnfl  25315  itg2addnclem  25317  itg2addnclem2  25318  itg2addnc  25319  ibladdnclem  25321  itgaddnclem1  25323  itgaddnclem2  25324  iblabsnclem  25328  iblabsnc  25329  iblmulc2nc  25330  itgmulc2nclem1  25331  itgmulc2nclem2  25332  itgabsnc  25334  bddiblnc  25335  itggt0cn  25337  ftc1cnnclem  25338  dvreasin  25340  areacirclem2  25342  areacirclem3  25343  areacirclem4  25344  areacirclem5  25346  areacirc  25348  nn0prpwlem  25387  geomcau  25624  isbnd3  25656  isbnd3b  25657  ssbnd  25660  prdsbnd  25665  bfplem2  25695  bfp  25696  rrnequiv  25707  modelico  26054  irrapxlem1  26055  irrapxlem2  26056  irrapxlem3  26057  irrapxlem4  26058  pellexlem6  26067  pell14qrgt0  26092  elpell14qr2  26095  pell1qrgaplem  26106  pellfundex  26119  pellfundrp  26121  monotoddzzfi  26175  oddcomabszz  26177  zindbi  26179  jm2.24  26198  acongeq  26218  jm2.23  26237  jm2.26lem3  26242  jm3.1lem3  26260  hbtlem5  26480  dvconstbi  26699  ioovolcl  26890  itgsin0pilem1  26892  itgsinexplem1  26896  itgsinexp  26897  stoweidlem1  26898  stoweidlem3  26900  stoweidlem7  26904  stoweidlem11  26908  stoweidlem17  26914  stoweidlem25  26922  stoweidlem26  26923  stoweidlem34  26931  stoweidlem36  26933  stoweidlem38  26935  stoweidlem41  26938  stoweidlem42  26939  stoweidlem44  26941  stoweidlem45  26942  stoweidlem55  26952  stoweid  26960  wallispilem1  26962  wallispilem2  26963  wallispilem3  26964  wallispilem4  26965  wallispi  26967  wallispi2lem1  26968  wallispi2lem2  26969  wallispi2  26970  stirlinglem1  26971  stirlinglem3  26973  stirlinglem4  26974  stirlinglem5  26975  stirlinglem6  26976  stirlinglem7  26977  stirlinglem8  26978  stirlinglem10  26980  stirlinglem11  26981  stirlinglem12  26982  stirlinglem13  26983  stirlinglem14  26984  stirlinglem15  26985  stirlingr  26987  sharhght  27003  elfznelfzo  27275  hashgt12el  27280  hashgt12el2  27281  usgraexvlem  27360  usgraex0elv  27361  spthispth  27475  nvnencycllem  27527  vdgre0  27568  ex-gt  27647  sgnpnf  27699  sgnmnf  27701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-i2m1 8850  ax-1ne0 8851  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903
  Copyright terms: Public domain W3C validator