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

Theorem 0re 9919
Description: 0 is a real number. See also 0reALT 10257. (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 9918 . 2 1 ∈ ℝ
2 ax-rnegex 9886 . 2 (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3 readdcl 9898 . . . . 5 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
41, 3mpan 702 . . . 4 (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5 eleq1 2676 . . . 4 ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 234 . . 3 (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
76rexlimiv 3009 . 2 (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
81, 2, 7mp2b 10 1 0 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  wcel 1977  wrex 2897  (class class class)co 6549  cr 9814  0cc0 9815  1c1 9816   + caddc 9818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552
This theorem is referenced by:  0red  9920  0xr  9965  axmulgt0  9991  ne0gt0  10021  00id  10090  mul02lem1  10091  mul02lem2  10092  mul02  10093  addid1  10095  ltaddneg  10130  addgt0  10393  addgegt0  10394  addgtge0  10395  addge0  10396  ltaddpos  10397  ltneg  10407  leneg  10410  lt0neg1  10413  lt0neg2  10414  le0neg1  10415  le0neg2  10416  addge01  10417  suble0  10421  mulge0  10425  msqge0  10428  0le1  10430  relin01  10431  gt0ne0i  10442  gt0ne0d  10471  lt0ne0d  10472  elimge0  10739  ltm1  10742  recgt0  10746  prodgt0  10747  lemul1a  10756  ltmul12a  10758  lemul12a  10760  mulgt1  10761  gt0div  10768  ge0div  10769  mulge0b  10772  lediv12a  10795  recgt1i  10799  recreclt  10801  ledivp1  10804  squeeze0  10805  recgt0ii  10808  ledivp1i  10828  ltdivp1i  10829  fimaxre2  10848  inelr  10887  crne0  10890  nnge1  10923  nngt0  10926  nnnle0  10928  nnrecgt0  10935  0le0  10987  neg1lt0  11004  halfge0  11126  nn0ssre  11173  nn0ge0  11195  nn0nlt0  11196  nn0le0eq0  11198  0mnnnnn0  11202  elnnnn0b  11214  elnnnn0c  11215  nn0sub  11220  elnnz  11264  0z  11265  elnn0z  11267  elnnz1  11280  recnz  11328  gtndiv  11330  fnn0ind  11352  rpge0  11721  rpneg  11739  0nrp  11741  zgt1rpn0n1  11747  0ltpnf  11832  mnflt0  11835  qsqueeze  11906  xneg0  11917  xaddid1  11946  xnn0xadd0  11949  xmulpnf1  11976  xlemul1a  11990  xadddi  11997  xrsupsslem  12009  xrinfmsslem  12010  elrege0  12149  0e0icopnf  12153  0elunit  12161  1elunit  12162  divelunit  12185  lincmb01cmp  12186  iccf1o  12187  unitssre  12190  0nelfz1  12231  fzpreddisj  12260  fz0to4untppr  12311  nn0p1elfzo  12378  ico01fl0  12482  rpsup  12527  modelico  12542  0mod  12563  1mod  12564  expubnd  12783  le2sq2  12801  sqlecan  12833  bernneq2  12853  expnbnd  12855  expnlbnd  12856  expmulnbnd  12858  discr1  12862  discr  12863  facdiv  12936  faclbnd  12939  faclbnd3  12941  faclbnd6  12948  bcval4  12956  bcval5  12967  bcpasc  12970  hasheq0  13015  hashneq0  13016  hashnn0n0nn  13041  hashgt12el  13070  hashgt12el2  13071  hashge2el2dif  13117  lsw0  13205  reim0  13706  re0  13740  im0  13741  rei  13744  imi  13745  cj0  13746  sqeqd  13754  rennim  13827  cnpart  13828  sqr0lem  13829  sqrlem4  13834  resqrex  13839  sqrtgt0  13847  sqrt00  13852  sqrtneglem  13855  sqrt9  13862  sqrt2gt1lt2  13863  leabs  13887  absor  13888  max0add  13898  eqsqrt2d  13956  sqrtpclii  13970  rlimconst  14123  rlimrege0  14158  lo1mul  14206  iserge0  14239  fsum00  14371  isumless  14416  arisum2  14432  georeclim  14442  geo2sum  14443  geo2lim  14445  geoisumr  14448  0.999...  14451  0.999...OLD  14452  cvgrat  14454  bpoly4  14629  cos0  14719  ef01bndlem  14753  sin01bnd  14754  cos01bnd  14755  cos2bnd  14757  sin01gt0  14759  cos01gt0  14760  sincos2sgn  14763  sin4lt0  14764  absef  14766  absefib  14767  efieq1re  14768  epos  14774  znnenlem  14779  rpnnen2lem2  14783  rpnnen2lem3  14784  rpnnen2lem4  14785  rpnnen2lem9  14790  rpnnen2lem12  14793  ruclem6  14803  dvdslelem  14869  divalglem1  14955  divalglem5  14958  divalglem6  14959  flodddiv4  14975  bitsp1o  14993  sadcadd  15018  gcdn0gt0  15077  nn0seqcvgd  15121  algcvgblem  15128  algcvga  15130  pythagtriplem12  15369  pythagtriplem13  15370  pythagtriplem14  15371  pythagtriplem16  15373  prmreclem4  15461  prmreclem5  15462  prmreclem6  15463  1arith  15469  vdwap0  15518  ramz  15567  mulgnegnn  17374  subgmulg  17431  srgbinomlem4  18366  isabvd  18643  abvtrivd  18663  psrbaglesupp  19189  xrs1mnd  19603  xrs10  19604  rge0srg  19636  psgnodpmr  19755  re0g  19777  mnfnei  20835  imasdsf1olem  21988  ssblps  22037  ssbl  22038  xmeter  22048  dscmet  22187  dscopn  22188  nmoi  22342  nmoeq0  22350  0nghm  22355  idnghm  22357  cnbl0  22387  blcvx  22409  xrsxmet  22420  metdseq0  22465  iicmp  22497  iicon  22498  iirev  22536  iihalf1  22538  iihalf1cn  22539  iihalf2  22540  elii1  22542  elii2  22543  iimulcl  22544  icopnfcnv  22549  icopnfhmeo  22550  iccpnfcnv  22551  iccpnfhmeo  22552  xrhmeo  22553  xrhmph  22554  lebnumii  22573  htpycc  22587  reparphti  22605  pcoval1  22621  pco0  22622  pcoval2  22624  pcocn  22625  pcohtpylem  22627  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  reust  22977  recusp  22978  minveclem4c  23004  minveclem2  23005  minveclem3b  23007  minveclem4  23011  minveclem7  23014  pjthlem1  23016  cniccbdd  23037  ovolunnul  23075  ovoliunnul  23082  ovolicc1  23091  ovolre  23100  iccvolcl  23142  ovolioo  23143  ioovolcl  23144  ioorcl  23151  vitalilem2  23184  vitalilem4  23186  vitalilem5  23187  vitali  23188  ismbf  23203  mbfmulc2lem  23220  mbfpos  23224  mbfposr  23225  i1f0  23260  i1f1  23263  itg1addlem2  23270  itg1addlem4  23272  itg1addlem5  23273  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  mbfi1flimlem  23295  xrge0f  23304  itg2ge0  23308  itg2const  23313  itg2mulc  23320  itg2splitlem  23321  itg2gt0  23333  itg2cnlem1  23334  ibl0  23359  iblrelem  23363  iblposlem  23364  iblpos  23365  iblre  23366  itgreval  23369  itgneg  23376  iblss  23377  i1fibl  23380  itgitg1  23381  itgle  23382  itgeqa  23386  itgless  23389  iblconst  23390  itgconst  23391  ibladdlem  23392  itgaddlem2  23396  iblabslem  23400  iblabsr  23402  iblmulc2  23403  itgmulc2lem2  23405  itgabs  23407  itgsplit  23408  bddmulibl  23411  dvferm1  23552  dvferm2  23554  dvferm  23555  dvlip  23560  c1lip1  23564  dveq0  23567  dv11cn  23568  dvne0  23578  ftc1lem4  23606  ply1divex  23700  dgrco  23835  plyrecj  23839  vieta1lem2  23870  aalioulem2  23892  aalioulem3  23893  pserulm  23980  psercnlem2  23982  psercnlem1  23983  psercn  23984  abelthlem6  23994  abelth  23999  abelth2  24000  reeff1olem  24004  reeff1o  24005  pilem2  24010  pilem3  24011  pipos  24016  sinhalfpilem  24019  sincosq1sgn  24054  sincosq2sgn  24055  coseq00topi  24058  coseq0negpitopi  24059  tangtx  24061  tanabsge  24062  sinq12ge0  24064  sinq34lt0t  24065  cosq14ge0  24067  sincos4thpi  24069  sincos6thpi  24071  pige3  24073  sineq0  24077  cosordlem  24081  cosord  24082  cos11  24083  sinord  24084  recosf1o  24085  resinf1o  24086  tanord1  24087  tanord  24088  tanregt0  24089  efif1olem4  24095  efifo  24097  relogrn  24112  log1  24136  logneg  24138  argregt0  24160  argrege0  24161  argimgt0  24162  logneg2  24165  logdivlti  24170  logdivlt  24171  ellogdm  24185  logdmn0  24186  logdmnrp  24187  logcnlem3  24190  dvloglem  24194  logdmopn  24195  logf1o2  24196  dvlog2lem  24198  efopnlem1  24202  logtayl  24206  recxpcl  24221  cxpge0  24229  cxple2  24243  cxple2a  24245  cxpsqrtlem  24248  cxpcn3  24289  cxpaddlelem  24292  cxpaddle  24293  loglesqrt  24299  logbrec  24320  ang180lem3  24341  ang180lem4  24342  chordthmlem4  24362  heron  24365  asinneg  24413  asin1  24421  reasinsin  24423  acosbnd  24427  atan0  24435  atanrecl  24438  atanlogaddlem  24440  atanlogsublem  24442  atanlogsub  24443  atantan  24450  atanbnd  24453  atan1  24455  atans2  24458  ressatans  24461  leibpi  24469  log2cnv  24471  log2tlbnd  24472  log2ub  24476  log2le1  24477  rlimcnp  24492  rlimcnp2  24493  o1cxp  24501  jensenlem2  24514  jensen  24515  amgm  24517  emgt0  24533  harmonicbnd3  24534  harmoniclbnd  24535  harmonicbnd4  24537  zetacvg  24541  eldmgm  24548  lgamgulmlem2  24556  basellem3  24609  basellem8  24614  efnnfsumcl  24629  ppisval  24630  vmage0  24647  chpge0  24652  efchtdvds  24685  ppiltx  24703  ppiub  24729  chpeq0  24733  chteq0  24734  chtleppi  24735  chpchtsum  24744  chpub  24745  dchr1re  24788  bcmono  24802  efexple  24806  bposlem1  24809  bposlem4  24812  bposlem5  24813  bposlem7  24815  bposlem8  24816  bposlem9  24817  lgsval2lem  24832  lgsval4a  24844  lgsneg  24846  lgsdilem  24849  lgsdir2lem1  24850  2lgsoddprmlem3a  24935  2lgsoddprmlem3b  24936  2lgsoddprmlem3c  24937  2lgsoddprmlem3d  24938  rplogsumlem2  24974  rpvmasumlem  24976  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0fno1  25000  rplogsum  25016  logdivsum  25022  mulog2sumlem2  25024  selberg2lem  25039  logdivbnd  25045  pntrsumo1  25054  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntpbnd1  25075  pntpbnd2  25076  pntlem3  25098  pntleml  25100  ostth2  25126  trgcgrg  25210  ttgcontlem1  25565  brbtwn2  25585  ax5seglem1  25608  ax5seglem2  25609  ax5seglem3  25611  ax5seglem5  25613  ax5seglem6  25614  ax5seglem9  25617  ax5seg  25618  axbtwnid  25619  axpaschlem  25620  axpasch  25621  axlowdimlem1  25622  axlowdimlem6  25627  axlowdimlem7  25628  axlowdimlem10  25631  axlowdim1  25639  axlowdim2  25640  axlowdim  25641  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  umgrislfupgrlem  25788  lfgrnloop  25791  usgraex0elv  25924  spthispth  26103  vdgr0  26427  rusgranumwlks  26483  konigsberg  26514  ex-po  26684  ex-sqrt  26703  ex-gcd  26706  nvz0  26907  0blo  27031  nmlno0lem  27032  nmblolbii  27038  siilem2  27091  minvecolem2  27115  minvecolem3  27116  minvecolem4c  27119  minvecolem4  27120  minvecolem5  27121  minvecolem7  27123  htthlem  27158  hiidge0  27339  normlem6  27356  normgt0  27368  norm-i  27370  normpyc  27387  bcsiALT  27420  pjhthlem1  27634  pjneli  27966  nmlnop0iALT  28238  unopbd  28258  nmbdoplbi  28267  nmcoplbi  28271  nmbdfnlbi  28292  nmbdfnlb  28293  nmcfnlbi  28295  cnlnadjlem7  28316  nmopcoi  28338  branmfn  28348  leopmul  28377  nmopleid  28382  pjbdlni  28392  pjnormssi  28411  stge0  28467  stle1  28468  stle0i  28482  strlem3a  28495  cdj3lem1  28677  xaddeq0  28907  xdiv0  28968  xrge0slmod  29175  elunitrn  29271  elunitge0  29273  unitdivcld  29275  sqsscirc1  29282  xrge0iifcnv  29307  xrge0iifiso  29309  xrge0iifhom  29311  rezh  29343  indf  29405  indfval  29406  pr01ssre  29407  esumcvgsum  29477  voliune  29619  volfiniune  29620  sibfinima  29728  sitmcl  29740  0rrv  29840  coinfliprv  29871  ballotlem2  29877  ballotlem4  29887  ballotlemi1  29891  ballotlemic  29895  sgnclre  29928  sgnnbi  29934  sgnpbi  29935  plymulx0  29950  signsply0  29954  signswch  29964  signstf  29969  signstf0  29971  signstfveq0  29980  signlem0  29990  rescon  30482  iiscon  30488  iillyscon  30489  cvmliftlem10  30530  snmlff  30565  fz0n  30869  logi  30873  bcneg1  30875  nn0prpwlem  31487  dnizeq0  31635  dnizphlfeqhlf  31636  knoppndvlem13  31685  cnndvlem1  31698  bj-pinftyccb  32285  bj-minftyccb  32289  bj-pinftynminfty  32291  taupilemrplb  32343  sin2h  32569  tan2h  32571  ptrecube  32579  poimirlem16  32595  poimirlem17  32596  poimirlem20  32599  poimirlem22  32601  poimirlem23  32602  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  poimir  32612  heicant  32614  mblfinlem2  32617  ismblfin  32620  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  mbfposadd  32627  itg2addnclem  32631  itg2addnclem2  32632  ibladdnclem  32636  itgaddnclem2  32639  iblabsnclem  32643  iblmulc2nc  32645  itgmulc2nclem2  32647  itgabsnc  32649  ftc1cnnclem  32653  ftc1anclem5  32659  ftc1anclem8  32662  asindmre  32665  dvasin  32666  areacirclem4  32673  areacirc  32675  isbnd3  32753  ssbnd  32757  prdsbnd  32762  bfplem2  32792  bfp  32793  renegclALT  33267  pellexlem6  36416  elpell14qr2  36444  oddcomabszz  36527  zindbi  36529  jm2.24  36548  acongeq  36568  arearect  36820  areaquad  36821  relexp01min  37024  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  dvconstbi  37555  binomcxplemnn0  37570  binomcxplemdvbinom  37574  binomcxplemcvg  37575  binomcxplemnotnn0  37577  sineq0ALT  38195  halffl  38451  sqrlearg  38627  dvnmptdivc  38828  dvnmul  38833  itgsin0pilem1  38841  itgsinexplem1  38845  itgsinexp  38846  iblempty  38857  stoweidlem17  38910  stoweidlem36  38929  stoweidlem55  38948  wallispilem1  38958  wallispilem2  38959  wallispilem4  38961  stirlinglem4  38970  stirlinglem13  38979  stirlinglem14  38980  stirlinglem15  38981  stirlingr  38983  dirker2re  38985  dirkerdenne0  38986  dirkerre  38988  dirkertrigeqlem1  38991  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem11  39011  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem41  39041  fourierdlem42  39042  fourierdlem48  39047  fourierdlem62  39061  fourierdlem66  39065  fourierdlem79  39078  fourierdlem83  39082  fourierdlem94  39093  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  fourierdlem114  39113  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  etransclem23  39150  etransclem44  39171  etransclem46  39173  salexct3  39236  salgensscntex  39238  sge0rnn0  39261  sge00  39269  0ome  39419  ovn0lem  39455  ovnhoilem1  39491  smfmullem1  39676  smfmullem2  39677  smfmullem3  39678  smfmullem4  39679  m1mod0mod1  39949  fmtnoprmfac2lem1  40016  31prm  40050  mod42tp1mod8  40057  tgblthelfgott  40229  tgblthelfgottOLD  40236  zm1nn  40348  lfuhgr1v0e  40480  pthdlem2  40974  crctcsh1wlkn0lem7  41019  rusgrnumwwlks  41177  konigsberg-av  41427  altgsumbcALT  41924  expnegico01  42102  dignnld  42195  ex-gt  42268
  Copyright terms: Public domain W3C validator