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

Theorem 0re 7233
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 7232 . 2 1 ∈ ℝ
2 ax-rnegex 7199 . 2 (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3 readdcl 7213 . . . . 5 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
41, 3mpan 415 . . . 4 (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5 eleq1 2145 . . . 4 ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 153 . . 3 (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
76rexlimiv 2476 . 2 (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
81, 2, 7mp2b 8 1 0 ∈ ℝ
Colors of variables: wff set class
Syntax hints:   = wceq 1285  wcel 1434  wrex 2354  (class class class)co 5563  cr 7094  0cc0 7095  1c1 7096   + caddc 7098
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-1re 7184  ax-addrcl 7187  ax-rnegex 7199
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-cleq 2076  df-clel 2079  df-ral 2358  df-rex 2359
This theorem is referenced by:  0red  7234  0xr  7279  axmulgt0  7303  gtso  7309  0lt1  7355  ine0  7617  ltaddneg  7647  addgt0  7671  addgegt0  7672  addgtge0  7673  addge0  7674  ltaddpos  7675  ltneg  7685  leneg  7688  lt0neg1  7691  lt0neg2  7692  le0neg1  7693  le0neg2  7694  addge01  7695  suble0  7699  0le1  7704  gt0ne0i  7706  gt0ne0d  7732  lt0ne0d  7733  recexre  7797  recexgt0  7799  inelr  7803  rimul  7804  1ap0  7809  reapmul1  7814  apsqgt0  7820  msqge0  7835  mulge0  7838  recexaplem2  7861  recexap  7862  rerecclap  7937  ltm1  8043  recgt0  8047  ltmul12a  8057  lemul12a  8059  mulgt1  8060  gt0div  8067  ge0div  8068  recgt1i  8095  recreclt  8097  crap0  8154  nnge1  8181  nngt0  8183  nnrecgt0  8195  0ne1  8225  0le0  8247  neg1lt0  8266  halfge0  8366  iap0  8373  nn0ssre  8411  nn0ge0  8432  nn0nlt0  8433  nn0le0eq0  8435  0mnnnnn0  8439  elnnnn0b  8451  elnnnn0c  8452  elnnz  8494  0z  8495  elnnz1  8507  nn0lt10b  8561  recnz  8573  gtndiv  8575  fnn0ind  8596  rpge0  8879  rpnegap  8899  0nrp  8900  0ltpnf  8985  mnflt0  8987  xneg0  9026  elrege0  9127  0e0icopnf  9130  0elunit  9136  1elunit  9137  divelunit  9152  lincmb01cmp  9153  iccf1o  9154  unitssre  9155  modqelico  9468  modqmuladdim  9501  addmodid  9506  expubnd  9682  le2sq2  9700  bernneq2  9743  expnbnd  9745  expnlbnd  9746  faclbnd  9817  faclbnd3  9819  faclbnd6  9820  bcval4  9828  bcpasc  9842  reim0  9949  re0  9983  im0  9984  rei  9987  imi  9988  cj0  9989  caucvgre  10068  rennim  10089  sqrt0rlem  10090  sqrt0  10091  resqrexlemdecn  10099  resqrexlemnm  10105  resqrexlemgt0  10107  sqrt00  10127  sqrt9  10135  sqrt2gt1lt2  10136  leabs  10161  ltabs  10174  sqrtpclii  10217  max0addsup  10306  fimaxre2  10310  climge0  10364  iserige0  10382  flodddiv4  10541  gcdn0gt0  10576  nn0seqcvgd  10630  algcvgblem  10638  ialgcvga  10640  ex-gcd  10828
  Copyright terms: Public domain W3C validator