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

Theorem 0re 10327
Description: The number 0 is real. See also 0reALT 10663. (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 10325 . 2 1 ∈ ℝ
2 ax-rnegex 10292 . 2 (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3 readdcl 10304 . . . . 5 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
41, 3mpan 673 . . . 4 (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5 eleq1 2873 . . . 4 ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 236 . . 3 (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
76rexlimiv 3215 . 2 (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
81, 2, 7mp2b 10 1 0 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wcel 2156  wrex 3097  (class class class)co 6874  cr 10220  0cc0 10221  1c1 10222   + caddc 10224
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-i2m1 10289  ax-1ne0 10290  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-iota 6064  df-fv 6109  df-ov 6877
This theorem is referenced by:  0red  10328  0xr  10371  axmulgt0  10397  ne0gt0  10427  00id  10496  mul02lem1  10497  mul02lem2  10498  mul02  10499  addid1  10501  ltaddneg  10536  addgt0  10799  addgegt0  10800  addgtge0  10801  addge0  10802  ltaddpos  10803  ltneg  10813  leneg  10816  lt0neg1  10819  lt0neg2  10820  le0neg1  10821  le0neg2  10822  addge01  10823  suble0  10827  mulge0  10831  msqge0  10834  0le1  10836  relin01  10837  gt0ne0i  10848  gt0ne0d  10877  lt0ne0d  10878  elimge0  11145  ltm1  11148  recgt0  11152  prodgt0  11153  lemul1a  11162  ltmul12a  11164  lemul12a  11166  mulgt1  11167  gt0div  11174  ge0div  11175  mulge0b  11178  lediv12a  11201  recgt1i  11205  recreclt  11207  ledivp1  11210  squeeze0  11211  recgt0ii  11214  ledivp1i  11234  ltdivp1i  11235  fimaxre2  11254  inelr  11295  crne0  11298  nnge1  11332  nngt0  11335  nnnle0  11337  nnrecgt0  11344  0le0  11393  neg1lt0  11409  halfge0  11516  nn0ssre  11563  nn0ge0  11584  nn0nlt0  11585  nn0le0eq0  11587  0mnnnnn0  11591  elnnnn0b  11603  elnnnn0c  11604  nn0sub  11609  elnnz  11653  0z  11654  elnn0z  11656  elnnz1  11669  recnz  11718  gtndiv  11720  fnn0ind  11742  rpge0  12059  rpneg  12077  0nrp  12079  0ltpnf  12172  mnflt0  12175  qsqueeze  12250  xneg0  12261  xaddid1  12290  xnn0xadd0  12295  xmulpnf1  12322  xlemul1a  12336  xadddi  12343  xrsupsslem  12355  xrinfmsslem  12356  elrege0  12498  0e0icopnf  12502  elicc01  12510  0elunit  12511  lincmb01cmp  12538  unitssre  12542  0nelfz1  12583  fzpreddisj  12613  fz0to4untppr  12666  nn0p1elfzo  12735  ico01fl0  12844  rpsup  12889  modelico  12904  0mod  12925  1mod  12926  expubnd  13144  le2sq2  13162  sqlecan  13194  bernneq2  13214  expnbnd  13216  expnlbnd  13217  expmulnbnd  13219  discr1  13223  discr  13224  facdiv  13294  faclbnd  13297  faclbnd3  13299  faclbnd6  13306  bcval4  13314  bcval5  13325  bcpasc  13328  hasheq0  13372  hashneq0  13373  hashnn0n0nn  13398  hashgt12el  13427  hashgt12el2  13428  hashge2el2dif  13479  lsw0  13564  reim0  14081  re0  14115  im0  14116  rei  14119  imi  14120  cj0  14121  sqeqd  14129  rennim  14202  cnpart  14203  sqr0lem  14204  sqrlem4  14209  resqrex  14214  sqrtgt0  14222  sqrt00  14227  sqrtneglem  14230  sqrt9  14237  sqrt2gt1lt2  14238  leabs  14262  absor  14263  max0add  14273  eqsqrt2d  14331  sqrtpclii  14345  rlimconst  14498  rlimrege0  14533  lo1mul  14581  iserge0  14614  fsum00  14752  isumless  14799  arisum2  14815  georeclim  14825  geo2sum  14826  geo2lim  14828  geoisumr  14831  0.999...  14834  cvgrat  14836  bpoly4  15010  cos0  15100  ef01bndlem  15134  sin01bnd  15135  cos01bnd  15136  cos2bnd  15138  sin01gt0  15140  cos01gt0  15141  sincos2sgn  15144  sin4lt0  15145  absef  15147  absefib  15148  efieq1re  15149  epos  15155  znnenlemOLD  15160  rpnnen2lem2  15164  rpnnen2lem3  15165  rpnnen2lem4  15166  rpnnen2lem9  15171  ruclem6  15184  dvdslelem  15254  divalglem1  15337  divalglem5  15340  divalglem6  15341  flodddiv4  15356  bitsp1o  15374  sadcadd  15399  gcdn0gt0  15458  nn0seqcvgd  15502  algcvgblem  15509  algcvga  15511  pythagtriplem12  15748  pythagtriplem13  15749  pythagtriplem14  15750  pythagtriplem16  15752  prmreclem4  15840  prmreclem5  15841  prmreclem6  15842  1arith  15848  vdwap0  15897  ramz  15946  mulgnegnn  17756  subgmulg  17810  srgbinomlem4  18745  isabvd  19024  abvtrivd  19044  psrbaglesupp  19577  xrs1mnd  19992  xrs10  19993  rge0srg  20025  psgnodpmr  20143  re0g  20167  mnfnei  21239  imasdsf1olem  22391  ssblps  22440  ssbl  22441  xmeter  22451  dscmet  22590  dscopn  22591  nmoi  22745  nmoeq0  22753  0nghm  22758  idnghm  22760  cnbl0  22790  blcvx  22814  xrsxmet  22825  metdseq0  22870  iicmp  22902  iiconn  22903  iihalf1  22943  iihalf1cn  22944  elii1  22947  icopnfcnv  22954  icopnfhmeo  22955  iccpnfcnv  22956  xrhmeo  22958  xrhmph  22959  htpycc  22992  reparphti  23009  pcoval1  23025  pco0  23026  pcoval2  23028  pcocn  23029  pcohtpylem  23031  pcopt  23034  pcopt2  23035  pcoass  23036  pcorevlem  23038  reust  23381  recusp  23382  minveclem4c  23408  minveclem2  23409  minveclem3b  23411  minveclem4  23415  minveclem7  23418  pjthlem1  23420  cniccbdd  23442  ovolunnul  23481  ovoliunnul  23488  ovolicc1  23497  ovolre  23506  iccvolcl  23548  ovolioo  23549  ioovolcl  23551  ioorcl  23558  vitalilem4  23592  vitalilem5  23593  vitali  23594  ismbf  23609  mbfmulc2lem  23628  mbfpos  23632  mbfposr  23633  i1f0  23668  i1f1  23671  itg1addlem2  23678  itg1addlem4  23680  itg1addlem5  23681  mbfi1fseqlem4  23699  mbfi1fseqlem5  23700  mbfi1fseqlem6  23701  mbfi1flimlem  23703  xrge0f  23712  itg2ge0  23716  itg2const  23721  itg2mulc  23728  itg2splitlem  23729  itg2gt0  23741  itg2cnlem1  23742  ibl0  23767  iblrelem  23771  iblposlem  23772  iblpos  23773  iblre  23774  itgreval  23777  itgneg  23784  iblss  23785  i1fibl  23788  itgitg1  23789  itgle  23790  itgeqa  23794  itgless  23797  iblconst  23798  itgconst  23799  ibladdlem  23800  itgaddlem2  23804  iblabslem  23808  iblabsr  23810  iblmulc2  23811  itgmulc2lem2  23813  itgabs  23815  itgsplit  23816  bddmulibl  23819  dvferm1  23962  dvferm2  23964  dvferm  23965  dvlip  23970  c1lip1  23974  dveq0  23977  dv11cn  23978  dvne0  23988  ftc1lem4  24016  ply1divex  24110  dgrco  24245  plyrecj  24249  vieta1lem2  24280  aalioulem2  24302  aalioulem3  24303  pserulm  24390  psercnlem2  24392  psercnlem1  24393  psercn  24394  abelthlem6  24404  abelth  24409  reeff1olem  24414  reeff1o  24415  pilem2  24420  pilem3  24421  pilem3OLD  24422  pipos  24427  sinhalfpilem  24430  sincosq1sgn  24465  sincosq2sgn  24466  coseq00topi  24469  coseq0negpitopi  24470  tangtx  24472  tanabsge  24473  sinq12ge0  24475  sinq34lt0t  24476  cosq14ge0  24478  sincos4thpi  24480  sincos6thpi  24482  pige3  24484  sineq0  24488  cosordlem  24492  cosord  24493  cos11  24494  sinord  24495  recosf1o  24496  resinf1o  24497  tanord1  24498  tanord  24499  tanregt0  24500  efif1olem4  24506  efifo  24508  relogrn  24522  log1  24546  logneg  24548  argregt0  24570  argrege0  24571  argimgt0  24572  logneg2  24575  logdivlti  24580  logdivlt  24581  ellogdm  24599  logdmn0  24600  logdmnrp  24601  logcnlem3  24604  dvloglem  24608  logdmopn  24609  logf1o2  24610  dvlog2lem  24612  efopnlem1  24616  logtayl  24620  recxpcl  24635  cxpge0  24643  cxple2  24657  cxple2a  24659  cxpsqrtlem  24662  cxpcn3  24703  cxpaddlelem  24706  cxpaddle  24707  loglesqrt  24713  logbrec  24734  ang180lem3  24755  ang180lem4  24756  chordthmlem4  24776  heron  24779  asinneg  24827  asin1  24835  reasinsin  24837  acosbnd  24841  atan0  24849  atanrecl  24852  atanlogaddlem  24854  atanlogsublem  24856  atanlogsub  24857  atantan  24864  atanbnd  24867  atan1  24869  atans2  24872  ressatans  24875  log2cnv  24885  log2tlbnd  24886  log2ub  24890  log2le1  24891  rlimcnp  24906  rlimcnp2  24907  o1cxp  24915  jensen  24929  amgm  24931  emgt0  24947  harmonicbnd3  24948  harmoniclbnd  24949  harmonicbnd4  24951  zetacvg  24955  eldmgm  24962  lgamgulmlem2  24970  basellem3  25023  basellem8  25028  efnnfsumcl  25043  ppisval  25044  vmage0  25061  chpge0  25066  efchtdvds  25099  ppiltx  25117  ppiub  25143  chpeq0  25147  chteq0  25148  chtleppi  25149  chpchtsum  25158  chpub  25159  dchr1re  25202  bcmono  25216  efexple  25220  bposlem1  25223  bposlem4  25226  bposlem5  25227  bposlem7  25229  bposlem8  25230  bposlem9  25231  lgsval2lem  25246  lgsval4a  25258  lgsneg  25260  lgsdilem  25263  lgsdir2lem1  25264  2lgsoddprmlem3a  25349  2lgsoddprmlem3b  25350  2lgsoddprmlem3c  25351  2lgsoddprmlem3d  25352  rplogsumlem2  25388  rpvmasumlem  25390  dchrisum0flblem1  25411  dchrisum0flblem2  25412  dchrisum0fno1  25414  rplogsum  25430  logdivsum  25436  mulog2sumlem2  25438  selberg2lem  25453  logdivbnd  25459  pntrsumo1  25468  pntrlog2bndlem4  25483  pntrlog2bndlem5  25484  pntpbnd1  25489  pntpbnd2  25490  pntlem3  25512  pntleml  25514  ostth2  25540  trgcgrg  25624  ttgcontlem1  25979  axlowdimlem1  26036  axlowdimlem6  26041  axlowdimlem7  26042  axlowdimlem10  26045  axlowdim1  26053  axlowdim2  26054  axlowdim  26055  umgrislfupgrlem  26231  lfgrnloop  26234  lfuhgr1v0e  26362  usgrexmplef  26367  pthdlem2  26892  crctcshwlkn0lem7  26937  rusgrnumwwlks  27116  clwwlkn0  27175  konigsberg  27430  ex-po  27623  ex-sqrt  27642  ex-gcd  27645  nvz0  27851  0blo  27975  nmlno0lem  27976  nmblolbii  27982  siilem2  28035  minvecolem2  28059  minvecolem3  28060  minvecolem4c  28063  minvecolem4  28064  minvecolem5  28065  minvecolem7  28067  htthlem  28102  hiidge0  28283  normlem6  28300  normgt0  28312  norm-i  28314  normpyc  28331  bcsiALT  28364  pjhthlem1  28578  pjneli  28910  nmlnop0iALT  29182  unopbd  29202  nmbdoplbi  29211  nmcoplbi  29215  nmbdfnlbi  29236  nmbdfnlb  29237  nmcfnlbi  29239  cnlnadjlem7  29260  nmopcoi  29282  branmfn  29292  leopmul  29321  nmopleid  29326  pjbdlni  29336  pjnormssi  29355  stle0i  29426  cdj3lem1  29621  xaddeq0  29845  pr01ssre  29897  dp20u  29911  dp20h  29912  dp2clq  29914  dp2lt10  29917  dp2lt  29918  dp0u  29934  dplti  29938  dpexpp1  29941  xdiv0  29962  xrge0slmod  30169  unitdivcld  30272  sqsscirc1  30279  xrge0iifcnv  30304  xrge0iifiso  30306  rezh  30340  indf  30402  indfval  30403  esumcvgsum  30475  voliune  30617  volfiniune  30618  sibfinima  30726  sitmcl  30738  0rrv  30838  coinfliprv  30869  ballotlem2  30875  ballotlem4  30885  ballotlemi1  30889  ballotlemic  30893  sgnclre  30926  sgnnbi  30932  sgnpbi  30933  plymulx0  30949  signsply0  30953  signswch  30963  signstf  30968  signstf0  30970  signstfveq0  30979  signlem0  30989  itgexpif  31009  hgt750lemd  31051  hgt750lem  31054  hgt750lem2  31055  hgt750leme  31061  iisconn  31557  iillysconn  31558  cvmliftlem10  31599  fz0n  31938  logi  31942  bcneg1  31944  nn0prpwlem  32638  dnizeq0  32782  dnizphlfeqhlf  32783  knoppndvlem13  32832  cnndvlem1  32845  bj-pinftyccb  33425  bj-minftyccb  33429  bj-pinftynminfty  33431  taupilemrplb  33483  sin2h  33712  tan2h  33714  ptrecube  33722  poimirlem16  33738  poimirlem17  33739  poimirlem20  33742  poimirlem22  33744  poimirlem23  33745  poimirlem29  33751  poimirlem31  33753  poimir  33755  heicant  33757  mblfinlem2  33760  ismblfin  33763  ovoliunnfl  33764  voliunnfl  33766  volsupnfl  33767  mbfposadd  33769  itg2addnclem  33773  itg2addnclem2  33774  ibladdnclem  33778  itgaddnclem2  33781  iblabsnclem  33785  iblmulc2nc  33787  itgmulc2nclem2  33789  itgabsnc  33791  ftc1cnnclem  33795  ftc1anclem5  33801  ftc1anclem8  33804  asindmre  33807  dvasin  33808  areacirclem4  33815  areacirc  33817  isbnd3  33894  ssbnd  33898  prdsbnd  33903  bfplem2  33933  bfp  33934  renegclALT  34742  pellexlem6  37900  elpell14qr2  37928  oddcomabszz  38010  zindbi  38012  jm2.24  38031  acongeq  38051  arearect  38301  areaquad  38302  relexp01min  38505  imo72b2lem0  38965  imo72b2lem2  38967  imo72b2lem1  38971  imo72b2  38975  dvconstbi  39033  binomcxplemnn0  39048  binomcxplemdvbinom  39052  binomcxplemcvg  39053  binomcxplemnotnn0  39055  sineq0ALT  39667  halffl  39991  ren0  40105  sqrlearg  40260  limsup10ex  40485  liminf10ex  40486  dvnmptdivc  40633  dvnmul  40638  itgsin0pilem1  40645  itgsinexplem1  40649  itgsinexp  40650  iblempty  40660  stoweidlem17  40713  stoweidlem36  40732  stoweidlem55  40751  wallispilem1  40761  wallispilem2  40762  wallispilem4  40764  stirlinglem4  40773  stirlinglem13  40782  stirlinglem14  40783  stirlinglem15  40784  stirlingr  40786  dirker2re  40788  dirkerdenne0  40789  dirkerre  40791  dirkertrigeqlem1  40794  dirkercncflem2  40800  dirkercncflem4  40802  fourierdlem11  40814  fourierdlem16  40819  fourierdlem21  40824  fourierdlem22  40825  fourierdlem41  40844  fourierdlem42  40845  fourierdlem48  40850  fourierdlem62  40864  fourierdlem66  40868  fourierdlem79  40881  fourierdlem83  40885  fourierdlem94  40896  fourierdlem102  40904  fourierdlem103  40905  fourierdlem104  40906  fourierdlem111  40913  fourierdlem112  40914  fourierdlem113  40915  fourierdlem114  40916  sqwvfoura  40924  sqwvfourb  40925  fourierswlem  40926  fouriersw  40927  etransclem23  40953  etransclem44  40974  etransclem46  40976  salexct3  41039  salgensscntex  41041  sge0rnn0  41064  sge00  41072  0ome  41225  ovn0lem  41261  ovnhoilem1  41297  smfmullem1  41480  smfmullem2  41481  smfmullem3  41482  smfmullem4  41483  zm1nn  41892  m1mod0mod1  41914  fmtnoprmfac2lem1  42053  31prm  42087  mod42tp1mod8  42094  tgblthelfgott  42278  altgsumbcALT  42699  expnegico01  42876  dignnld  42965  ex-gt  43040
  Copyright terms: Public domain W3C validator