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

Theorem 0re 9047
Description:  0 is a real number. See also 0reALT 9353. (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 9046 . 2  |-  1  e.  RR
2 ax-rnegex 9017 . 2  |-  ( 1  e.  RR  ->  E. x  e.  RR  ( 1  +  x )  =  0 )
3 readdcl 9029 . . . . 5  |-  ( ( 1  e.  RR  /\  x  e.  RR )  ->  ( 1  +  x
)  e.  RR )
41, 3mpan 652 . . . 4  |-  ( x  e.  RR  ->  (
1  +  x )  e.  RR )
5 eleq1 2464 . . . 4  |-  ( ( 1  +  x )  =  0  ->  (
( 1  +  x
)  e.  RR  <->  0  e.  RR ) )
64, 5syl5ibcom 212 . . 3  |-  ( x  e.  RR  ->  (
( 1  +  x
)  =  0  -> 
0  e.  RR ) )
76rexlimiv 2784 . 2  |-  ( E. x  e.  RR  (
1  +  x )  =  0  ->  0  e.  RR )
81, 2, 7mp2b 10 1  |-  0  e.  RR
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721   E.wrex 2667  (class class class)co 6040   RRcr 8945   0cc0 8946   1c1 8947    + caddc 8949
This theorem is referenced by:  0xr  9087  axmulgt0  9106  ne0gt0  9134  00id  9197  mul02lem1  9198  mul02lem2  9199  mul02  9200  addid1  9202  gt0ne0  9449  addgt0  9470  addgegt0  9471  addgtge0  9472  addge0  9473  ltaddpos  9474  ltneg  9484  leneg  9487  lt0neg1  9490  lt0neg2  9491  le0neg1  9492  le0neg2  9493  addge01  9494  add20  9496  subge0  9497  suble0  9498  lesub0  9500  mulge0  9501  msqgt0  9504  msqge0  9505  0le1  9507  gt0ne0i  9518  gt0ne0d  9547  lt0ne0d  9548  addgt0d  9557  elimge0  9803  ltm1  9806  recgt0  9810  prodgt0  9811  prodge0  9813  lemul1a  9820  ltmul12a  9822  lemul12a  9824  mulgt1  9825  gt0div  9832  ge0div  9833  lt2msq1  9849  lediv12a  9859  recgt1i  9863  recreclt  9865  ledivp1  9868  squeeze0  9869  recgt0ii  9872  ledivp1i  9892  ltdivp1i  9893  fimaxre2  9912  supmul1  9929  supmul  9932  inelr  9946  crne0  9949  nnge1  9982  nngt0  9985  nnrecgt0  9993  0le0  10037  nn0ssre  10181  nn0ge0  10203  nn0nlt0  10204  nn0le0eq0  10206  elnnnn0b  10220  elnnnn0c  10221  nn0sub  10226  elnnz  10248  0z  10249  elnn0z  10250  elnnz1  10263  nn0lt10b  10292  recnz  10301  gtndiv  10303  uzindOLD  10320  fnn0ind  10325  rpge0  10580  rpgecl  10593  ge0p1rp  10596  rpneg  10597  0nrp  10598  ge0gtmnf  10716  max0sub  10738  qsqueeze  10743  xneg0  10754  xaddid1  10781  xsubge0  10796  xmulpnf1  10809  xmulgt0  10818  xlemul1a  10823  xadddi  10830  xrsupsslem  10841  xrinfmsslem  10842  elrege0  10963  0elunit  10971  1elunit  10972  lincmb01cmp  10994  iccf1o  10995  xov1plusxeqvd  10997  unitssre  10998  elfznelfzo  11147  rpsup  11202  0mod  11227  1mod  11228  expgt1  11373  ltexp2a  11386  expcan  11387  ltexp2  11388  leexp2  11389  leexp2a  11390  expubnd  11395  le2sq2  11412  sqlecan  11442  bernneq2  11461  expnbnd  11463  expnlbnd  11464  expnlbnd2  11465  expmulnbnd  11466  discr1  11470  discr  11471  facdiv  11533  faclbnd  11536  faclbnd3  11538  faclbnd6  11545  bcval4  11553  bcval5  11564  bcpasc  11567  hasheq0  11599  hashnn0n0nn  11619  hashgt12el  11637  hashgt12el2  11638  brfi1uzind  11670  reim0  11878  re0  11912  im0  11913  rei  11916  imi  11917  cj0  11918  sqeqd  11926  rennim  11999  cnpart  12000  sqr0lem  12001  sqrlem4  12006  resqrex  12011  sqrgt0  12019  sqr00  12024  sqrneglem  12027  sqr4  12033  sqr9  12034  sqr2gt1lt2  12035  leabs  12059  absor  12060  max0add  12070  absgt0  12083  sqreulem  12118  eqsqr2d  12127  amgm2  12128  sqrpclii  12141  rlimconst  12293  rlimrege0  12328  lo1mul  12376  iserge0  12409  iseraltlem2  12431  fsumrecl  12483  fsumge0  12529  fsum00  12532  o1fsum  12547  cvgcmp  12550  cvgcmpce  12552  isumless  12580  arisum2  12595  georeclim  12604  geo2sum  12605  geo2lim  12607  geomulcvg  12608  geoisumr  12610  0.999...  12613  cvgrat  12615  mertenslem2  12617  efcllem  12635  ege2le3  12647  cos0  12706  ef01bndlem  12740  sin01bnd  12741  cos01bnd  12742  cos2bnd  12744  sin01gt0  12746  cos01gt0  12747  sincos2sgn  12750  sin4lt0  12751  absef  12753  absefib  12754  efieq1re  12755  epos  12761  znnenlem  12766  rpnnen2lem2  12770  rpnnen2lem3  12771  rpnnen2lem4  12772  rpnnen2lem9  12777  rpnnen2  12780  ruclem6  12789  nthruz  12806  moddvds  12814  dvdslelem  12849  divalglem1  12869  divalglem5  12872  divalglem6  12873  bitsp1o  12900  bitsinv1lem  12908  sadcaddlem  12924  sadcadd  12925  gcdn0gt0  12977  nn0seqcvgd  13016  algcvgblem  13023  algcvga  13025  qnumgt0  13097  pythagtriplem12  13155  pythagtriplem13  13156  pythagtriplem14  13157  pythagtriplem16  13159  qexpz  13225  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  1arith  13250  4sqlem6  13266  vdwap0  13299  ramz  13348  mulgnegnn  14855  subgmulg  14913  isabvd  15863  abvf  15866  abvtrivd  15883  psrbaglesupp  16388  xrs1mnd  16691  xrs10  16692  rege0subm  16710  gzrngunit  16719  leordtval2  17230  pnfnei  17238  mnfnei  17239  prdsmet  18353  imasdsf1olem  18356  ssblps  18405  ssbl  18406  xmeter  18416  metustexhalfOLD  18546  metustexhalf  18547  dscmet  18573  dscopn  18574  nlmvscnlem2  18674  nlmvscnlem1  18675  nmoi  18715  nmo0  18722  nmoeq0  18723  0nghm  18728  idnghm  18730  cnbl0  18761  blcvx  18782  xrsxmet  18793  metdseq0  18837  iicmp  18869  iicon  18870  iirev  18907  iihalf1  18909  iihalf1cn  18910  iihalf2  18911  elii1  18913  elii2  18914  iimulcl  18915  icopnfcnv  18920  icopnfhmeo  18921  iccpnfcnv  18922  iccpnfhmeo  18923  xrhmeo  18924  xrhmph  18925  evth  18937  lebnumlem1  18939  lebnumii  18944  htpycc  18958  reparphti  18975  pcoval1  18991  pco0  18992  pcoval2  18994  pcocn  18995  pcohtpylem  18997  pcopt  19000  pcopt2  19001  pcoass  19002  pcorevlem  19004  nmoleub2lem3  19076  cphsqrcl  19100  ipcnlem2  19151  ipcnlem1  19152  minveclem4c  19279  minveclem2  19280  minveclem3b  19282  minveclem4  19286  minveclem6  19288  minveclem7  19289  pjthlem1  19291  cniccbdd  19311  ovollb2lem  19337  ovollb2  19338  ovolunlem1a  19345  ovolunlem1  19346  ovolunnul  19349  ovoliunlem1  19351  ovoliunnul  19356  ovolicc1  19365  ovolicc2lem4  19369  ovolicopnf  19373  ovolre  19374  voliunlem3  19399  volsup  19403  ioombl1lem2  19406  ioombl1lem4  19408  iccvolcl  19414  ovolioo  19415  ioorcl2  19417  ioorcl  19422  uniioombllem1  19426  uniioombllem2  19428  uniioombllem3  19430  uniioombllem6  19433  volivth  19452  vitalilem2  19454  vitalilem4  19456  vitalilem5  19457  vitali  19458  ismbf  19475  mbfmulc2lem  19492  mbfpos  19496  mbfposr  19497  0plef  19517  i1f0  19532  i1f1  19535  itg1addlem2  19542  itg1addlem4  19544  itg1addlem5  19545  i1fmulc  19548  itg1mulc  19549  itg1ge0a  19556  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1fseqlem6  19565  mbfi1flimlem  19567  mbfi1flim  19568  xrge0f  19576  itg2ge0  19580  itg2const  19585  itg2seq  19587  itg2mulclem  19591  itg2mulc  19592  itg2splitlem  19593  itg2split  19594  itg2monolem1  19595  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  itg2i1fseq  19600  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  ibl0  19631  iblrelem  19635  iblposlem  19636  iblpos  19637  iblre  19638  itgreval  19641  itgneg  19648  iblss  19649  i1fibl  19652  itgitg1  19653  itgle  19654  itgge0  19655  itgeqa  19658  itgless  19661  iblconst  19662  itgconst  19663  ibladdlem  19664  itgaddlem1  19667  itgaddlem2  19668  iblabslem  19672  iblabs  19673  iblabsr  19674  iblmulc2  19675  itgmulc2lem1  19676  itgmulc2lem2  19677  itgabs  19679  itgsplit  19680  bddmulibl  19683  itggt0  19686  itgcn  19687  dvferm1  19822  dvferm2  19824  dvferm  19825  dvlip  19830  dvlipcn  19831  c1lip1  19834  dveq0  19837  dv11cn  19838  dvlt0  19842  dvne0  19848  dvfsumge  19859  ftc1lem4  19876  deg1lt0  19967  ply1divex  20012  plypf1  20084  dgradd2  20139  dgrco  20146  plyrecj  20150  plydivlem3  20165  vieta1lem2  20181  aalioulem2  20203  aalioulem3  20204  mtest  20273  radcnvlem1  20282  radcnv0  20285  radcnvlt1  20287  radcnvle  20289  pserulm  20291  psercnlem2  20293  psercnlem1  20294  psercn  20295  pserdvlem1  20296  pserdv  20298  abelthlem2  20301  abelthlem6  20305  abelthlem7  20307  abelth  20310  abelth2  20311  reeff1olem  20315  reeff1o  20316  pilem2  20321  pilem3  20322  pipos  20326  sinhalfpilem  20327  sincosq1sgn  20359  sincosq2sgn  20360  coseq00topi  20363  coseq0negpitopi  20364  tangtx  20366  tanabsge  20367  sinq12ge0  20369  sinq34lt0t  20370  cosq14ge0  20372  sincos4thpi  20374  tan4thpi  20375  sincos6thpi  20376  pige3  20378  sineq0  20382  cosordlem  20386  cosord  20387  cos11  20388  sinord  20389  recosf1o  20390  resinf1o  20391  tanord1  20392  tanord  20393  tanregt0  20394  efif1olem4  20400  efifo  20402  relogrn  20412  log1  20433  logneg  20435  logne0  20450  rplogcl  20452  argregt0  20458  argrege0  20459  argimgt0  20460  logneg2  20463  logdivlti  20468  logdivlt  20469  logdivle  20470  ellogdm  20483  logdmn0  20484  logdmnrp  20485  logcnlem3  20488  logcnlem4  20489  dvloglem  20492  logdmopn  20493  logf1o2  20494  dvlog2lem  20496  efopnlem1  20500  logtayl  20504  recxpcl  20519  cxpge0  20527  abscxp2  20537  cxplt  20538  cxple  20539  cxple2  20541  cxple2a  20543  cxpsqrlem  20546  cxpcn3lem  20584  cxpcn3  20585  cxpaddlelem  20588  cxpaddle  20589  abscxpbnd  20590  loglesqr  20595  ang180lem3  20606  ang180lem4  20607  chordthmlem4  20629  chordthmlem5  20630  asinlem3  20664  atanre  20678  asinneg  20679  asin1  20687  reasinsin  20689  acosbnd  20693  atan0  20701  atanrecl  20704  atanlogaddlem  20706  atanlogadd  20707  atanlogsublem  20708  atanlogsub  20709  atantan  20716  atanbnd  20719  atan1  20721  atans2  20724  ressatans  20727  leibpi  20735  log2cnv  20737  log2tlbnd  20738  log2ublem3  20741  log2ub  20742  rlimcnp  20757  rlimcnp2  20758  rlimcnp3  20759  efrlim  20761  o1cxp  20766  cxp2limlem  20767  cxp2lim  20768  cxploglim2  20770  divsqrsumlem  20771  jensenlem1  20778  jensenlem2  20779  jensen  20780  amgm  20782  emgt0  20798  harmonicbnd3  20799  harmoniclbnd  20800  harmonicubnd  20801  harmonicbnd4  20802  fsumharmonic  20803  ftalem1  20808  ftalem2  20809  ftalem5  20812  basellem3  20818  basellem8  20823  efnnfsumcl  20838  ppisval  20839  vmacl  20854  vmage0  20857  chpge0  20862  chtwordi  20892  efchtdvds  20895  ppiwordi  20898  chtrpcl  20911  ppiltx  20913  fsumfldivdiaglem  20927  ppiub  20941  chpeq0  20945  chteq0  20946  chtleppi  20947  fsumvma2  20951  chpval2  20955  chpchtsum  20956  chpub  20957  logfacbnd3  20960  logexprlim  20962  mersenne  20964  dchr1re  21000  bcmono  21014  efexple  21018  bposlem1  21021  bposlem4  21024  bposlem5  21025  bposlem7  21027  bposlem8  21028  bposlem9  21029  lgslem4  21036  lgsval2lem  21043  lgsval4a  21055  lgsneg  21056  lgsdilem  21059  lgsdir2lem1  21060  lgsne0  21070  lgseisen  21090  lgsquadlem1  21091  lgsquadlem2  21092  m1lgs  21099  2sqlem11  21112  chebbnd1lem2  21117  chebbnd1lem3  21118  chebbnd1  21119  chtppilimlem1  21120  chtppilimlem2  21121  chtppilim  21122  chebbnd2  21124  chto1lb  21125  chpchtlim  21126  chpo1ub  21127  rplogsumlem2  21132  rpvmasumlem  21134  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  dchrmusumlema  21140  dchrvmasumlem2  21145  dchrvmasumiflem1  21148  dchrisum0flblem1  21155  dchrisum0flblem2  21156  dchrisum0fno1  21158  dchrisum0re  21160  dchrisum0lema  21161  dchrisum0  21167  rplogsum  21174  dirith2  21175  logdivsum  21180  mulog2sumlem1  21181  mulog2sumlem2  21182  vmalogdivsum2  21185  log2sumbnd  21191  selberg2lem  21197  chpdifbndlem1  21200  chpdifbndlem2  21201  chpdifbnd  21202  logdivbnd  21203  selberg3lem1  21204  pntrmax  21211  pntrsumo1  21212  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntpbnd1a  21232  pntpbnd1  21233  pntpbnd2  21234  pntlemg  21245  pntlemj  21250  pntlemk  21253  pntlem3  21256  pntleml  21258  pnt2  21260  pnt  21261  ostth2lem1  21265  padicabv  21277  padicabvcxp  21279  ostth2lem3  21282  ostth2lem4  21283  ostth2  21284  ostth3  21285  usgraexvlem  21367  usgraex0elv  21368  spthispth  21526  nvnencycllem  21583  vdgr0  21624  konigsberg  21662  ex-po  21696  gxnval  21801  readdsubgo  21894  nvz0  22110  ipidsq  22162  0blo  22246  nmlno0lem  22247  nmblolbii  22253  siilem2  22306  minvecolem2  22330  minvecolem3  22331  minvecolem4c  22334  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  minvecolem7  22338  htthlem  22373  hiidge0  22553  normlem6  22570  normgt0  22582  norm-i  22584  normpyc  22601  normpar2i  22611  bcsiALT  22634  pjhthlem1  22846  pjneli  23178  0bdop  23449  nmlnop0iALT  23451  unopbd  23471  nmbdoplbi  23480  nmcoplbi  23484  nmbdfnlbi  23505  nmbdfnlb  23506  nmcfnlbi  23508  cnlnadjlem7  23529  nmopcoi  23551  branmfn  23561  leopmul  23590  nmopleid  23595  pjbdlni  23605  pjnormssi  23624  stge0  23680  stle1  23681  stle0i  23695  strlem3a  23708  cdj3lem1  23890  xaddeq0  24072  xlt2addrd  24077  bcm1n  24104  xdiv0  24128  xrge00  24161  xrge0neqmnf  24165  xrge0adddir  24168  fsumrp0cl  24170  re0g  24226  elunitrn  24248  elunitge0  24250  unitdivcld  24252  sqsscirc1  24259  xrge0iifcnv  24272  xrge0iifiso  24274  xrge0iifhom  24276  xrge0mulc1cn  24280  lmlimxrge0  24287  rge0scvg  24288  pnfneige0  24289  lmxrge0  24290  lmdvg  24291  reust  24297  recusp  24298  rezh  24308  rrhre  24340  rnlogblem  24352  logbrec  24358  log2le1  24360  indf  24366  indfval  24367  pr01ssre  24368  indf1o  24374  esumfsupre  24414  esumpfinvallem  24417  esumpfinval  24418  esumpfinvalf  24419  esumpcvgval  24421  esumcvg  24429  measinb  24528  voliune  24538  volfiniune  24539  sibfof  24607  sitgclg  24609  sitmcl  24616  0rrv  24662  coinfliprv  24693  ballotlem2  24699  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemodife  24708  ballotlem4  24709  ballotlemi1  24713  ballotlemic  24717  zetacvg  24752  eldmgm  24759  dmlogdmgm  24761  lgamgulmlem1  24766  lgamgulmlem2  24767  rescon  24886  iiscon  24892  iillyscon  24893  cvmliftlem2  24926  cvmliftlem10  24934  snmlff  24969  divelunit  25138  mulge0b  25144  relin01  25147  fz0n  25155  4bc2eq6  25157  brbtwn2  25748  axsegconlem7  25766  axsegconlem10  25769  ax5seglem1  25771  ax5seglem2  25772  ax5seglem3  25774  ax5seglem5  25776  ax5seglem6  25777  ax5seglem9  25780  ax5seg  25781  axbtwnid  25782  axpaschlem  25783  axpasch  25784  axlowdimlem1  25785  axlowdimlem6  25790  axlowdimlem7  25791  axlowdimlem10  25794  axlowdim1  25802  axlowdim2  25803  axlowdim  25804  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem10  25816  bpoly4  26009  mblfinlem  26143  ismblfin  26146  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  mbfposadd  26153  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  ibladdnclem  26160  itgaddnclem1  26162  itgaddnclem2  26163  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  itgmulc2nclem1  26170  itgmulc2nclem2  26171  itgabsnc  26173  bddiblnc  26174  itggt0cn  26176  ftc1cnnclem  26177  dvreasin  26179  areacirclem2  26181  areacirclem3  26182  areacirclem4  26183  areacirclem5  26185  areacirc  26187  nn0prpwlem  26215  geomcau  26355  isbnd3  26383  isbnd3b  26384  ssbnd  26387  prdsbnd  26392  bfplem2  26422  bfp  26423  rrnequiv  26434  modelico  26774  irrapxlem1  26775  irrapxlem2  26776  irrapxlem3  26777  irrapxlem4  26778  pellexlem6  26787  pell14qrgt0  26812  elpell14qr2  26815  pell1qrgaplem  26826  pellfundex  26839  pellfundrp  26841  monotoddzzfi  26895  oddcomabszz  26897  zindbi  26899  jm2.24  26918  acongeq  26938  jm2.23  26957  jm2.26lem3  26962  jm3.1lem3  26980  hbtlem5  27200  dvconstbi  27419  ioovolcl  27609  itgsin0pilem1  27611  itgsinexplem1  27615  itgsinexp  27616  stoweidlem1  27617  stoweidlem7  27623  stoweidlem11  27627  stoweidlem17  27633  stoweidlem25  27641  stoweidlem26  27642  stoweidlem34  27650  stoweidlem36  27652  stoweidlem41  27657  stoweidlem42  27658  stoweidlem44  27660  stoweidlem45  27661  stoweidlem55  27671  stoweid  27679  wallispilem1  27681  wallispilem2  27682  wallispilem3  27683  wallispilem4  27684  wallispi  27686  wallispi2lem1  27687  wallispi2  27689  stirlinglem1  27690  stirlinglem3  27692  stirlinglem4  27693  stirlinglem5  27694  stirlinglem6  27695  stirlinglem7  27696  stirlinglem10  27699  stirlinglem11  27700  stirlinglem12  27701  stirlinglem13  27702  stirlinglem14  27703  stirlinglem15  27704  stirlingr  27706  sharhght  27722  0mnnnnn0  27971  fzo1fzo0n0  27988  swrdnd  28001  swrdswrdlem  28010  swrdswrd  28011  swrdccatin12b  28027  swrdccat3  28029  swrdccat3b  28031  usgra2pthlem1  28040  ex-gt  28185  sgnpnf  28237  sgnmnf  28239
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-i2m1 9014  ax-1ne0 9015  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019
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 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator