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

Theorem 0re 10078
Description: 0 is a real number. See also 0reALT 10416. (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 10077 . 2 1 ∈ ℝ
2 ax-rnegex 10045 . 2 (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3 readdcl 10057 . . . . 5 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
41, 3mpan 706 . . . 4 (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5 eleq1 2718 . . . 4 ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 235 . . 3 (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
76rexlimiv 3056 . 2 (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
81, 2, 7mp2b 10 1 0 ∈ ℝ
Colors of variables: wff setvar class
Syntax hints:   = wceq 1523  wcel 2030  wrex 2942  (class class class)co 6690  cr 9973  0cc0 9974  1c1 9975   + caddc 9977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693
This theorem is referenced by:  0red  10079  0xr  10124  axmulgt0  10150  ne0gt0  10180  00id  10249  mul02lem1  10250  mul02lem2  10251  mul02  10252  addid1  10254  ltaddneg  10289  addgt0  10552  addgegt0  10553  addgtge0  10554  addge0  10555  ltaddpos  10556  ltneg  10566  leneg  10569  lt0neg1  10572  lt0neg2  10573  le0neg1  10574  le0neg2  10575  addge01  10576  suble0  10580  mulge0  10584  msqge0  10587  0le1  10589  relin01  10590  gt0ne0i  10601  gt0ne0d  10630  lt0ne0d  10631  elimge0  10898  ltm1  10901  recgt0  10905  prodgt0  10906  lemul1a  10915  ltmul12a  10917  lemul12a  10919  mulgt1  10920  gt0div  10927  ge0div  10928  mulge0b  10931  lediv12a  10954  recgt1i  10958  recreclt  10960  ledivp1  10963  squeeze0  10964  recgt0ii  10967  ledivp1i  10987  ltdivp1i  10988  fimaxre2  11007  inelr  11048  crne0  11051  nnge1  11084  nngt0  11087  nnnle0  11089  nnrecgt0  11096  0le0  11148  neg1lt0  11165  halfge0  11287  nn0ssre  11334  nn0ge0  11356  nn0nlt0  11357  nn0le0eq0  11359  0mnnnnn0  11363  elnnnn0b  11375  elnnnn0c  11376  nn0sub  11381  elnnz  11425  0z  11426  elnn0z  11428  elnnz1  11441  recnz  11490  gtndiv  11492  fnn0ind  11514  rpge0  11883  rpneg  11901  0nrp  11903  zgt1rpn0n1  11909  0ltpnf  11994  mnflt0  11997  qsqueeze  12070  xneg0  12081  xaddid1  12110  xnn0xadd0  12115  xmulpnf1  12142  xlemul1a  12156  xadddi  12163  xrsupsslem  12175  xrinfmsslem  12176  elrege0  12316  0e0icopnf  12320  0elunit  12328  1elunit  12329  divelunit  12352  lincmb01cmp  12353  iccf1o  12354  unitssre  12357  0nelfz1  12398  fzpreddisj  12428  fz0to4untppr  12481  nn0p1elfzo  12550  ico01fl0  12660  rpsup  12705  modelico  12720  0mod  12741  1mod  12742  expubnd  12961  le2sq2  12979  sqlecan  13011  bernneq2  13031  expnbnd  13033  expnlbnd  13034  expmulnbnd  13036  discr1  13040  discr  13041  facdiv  13114  faclbnd  13117  faclbnd3  13119  faclbnd6  13126  bcval4  13134  bcval5  13145  bcpasc  13148  hasheq0  13192  hashneq0  13193  hashnn0n0nn  13218  hashgt12el  13248  hashgt12el2  13249  hashge2el2dif  13300  lsw0  13385  reim0  13902  re0  13936  im0  13937  rei  13940  imi  13941  cj0  13942  sqeqd  13950  rennim  14023  cnpart  14024  sqr0lem  14025  sqrlem4  14030  resqrex  14035  sqrtgt0  14043  sqrt00  14048  sqrtneglem  14051  sqrt9  14058  sqrt2gt1lt2  14059  leabs  14083  absor  14084  max0add  14094  eqsqrt2d  14152  sqrtpclii  14166  rlimconst  14319  rlimrege0  14354  lo1mul  14402  iserge0  14435  fsum00  14574  isumless  14621  arisum2  14637  georeclim  14647  geo2sum  14648  geo2lim  14650  geoisumr  14653  0.999...  14656  0.999...OLD  14657  cvgrat  14659  bpoly4  14834  cos0  14924  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  cos2bnd  14962  sin01gt0  14964  cos01gt0  14965  sincos2sgn  14968  sin4lt0  14969  absef  14971  absefib  14972  efieq1re  14973  epos  14979  znnenlem  14984  rpnnen2lem2  14988  rpnnen2lem3  14989  rpnnen2lem4  14990  rpnnen2lem9  14995  rpnnen2lem12  14998  ruclem6  15008  dvdslelem  15078  divalglem1  15164  divalglem5  15167  divalglem6  15168  flodddiv4  15184  bitsp1o  15202  sadcadd  15227  gcdn0gt0  15286  nn0seqcvgd  15330  algcvgblem  15337  algcvga  15339  pythagtriplem12  15578  pythagtriplem13  15579  pythagtriplem14  15580  pythagtriplem16  15582  prmreclem4  15670  prmreclem5  15671  prmreclem6  15672  1arith  15678  vdwap0  15727  ramz  15776  mulgnegnn  17598  subgmulg  17655  srgbinomlem4  18589  isabvd  18868  abvtrivd  18888  psrbaglesupp  19416  xrs1mnd  19832  xrs10  19833  rge0srg  19865  psgnodpmr  19984  re0g  20006  mnfnei  21073  imasdsf1olem  22225  ssblps  22274  ssbl  22275  xmeter  22285  dscmet  22424  dscopn  22425  nmoi  22579  nmoeq0  22587  0nghm  22592  idnghm  22594  cnbl0  22624  blcvx  22648  xrsxmet  22659  metdseq0  22704  iicmp  22736  iiconn  22737  iirev  22775  iihalf1  22777  iihalf1cn  22778  iihalf2  22779  elii1  22781  elii2  22782  iimulcl  22783  icopnfcnv  22788  icopnfhmeo  22789  iccpnfcnv  22790  iccpnfhmeo  22791  xrhmeo  22792  xrhmph  22793  lebnumii  22812  htpycc  22826  reparphti  22843  pcoval1  22859  pco0  22860  pcoval2  22862  pcocn  22863  pcohtpylem  22865  pcopt  22868  pcopt2  22869  pcoass  22870  pcorevlem  22872  reust  23215  recusp  23216  minveclem4c  23242  minveclem2  23243  minveclem3b  23245  minveclem4  23249  minveclem7  23252  pjthlem1  23254  cniccbdd  23276  ovolunnul  23314  ovoliunnul  23321  ovolicc1  23330  ovolre  23339  iccvolcl  23381  ovolioo  23382  ioovolcl  23384  ioorcl  23391  vitalilem2  23423  vitalilem4  23425  vitalilem5  23426  vitali  23427  ismbf  23442  mbfmulc2lem  23459  mbfpos  23463  mbfposr  23464  i1f0  23499  i1f1  23502  itg1addlem2  23509  itg1addlem4  23511  itg1addlem5  23512  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1fseqlem6  23532  mbfi1flimlem  23534  xrge0f  23543  itg2ge0  23547  itg2const  23552  itg2mulc  23559  itg2splitlem  23560  itg2gt0  23572  itg2cnlem1  23573  ibl0  23598  iblrelem  23602  iblposlem  23603  iblpos  23604  iblre  23605  itgreval  23608  itgneg  23615  iblss  23616  i1fibl  23619  itgitg1  23620  itgle  23621  itgeqa  23625  itgless  23628  iblconst  23629  itgconst  23630  ibladdlem  23631  itgaddlem2  23635  iblabslem  23639  iblabsr  23641  iblmulc2  23642  itgmulc2lem2  23644  itgabs  23646  itgsplit  23647  bddmulibl  23650  dvferm1  23793  dvferm2  23795  dvferm  23796  dvlip  23801  c1lip1  23805  dveq0  23808  dv11cn  23809  dvne0  23819  ftc1lem4  23847  ply1divex  23941  dgrco  24076  plyrecj  24080  vieta1lem2  24111  aalioulem2  24133  aalioulem3  24134  pserulm  24221  psercnlem2  24223  psercnlem1  24224  psercn  24225  abelthlem6  24235  abelth  24240  abelth2  24241  reeff1olem  24245  reeff1o  24246  pilem2  24251  pilem3  24252  pipos  24257  sinhalfpilem  24260  sincosq1sgn  24295  sincosq2sgn  24296  coseq00topi  24299  coseq0negpitopi  24300  tangtx  24302  tanabsge  24303  sinq12ge0  24305  sinq34lt0t  24306  cosq14ge0  24308  sincos4thpi  24310  sincos6thpi  24312  pige3  24314  sineq0  24318  cosordlem  24322  cosord  24323  cos11  24324  sinord  24325  recosf1o  24326  resinf1o  24327  tanord1  24328  tanord  24329  tanregt0  24330  efif1olem4  24336  efifo  24338  relogrn  24353  log1  24377  logneg  24379  argregt0  24401  argrege0  24402  argimgt0  24403  logneg2  24406  logdivlti  24411  logdivlt  24412  ellogdm  24430  logdmn0  24431  logdmnrp  24432  logcnlem3  24435  dvloglem  24439  logdmopn  24440  logf1o2  24441  dvlog2lem  24443  efopnlem1  24447  logtayl  24451  recxpcl  24466  cxpge0  24474  cxple2  24488  cxple2a  24490  cxpsqrtlem  24493  cxpcn3  24534  cxpaddlelem  24537  cxpaddle  24538  loglesqrt  24544  logbrec  24565  ang180lem3  24586  ang180lem4  24587  chordthmlem4  24607  heron  24610  asinneg  24658  asin1  24666  reasinsin  24668  acosbnd  24672  atan0  24680  atanrecl  24683  atanlogaddlem  24685  atanlogsublem  24687  atanlogsub  24688  atantan  24695  atanbnd  24698  atan1  24700  atans2  24703  ressatans  24706  leibpi  24714  log2cnv  24716  log2tlbnd  24717  log2ub  24721  log2le1  24722  rlimcnp  24737  rlimcnp2  24738  o1cxp  24746  jensenlem2  24759  jensen  24760  amgm  24762  emgt0  24778  harmonicbnd3  24779  harmoniclbnd  24780  harmonicbnd4  24782  zetacvg  24786  eldmgm  24793  lgamgulmlem2  24801  basellem3  24854  basellem8  24859  efnnfsumcl  24874  ppisval  24875  vmage0  24892  chpge0  24897  efchtdvds  24930  ppiltx  24948  ppiub  24974  chpeq0  24978  chteq0  24979  chtleppi  24980  chpchtsum  24989  chpub  24990  dchr1re  25033  bcmono  25047  efexple  25051  bposlem1  25054  bposlem4  25057  bposlem5  25058  bposlem7  25060  bposlem8  25061  bposlem9  25062  lgsval2lem  25077  lgsval4a  25089  lgsneg  25091  lgsdilem  25094  lgsdir2lem1  25095  2lgsoddprmlem3a  25180  2lgsoddprmlem3b  25181  2lgsoddprmlem3c  25182  2lgsoddprmlem3d  25183  rplogsumlem2  25219  rpvmasumlem  25221  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0fno1  25245  rplogsum  25261  logdivsum  25267  mulog2sumlem2  25269  selberg2lem  25284  logdivbnd  25290  pntrsumo1  25299  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntpbnd1  25320  pntpbnd2  25321  pntlem3  25343  pntleml  25345  ostth2  25371  trgcgrg  25455  ttgcontlem1  25810  brbtwn2  25830  ax5seglem1  25853  ax5seglem2  25854  ax5seglem3  25856  ax5seglem5  25858  ax5seglem6  25859  ax5seglem9  25862  ax5seg  25863  axbtwnid  25864  axpaschlem  25865  axpasch  25866  axlowdimlem1  25867  axlowdimlem6  25872  axlowdimlem7  25873  axlowdimlem10  25876  axlowdim1  25884  axlowdim2  25885  axlowdim  25886  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  umgrislfupgrlem  26062  lfgrnloop  26065  lfuhgr1v0e  26191  usgrexmplef  26196  pthdlem2  26720  crctcshwlkn0lem7  26764  rusgrnumwwlks  26941  clwwlkn0  26989  konigsberg  27235  ex-po  27422  ex-sqrt  27441  ex-gcd  27444  nvz0  27651  0blo  27775  nmlno0lem  27776  nmblolbii  27782  siilem2  27835  minvecolem2  27859  minvecolem3  27860  minvecolem4c  27863  minvecolem4  27864  minvecolem5  27865  minvecolem7  27867  htthlem  27902  hiidge0  28083  normlem6  28100  normgt0  28112  norm-i  28114  normpyc  28131  bcsiALT  28164  pjhthlem1  28378  pjneli  28710  nmlnop0iALT  28982  unopbd  29002  nmbdoplbi  29011  nmcoplbi  29015  nmbdfnlbi  29036  nmbdfnlb  29037  nmcfnlbi  29039  cnlnadjlem7  29060  nmopcoi  29082  branmfn  29092  leopmul  29121  nmopleid  29126  pjbdlni  29136  pjnormssi  29155  stge0  29211  stle1  29212  stle0i  29226  strlem3a  29239  cdj3lem1  29421  xaddeq0  29646  pr01ssre  29698  dp20u  29713  dp20h  29714  dp2clq  29716  dp2lt10  29719  dp2lt  29720  dp0u  29737  dplti  29741  dpexpp1  29744  xdiv0  29765  xrge0slmod  29972  elunitrn  30071  elunitge0  30073  unitdivcld  30075  sqsscirc1  30082  xrge0iifcnv  30107  xrge0iifiso  30109  xrge0iifhom  30111  rezh  30143  indf  30205  indfval  30206  esumcvgsum  30278  voliune  30420  volfiniune  30421  sibfinima  30529  sitmcl  30541  0rrv  30641  coinfliprv  30672  ballotlem2  30678  ballotlem4  30688  ballotlemi1  30692  ballotlemic  30696  sgnclre  30729  sgnnbi  30735  sgnpbi  30736  plymulx0  30752  signsply0  30756  signswch  30766  signstf  30771  signstf0  30773  signstfveq0  30782  signlem0  30792  itgexpif  30812  hgt750lemd  30854  hgt750lem  30857  hgt750lem2  30858  hgt750leme  30864  resconn  31354  iisconn  31360  iillysconn  31361  cvmliftlem10  31402  snmlff  31437  fz0n  31742  logi  31746  bcneg1  31748  nn0prpwlem  32442  dnizeq0  32590  dnizphlfeqhlf  32591  knoppndvlem13  32640  cnndvlem1  32653  bj-pinftyccb  33238  bj-minftyccb  33242  bj-pinftynminfty  33244  taupilemrplb  33296  sin2h  33529  tan2h  33531  ptrecube  33539  poimirlem16  33555  poimirlem17  33556  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  poimir  33572  heicant  33574  mblfinlem2  33577  ismblfin  33580  ovoliunnfl  33581  voliunnfl  33583  volsupnfl  33584  mbfposadd  33587  itg2addnclem  33591  itg2addnclem2  33592  ibladdnclem  33596  itgaddnclem2  33599  iblabsnclem  33603  iblmulc2nc  33605  itgmulc2nclem2  33607  itgabsnc  33609  ftc1cnnclem  33613  ftc1anclem5  33619  ftc1anclem8  33622  asindmre  33625  dvasin  33626  areacirclem4  33633  areacirc  33635  isbnd3  33713  ssbnd  33717  prdsbnd  33722  bfplem2  33752  bfp  33753  renegclALT  34567  pellexlem6  37715  elpell14qr2  37743  oddcomabszz  37826  zindbi  37828  jm2.24  37847  acongeq  37867  arearect  38118  areaquad  38119  relexp01min  38322  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  dvconstbi  38850  binomcxplemnn0  38865  binomcxplemdvbinom  38869  binomcxplemcvg  38870  binomcxplemnotnn0  38872  sineq0ALT  39487  halffl  39824  ren0  39939  sqrlearg  40098  limsup10ex  40323  liminf10ex  40324  dvnmptdivc  40471  dvnmul  40476  itgsin0pilem1  40483  itgsinexplem1  40487  itgsinexp  40488  iblempty  40499  stoweidlem17  40552  stoweidlem36  40571  stoweidlem55  40590  wallispilem1  40600  wallispilem2  40601  wallispilem4  40603  stirlinglem4  40612  stirlinglem13  40621  stirlinglem14  40622  stirlinglem15  40623  stirlingr  40625  dirker2re  40627  dirkerdenne0  40628  dirkerre  40630  dirkertrigeqlem1  40633  dirkercncflem2  40639  dirkercncflem4  40641  fourierdlem11  40653  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem41  40683  fourierdlem42  40684  fourierdlem48  40689  fourierdlem62  40703  fourierdlem66  40707  fourierdlem79  40720  fourierdlem83  40724  fourierdlem94  40735  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  fourierdlem114  40755  sqwvfoura  40763  sqwvfourb  40764  fourierswlem  40765  fouriersw  40766  etransclem23  40792  etransclem44  40813  etransclem46  40815  salexct3  40878  salgensscntex  40880  sge0rnn0  40903  sge00  40911  0ome  41064  ovn0lem  41100  ovnhoilem1  41136  smfmullem1  41319  smfmullem2  41320  smfmullem3  41321  smfmullem4  41322  zm1nn  41641  m1mod0mod1  41664  fmtnoprmfac2lem1  41803  31prm  41837  mod42tp1mod8  41844  tgblthelfgott  42028  tgblthelfgottOLD  42034  altgsumbcALT  42456  expnegico01  42633  dignnld  42722  ex-gt  42797
  Copyright terms: Public domain W3C validator