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

Theorem 0re 8838
Description:  0 is a real number. See also 0reALT 9143. (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 8837 . 2  |-  1  e.  RR
2 ax-rnegex 8808 . 2  |-  ( 1  e.  RR  ->  E. x  e.  RR  ( 1  +  x )  =  0 )
3 readdcl 8820 . . . . 5  |-  ( ( 1  e.  RR  /\  x  e.  RR )  ->  ( 1  +  x
)  e.  RR )
41, 3mpan 651 . . . 4  |-  ( x  e.  RR  ->  (
1  +  x )  e.  RR )
5 eleq1 2343 . . . 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 2661 . 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 1623    e. wcel 1684   E.wrex 2544  (class class class)co 5858   RRcr 8736   0cc0 8737   1c1 8738    + caddc 8740
This theorem is referenced by:  0xr  8878  axmulgt0  8897  ne0gt0  8925  00id  8987  mul02lem1  8988  mul02lem2  8989  mul02  8990  addid1  8992  gt0ne0  9239  addgt0  9260  addgegt0  9261  addgtge0  9262  addge0  9263  ltaddpos  9264  ltneg  9274  leneg  9277  lt0neg1  9280  lt0neg2  9281  le0neg1  9282  le0neg2  9283  addge01  9284  add20  9286  subge0  9287  suble0  9288  lesub0  9290  mulge0  9291  msqgt0  9294  msqge0  9295  0le1  9297  gt0ne0i  9308  gt0ne0d  9337  lt0ne0d  9338  addgt0d  9347  elimge0  9593  ltm1  9596  recgt0  9600  prodgt0  9601  prodge0  9603  lemul1a  9610  ltmul12a  9612  lemul12a  9614  mulgt1  9615  gt0div  9622  ge0div  9623  lt2msq1  9639  lediv12a  9649  recgt1i  9653  recreclt  9655  ledivp1  9658  squeeze0  9659  recgt0ii  9662  ledivp1i  9682  ltdivp1i  9683  fimaxre2  9702  supmul1  9719  supmul  9722  inelr  9736  crne0  9739  nnge1  9772  nngt0  9775  nnrecgt0  9783  0le0  9827  nn0ssre  9969  nn0ge0  9991  nn0nlt0  9992  nn0le0eq0  9994  elnnnn0b  10008  elnnnn0c  10009  nn0sub  10014  elnnz  10034  0z  10035  elnn0z  10036  elnnz1  10049  nn0lt10b  10078  recnz  10087  gtndiv  10089  uzindOLD  10106  fnn0ind  10111  rpge0  10366  rpgecl  10379  ge0p1rp  10382  rpneg  10383  0nrp  10384  ge0gtmnf  10501  max0sub  10523  qsqueeze  10528  xneg0  10539  xaddid1  10566  xsubge0  10581  xmulpnf1  10594  xmulgt0  10603  xlemul1a  10608  xadddi  10615  xrsupsslem  10625  xrinfmsslem  10626  elrege0  10746  0elunit  10754  1elunit  10755  lincmb01cmp  10777  iccf1o  10778  xov1plusxeqvd  10780  unitssre  10781  rpsup  10970  0mod  10995  1mod  10996  expgt1  11140  ltexp2a  11153  expcan  11154  ltexp2  11155  leexp2  11156  leexp2a  11157  expubnd  11162  le2sq2  11179  sqlecan  11209  bernneq2  11228  expnbnd  11230  expnlbnd  11231  expnlbnd2  11232  expmulnbnd  11233  discr1  11237  discr  11238  facdiv  11300  faclbnd  11303  faclbnd3  11305  faclbnd6  11312  bcval4  11320  bcval5  11330  bcpasc  11333  hasheq0  11353  reim0  11603  re0  11637  im0  11638  rei  11641  imi  11642  cj0  11643  sqeqd  11651  rennim  11724  cnpart  11725  sqr0lem  11726  sqrlem4  11731  resqrex  11736  sqrgt0  11744  sqr00  11749  sqrneglem  11752  sqr4  11758  sqr9  11759  sqr2gt1lt2  11760  leabs  11784  absor  11785  max0add  11795  absgt0  11808  sqreulem  11843  eqsqr2d  11852  amgm2  11853  sqrpclii  11866  rlimconst  12018  rlimrege0  12053  lo1mul  12101  iserge0  12134  iseraltlem2  12155  fsumrecl  12207  fsumge0  12253  fsum00  12256  o1fsum  12271  cvgcmp  12274  cvgcmpce  12276  isumless  12304  arisum2  12319  georeclim  12328  geo2sum  12329  geo2lim  12331  geomulcvg  12332  geoisumr  12334  0.999...  12337  cvgrat  12339  mertenslem2  12341  efcllem  12359  ege2le3  12371  cos0  12430  ef01bndlem  12464  sin01bnd  12465  cos01bnd  12466  cos2bnd  12468  sin01gt0  12470  cos01gt0  12471  sincos2sgn  12474  sin4lt0  12475  absef  12477  absefib  12478  efieq1re  12479  epos  12485  znnenlem  12490  rpnnen2lem2  12494  rpnnen2lem3  12495  rpnnen2lem4  12496  rpnnen2lem9  12501  rpnnen2  12504  rpnnen  12505  ruclem6  12513  nthruz  12530  moddvds  12538  dvdslelem  12573  divalglem1  12593  divalglem5  12596  divalglem6  12597  bitsp1o  12624  bitsinv1lem  12632  sadcaddlem  12648  sadcadd  12649  gcdn0gt0  12701  nn0seqcvgd  12740  algcvgblem  12747  algcvga  12749  qnumgt0  12821  pythagtriplem12  12879  pythagtriplem13  12880  pythagtriplem14  12881  pythagtriplem16  12883  qexpz  12949  prmreclem4  12966  prmreclem5  12967  prmreclem6  12968  1arith  12974  4sqlem6  12990  vdwap0  13023  ramz  13072  mulgnegnn  14577  subgmulg  14635  isabvd  15585  abvf  15588  abvtrivd  15605  psrbaglesupp  16114  xrs1mnd  16409  xrs10  16410  rege0subm  16428  gzrngunit  16437  leordtval2  16942  pnfnei  16950  mnfnei  16951  prdsmet  17934  imasdsf1olem  17937  ssbl  17971  xmeter  17979  dscmet  18095  dscopn  18096  nlmvscnlem2  18196  nlmvscnlem1  18197  nmoi  18237  nmo0  18244  nmoeq0  18245  0nghm  18250  idnghm  18252  cnbl0  18283  blcvx  18304  xrsxmet  18315  metdseq0  18358  iitopon  18383  dfii2  18386  dfii3  18387  dfii5  18389  iicmp  18390  iicon  18391  iirev  18427  iirevcn  18428  iihalf1  18429  iihalf1cn  18430  iihalf2  18431  iihalf2cn  18432  elii1  18433  elii2  18434  iimulcl  18435  iimulcn  18436  icchmeo  18439  icopnfcnv  18440  icopnfhmeo  18441  iccpnfcnv  18442  iccpnfhmeo  18443  xrhmeo  18444  xrhmph  18445  icccvx  18448  evth  18457  lebnumlem1  18459  lebnumii  18464  htpycc  18478  reparphti  18495  pcoval1  18511  pco0  18512  pcoval2  18514  pcocn  18515  pcohtpylem  18517  pcopt  18520  pcopt2  18521  pcoass  18522  pcorevlem  18524  pcorev2  18526  pi1xfrcnv  18555  nmoleub2lem3  18596  cphsqrcl  18620  ipcnlem2  18671  ipcnlem1  18672  minveclem4c  18789  minveclem2  18790  minveclem3b  18792  minveclem4  18796  minveclem6  18798  minveclem7  18799  pjthlem1  18801  cniccbdd  18821  ovollb2lem  18847  ovollb2  18848  ovolunlem1a  18855  ovolunlem1  18856  ovolunnul  18859  ovoliunlem1  18861  ovoliunnul  18866  ovolicc1  18875  ovolicc2lem4  18879  ovolicopnf  18883  ovolre  18884  voliunlem3  18909  volsup  18913  ioombl1lem2  18916  ioombl1lem4  18918  iccvolcl  18924  ovolioo  18925  ioorcl2  18927  ioorcl  18932  uniioombllem1  18936  uniioombllem2  18938  uniioombllem3  18940  uniioombllem6  18943  volivth  18962  vitalilem1  18963  vitalilem2  18964  vitalilem4  18966  vitalilem5  18967  vitali  18968  ismbf  18985  mbfmulc2lem  19002  mbfpos  19006  mbfposr  19007  0plef  19027  i1f0  19042  i1f1  19045  itg1addlem2  19052  itg1addlem4  19054  itg1addlem5  19055  i1fmulc  19058  itg1mulc  19059  itg1ge0a  19066  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1fseqlem6  19075  mbfi1flimlem  19077  mbfi1flim  19078  xrge0f  19086  itg2ge0  19090  itg2const  19095  itg2seq  19097  itg2mulclem  19101  itg2mulc  19102  itg2splitlem  19103  itg2split  19104  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseq  19110  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  ibl0  19141  iblrelem  19145  iblposlem  19146  iblpos  19147  iblre  19148  itgreval  19151  itgneg  19158  iblss  19159  i1fibl  19162  itgitg1  19163  itgle  19164  itgge0  19165  itgeqa  19168  itgless  19171  iblconst  19172  itgconst  19173  ibladdlem  19174  itgaddlem1  19177  itgaddlem2  19178  iblabslem  19182  iblabs  19183  iblabsr  19184  iblmulc2  19185  itgmulc2lem1  19186  itgmulc2lem2  19187  itgabs  19189  itgsplit  19190  bddmulibl  19193  itggt0  19196  itgcn  19197  dvferm1  19332  dvferm2  19334  dvferm  19335  dvlip  19340  dvlipcn  19341  c1lip1  19344  dveq0  19347  dv11cn  19348  dvlt0  19352  dvne0  19358  dvfsumge  19369  ftc1lem4  19386  deg1lt0  19477  ply1divex  19522  plypf1  19594  dgradd2  19649  dgrco  19656  plyrecj  19660  plydivlem3  19675  vieta1lem2  19691  aalioulem2  19713  aalioulem3  19714  mtest  19781  radcnvlem1  19789  radcnv0  19792  radcnvlt1  19794  radcnvle  19796  pserulm  19798  psercnlem2  19800  psercnlem1  19801  psercn  19802  pserdvlem1  19803  pserdv  19805  abelthlem2  19808  abelthlem6  19812  abelthlem7  19814  abelth  19817  abelth2  19818  reeff1olem  19822  reeff1o  19823  pilem2  19828  pilem3  19829  pipos  19833  sinhalfpilem  19834  sincosq1sgn  19866  sincosq2sgn  19867  coseq00topi  19870  coseq0negpitopi  19871  tangtx  19873  tanabsge  19874  sinq12ge0  19876  sinq34lt0t  19877  cosq14ge0  19879  sincos4thpi  19881  tan4thpi  19882  sincos6thpi  19883  pige3  19885  sineq0  19889  cosordlem  19893  cosord  19894  cos11  19895  sinord  19896  recosf1o  19897  resinf1o  19898  tanord1  19899  tanord  19900  tanregt0  19901  efif1olem4  19907  efifo  19909  relogrn  19919  log1  19939  logneg  19941  logne0  19956  rplogcl  19958  argregt0  19964  argrege0  19965  argimgt0  19966  logneg2  19969  logdivlti  19971  logdivlt  19972  logdivle  19973  ellogdm  19986  logdmn0  19987  logdmnrp  19988  logcnlem3  19991  logcnlem4  19992  dvloglem  19995  logdmopn  19996  logf1o2  19997  dvlog2lem  19999  efopnlem1  20003  logtayl  20007  recxpcl  20022  cxpge0  20030  abscxp2  20040  cxplt  20041  cxple  20042  cxple2  20044  cxple2a  20046  cxpsqrlem  20049  cxpcn3lem  20087  cxpcn3  20088  cxpaddlelem  20091  cxpaddle  20092  abscxpbnd  20093  loglesqr  20098  ang180lem3  20109  ang180lem4  20110  chordthmlem4  20132  chordthmlem5  20133  asinlem3  20167  atanre  20181  asinneg  20182  asin1  20190  reasinsin  20192  acosbnd  20196  atan0  20204  atanrecl  20207  atanlogaddlem  20209  atanlogadd  20210  atanlogsublem  20211  atanlogsub  20212  atantan  20219  atanbnd  20222  atan1  20224  atans2  20227  ressatans  20230  leibpi  20238  log2cnv  20240  log2tlbnd  20241  log2ublem3  20244  log2ub  20245  rlimcnp  20260  rlimcnp2  20261  rlimcnp3  20262  efrlim  20264  o1cxp  20269  cxp2limlem  20270  cxp2lim  20271  cxploglim2  20273  divsqrsumlem  20274  cvxcl  20279  scvxcvx  20280  jensenlem1  20281  jensenlem2  20282  jensen  20283  amgm  20285  emgt0  20300  harmonicbnd3  20301  harmoniclbnd  20302  harmonicubnd  20303  harmonicbnd4  20304  fsumharmonic  20305  ftalem1  20310  ftalem2  20311  ftalem5  20314  basellem3  20320  basellem8  20325  efnnfsumcl  20340  ppisval  20341  vmacl  20356  vmage0  20359  chpge0  20364  chtwordi  20394  efchtdvds  20397  ppiwordi  20400  chtrpcl  20413  ppiltx  20415  fsumfldivdiaglem  20429  ppiub  20443  chpeq0  20447  chteq0  20448  chtleppi  20449  fsumvma2  20453  chpval2  20457  chpchtsum  20458  chpub  20459  logfacbnd3  20462  logexprlim  20464  mersenne  20466  dchr1re  20502  bcmono  20516  efexple  20520  bposlem1  20523  bposlem4  20526  bposlem5  20527  bposlem7  20529  bposlem8  20530  bposlem9  20531  lgslem4  20538  lgsval2lem  20545  lgsval4a  20557  lgsneg  20558  lgsdilem  20561  lgsdir2lem1  20562  lgsne0  20572  lgseisen  20592  lgsquadlem1  20593  lgsquadlem2  20594  m1lgs  20601  2sqlem11  20614  chebbnd1lem2  20619  chebbnd1lem3  20620  chebbnd1  20621  chtppilimlem1  20622  chtppilimlem2  20623  chtppilim  20624  chebbnd2  20626  chto1lb  20627  chpchtlim  20628  chpo1ub  20629  rplogsumlem2  20634  rpvmasumlem  20636  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  dchrmusumlema  20642  dchrvmasumlem2  20647  dchrvmasumiflem1  20650  dchrisum0flblem1  20657  dchrisum0flblem2  20658  dchrisum0fno1  20660  dchrisum0re  20662  dchrisum0lema  20663  dchrisum0  20669  rplogsum  20676  dirith2  20677  logdivsum  20682  mulog2sumlem1  20683  mulog2sumlem2  20684  vmalogdivsum2  20687  log2sumbnd  20693  selberg2lem  20699  chpdifbndlem1  20702  chpdifbndlem2  20703  chpdifbnd  20704  logdivbnd  20705  selberg3lem1  20706  pntrmax  20713  pntrsumo1  20714  pntrlog2bndlem4  20729  pntrlog2bndlem5  20730  pntpbnd1a  20734  pntpbnd1  20735  pntpbnd2  20736  pntlemg  20747  pntlemj  20752  pntlemk  20755  pntlem3  20758  pntleml  20760  pnt2  20762  pnt  20763  ostth2lem1  20767  padicabv  20779  padicabvcxp  20781  ostth2lem3  20784  ostth2lem4  20785  ostth2  20786  ostth3  20787  ex-po  20822  gxnval  20927  readdsubgo  21020  nvz0  21234  ipidsq  21286  0blo  21370  nmlno0lem  21371  nmblolbii  21377  siilem2  21430  minvecolem2  21454  minvecolem3  21455  minvecolem4c  21458  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  minvecolem7  21462  htthlem  21497  hiidge0  21677  normlem6  21694  normgt0  21706  norm-i  21708  normpyc  21725  normpar2i  21735  bcsiALT  21758  pjhthlem1  21970  pjneli  22302  0bdop  22573  nmlnop0iALT  22575  unopbd  22595  nmbdoplbi  22604  nmcoplbi  22608  nmbdfnlbi  22629  nmbdfnlb  22630  nmcfnlbi  22632  cnlnadjlem7  22653  nmopcoi  22675  branmfn  22685  leopmul  22714  nmopleid  22719  pjbdlni  22729  pjnormssi  22748  stcl  22796  stge0  22804  stle1  22805  stle0i  22819  strlem3a  22832  cdj3lem1  23014  bcm1n  23032  ballotlem2  23047  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemodife  23056  ballotlem4  23057  ballotlemi1  23061  ballotlemic  23065  xdiv0  23112  xlt2addrd  23253  unitsscn  23280  elunitrn  23281  elunitge0  23283  unitdivcld  23285  sqsscirc1  23292  xaddeq0  23304  xrge00  23311  xrge0iifcnv  23315  xrge0iifiso  23317  xrge0iifhom  23319  xrge0mulc1cn  23323  xrge0neqmnf  23330  xrge0adddir  23332  fsumrp0cl  23334  lmlimxrge0  23372  rge0scvg  23373  pnfneige0  23374  lmxrge0  23375  lmdvg  23376  rnlogblem  23401  logbrec  23407  log2le1  23409  esumpfinvallem  23442  esumpfinval  23443  esumpfinvalf  23444  esumpcvgval  23446  esumcvg  23454  measinb  23548  indf  23599  indfval  23600  pr01ssre  23601  indf1o  23607  probvalrnd  23627  probmeasb  23633  cndprobprob  23641  0rrv  23654  coinfliprv  23683  zetacvg  23689  eldmgm  23694  cvxpcon  23773  cvxscon  23774  rescon  23777  iiscon  23783  iillyscon  23784  cvmliftlem2  23817  cvmliftlem8  23823  cvmliftlem10  23825  konigsberg  23911  snmlff  23912  divelunit  24080  mulge0b  24086  relin01  24089  fz0n  24097  4bc2eq6  24099  brbtwn2  24533  axsegconlem7  24551  axsegconlem10  24554  ax5seglem1  24556  ax5seglem2  24557  ax5seglem3  24559  ax5seglem5  24561  ax5seglem6  24562  ax5seglem9  24565  ax5seg  24566  axbtwnid  24567  axpaschlem  24568  axpasch  24569  axlowdimlem1  24570  axlowdimlem6  24575  axlowdimlem7  24576  axlowdimlem10  24579  axlowdim1  24587  axlowdim2  24588  axlowdim  24589  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem10  24601  bpoly0  24785  bpoly4  24794  dvreasin  24923  areacirclem2  24925  areacirclem3  24926  areacirclem4  24927  areacirclem5  24929  areacirc  24931  cntrset  25602  iintlem1  25610  lvsovso  25626  clscnc  26010  nn0prpwlem  26238  geomcau  26475  isbnd3  26508  isbnd3b  26509  ssbnd  26512  prdsbnd  26517  bfplem2  26547  bfp  26548  rrnequiv  26559  modelico  26906  irrapxlem1  26907  irrapxlem2  26908  irrapxlem3  26909  irrapxlem4  26910  pellexlem6  26919  pell14qrgt0  26944  elpell14qr2  26947  pell1qrgaplem  26958  pellfundex  26971  pellfundrp  26973  monotoddzzfi  27027  oddcomabszz  27029  zindbi  27031  jm2.24  27050  acongeq  27070  jm2.23  27089  jm2.26lem3  27094  jm3.1lem3  27112  hbtlem5  27332  dvconstbi  27551  ioovolcl  27742  itgsin0pilem1  27744  itgsinexplem1  27748  itgsinexp  27749  stoweidlem1  27750  stoweidlem3  27752  stoweidlem7  27756  stoweidlem11  27760  stoweidlem17  27766  stoweidlem25  27774  stoweidlem26  27775  stoweidlem34  27783  stoweidlem36  27785  stoweidlem38  27787  stoweidlem41  27790  stoweidlem42  27791  stoweidlem44  27793  stoweidlem45  27794  stoweidlem55  27804  stoweid  27812  wallispilem1  27814  wallispilem2  27815  wallispilem3  27816  wallispilem4  27817  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  wallispi2  27822  stirlinglem1  27823  stirlinglem3  27825  stirlinglem4  27826  stirlinglem5  27827  stirlinglem6  27828  stirlinglem7  27829  stirlinglem8  27830  stirlinglem10  27832  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  stirlinglem14  27836  stirlinglem15  27837  stirlingr  27839  sharhght  27855  usgraexvlem  28127  ex-gt  28198  sgnpnf  28250  sgnmnf  28252
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-i2m1 8805  ax-1ne0 8806  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator