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

Theorem 0re 9896
Description: 0 is a real number. See also 0reALT 10229. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
0re 0 ∈ ℝ

Proof of Theorem 0re
StepHypRef Expression
1 1re 9895 . 2 1 ∈ ℝ
2 ax-rnegex 9863 . 2 (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3 readdcl 9875 . . . . 5 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
41, 3mpan 701 . . . 4 (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5 eleq1 2675 . . . 4 ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 233 . . 3 (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
76rexlimiv 3008 . 2 (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
81, 2, 7mp2b 10 1 0 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  wrex 2896  (class class class)co 6527  cr 9791  0cc0 9792  1c1 9793   + caddc 9795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530
This theorem is referenced by:  0red  9897  0xr  9942  axmulgt0  9963  ne0gt0  9993  00id  10062  mul02lem1  10063  mul02lem2  10064  mul02  10065  addid1  10067  ltaddneg  10102  addgt0  10363  addgegt0  10364  addgtge0  10365  addge0  10366  ltaddpos  10367  ltneg  10377  leneg  10380  lt0neg1  10383  lt0neg2  10384  le0neg1  10385  le0neg2  10386  addge01  10387  suble0  10391  mulge0  10395  msqge0  10398  0le1  10400  relin01  10401  gt0ne0i  10412  gt0ne0d  10441  lt0ne0d  10442  elimge0  10709  ltm1  10712  recgt0  10716  prodgt0  10717  lemul1a  10726  ltmul12a  10728  lemul12a  10730  mulgt1  10731  gt0div  10738  ge0div  10739  mulge0b  10742  lediv12a  10765  recgt1i  10769  recreclt  10771  ledivp1  10774  squeeze0  10775  recgt0ii  10778  ledivp1i  10798  ltdivp1i  10799  fimaxre2  10818  inelr  10857  crne0  10860  nnge1  10893  nngt0  10896  nnnle0  10898  nnrecgt0  10905  0le0  10957  neg1lt0  10974  halfge0  11096  nn0ssre  11143  nn0ge0  11165  nn0nlt0  11166  nn0le0eq0  11168  0mnnnnn0  11172  elnnnn0b  11184  elnnnn0c  11185  nn0sub  11190  elnnz  11220  0z  11221  elnn0z  11223  elnnz1  11236  recnz  11284  gtndiv  11286  fnn0ind  11308  rpge0  11677  rpneg  11695  0nrp  11697  zgt1rpn0n1  11703  0ltpnf  11793  mnflt0  11796  qsqueeze  11865  xneg0  11876  xaddid1  11904  xmulpnf1  11933  xlemul1a  11947  xadddi  11954  xrsupsslem  11965  xrinfmsslem  11966  elrege0  12105  0e0icopnf  12109  0elunit  12117  1elunit  12118  divelunit  12141  lincmb01cmp  12142  iccf1o  12143  unitssre  12146  0nelfz1  12186  fzpreddisj  12215  fz0to4untppr  12266  nn0p1elfzo  12333  ico01fl0  12437  rpsup  12482  modelico  12497  0mod  12518  1mod  12519  expubnd  12738  le2sq2  12756  sqlecan  12788  bernneq2  12808  expnbnd  12810  expnlbnd  12811  expmulnbnd  12813  discr1  12817  discr  12818  facdiv  12891  faclbnd  12894  faclbnd3  12896  faclbnd6  12903  bcval4  12911  bcval5  12922  bcpasc  12925  hasheq0  12967  hashneq0  12968  hashnn0n0nn  12993  hashgt12el  13022  hashgt12el2  13023  hashge2el2dif  13067  lsw0  13151  reim0  13652  re0  13686  im0  13687  rei  13690  imi  13691  cj0  13692  sqeqd  13700  rennim  13773  cnpart  13774  sqr0lem  13775  sqrlem4  13780  resqrex  13785  sqrtgt0  13793  sqrt00  13798  sqrtneglem  13801  sqrt9  13808  sqrt2gt1lt2  13809  leabs  13833  absor  13834  max0add  13844  eqsqrt2d  13902  sqrtpclii  13916  rlimconst  14069  rlimrege0  14104  lo1mul  14152  iserge0  14185  fsum00  14317  isumless  14362  arisum2  14378  georeclim  14388  geo2sum  14389  geo2lim  14391  geoisumr  14394  0.999...  14397  0.999...OLD  14398  cvgrat  14400  bpoly4  14575  cos0  14665  ef01bndlem  14699  sin01bnd  14700  cos01bnd  14701  cos2bnd  14703  sin01gt0  14705  cos01gt0  14706  sincos2sgn  14709  sin4lt0  14710  absef  14712  absefib  14713  efieq1re  14714  epos  14720  znnenlem  14725  rpnnen2lem2  14729  rpnnen2lem3  14730  rpnnen2lem4  14731  rpnnen2lem9  14736  rpnnen2lem12  14739  ruclem6  14749  dvdslelem  14815  divalglem1  14901  divalglem5  14904  divalglem6  14905  flodddiv4  14921  bitsp1o  14939  sadcadd  14964  gcdn0gt0  15023  nn0seqcvgd  15067  algcvgblem  15074  algcvga  15076  pythagtriplem12  15315  pythagtriplem13  15316  pythagtriplem14  15317  pythagtriplem16  15319  prmreclem4  15407  prmreclem5  15408  prmreclem6  15409  1arith  15415  vdwap0  15464  ramz  15513  mulgnegnn  17320  subgmulg  17377  srgbinomlem4  18312  isabvd  18589  abvtrivd  18609  psrbaglesupp  19135  xrs1mnd  19549  xrs10  19550  rge0srg  19582  psgnodpmr  19700  re0g  19722  mnfnei  20777  imasdsf1olem  21929  ssblps  21978  ssbl  21979  xmeter  21989  dscmet  22128  dscopn  22129  nmoi  22274  nmoeq0  22282  0nghm  22287  idnghm  22289  cnbl0  22319  blcvx  22341  xrsxmet  22352  metdseq0  22396  iicmp  22428  iicon  22429  iirev  22467  iihalf1  22469  iihalf1cn  22470  iihalf2  22471  elii1  22473  elii2  22474  iimulcl  22475  icopnfcnv  22480  icopnfhmeo  22481  iccpnfcnv  22482  iccpnfhmeo  22483  xrhmeo  22484  xrhmph  22485  lebnumii  22504  htpycc  22518  reparphti  22536  pcoval1  22552  pco0  22553  pcoval2  22555  pcocn  22556  pcohtpylem  22558  pcopt  22561  pcopt2  22562  pcoass  22563  pcorevlem  22565  reust  22894  recusp  22895  minveclem4c  22921  minveclem2  22922  minveclem3b  22924  minveclem4  22928  minveclem7  22931  pjthlem1  22933  cniccbdd  22954  ovolunnul  22992  ovoliunnul  22999  ovolicc1  23008  ovolre  23017  iccvolcl  23059  ovolioo  23060  ioovolcl  23061  ioorcl  23068  vitalilem2  23101  vitalilem4  23103  vitalilem5  23104  vitali  23105  ismbf  23120  mbfmulc2lem  23137  mbfpos  23141  mbfposr  23142  i1f0  23177  i1f1  23180  itg1addlem2  23187  itg1addlem4  23189  itg1addlem5  23190  mbfi1fseqlem4  23208  mbfi1fseqlem5  23209  mbfi1fseqlem6  23210  mbfi1flimlem  23212  xrge0f  23221  itg2ge0  23225  itg2const  23230  itg2mulc  23237  itg2splitlem  23238  itg2gt0  23250  itg2cnlem1  23251  ibl0  23276  iblrelem  23280  iblposlem  23281  iblpos  23282  iblre  23283  itgreval  23286  itgneg  23293  iblss  23294  i1fibl  23297  itgitg1  23298  itgle  23299  itgeqa  23303  itgless  23306  iblconst  23307  itgconst  23308  ibladdlem  23309  itgaddlem2  23313  iblabslem  23317  iblabsr  23319  iblmulc2  23320  itgmulc2lem2  23322  itgabs  23324  itgsplit  23325  bddmulibl  23328  dvferm1  23469  dvferm2  23471  dvferm  23472  dvlip  23477  c1lip1  23481  dveq0  23484  dv11cn  23485  dvne0  23495  ftc1lem4  23523  ply1divex  23617  dgrco  23752  plyrecj  23756  vieta1lem2  23787  aalioulem2  23809  aalioulem3  23810  pserulm  23897  psercnlem2  23899  psercnlem1  23900  psercn  23901  abelthlem6  23911  abelth  23916  abelth2  23917  reeff1olem  23921  reeff1o  23922  pilem2  23927  pilem3  23928  pipos  23933  sinhalfpilem  23936  sincosq1sgn  23971  sincosq2sgn  23972  coseq00topi  23975  coseq0negpitopi  23976  tangtx  23978  tanabsge  23979  sinq12ge0  23981  sinq34lt0t  23982  cosq14ge0  23984  sincos4thpi  23986  sincos6thpi  23988  pige3  23990  sineq0  23994  cosordlem  23998  cosord  23999  cos11  24000  sinord  24001  recosf1o  24002  resinf1o  24003  tanord1  24004  tanord  24005  tanregt0  24006  efif1olem4  24012  efifo  24014  relogrn  24029  log1  24053  logneg  24055  argregt0  24077  argrege0  24078  argimgt0  24079  logneg2  24082  logdivlti  24087  logdivlt  24088  ellogdm  24102  logdmn0  24103  logdmnrp  24104  logcnlem3  24107  dvloglem  24111  logdmopn  24112  logf1o2  24113  dvlog2lem  24115  efopnlem1  24119  logtayl  24123  recxpcl  24138  cxpge0  24146  cxple2  24160  cxple2a  24162  cxpsqrtlem  24165  cxpcn3  24206  cxpaddlelem  24209  cxpaddle  24210  loglesqrt  24216  logbrec  24237  ang180lem3  24258  ang180lem4  24259  chordthmlem4  24279  heron  24282  asinneg  24330  asin1  24338  reasinsin  24340  acosbnd  24344  atan0  24352  atanrecl  24355  atanlogaddlem  24357  atanlogsublem  24359  atanlogsub  24360  atantan  24367  atanbnd  24370  atan1  24372  atans2  24375  ressatans  24378  leibpi  24386  log2cnv  24388  log2tlbnd  24389  log2ub  24393  log2le1  24394  rlimcnp  24409  rlimcnp2  24410  o1cxp  24418  jensenlem2  24431  jensen  24432  amgm  24434  emgt0  24450  harmonicbnd3  24451  harmoniclbnd  24452  harmonicbnd4  24454  zetacvg  24458  eldmgm  24465  lgamgulmlem2  24473  basellem3  24526  basellem8  24531  efnnfsumcl  24546  ppisval  24547  vmage0  24564  chpge0  24569  efchtdvds  24602  ppiltx  24620  ppiub  24646  chpeq0  24650  chteq0  24651  chtleppi  24652  chpchtsum  24661  chpub  24662  dchr1re  24705  bcmono  24719  efexple  24723  bposlem1  24726  bposlem4  24729  bposlem5  24730  bposlem7  24732  bposlem8  24733  bposlem9  24734  lgsval2lem  24749  lgsval4a  24761  lgsneg  24763  lgsdilem  24766  lgsdir2lem1  24767  2lgsoddprmlem3a  24852  2lgsoddprmlem3b  24853  2lgsoddprmlem3c  24854  2lgsoddprmlem3d  24855  rplogsumlem2  24891  rpvmasumlem  24893  dchrisum0flblem1  24914  dchrisum0flblem2  24915  dchrisum0fno1  24917  rplogsum  24933  logdivsum  24939  mulog2sumlem2  24941  selberg2lem  24956  logdivbnd  24962  pntrsumo1  24971  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  pntpbnd1  24992  pntpbnd2  24993  pntlem3  25015  pntleml  25017  ostth2  25043  trgcgrg  25128  ttgcontlem1  25483  brbtwn2  25503  ax5seglem1  25526  ax5seglem2  25527  ax5seglem3  25529  ax5seglem5  25531  ax5seglem6  25532  ax5seglem9  25535  ax5seg  25536  axbtwnid  25537  axpaschlem  25538  axpasch  25539  axlowdimlem1  25540  axlowdimlem6  25545  axlowdimlem7  25546  axlowdimlem10  25549  axlowdim1  25557  axlowdim2  25558  axlowdim  25559  axcontlem2  25563  axcontlem4  25565  axcontlem7  25568  usgraex0elv  25690  spthispth  25869  vdgr0  26193  rusgranumwlks  26249  konigsberg  26280  ex-po  26450  ex-sqrt  26469  ex-gcd  26472  nvz0  26701  0blo  26837  nmlno0lem  26838  nmblolbii  26844  siilem2  26897  minvecolem2  26921  minvecolem3  26922  minvecolem4c  26925  minvecolem4  26926  minvecolem5  26927  minvecolem7  26929  htthlem  26964  hiidge0  27145  normlem6  27162  normgt0  27174  norm-i  27176  normpyc  27193  bcsiALT  27226  pjhthlem1  27440  pjneli  27772  nmlnop0iALT  28044  unopbd  28064  nmbdoplbi  28073  nmcoplbi  28077  nmbdfnlbi  28098  nmbdfnlb  28099  nmcfnlbi  28101  cnlnadjlem7  28122  nmopcoi  28144  branmfn  28154  leopmul  28183  nmopleid  28188  pjbdlni  28198  pjnormssi  28217  stge0  28273  stle1  28274  stle0i  28288  strlem3a  28301  cdj3lem1  28483  xaddeq0  28713  xdiv0  28774  xrge0slmod  28981  elunitrn  29077  elunitge0  29079  unitdivcld  29081  sqsscirc1  29088  xrge0iifcnv  29113  xrge0iifiso  29115  xrge0iifhom  29117  rezh  29149  indf  29211  indfval  29212  pr01ssre  29213  esumcvgsum  29283  voliune  29425  volfiniune  29426  sibfinima  29534  sitmcl  29546  0rrv  29646  coinfliprv  29677  ballotlem2  29683  ballotlem4  29693  ballotlemi1  29697  ballotlemic  29701  sgnclre  29734  sgnnbi  29740  sgnpbi  29741  plymulx0  29756  signsply0  29760  signswch  29770  signstf  29775  signstf0  29777  signstfveq0  29786  signlem0  29796  rescon  30288  iiscon  30294  iillyscon  30295  cvmliftlem10  30336  snmlff  30371  fz0n  30675  logi  30679  bcneg1  30681  nn0prpwlem  31293  dnizeq0  31441  dnizphlfeqhlf  31442  knoppndvlem13  31491  cnndvlem1  31504  bj-pinftyccb  32081  bj-minftyccb  32085  bj-pinftynminfty  32087  taupilemrplb  32139  sin2h  32365  tan2h  32367  ptrecube  32375  poimirlem16  32391  poimirlem17  32392  poimirlem20  32395  poimirlem22  32397  poimirlem23  32398  poimirlem29  32404  poimirlem30  32405  poimirlem31  32406  poimirlem32  32407  poimir  32408  heicant  32410  mblfinlem2  32413  ismblfin  32416  ovoliunnfl  32417  voliunnfl  32419  volsupnfl  32420  mbfposadd  32423  itg2addnclem  32427  itg2addnclem2  32428  ibladdnclem  32432  itgaddnclem2  32435  iblabsnclem  32439  iblmulc2nc  32441  itgmulc2nclem2  32443  itgabsnc  32445  ftc1cnnclem  32449  ftc1anclem5  32455  ftc1anclem8  32458  asindmre  32461  dvasin  32462  areacirclem4  32469  areacirc  32471  isbnd3  32549  ssbnd  32553  prdsbnd  32558  bfplem2  32588  bfp  32589  renegclALT  33063  pellexlem6  36212  elpell14qr2  36240  oddcomabszz  36323  zindbi  36325  jm2.24  36344  acongeq  36364  arearect  36616  areaquad  36617  relexp01min  36820  imo72b2lem0  37283  imo72b2lem2  37285  imo72b2lem1  37289  imo72b2  37293  dvconstbi  37351  binomcxplemnn0  37366  binomcxplemdvbinom  37370  binomcxplemcvg  37371  binomcxplemnotnn0  37373  sineq0ALT  37991  halffl  38247  sqrlearg  38424  dvnmptdivc  38625  dvnmul  38630  itgsin0pilem1  38638  itgsinexplem1  38642  itgsinexp  38643  iblempty  38654  stoweidlem17  38707  stoweidlem36  38726  stoweidlem55  38745  wallispilem1  38755  wallispilem2  38756  wallispilem4  38758  stirlinglem4  38767  stirlinglem13  38776  stirlinglem14  38777  stirlinglem15  38778  stirlingr  38780  dirker2re  38782  dirkerdenne0  38783  dirkerre  38785  dirkertrigeqlem1  38788  dirkercncflem2  38794  dirkercncflem4  38796  fourierdlem11  38808  fourierdlem16  38813  fourierdlem21  38818  fourierdlem22  38819  fourierdlem41  38838  fourierdlem42  38839  fourierdlem48  38844  fourierdlem62  38858  fourierdlem66  38862  fourierdlem79  38875  fourierdlem83  38879  fourierdlem94  38890  fourierdlem102  38898  fourierdlem103  38899  fourierdlem104  38900  fourierdlem111  38907  fourierdlem112  38908  fourierdlem113  38909  fourierdlem114  38910  sqwvfoura  38918  sqwvfourb  38919  fourierswlem  38920  fouriersw  38921  etransclem23  38947  etransclem44  38968  etransclem46  38970  salexct3  39033  salgensscntex  39035  sge0rnn0  39058  sge00  39066  0ome  39216  ovn0lem  39252  ovnhoilem1  39288  smfmullem1  39473  smfmullem2  39474  smfmullem3  39475  smfmullem4  39476  m1mod0mod1  39747  fmtnoprmfac2lem1  39814  31prm  39848  mod42tp1mod8  39855  tgblthelfgott  40027  tgblthelfgottOLD  40034  zm1nn  40168  xnn0xadd0  40210  umgrislfupgrlem  40342  lfgrnloop  40345  lfuhgr1v0e  40475  pthdlem2  40969  crctcsh1wlkn0lem7  41014  rusgrnumwwlks  41172  konigsberg-av  41422  altgsumbcALT  41919  expnegico01  42097  dignnld  42190  ex-gt  42224
  Copyright terms: Public domain W3C validator