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

Theorem 0re 8854
Description:  0 is a real number. See also 0reALT 9159. (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 8853 . 2  |-  1  e.  RR
2 ax-rnegex 8824 . 2  |-  ( 1  e.  RR  ->  E. x  e.  RR  ( 1  +  x )  =  0 )
3 readdcl 8836 . . . . 5  |-  ( ( 1  e.  RR  /\  x  e.  RR )  ->  ( 1  +  x
)  e.  RR )
41, 3mpan 651 . . . 4  |-  ( x  e.  RR  ->  (
1  +  x )  e.  RR )
5 eleq1 2356 . . . 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 2674 . 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 1632    e. wcel 1696   E.wrex 2557  (class class class)co 5874   RRcr 8752   0cc0 8753   1c1 8754    + caddc 8756
This theorem is referenced by:  0xr  8894  axmulgt0  8913  ne0gt0  8941  00id  9003  mul02lem1  9004  mul02lem2  9005  mul02  9006  addid1  9008  gt0ne0  9255  addgt0  9276  addgegt0  9277  addgtge0  9278  addge0  9279  ltaddpos  9280  ltneg  9290  leneg  9293  lt0neg1  9296  lt0neg2  9297  le0neg1  9298  le0neg2  9299  addge01  9300  add20  9302  subge0  9303  suble0  9304  lesub0  9306  mulge0  9307  msqgt0  9310  msqge0  9311  0le1  9313  gt0ne0i  9324  gt0ne0d  9353  lt0ne0d  9354  addgt0d  9363  elimge0  9609  ltm1  9612  recgt0  9616  prodgt0  9617  prodge0  9619  lemul1a  9626  ltmul12a  9628  lemul12a  9630  mulgt1  9631  gt0div  9638  ge0div  9639  lt2msq1  9655  lediv12a  9665  recgt1i  9669  recreclt  9671  ledivp1  9674  squeeze0  9675  recgt0ii  9678  ledivp1i  9698  ltdivp1i  9699  fimaxre2  9718  supmul1  9735  supmul  9738  inelr  9752  crne0  9755  nnge1  9788  nngt0  9791  nnrecgt0  9799  0le0  9843  nn0ssre  9985  nn0ge0  10007  nn0nlt0  10008  nn0le0eq0  10010  elnnnn0b  10024  elnnnn0c  10025  nn0sub  10030  elnnz  10050  0z  10051  elnn0z  10052  elnnz1  10065  nn0lt10b  10094  recnz  10103  gtndiv  10105  uzindOLD  10122  fnn0ind  10127  rpge0  10382  rpgecl  10395  ge0p1rp  10398  rpneg  10399  0nrp  10400  ge0gtmnf  10517  max0sub  10539  qsqueeze  10544  xneg0  10555  xaddid1  10582  xsubge0  10597  xmulpnf1  10610  xmulgt0  10619  xlemul1a  10624  xadddi  10631  xrsupsslem  10641  xrinfmsslem  10642  elrege0  10762  0elunit  10770  1elunit  10771  lincmb01cmp  10793  iccf1o  10794  xov1plusxeqvd  10796  unitssre  10797  rpsup  10986  0mod  11011  1mod  11012  expgt1  11156  ltexp2a  11169  expcan  11170  ltexp2  11171  leexp2  11172  leexp2a  11173  expubnd  11178  le2sq2  11195  sqlecan  11225  bernneq2  11244  expnbnd  11246  expnlbnd  11247  expnlbnd2  11248  expmulnbnd  11249  discr1  11253  discr  11254  facdiv  11316  faclbnd  11319  faclbnd3  11321  faclbnd6  11328  bcval4  11336  bcval5  11346  bcpasc  11349  hasheq0  11369  reim0  11619  re0  11653  im0  11654  rei  11657  imi  11658  cj0  11659  sqeqd  11667  rennim  11740  cnpart  11741  sqr0lem  11742  sqrlem4  11747  resqrex  11752  sqrgt0  11760  sqr00  11765  sqrneglem  11768  sqr4  11774  sqr9  11775  sqr2gt1lt2  11776  leabs  11800  absor  11801  max0add  11811  absgt0  11824  sqreulem  11859  eqsqr2d  11868  amgm2  11869  sqrpclii  11882  rlimconst  12034  rlimrege0  12069  lo1mul  12117  iserge0  12150  iseraltlem2  12171  fsumrecl  12223  fsumge0  12269  fsum00  12272  o1fsum  12287  cvgcmp  12290  cvgcmpce  12292  isumless  12320  arisum2  12335  georeclim  12344  geo2sum  12345  geo2lim  12347  geomulcvg  12348  geoisumr  12350  0.999...  12353  cvgrat  12355  mertenslem2  12357  efcllem  12375  ege2le3  12387  cos0  12446  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  cos2bnd  12484  sin01gt0  12486  cos01gt0  12487  sincos2sgn  12490  sin4lt0  12491  absef  12493  absefib  12494  efieq1re  12495  epos  12501  znnenlem  12506  rpnnen2lem2  12510  rpnnen2lem3  12511  rpnnen2lem4  12512  rpnnen2lem9  12517  rpnnen2  12520  rpnnen  12521  ruclem6  12529  nthruz  12546  moddvds  12554  dvdslelem  12589  divalglem1  12609  divalglem5  12612  divalglem6  12613  bitsp1o  12640  bitsinv1lem  12648  sadcaddlem  12664  sadcadd  12665  gcdn0gt0  12717  nn0seqcvgd  12756  algcvgblem  12763  algcvga  12765  qnumgt0  12837  pythagtriplem12  12895  pythagtriplem13  12896  pythagtriplem14  12897  pythagtriplem16  12899  qexpz  12965  prmreclem4  12982  prmreclem5  12983  prmreclem6  12984  1arith  12990  4sqlem6  13006  vdwap0  13039  ramz  13088  mulgnegnn  14593  subgmulg  14651  isabvd  15601  abvf  15604  abvtrivd  15621  psrbaglesupp  16130  xrs1mnd  16425  xrs10  16426  rege0subm  16444  gzrngunit  16453  leordtval2  16958  pnfnei  16966  mnfnei  16967  prdsmet  17950  imasdsf1olem  17953  ssbl  17987  xmeter  17995  dscmet  18111  dscopn  18112  nlmvscnlem2  18212  nlmvscnlem1  18213  nmoi  18253  nmo0  18260  nmoeq0  18261  0nghm  18266  idnghm  18268  cnbl0  18299  blcvx  18320  xrsxmet  18331  metdseq0  18374  iitopon  18399  dfii2  18402  dfii3  18403  dfii5  18405  iicmp  18406  iicon  18407  iirev  18443  iirevcn  18444  iihalf1  18445  iihalf1cn  18446  iihalf2  18447  iihalf2cn  18448  elii1  18449  elii2  18450  iimulcl  18451  iimulcn  18452  icchmeo  18455  icopnfcnv  18456  icopnfhmeo  18457  iccpnfcnv  18458  iccpnfhmeo  18459  xrhmeo  18460  xrhmph  18461  icccvx  18464  evth  18473  lebnumlem1  18475  lebnumii  18480  htpycc  18494  reparphti  18511  pcoval1  18527  pco0  18528  pcoval2  18530  pcocn  18531  pcohtpylem  18533  pcopt  18536  pcopt2  18537  pcoass  18538  pcorevlem  18540  pcorev2  18542  pi1xfrcnv  18571  nmoleub2lem3  18612  cphsqrcl  18636  ipcnlem2  18687  ipcnlem1  18688  minveclem4c  18805  minveclem2  18806  minveclem3b  18808  minveclem4  18812  minveclem6  18814  minveclem7  18815  pjthlem1  18817  cniccbdd  18837  ovollb2lem  18863  ovollb2  18864  ovolunlem1a  18871  ovolunlem1  18872  ovolunnul  18875  ovoliunlem1  18877  ovoliunnul  18882  ovolicc1  18891  ovolicc2lem4  18895  ovolicopnf  18899  ovolre  18900  voliunlem3  18925  volsup  18929  ioombl1lem2  18932  ioombl1lem4  18934  iccvolcl  18940  ovolioo  18941  ioorcl2  18943  ioorcl  18948  uniioombllem1  18952  uniioombllem2  18954  uniioombllem3  18956  uniioombllem6  18959  volivth  18978  vitalilem1  18979  vitalilem2  18980  vitalilem4  18982  vitalilem5  18983  vitali  18984  ismbf  19001  mbfmulc2lem  19018  mbfpos  19022  mbfposr  19023  0plef  19043  i1f0  19058  i1f1  19061  itg1addlem2  19068  itg1addlem4  19070  itg1addlem5  19071  i1fmulc  19074  itg1mulc  19075  itg1ge0a  19082  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1fseqlem6  19091  mbfi1flimlem  19093  mbfi1flim  19094  xrge0f  19102  itg2ge0  19106  itg2const  19111  itg2seq  19113  itg2mulclem  19117  itg2mulc  19118  itg2splitlem  19119  itg2split  19120  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itg2i1fseq  19126  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  ibl0  19157  iblrelem  19161  iblposlem  19162  iblpos  19163  iblre  19164  itgreval  19167  itgneg  19174  iblss  19175  i1fibl  19178  itgitg1  19179  itgle  19180  itgge0  19181  itgeqa  19184  itgless  19187  iblconst  19188  itgconst  19189  ibladdlem  19190  itgaddlem1  19193  itgaddlem2  19194  iblabslem  19198  iblabs  19199  iblabsr  19200  iblmulc2  19201  itgmulc2lem1  19202  itgmulc2lem2  19203  itgabs  19205  itgsplit  19206  bddmulibl  19209  itggt0  19212  itgcn  19213  dvferm1  19348  dvferm2  19350  dvferm  19351  dvlip  19356  dvlipcn  19357  c1lip1  19360  dveq0  19363  dv11cn  19364  dvlt0  19368  dvne0  19374  dvfsumge  19385  ftc1lem4  19402  deg1lt0  19493  ply1divex  19538  plypf1  19610  dgradd2  19665  dgrco  19672  plyrecj  19676  plydivlem3  19691  vieta1lem2  19707  aalioulem2  19729  aalioulem3  19730  mtest  19797  radcnvlem1  19805  radcnv0  19808  radcnvlt1  19810  radcnvle  19812  pserulm  19814  psercnlem2  19816  psercnlem1  19817  psercn  19818  pserdvlem1  19819  pserdv  19821  abelthlem2  19824  abelthlem6  19828  abelthlem7  19830  abelth  19833  abelth2  19834  reeff1olem  19838  reeff1o  19839  pilem2  19844  pilem3  19845  pipos  19849  sinhalfpilem  19850  sincosq1sgn  19882  sincosq2sgn  19883  coseq00topi  19886  coseq0negpitopi  19887  tangtx  19889  tanabsge  19890  sinq12ge0  19892  sinq34lt0t  19893  cosq14ge0  19895  sincos4thpi  19897  tan4thpi  19898  sincos6thpi  19899  pige3  19901  sineq0  19905  cosordlem  19909  cosord  19910  cos11  19911  sinord  19912  recosf1o  19913  resinf1o  19914  tanord1  19915  tanord  19916  tanregt0  19917  efif1olem4  19923  efifo  19925  relogrn  19935  log1  19955  logneg  19957  logne0  19972  rplogcl  19974  argregt0  19980  argrege0  19981  argimgt0  19982  logneg2  19985  logdivlti  19987  logdivlt  19988  logdivle  19989  ellogdm  20002  logdmn0  20003  logdmnrp  20004  logcnlem3  20007  logcnlem4  20008  dvloglem  20011  logdmopn  20012  logf1o2  20013  dvlog2lem  20015  efopnlem1  20019  logtayl  20023  recxpcl  20038  cxpge0  20046  abscxp2  20056  cxplt  20057  cxple  20058  cxple2  20060  cxple2a  20062  cxpsqrlem  20065  cxpcn3lem  20103  cxpcn3  20104  cxpaddlelem  20107  cxpaddle  20108  abscxpbnd  20109  loglesqr  20114  ang180lem3  20125  ang180lem4  20126  chordthmlem4  20148  chordthmlem5  20149  asinlem3  20183  atanre  20197  asinneg  20198  asin1  20206  reasinsin  20208  acosbnd  20212  atan0  20220  atanrecl  20223  atanlogaddlem  20225  atanlogadd  20226  atanlogsublem  20227  atanlogsub  20228  atantan  20235  atanbnd  20238  atan1  20240  atans2  20243  ressatans  20246  leibpi  20254  log2cnv  20256  log2tlbnd  20257  log2ublem3  20260  log2ub  20261  rlimcnp  20276  rlimcnp2  20277  rlimcnp3  20278  efrlim  20280  o1cxp  20285  cxp2limlem  20286  cxp2lim  20287  cxploglim2  20289  divsqrsumlem  20290  cvxcl  20295  scvxcvx  20296  jensenlem1  20297  jensenlem2  20298  jensen  20299  amgm  20301  emgt0  20316  harmonicbnd3  20317  harmoniclbnd  20318  harmonicubnd  20319  harmonicbnd4  20320  fsumharmonic  20321  ftalem1  20326  ftalem2  20327  ftalem5  20330  basellem3  20336  basellem8  20341  efnnfsumcl  20356  ppisval  20357  vmacl  20372  vmage0  20375  chpge0  20380  chtwordi  20410  efchtdvds  20413  ppiwordi  20416  chtrpcl  20429  ppiltx  20431  fsumfldivdiaglem  20445  ppiub  20459  chpeq0  20463  chteq0  20464  chtleppi  20465  fsumvma2  20469  chpval2  20473  chpchtsum  20474  chpub  20475  logfacbnd3  20478  logexprlim  20480  mersenne  20482  dchr1re  20518  bcmono  20532  efexple  20536  bposlem1  20539  bposlem4  20542  bposlem5  20543  bposlem7  20545  bposlem8  20546  bposlem9  20547  lgslem4  20554  lgsval2lem  20561  lgsval4a  20573  lgsneg  20574  lgsdilem  20577  lgsdir2lem1  20578  lgsne0  20588  lgseisen  20608  lgsquadlem1  20609  lgsquadlem2  20610  m1lgs  20617  2sqlem11  20630  chebbnd1lem2  20635  chebbnd1lem3  20636  chebbnd1  20637  chtppilimlem1  20638  chtppilimlem2  20639  chtppilim  20640  chebbnd2  20642  chto1lb  20643  chpchtlim  20644  chpo1ub  20645  rplogsumlem2  20650  rpvmasumlem  20652  dchrisumlema  20653  dchrisumlem2  20655  dchrisumlem3  20656  dchrmusumlema  20658  dchrvmasumlem2  20663  dchrvmasumiflem1  20666  dchrisum0flblem1  20673  dchrisum0flblem2  20674  dchrisum0fno1  20676  dchrisum0re  20678  dchrisum0lema  20679  dchrisum0  20685  rplogsum  20692  dirith2  20693  logdivsum  20698  mulog2sumlem1  20699  mulog2sumlem2  20700  vmalogdivsum2  20703  log2sumbnd  20709  selberg2lem  20715  chpdifbndlem1  20718  chpdifbndlem2  20719  chpdifbnd  20720  logdivbnd  20721  selberg3lem1  20722  pntrmax  20729  pntrsumo1  20730  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntpbnd1a  20750  pntpbnd1  20751  pntpbnd2  20752  pntlemg  20763  pntlemj  20768  pntlemk  20771  pntlem3  20774  pntleml  20776  pnt2  20778  pnt  20779  ostth2lem1  20783  padicabv  20795  padicabvcxp  20797  ostth2lem3  20800  ostth2lem4  20801  ostth2  20802  ostth3  20803  ex-po  20838  gxnval  20943  readdsubgo  21036  nvz0  21250  ipidsq  21302  0blo  21386  nmlno0lem  21387  nmblolbii  21393  siilem2  21446  minvecolem2  21470  minvecolem3  21471  minvecolem4c  21474  minvecolem4  21475  minvecolem5  21476  minvecolem6  21477  minvecolem7  21478  htthlem  21513  hiidge0  21693  normlem6  21710  normgt0  21722  norm-i  21724  normpyc  21741  normpar2i  21751  bcsiALT  21774  pjhthlem1  21986  pjneli  22318  0bdop  22589  nmlnop0iALT  22591  unopbd  22611  nmbdoplbi  22620  nmcoplbi  22624  nmbdfnlbi  22645  nmbdfnlb  22646  nmcfnlbi  22648  cnlnadjlem7  22669  nmopcoi  22691  branmfn  22701  leopmul  22730  nmopleid  22735  pjbdlni  22745  pjnormssi  22764  stcl  22812  stge0  22820  stle1  22821  stle0i  22835  strlem3a  22848  cdj3lem1  23030  bcm1n  23048  ballotlem2  23063  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemodife  23072  ballotlem4  23073  ballotlemi1  23077  ballotlemic  23081  xdiv0  23128  xlt2addrd  23268  unitsscn  23295  elunitrn  23296  elunitge0  23298  unitdivcld  23300  sqsscirc1  23307  xaddeq0  23319  xrge00  23326  xrge0iifcnv  23330  xrge0iifiso  23332  xrge0iifhom  23334  xrge0mulc1cn  23338  xrge0neqmnf  23345  xrge0adddir  23347  fsumrp0cl  23349  lmlimxrge0  23387  rge0scvg  23388  pnfneige0  23389  lmxrge0  23390  lmdvg  23391  rnlogblem  23416  logbrec  23422  log2le1  23424  esumpfinvallem  23457  esumpfinval  23458  esumpfinvalf  23459  esumpcvgval  23461  esumcvg  23469  measinb  23563  indf  23614  indfval  23615  pr01ssre  23616  indf1o  23622  probvalrnd  23642  probmeasb  23648  cndprobprob  23656  0rrv  23669  coinfliprv  23698  zetacvg  23704  eldmgm  23709  cvxpcon  23788  cvxscon  23789  rescon  23792  iiscon  23798  iillyscon  23799  cvmliftlem2  23832  cvmliftlem8  23838  cvmliftlem10  23840  konigsberg  23926  snmlff  23927  divelunit  24095  mulge0b  24101  relin01  24104  fz0n  24112  4bc2eq6  24114  brbtwn2  24604  axsegconlem7  24622  axsegconlem10  24625  ax5seglem1  24627  ax5seglem2  24628  ax5seglem3  24630  ax5seglem5  24632  ax5seglem6  24633  ax5seglem9  24636  ax5seg  24637  axbtwnid  24638  axpaschlem  24639  axpasch  24640  axlowdimlem1  24641  axlowdimlem6  24646  axlowdimlem7  24647  axlowdimlem10  24650  axlowdim1  24658  axlowdim2  24659  axlowdim  24660  axeuclidlem  24661  axcontlem2  24664  axcontlem4  24666  axcontlem7  24669  axcontlem10  24672  bpoly0  24856  bpoly4  24865  ovoliunnfl  25000  itg2addnclem  25002  itg2addnclem2  25003  itg2addnc  25004  ibladdnclem  25006  itgaddnclem1  25008  itgaddnclem2  25009  iblabsnclem  25013  iblabsnc  25014  iblmulc2nc  25015  itgmulc2nclem1  25016  itgmulc2nclem2  25017  itgabsnc  25019  bddiblnc  25020  itggt0cn  25022  ftc1cnnclem  25023  dvreasin  25025  areacirclem2  25027  areacirclem3  25028  areacirclem4  25029  areacirclem5  25031  areacirc  25033  cntrset  25704  iintlem1  25712  lvsovso  25728  clscnc  26112  nn0prpwlem  26340  geomcau  26577  isbnd3  26610  isbnd3b  26611  ssbnd  26614  prdsbnd  26619  bfplem2  26649  bfp  26650  rrnequiv  26661  modelico  27008  irrapxlem1  27009  irrapxlem2  27010  irrapxlem3  27011  irrapxlem4  27012  pellexlem6  27021  pell14qrgt0  27046  elpell14qr2  27049  pell1qrgaplem  27060  pellfundex  27073  pellfundrp  27075  monotoddzzfi  27129  oddcomabszz  27131  zindbi  27133  jm2.24  27152  acongeq  27172  jm2.23  27191  jm2.26lem3  27196  jm3.1lem3  27214  hbtlem5  27434  dvconstbi  27653  ioovolcl  27844  itgsin0pilem1  27846  itgsinexplem1  27850  itgsinexp  27851  stoweidlem1  27852  stoweidlem3  27854  stoweidlem7  27858  stoweidlem11  27862  stoweidlem17  27868  stoweidlem25  27876  stoweidlem26  27877  stoweidlem34  27885  stoweidlem36  27887  stoweidlem38  27889  stoweidlem41  27892  stoweidlem42  27893  stoweidlem44  27895  stoweidlem45  27896  stoweidlem55  27906  stoweid  27914  wallispilem1  27916  wallispilem2  27917  wallispilem3  27918  wallispilem4  27919  wallispi  27921  wallispi2lem1  27922  wallispi2lem2  27923  wallispi2  27924  stirlinglem1  27925  stirlinglem3  27927  stirlinglem4  27928  stirlinglem5  27929  stirlinglem6  27930  stirlinglem7  27931  stirlinglem8  27932  stirlinglem10  27934  stirlinglem11  27935  stirlinglem12  27936  stirlinglem13  27937  stirlinglem14  27938  stirlinglem15  27939  stirlingr  27941  sharhght  27957  elfznelfzo  28212  hashgt12el  28217  hashgt12el2  28218  usgraexvlem  28260  spthispth  28358  nvnencycllem  28388  constr3lem4  28392  ex-gt  28451  sgnpnf  28503  sgnmnf  28505
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-i2m1 8821  ax-1ne0 8822  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877
  Copyright terms: Public domain W3C validator