ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0re GIF version

Theorem 0re 7789
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 ∈ ℝ

Proof of Theorem 0re
StepHypRef Expression
1 1re 7788 . 2 1 ∈ ℝ
2 ax-rnegex 7752 . 2 (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3 readdcl 7769 . . . . 5 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
41, 3mpan 421 . . . 4 (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5 eleq1 2203 . . . 4 ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 154 . . 3 (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
76rexlimiv 2546 . 2 (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
81, 2, 7mp2b 8 1 0 ∈ ℝ
Colors of variables: wff set class
Syntax hints:   = wceq 1332  wcel 1481  wrex 2418  (class class class)co 5781  cr 7642  0cc0 7643  1c1 7644   + caddc 7646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-1re 7737  ax-addrcl 7740  ax-rnegex 7752
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-cleq 2133  df-clel 2136  df-ral 2422  df-rex 2423
This theorem is referenced by:  0red  7790  0xr  7835  axmulgt0  7859  gtso  7866  0lt1  7912  ine0  8179  ltaddneg  8209  addgt0  8233  addgegt0  8234  addgtge0  8235  addge0  8236  ltaddpos  8237  ltneg  8247  leneg  8250  lt0neg1  8253  lt0neg2  8254  le0neg1  8255  le0neg2  8256  addge01  8257  suble0  8261  0le1  8266  gt0ne0i  8271  gt0ne0d  8297  lt0ne0d  8298  recexre  8363  recexgt0  8365  inelr  8369  rimul  8370  1ap0  8375  reapmul1  8380  apsqgt0  8386  msqge0  8401  mulge0  8404  recexaplem2  8436  recexap  8437  rerecclap  8513  ltm1  8627  recgt0  8631  ltmul12a  8641  lemul12a  8643  mulgt1  8644  gt0div  8651  ge0div  8652  recgt1i  8679  recreclt  8681  sup3exmid  8738  crap0  8739  nnge1  8766  nngt0  8768  nnrecgt0  8781  0ne1  8810  0le0  8832  neg1lt0  8851  halfge0  8959  iap0  8966  nn0ssre  9004  nn0ge0  9025  nn0nlt0  9026  nn0le0eq0  9028  0mnnnnn0  9032  elnnnn0b  9044  elnnnn0c  9045  elnnz  9087  0z  9088  elnnz1  9100  nn0lt10b  9154  recnz  9167  gtndiv  9169  fnn0ind  9190  rpge0  9482  rpnegap  9502  0nrp  9505  0ltpnf  9597  mnflt0  9599  xneg0  9643  xaddid1  9674  xnn0xadd0  9679  xposdif  9694  elrege0  9788  0e0icopnf  9791  0elunit  9798  1elunit  9799  divelunit  9814  lincmb01cmp  9815  iccf1o  9816  unitssre  9817  modqelico  10137  modqmuladdim  10170  addmodid  10175  expubnd  10380  le2sq2  10398  bernneq2  10443  expnbnd  10445  expnlbnd  10446  faclbnd  10518  faclbnd3  10520  faclbnd6  10521  bcval4  10529  bcpasc  10543  reim0  10664  re0  10698  im0  10699  rei  10702  imi  10703  cj0  10704  caucvgre  10784  rennim  10805  sqrt0rlem  10806  sqrt0  10807  resqrexlemdecn  10815  resqrexlemnm  10821  resqrexlemgt0  10823  sqrt00  10843  sqrt9  10851  sqrt2gt1lt2  10852  leabs  10877  ltabs  10890  sqrtpclii  10933  max0addsup  11022  fimaxre2  11029  climge0  11125  iserge0  11143  fsum00  11262  arisum2  11299  0.999...  11321  cos0  11471  ef01bndlem  11497  sin01bnd  11498  cos01bnd  11499  cos2bnd  11501  sin01gt0  11502  cos01gt0  11503  sincos2sgn  11506  sin4lt0  11507  absef  11510  absefib  11511  efieq1re  11512  epos  11521  flodddiv4  11665  gcdn0gt0  11700  nn0seqcvgd  11756  algcvgblem  11764  algcvga  11766  ssblps  12631  ssbl  12632  xmeter  12642  cnbl0  12740  reeff1olem  12898  pilem3  12910  pipos  12915  sinhalfpilem  12918  sincosq1sgn  12953  sincosq2sgn  12954  sinq34lt0t  12958  coseq0q4123  12961  coseq00topi  12962  coseq0negpitopi  12963  tangtx  12965  sincos4thpi  12967  sincos6thpi  12969  cosordlem  12976  cosq34lt1  12977  cos02pilt1  12978  cos0pilt1  12979  cos11  12980  ioocosf1o  12981  log1  12993  logrpap0b  13003  logdivlti  13008  rpabscxpbnd  13065  ex-gcd  13112  trilpolemclim  13402  trilpolemcl  13403  trilpolemisumle  13404  trilpolemeq1  13406  trilpolemlt1  13407  trirec0  13410  apdiff  13414  dcapncf  13421
  Copyright terms: Public domain W3C validator