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

Theorem 0re 9024
Description:  0 is a real number. See also 0reALT 9329. (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 9023 . 2  |-  1  e.  RR
2 ax-rnegex 8994 . 2  |-  ( 1  e.  RR  ->  E. x  e.  RR  ( 1  +  x )  =  0 )
3 readdcl 9006 . . . . 5  |-  ( ( 1  e.  RR  /\  x  e.  RR )  ->  ( 1  +  x
)  e.  RR )
41, 3mpan 652 . . . 4  |-  ( x  e.  RR  ->  (
1  +  x )  e.  RR )
5 eleq1 2447 . . . 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 2767 . 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 1717   E.wrex 2650  (class class class)co 6020   RRcr 8922   0cc0 8923   1c1 8924    + caddc 8926
This theorem is referenced by:  0xr  9064  axmulgt0  9083  ne0gt0  9111  00id  9173  mul02lem1  9174  mul02lem2  9175  mul02  9176  addid1  9178  gt0ne0  9425  addgt0  9446  addgegt0  9447  addgtge0  9448  addge0  9449  ltaddpos  9450  ltneg  9460  leneg  9463  lt0neg1  9466  lt0neg2  9467  le0neg1  9468  le0neg2  9469  addge01  9470  add20  9472  subge0  9473  suble0  9474  lesub0  9476  mulge0  9477  msqgt0  9480  msqge0  9481  0le1  9483  gt0ne0i  9494  gt0ne0d  9523  lt0ne0d  9524  addgt0d  9533  elimge0  9779  ltm1  9782  recgt0  9786  prodgt0  9787  prodge0  9789  lemul1a  9796  ltmul12a  9798  lemul12a  9800  mulgt1  9801  gt0div  9808  ge0div  9809  lt2msq1  9825  lediv12a  9835  recgt1i  9839  recreclt  9841  ledivp1  9844  squeeze0  9845  recgt0ii  9848  ledivp1i  9868  ltdivp1i  9869  fimaxre2  9888  supmul1  9905  supmul  9908  inelr  9922  crne0  9925  nnge1  9958  nngt0  9961  nnrecgt0  9969  0le0  10013  nn0ssre  10157  nn0ge0  10179  nn0nlt0  10180  nn0le0eq0  10182  elnnnn0b  10196  elnnnn0c  10197  nn0sub  10202  elnnz  10224  0z  10225  elnn0z  10226  elnnz1  10239  nn0lt10b  10268  recnz  10277  gtndiv  10279  uzindOLD  10296  fnn0ind  10301  rpge0  10556  rpgecl  10569  ge0p1rp  10572  rpneg  10573  0nrp  10574  ge0gtmnf  10692  max0sub  10714  qsqueeze  10719  xneg0  10730  xaddid1  10757  xsubge0  10772  xmulpnf1  10785  xmulgt0  10794  xlemul1a  10799  xadddi  10806  xrsupsslem  10817  xrinfmsslem  10818  elrege0  10939  0elunit  10947  1elunit  10948  lincmb01cmp  10970  iccf1o  10971  xov1plusxeqvd  10973  unitssre  10974  elfznelfzo  11119  rpsup  11174  0mod  11199  1mod  11200  expgt1  11345  ltexp2a  11358  expcan  11359  ltexp2  11360  leexp2  11361  leexp2a  11362  expubnd  11367  le2sq2  11384  sqlecan  11414  bernneq2  11433  expnbnd  11435  expnlbnd  11436  expnlbnd2  11437  expmulnbnd  11438  discr1  11442  discr  11443  facdiv  11505  faclbnd  11508  faclbnd3  11510  faclbnd6  11517  bcval4  11525  bcval5  11536  bcpasc  11539  hasheq0  11571  hashnn0n0nn  11591  hashgt12el  11609  hashgt12el2  11610  brfi1uzind  11642  reim0  11850  re0  11884  im0  11885  rei  11888  imi  11889  cj0  11890  sqeqd  11898  rennim  11971  cnpart  11972  sqr0lem  11973  sqrlem4  11978  resqrex  11983  sqrgt0  11991  sqr00  11996  sqrneglem  11999  sqr4  12005  sqr9  12006  sqr2gt1lt2  12007  leabs  12031  absor  12032  max0add  12042  absgt0  12055  sqreulem  12090  eqsqr2d  12099  amgm2  12100  sqrpclii  12113  rlimconst  12265  rlimrege0  12300  lo1mul  12348  iserge0  12381  iseraltlem2  12403  fsumrecl  12455  fsumge0  12501  fsum00  12504  o1fsum  12519  cvgcmp  12522  cvgcmpce  12524  isumless  12552  arisum2  12567  georeclim  12576  geo2sum  12577  geo2lim  12579  geomulcvg  12580  geoisumr  12582  0.999...  12585  cvgrat  12587  mertenslem2  12589  efcllem  12607  ege2le3  12619  cos0  12678  ef01bndlem  12712  sin01bnd  12713  cos01bnd  12714  cos2bnd  12716  sin01gt0  12718  cos01gt0  12719  sincos2sgn  12722  sin4lt0  12723  absef  12725  absefib  12726  efieq1re  12727  epos  12733  znnenlem  12738  rpnnen2lem2  12742  rpnnen2lem3  12743  rpnnen2lem4  12744  rpnnen2lem9  12749  rpnnen2  12752  ruclem6  12761  nthruz  12778  moddvds  12786  dvdslelem  12821  divalglem1  12841  divalglem5  12844  divalglem6  12845  bitsp1o  12872  bitsinv1lem  12880  sadcaddlem  12896  sadcadd  12897  gcdn0gt0  12949  nn0seqcvgd  12988  algcvgblem  12995  algcvga  12997  qnumgt0  13069  pythagtriplem12  13127  pythagtriplem13  13128  pythagtriplem14  13129  pythagtriplem16  13131  qexpz  13197  prmreclem4  13214  prmreclem5  13215  prmreclem6  13216  1arith  13222  4sqlem6  13238  vdwap0  13271  ramz  13320  mulgnegnn  14827  subgmulg  14885  isabvd  15835  abvf  15838  abvtrivd  15855  psrbaglesupp  16360  xrs1mnd  16659  xrs10  16660  rege0subm  16678  gzrngunit  16687  leordtval2  17198  pnfnei  17206  mnfnei  17207  prdsmet  18308  imasdsf1olem  18311  ssbl  18345  xmeter  18353  metustexhalf  18476  dscmet  18491  dscopn  18492  nlmvscnlem2  18592  nlmvscnlem1  18593  nmoi  18633  nmo0  18640  nmoeq0  18641  0nghm  18646  idnghm  18648  cnbl0  18679  blcvx  18700  xrsxmet  18711  metdseq0  18755  iicmp  18787  iicon  18788  iirev  18825  iihalf1  18827  iihalf1cn  18828  iihalf2  18829  elii1  18831  elii2  18832  iimulcl  18833  icopnfcnv  18838  icopnfhmeo  18839  iccpnfcnv  18840  iccpnfhmeo  18841  xrhmeo  18842  xrhmph  18843  evth  18855  lebnumlem1  18857  lebnumii  18862  htpycc  18876  reparphti  18893  pcoval1  18909  pco0  18910  pcoval2  18912  pcocn  18913  pcohtpylem  18915  pcopt  18918  pcopt2  18919  pcoass  18920  pcorevlem  18922  nmoleub2lem3  18994  cphsqrcl  19018  ipcnlem2  19069  ipcnlem1  19070  minveclem4c  19193  minveclem2  19194  minveclem3b  19196  minveclem4  19200  minveclem6  19202  minveclem7  19203  pjthlem1  19205  cniccbdd  19225  ovollb2lem  19251  ovollb2  19252  ovolunlem1a  19259  ovolunlem1  19260  ovolunnul  19263  ovoliunlem1  19265  ovoliunnul  19270  ovolicc1  19279  ovolicc2lem4  19283  ovolicopnf  19287  ovolre  19288  voliunlem3  19313  volsup  19317  ioombl1lem2  19320  ioombl1lem4  19322  iccvolcl  19328  ovolioo  19329  ioorcl2  19331  ioorcl  19336  uniioombllem1  19340  uniioombllem2  19342  uniioombllem3  19344  uniioombllem6  19347  volivth  19366  vitalilem2  19368  vitalilem4  19370  vitalilem5  19371  vitali  19372  ismbf  19389  mbfmulc2lem  19406  mbfpos  19410  mbfposr  19411  0plef  19431  i1f0  19446  i1f1  19449  itg1addlem2  19456  itg1addlem4  19458  itg1addlem5  19459  i1fmulc  19462  itg1mulc  19463  itg1ge0a  19470  mbfi1fseqlem3  19476  mbfi1fseqlem4  19477  mbfi1fseqlem5  19478  mbfi1fseqlem6  19479  mbfi1flimlem  19481  mbfi1flim  19482  xrge0f  19490  itg2ge0  19494  itg2const  19499  itg2seq  19501  itg2mulclem  19505  itg2mulc  19506  itg2splitlem  19507  itg2split  19508  itg2monolem1  19509  itg2monolem2  19510  itg2monolem3  19511  itg2mono  19512  itg2i1fseq  19514  itg2gt0  19519  itg2cnlem1  19520  itg2cnlem2  19521  ibl0  19545  iblrelem  19549  iblposlem  19550  iblpos  19551  iblre  19552  itgreval  19555  itgneg  19562  iblss  19563  i1fibl  19566  itgitg1  19567  itgle  19568  itgge0  19569  itgeqa  19572  itgless  19575  iblconst  19576  itgconst  19577  ibladdlem  19578  itgaddlem1  19581  itgaddlem2  19582  iblabslem  19586  iblabs  19587  iblabsr  19588  iblmulc2  19589  itgmulc2lem1  19590  itgmulc2lem2  19591  itgabs  19593  itgsplit  19594  bddmulibl  19597  itggt0  19600  itgcn  19601  dvferm1  19736  dvferm2  19738  dvferm  19739  dvlip  19744  dvlipcn  19745  c1lip1  19748  dveq0  19751  dv11cn  19752  dvlt0  19756  dvne0  19762  dvfsumge  19773  ftc1lem4  19790  deg1lt0  19881  ply1divex  19926  plypf1  19998  dgradd2  20053  dgrco  20060  plyrecj  20064  plydivlem3  20079  vieta1lem2  20095  aalioulem2  20117  aalioulem3  20118  mtest  20187  radcnvlem1  20196  radcnv0  20199  radcnvlt1  20201  radcnvle  20203  pserulm  20205  psercnlem2  20207  psercnlem1  20208  psercn  20209  pserdvlem1  20210  pserdv  20212  abelthlem2  20215  abelthlem6  20219  abelthlem7  20221  abelth  20224  abelth2  20225  reeff1olem  20229  reeff1o  20230  pilem2  20235  pilem3  20236  pipos  20240  sinhalfpilem  20241  sincosq1sgn  20273  sincosq2sgn  20274  coseq00topi  20277  coseq0negpitopi  20278  tangtx  20280  tanabsge  20281  sinq12ge0  20283  sinq34lt0t  20284  cosq14ge0  20286  sincos4thpi  20288  tan4thpi  20289  sincos6thpi  20290  pige3  20292  sineq0  20296  cosordlem  20300  cosord  20301  cos11  20302  sinord  20303  recosf1o  20304  resinf1o  20305  tanord1  20306  tanord  20307  tanregt0  20308  efif1olem4  20314  efifo  20316  relogrn  20326  log1  20347  logneg  20349  logne0  20364  rplogcl  20366  argregt0  20372  argrege0  20373  argimgt0  20374  logneg2  20377  logdivlti  20382  logdivlt  20383  logdivle  20384  ellogdm  20397  logdmn0  20398  logdmnrp  20399  logcnlem3  20402  logcnlem4  20403  dvloglem  20406  logdmopn  20407  logf1o2  20408  dvlog2lem  20410  efopnlem1  20414  logtayl  20418  recxpcl  20433  cxpge0  20441  abscxp2  20451  cxplt  20452  cxple  20453  cxple2  20455  cxple2a  20457  cxpsqrlem  20460  cxpcn3lem  20498  cxpcn3  20499  cxpaddlelem  20502  cxpaddle  20503  abscxpbnd  20504  loglesqr  20509  ang180lem3  20520  ang180lem4  20521  chordthmlem4  20543  chordthmlem5  20544  asinlem3  20578  atanre  20592  asinneg  20593  asin1  20601  reasinsin  20603  acosbnd  20607  atan0  20615  atanrecl  20618  atanlogaddlem  20620  atanlogadd  20621  atanlogsublem  20622  atanlogsub  20623  atantan  20630  atanbnd  20633  atan1  20635  atans2  20638  ressatans  20641  leibpi  20649  log2cnv  20651  log2tlbnd  20652  log2ublem3  20655  log2ub  20656  rlimcnp  20671  rlimcnp2  20672  rlimcnp3  20673  efrlim  20675  o1cxp  20680  cxp2limlem  20681  cxp2lim  20682  cxploglim2  20684  divsqrsumlem  20685  jensenlem1  20692  jensenlem2  20693  jensen  20694  amgm  20696  emgt0  20712  harmonicbnd3  20713  harmoniclbnd  20714  harmonicubnd  20715  harmonicbnd4  20716  fsumharmonic  20717  ftalem1  20722  ftalem2  20723  ftalem5  20726  basellem3  20732  basellem8  20737  efnnfsumcl  20752  ppisval  20753  vmacl  20768  vmage0  20771  chpge0  20776  chtwordi  20806  efchtdvds  20809  ppiwordi  20812  chtrpcl  20825  ppiltx  20827  fsumfldivdiaglem  20841  ppiub  20855  chpeq0  20859  chteq0  20860  chtleppi  20861  fsumvma2  20865  chpval2  20869  chpchtsum  20870  chpub  20871  logfacbnd3  20874  logexprlim  20876  mersenne  20878  dchr1re  20914  bcmono  20928  efexple  20932  bposlem1  20935  bposlem4  20938  bposlem5  20939  bposlem7  20941  bposlem8  20942  bposlem9  20943  lgslem4  20950  lgsval2lem  20957  lgsval4a  20969  lgsneg  20970  lgsdilem  20973  lgsdir2lem1  20974  lgsne0  20984  lgseisen  21004  lgsquadlem1  21005  lgsquadlem2  21006  m1lgs  21013  2sqlem11  21026  chebbnd1lem2  21031  chebbnd1lem3  21032  chebbnd1  21033  chtppilimlem1  21034  chtppilimlem2  21035  chtppilim  21036  chebbnd2  21038  chto1lb  21039  chpchtlim  21040  chpo1ub  21041  rplogsumlem2  21046  rpvmasumlem  21048  dchrisumlema  21049  dchrisumlem2  21051  dchrisumlem3  21052  dchrmusumlema  21054  dchrvmasumlem2  21059  dchrvmasumiflem1  21062  dchrisum0flblem1  21069  dchrisum0flblem2  21070  dchrisum0fno1  21072  dchrisum0re  21074  dchrisum0lema  21075  dchrisum0  21081  rplogsum  21088  dirith2  21089  logdivsum  21094  mulog2sumlem1  21095  mulog2sumlem2  21096  vmalogdivsum2  21099  log2sumbnd  21105  selberg2lem  21111  chpdifbndlem1  21114  chpdifbndlem2  21115  chpdifbnd  21116  logdivbnd  21117  selberg3lem1  21118  pntrmax  21125  pntrsumo1  21126  pntrlog2bndlem4  21141  pntrlog2bndlem5  21142  pntpbnd1a  21146  pntpbnd1  21147  pntpbnd2  21148  pntlemg  21159  pntlemj  21164  pntlemk  21167  pntlem3  21170  pntleml  21172  pnt2  21174  pnt  21175  ostth2lem1  21179  padicabv  21191  padicabvcxp  21193  ostth2lem3  21196  ostth2lem4  21197  ostth2  21198  ostth3  21199  usgraexvlem  21280  usgraex0elv  21281  spthispth  21427  nvnencycllem  21478  vdgr0  21519  konigsberg  21557  ex-po  21591  gxnval  21696  readdsubgo  21789  nvz0  22005  ipidsq  22057  0blo  22141  nmlno0lem  22142  nmblolbii  22148  siilem2  22201  minvecolem2  22225  minvecolem3  22226  minvecolem4c  22229  minvecolem4  22230  minvecolem5  22231  minvecolem6  22232  minvecolem7  22233  htthlem  22268  hiidge0  22448  normlem6  22465  normgt0  22477  norm-i  22479  normpyc  22496  normpar2i  22506  bcsiALT  22529  pjhthlem1  22741  pjneli  23073  0bdop  23344  nmlnop0iALT  23346  unopbd  23366  nmbdoplbi  23375  nmcoplbi  23379  nmbdfnlbi  23400  nmbdfnlb  23401  nmcfnlbi  23403  cnlnadjlem7  23424  nmopcoi  23446  branmfn  23456  leopmul  23485  nmopleid  23490  pjbdlni  23500  pjnormssi  23519  stge0  23575  stle1  23576  stle0i  23590  strlem3a  23603  cdj3lem1  23785  xlt2addrd  23960  bcm1n  23987  xdiv0  24013  xaddeq0  24030  xrge00  24037  xrge0neqmnf  24041  xrge0adddir  24044  fsumrp0cl  24046  re0g  24089  elunitrn  24099  elunitge0  24101  unitdivcld  24103  sqsscirc1  24110  xrge0iifcnv  24123  xrge0iifiso  24125  xrge0iifhom  24127  xrge0mulc1cn  24131  lmlimxrge0  24138  rge0scvg  24139  pnfneige0  24140  lmxrge0  24141  lmdvg  24142  recusp  24146  rrhre  24183  rnlogblem  24195  logbrec  24201  log2le1  24203  indf  24209  indfval  24210  pr01ssre  24211  indf1o  24217  esumfsupre  24257  esumpfinvallem  24260  esumpfinval  24261  esumpfinvalf  24262  esumpcvgval  24264  esumcvg  24272  measinb  24369  voliune  24379  volfiniune  24380  0rrv  24488  coinfliprv  24519  ballotlem2  24525  ballotlemfc0  24529  ballotlemfcc  24530  ballotlemodife  24534  ballotlem4  24535  ballotlemi1  24539  ballotlemic  24543  zetacvg  24578  eldmgm  24585  dmlogdmgm  24587  lgamgulmlem1  24592  lgamgulmlem2  24593  rescon  24712  iiscon  24718  iillyscon  24719  cvmliftlem2  24752  cvmliftlem10  24760  snmlff  24795  divelunit  24964  mulge0b  24970  relin01  24973  fz0n  24981  4bc2eq6  24983  brbtwn2  25558  axsegconlem7  25576  axsegconlem10  25579  ax5seglem1  25581  ax5seglem2  25582  ax5seglem3  25584  ax5seglem5  25586  ax5seglem6  25587  ax5seglem9  25590  ax5seg  25591  axbtwnid  25592  axpaschlem  25593  axpasch  25594  axlowdimlem1  25595  axlowdimlem6  25600  axlowdimlem7  25601  axlowdimlem10  25604  axlowdim1  25612  axlowdim2  25613  axlowdim  25614  axcontlem2  25618  axcontlem4  25620  axcontlem7  25623  axcontlem10  25626  bpoly4  25819  ovoliunnfl  25953  voliunnfl  25955  volsupnfl  25956  itg2addnclem  25957  itg2addnclem2  25958  itg2addnc  25959  ibladdnclem  25961  itgaddnclem1  25963  itgaddnclem2  25964  iblabsnclem  25968  iblabsnc  25969  iblmulc2nc  25970  itgmulc2nclem1  25971  itgmulc2nclem2  25972  itgabsnc  25974  bddiblnc  25975  itggt0cn  25977  ftc1cnnclem  25978  dvreasin  25980  areacirclem2  25982  areacirclem3  25983  areacirclem4  25984  areacirclem5  25986  areacirc  25988  nn0prpwlem  26016  geomcau  26156  isbnd3  26184  isbnd3b  26185  ssbnd  26188  prdsbnd  26193  bfplem2  26223  bfp  26224  rrnequiv  26235  modelico  26575  irrapxlem1  26576  irrapxlem2  26577  irrapxlem3  26578  irrapxlem4  26579  pellexlem6  26588  pell14qrgt0  26613  elpell14qr2  26616  pell1qrgaplem  26627  pellfundex  26640  pellfundrp  26642  monotoddzzfi  26696  oddcomabszz  26698  zindbi  26700  jm2.24  26719  acongeq  26739  jm2.23  26758  jm2.26lem3  26763  jm3.1lem3  26781  hbtlem5  27001  dvconstbi  27220  ioovolcl  27410  itgsin0pilem1  27412  itgsinexplem1  27416  itgsinexp  27417  stoweidlem1  27418  stoweidlem7  27424  stoweidlem11  27428  stoweidlem17  27434  stoweidlem25  27442  stoweidlem26  27443  stoweidlem34  27451  stoweidlem36  27453  stoweidlem41  27458  stoweidlem42  27459  stoweidlem44  27461  stoweidlem45  27462  stoweidlem55  27472  stoweid  27480  wallispilem1  27482  wallispilem2  27483  wallispilem3  27484  wallispilem4  27485  wallispi  27487  wallispi2lem1  27488  wallispi2  27490  stirlinglem1  27491  stirlinglem3  27493  stirlinglem4  27494  stirlinglem5  27495  stirlinglem6  27496  stirlinglem7  27497  stirlinglem10  27500  stirlinglem11  27501  stirlinglem12  27502  stirlinglem13  27503  stirlinglem14  27504  stirlinglem15  27505  stirlingr  27507  sharhght  27523  ex-gt  27817  sgnpnf  27869  sgnmnf  27871
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
  Copyright terms: Public domain W3C validator