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

Theorem 0re 8834
Description:  0 is a real number. (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 8833 . 2  |-  1  e.  RR
2 ax-rnegex 8804 . 2  |-  ( 1  e.  RR  ->  E. x  e.  RR  ( 1  +  x )  =  0 )
3 readdcl 8816 . . . . 5  |-  ( ( 1  e.  RR  /\  x  e.  RR )  ->  ( 1  +  x
)  e.  RR )
41, 3mpan 653 . . . 4  |-  ( x  e.  RR  ->  (
1  +  x )  e.  RR )
5 eleq1 2345 . . . 4  |-  ( ( 1  +  x )  =  0  ->  (
( 1  +  x
)  e.  RR  <->  0  e.  RR ) )
64, 5syl5ibcom 213 . . 3  |-  ( x  e.  RR  ->  (
( 1  +  x
)  =  0  -> 
0  e.  RR ) )
76rexlimiv 2663 . 2  |-  ( E. x  e.  RR  (
1  +  x )  =  0  ->  0  e.  RR )
81, 2, 7mp2b 11 1  |-  0  e.  RR
Colors of variables: wff set class
Syntax hints:    = wceq 1624    e. wcel 1685   E.wrex 2546  (class class class)co 5820   RRcr 8732   0cc0 8733   1c1 8734    + caddc 8736
This theorem is referenced by:  0xr  8874  axmulgt0  8893  ne0gt0  8921  00id  8983  mul02lem1  8984  mul02lem2  8985  mul02  8986  addid1  8988  gt0ne0  9235  addgt0  9256  addgegt0  9257  addgtge0  9258  addge0  9259  ltaddpos  9260  ltneg  9270  leneg  9273  lt0neg1  9276  lt0neg2  9277  le0neg1  9278  le0neg2  9279  addge01  9280  add20  9282  subge0  9283  suble0  9284  lesub0  9286  mulge0  9287  msqgt0  9290  msqge0  9291  0le1  9293  gt0ne0i  9304  gt0ne0d  9333  lt0ne0d  9334  addgt0d  9343  elimge0  9589  ltm1  9592  recgt0  9596  prodgt0  9597  prodge0  9599  lemul1a  9606  ltmul12a  9608  lemul12a  9610  mulgt1  9611  gt0div  9618  ge0div  9619  lt2msq1  9635  lediv12a  9645  recgt1i  9649  recreclt  9651  ledivp1  9654  squeeze0  9655  recgt0ii  9658  ledivp1i  9678  ltdivp1i  9679  fimaxre2  9698  supmul1  9715  supmul  9718  inelr  9732  crne0  9735  nnge1  9768  nngt0  9771  nnrecgt0  9779  0le0  9823  nn0ssre  9965  nn0ge0  9987  nn0nlt0  9988  nn0le0eq0  9990  elnnnn0b  10004  elnnnn0c  10005  nn0sub  10010  elnnz  10030  0z  10031  elnn0z  10032  elnnz1  10045  nn0lt10b  10074  recnz  10083  gtndiv  10085  uzindOLD  10102  fnn0ind  10106  rpge0  10362  rpgecl  10375  ge0p1rp  10378  rpneg  10379  0nrp  10380  ge0gtmnf  10496  max0sub  10518  qsqueeze  10523  xneg0  10534  xaddid1  10561  xsubge0  10576  xmulpnf1  10589  xmulgt0  10598  xlemul1a  10603  xadddi  10610  xrsupsslem  10620  xrinfmsslem  10621  elrege0  10741  0elunit  10749  1elunit  10750  lincmb01cmp  10772  iccf1o  10773  xov1plusxeqvd  10775  unitssre  10776  rpsup  10965  0mod  10990  1mod  10991  expgt1  11135  ltexp2a  11148  expcan  11149  ltexp2  11150  leexp2  11151  leexp2a  11152  expubnd  11157  le2sq2  11174  sqlecan  11204  bernneq2  11223  expnbnd  11225  expnlbnd  11226  expnlbnd2  11227  expmulnbnd  11228  discr1  11232  discr  11233  facdiv  11295  faclbnd  11298  faclbnd3  11300  faclbnd6  11307  bcval4  11315  bcval5  11325  bcpasc  11328  hasheq0  11348  reim0  11598  re0  11632  im0  11633  rei  11636  imi  11637  cj0  11638  sqeqd  11646  rennim  11719  cnpart  11720  sqr0lem  11721  sqrlem4  11726  resqrex  11731  sqrgt0  11739  sqr00  11744  sqrneglem  11747  sqr4  11753  sqr9  11754  sqr2gt1lt2  11755  leabs  11779  absor  11780  max0add  11790  absgt0  11803  sqreulem  11838  eqsqr2d  11847  amgm2  11848  sqrpclii  11861  rlimconst  12013  rlimrege0  12048  lo1mul  12096  iserge0  12129  iseraltlem2  12150  fsumrecl  12202  fsumge0  12248  fsum00  12251  o1fsum  12266  cvgcmp  12269  cvgcmpce  12271  isumless  12299  arisum2  12314  georeclim  12323  geo2sum  12324  geo2lim  12326  geomulcvg  12327  geoisumr  12329  0.999...  12332  cvgrat  12334  mertenslem2  12336  efcllem  12354  ege2le3  12366  cos0  12425  ef01bndlem  12459  sin01bnd  12460  cos01bnd  12461  cos2bnd  12463  sin01gt0  12465  cos01gt0  12466  sincos2sgn  12469  sin4lt0  12470  absefib  12473  efieq1re  12474  epos  12480  znnenlem  12485  rpnnen2lem2  12489  rpnnen2lem3  12490  rpnnen2lem4  12491  rpnnen2lem9  12496  rpnnen2  12499  rpnnen  12500  ruclem6  12508  nthruz  12525  moddvds  12533  dvdslelem  12568  divalglem1  12588  divalglem5  12591  divalglem6  12592  bitsp1o  12619  bitsinv1lem  12627  sadcaddlem  12643  sadcadd  12644  gcdn0gt0  12696  nn0seqcvgd  12735  algcvgblem  12742  algcvga  12744  qnumgt0  12816  pythagtriplem12  12874  pythagtriplem13  12875  pythagtriplem14  12876  pythagtriplem16  12878  qexpz  12944  prmreclem4  12961  prmreclem5  12962  prmreclem6  12963  1arith  12969  4sqlem6  12985  vdwap0  13018  ramz  13067  mulgnegnn  14572  subgmulg  14630  isabvd  15580  abvf  15583  abvtrivd  15600  psrbaglesupp  16109  xrs1mnd  16404  xrs10  16405  rege0subm  16423  gzrngunit  16432  leordtval2  16937  pnfnei  16945  mnfnei  16946  prdsmet  17929  imasdsf1olem  17932  ssbl  17966  xmeter  17974  dscmet  18090  dscopn  18091  nlmvscnlem2  18191  nlmvscnlem1  18192  nmoi  18232  nmo0  18239  nmoeq0  18240  0nghm  18245  idnghm  18247  cnbl0  18278  blcvx  18299  xrsxmet  18310  metdseq0  18353  iitopon  18378  dfii2  18381  dfii3  18382  dfii5  18384  iicmp  18385  iicon  18386  iirev  18422  iirevcn  18423  iihalf1  18424  iihalf1cn  18425  iihalf2  18426  iihalf2cn  18427  elii1  18428  elii2  18429  iimulcl  18430  iimulcn  18431  icchmeo  18434  icopnfcnv  18435  icopnfhmeo  18436  iccpnfcnv  18437  iccpnfhmeo  18438  xrhmeo  18439  xrhmph  18440  icccvx  18443  evth  18452  lebnumlem1  18454  lebnumii  18459  htpycc  18473  reparphti  18490  pcoval1  18506  pco0  18507  pcoval2  18509  pcocn  18510  pcohtpylem  18512  pcopt  18515  pcopt2  18516  pcoass  18517  pcorevlem  18519  pcorev2  18521  pi1xfrcnv  18550  nmoleub2lem3  18591  cphsqrcl  18615  ipcnlem2  18666  ipcnlem1  18667  minveclem4c  18784  minveclem2  18785  minveclem3b  18787  minveclem4  18791  minveclem6  18793  minveclem7  18794  pjthlem1  18796  cniccbdd  18816  ovollb2lem  18842  ovollb2  18843  ovolunlem1a  18850  ovolunlem1  18851  ovolunnul  18854  ovoliunlem1  18856  ovoliunnul  18861  ovolicc1  18870  ovolicc2lem4  18874  ovolicopnf  18878  ovolre  18879  voliunlem3  18904  volsup  18908  ioombl1lem2  18911  ioombl1lem4  18913  iccvolcl  18919  ovolioo  18920  ioorcl2  18922  ioorcl  18927  uniioombllem1  18931  uniioombllem2  18933  uniioombllem3  18935  uniioombllem6  18938  volivth  18957  vitalilem1  18958  vitalilem2  18959  vitalilem4  18961  vitalilem5  18962  vitali  18963  ismbf  18980  mbfmulc2lem  18997  mbfpos  19001  mbfposr  19002  0plef  19022  i1f0  19037  i1f1  19040  itg1addlem2  19047  itg1addlem4  19049  itg1addlem5  19050  i1fmulc  19053  itg1mulc  19054  itg1ge0a  19061  mbfi1fseqlem3  19067  mbfi1fseqlem4  19068  mbfi1fseqlem5  19069  mbfi1fseqlem6  19070  mbfi1flimlem  19072  mbfi1flim  19073  xrge0f  19081  itg2ge0  19085  itg2const  19090  itg2seq  19092  itg2mulclem  19096  itg2mulc  19097  itg2splitlem  19098  itg2split  19099  itg2monolem1  19100  itg2monolem2  19101  itg2monolem3  19102  itg2mono  19103  itg2i1fseq  19105  itg2gt0  19110  itg2cnlem1  19111  itg2cnlem2  19112  ibl0  19136  iblrelem  19140  iblposlem  19141  iblpos  19142  iblre  19143  itgreval  19146  itgneg  19153  iblss  19154  i1fibl  19157  itgitg1  19158  itgle  19159  itgge0  19160  itgeqa  19163  itgless  19166  iblconst  19167  itgconst  19168  ibladdlem  19169  itgaddlem1  19172  itgaddlem2  19173  iblabslem  19177  iblabs  19178  iblabsr  19179  iblmulc2  19180  itgmulc2lem1  19181  itgmulc2lem2  19182  itgabs  19184  itgsplit  19185  bddmulibl  19188  itggt0  19191  itgcn  19192  dvferm1  19327  dvferm2  19329  dvferm  19330  dvlip  19335  dvlipcn  19336  c1lip1  19339  dveq0  19342  dv11cn  19343  dvlt0  19347  dvne0  19353  dvfsumge  19364  ftc1lem4  19381  deg1lt0  19472  plypf1  19589  dgradd2  19644  dgrco  19651  plyrecj  19655  plydivlem3  19670  vieta1lem2  19686  aalioulem2  19708  aalioulem3  19709  mtest  19776  radcnvlem1  19784  radcnv0  19787  radcnvlt1  19789  radcnvle  19791  pserulm  19793  psercnlem2  19795  psercnlem1  19796  psercn  19797  pserdvlem1  19798  pserdv  19800  abelthlem2  19803  abelthlem6  19807  abelthlem7  19809  abelth  19812  abelth2  19813  reeff1olem  19817  reeff1o  19818  pilem2  19823  pilem3  19824  pipos  19828  sinhalfpilem  19829  sincosq1sgn  19861  sincosq2sgn  19862  coseq00topi  19865  coseq0negpitopi  19866  tangtx  19868  tanabsge  19869  sinq12ge0  19871  sinq34lt0t  19872  cosq14ge0  19874  sincos4thpi  19876  tan4thpi  19877  sincos6thpi  19878  pige3  19880  sineq0  19884  cosordlem  19888  cosord  19889  cos11  19890  sinord  19891  recosf1o  19892  resinf1o  19893  tanord1  19894  tanord  19895  tanregt0  19896  efif1olem4  19902  efifo  19904  relogrn  19914  log1  19934  logneg  19936  logne0  19951  rplogcl  19953  argregt0  19959  argrege0  19960  argimgt0  19961  logneg2  19964  logdivlti  19966  logdivlt  19967  logdivle  19968  ellogdm  19981  logdmn0  19982  logdmnrp  19983  logcnlem3  19986  logcnlem4  19987  dvloglem  19990  logdmopn  19991  logf1o2  19992  dvlog2lem  19994  efopnlem1  19998  logtayl  20002  recxpcl  20017  cxpge0  20025  abscxp2  20035  cxplt  20036  cxple  20037  cxple2  20039  cxple2a  20041  cxpsqrlem  20044  cxpcn3lem  20082  cxpcn3  20083  cxpaddlelem  20086  cxpaddle  20087  abscxpbnd  20088  loglesqr  20093  ang180lem3  20104  ang180lem4  20105  chordthmlem4  20127  chordthmlem5  20128  asinlem3  20162  atanre  20176  asinneg  20177  asin1  20185  reasinsin  20187  acosbnd  20191  atan0  20199  atanrecl  20202  atanlogaddlem  20204  atanlogadd  20205  atanlogsublem  20206  atanlogsub  20207  atantan  20214  atanbnd  20217  atan1  20219  atans2  20222  ressatans  20225  leibpi  20233  log2cnv  20235  log2tlbnd  20236  log2ublem3  20239  log2ub  20240  rlimcnp  20255  rlimcnp2  20256  rlimcnp3  20257  efrlim  20259  o1cxp  20264  cxp2limlem  20265  cxp2lim  20266  cxploglim2  20268  divsqrsumlem  20269  cvxcl  20274  scvxcvx  20275  jensenlem1  20276  jensenlem2  20277  jensen  20278  amgm  20280  emgt0  20295  harmonicbnd3  20296  harmoniclbnd  20297  harmonicubnd  20298  harmonicbnd4  20299  fsumharmonic  20300  ftalem1  20305  ftalem2  20306  ftalem5  20309  basellem3  20315  basellem8  20320  efnnfsumcl  20335  ppisval  20336  vmacl  20351  vmage0  20354  chpge0  20359  chtwordi  20389  efchtdvds  20392  ppiwordi  20395  chtrpcl  20408  ppiltx  20410  fsumfldivdiaglem  20424  ppiub  20438  chpeq0  20442  chteq0  20443  chtleppi  20444  fsumvma2  20448  chpval2  20452  chpchtsum  20453  chpub  20454  logfacbnd3  20457  logexprlim  20459  mersenne  20461  dchr1re  20497  bcmono  20511  efexple  20515  bposlem1  20518  bposlem4  20521  bposlem5  20522  bposlem7  20524  bposlem8  20525  bposlem9  20526  lgslem4  20533  lgsval2lem  20540  lgsval4a  20552  lgsneg  20553  lgsdilem  20556  lgsdir2lem1  20557  lgsne0  20567  lgseisen  20587  lgsquadlem1  20588  lgsquadlem2  20589  m1lgs  20596  2sqlem11  20609  chebbnd1lem2  20614  chebbnd1lem3  20615  chebbnd1  20616  chtppilimlem1  20617  chtppilimlem2  20618  chtppilim  20619  chebbnd2  20621  chto1lb  20622  chpchtlim  20623  chpo1ub  20624  rplogsumlem2  20629  rpvmasumlem  20631  dchrisumlema  20632  dchrisumlem2  20634  dchrisumlem3  20635  dchrmusumlema  20637  dchrvmasumlem2  20642  dchrvmasumiflem1  20645  dchrisum0flblem1  20652  dchrisum0flblem2  20653  dchrisum0fno1  20655  dchrisum0re  20657  dchrisum0lema  20658  dchrisum0  20664  rplogsum  20671  dirith2  20672  logdivsum  20677  mulog2sumlem1  20678  mulog2sumlem2  20679  vmalogdivsum2  20682  log2sumbnd  20688  selberg2lem  20694  chpdifbndlem1  20697  chpdifbndlem2  20698  chpdifbnd  20699  logdivbnd  20700  selberg3lem1  20701  pntrmax  20708  pntrsumo1  20709  pntrlog2bndlem4  20724  pntrlog2bndlem5  20725  pntpbnd1a  20729  pntpbnd1  20730  pntpbnd2  20731  pntlemg  20742  pntlemj  20747  pntlemk  20750  pntlem3  20753  pntleml  20755  pnt2  20757  pnt  20758  ostth2lem1  20762  padicabv  20774  padicabvcxp  20776  ostth2lem3  20779  ostth2lem4  20780  ostth2  20781  ostth3  20782  ex-po  20798  gxnval  20920  readdsubgo  21013  nvz0  21227  ipidsq  21279  0blo  21363  nmlno0lem  21364  nmblolbii  21370  siilem2  21423  minvecolem2  21447  minvecolem3  21448  minvecolem4c  21451  minvecolem4  21452  minvecolem5  21453  minvecolem6  21454  minvecolem7  21455  htthlem  21490  hiidge0  21670  normlem6  21687  normgt0  21699  norm-i  21701  normpyc  21718  normpar2i  21728  bcsiALT  21751  pjhthlem1  21963  pjneli  22295  0bdop  22566  nmlnop0iALT  22568  unopbd  22588  nmbdoplbi  22597  nmcoplbi  22601  nmbdfnlbi  22622  nmbdfnlb  22623  nmcfnlbi  22625  cnlnadjlem7  22646  nmopcoi  22668  branmfn  22678  leopmul  22707  nmopleid  22712  pjbdlni  22722  pjnormssi  22741  stcl  22789  stge0  22797  stle1  22798  stle0i  22812  strlem3a  22825  cdj3lem1  23007  bcm1n  23025  ballotlem2  23041  ballotlemfc0  23045  ballotlemfcc  23046  ballotlemodife  23050  ballotlem4  23051  ballotlemi1  23055  ballotlemic  23059  zetacvg  23094  eldmgm  23099  cvxpcon  23178  cvxscon  23179  rescon  23182  iiscon  23188  iillyscon  23189  cvmliftlem2  23222  cvmliftlem8  23228  cvmliftlem10  23230  konigsberg  23316  snmlff  23317  divelunit  23484  mulge0b  23490  relin01  23493  fz0n  23501  brbtwn2  23941  axsegconlem7  23959  axsegconlem10  23962  ax5seglem1  23964  ax5seglem2  23965  ax5seglem3  23967  ax5seglem5  23969  ax5seglem6  23970  ax5seglem9  23973  ax5seg  23974  axbtwnid  23975  axpaschlem  23976  axpasch  23977  axlowdimlem1  23978  axlowdimlem6  23983  axlowdimlem7  23984  axlowdimlem10  23987  axlowdim1  23995  axlowdim2  23996  axlowdim  23997  axeuclidlem  23998  axcontlem2  24001  axcontlem4  24003  axcontlem7  24006  axcontlem10  24009  bpoly0  24193  cntrset  25002  iintlem1  25010  lvsovso  25026  clscnc  25410  nn0prpwlem  25638  geomcau  25875  isbnd3  25908  isbnd3b  25909  ssbnd  25912  prdsbnd  25917  bfplem2  25947  bfp  25948  rrnequiv  25959  modelico  26306  irrapxlem1  26307  irrapxlem2  26308  irrapxlem3  26309  pellexlem6  26319  pell14qrgt0  26344  elpell14qr2  26347  pell1qrgaplem  26358  pellfundrp  26373  monotoddzzfi  26427  oddcomabszz  26429  zindbi  26431  jm2.24  26450  acongeq  26470  jm2.23  26489  jm2.26lem3  26494  jm3.1lem3  26512  dvconstbi  26951  ioovolcl  27142  itgsin0pilem1  27144  itgsinexplem1  27148  itgsinexp  27149  stoweidlem1  27150  stoweidlem3  27152  stoweidlem7  27156  stoweidlem11  27160  stoweidlem17  27166  stoweidlem25  27174  stoweidlem26  27175  stoweidlem34  27183  stoweidlem36  27185  stoweidlem38  27187  stoweidlem41  27190  stoweidlem42  27191  stoweidlem44  27193  stoweidlem45  27194  stoweidlem55  27204  stoweid  27212  wallispilem1  27214  wallispilem2  27215  wallispilem3  27216  wallispilem4  27217  wallispi  27219  wallispi2lem1  27220  wallispi2lem2  27221  wallispi2  27222  stirlinglem1  27223  stirlinglem3  27225  stirlinglem4  27226  stirlinglem5  27227  stirlinglem6  27228  stirlinglem7  27229  stirlinglem8  27230  stirlinglem10  27232  stirlinglem11  27233  stirlinglem12  27234  stirlinglem13  27235  stirlinglem14  27236  stirlinglem15  27237  stirlingr  27239  ex-gt  27459  sgnpnf  27511  sgnmnf  27513
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266  ax-1cn 8791  ax-icn 8792  ax-addcl 8793  ax-addrcl 8794  ax-mulcl 8795  ax-mulrcl 8796  ax-i2m1 8801  ax-1ne0 8802  ax-rnegex 8804  ax-rrecex 8805  ax-cnre 8806
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-xp 4695  df-cnv 4697  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-fv 5230  df-ov 5823
  Copyright terms: Public domain W3C validator