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

Theorem 0re 7432
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 7431 . 2 1 ∈ ℝ
2 ax-rnegex 7398 . 2 (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3 readdcl 7412 . . . . 5 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
41, 3mpan 415 . . . 4 (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5 eleq1 2147 . . . 4 ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 153 . . 3 (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
76rexlimiv 2479 . 2 (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
81, 2, 7mp2b 8 1 0 ∈ ℝ
Colors of variables: wff set class
Syntax hints:   = wceq 1287  wcel 1436  wrex 2356  (class class class)co 5613  cr 7293  0cc0 7294  1c1 7295   + caddc 7297
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-1re 7383  ax-addrcl 7386  ax-rnegex 7398
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-cleq 2078  df-clel 2081  df-ral 2360  df-rex 2361
This theorem is referenced by:  0red  7433  0xr  7478  axmulgt0  7502  gtso  7508  0lt1  7554  ine0  7816  ltaddneg  7846  addgt0  7870  addgegt0  7871  addgtge0  7872  addge0  7873  ltaddpos  7874  ltneg  7884  leneg  7887  lt0neg1  7890  lt0neg2  7891  le0neg1  7892  le0neg2  7893  addge01  7894  suble0  7898  0le1  7903  gt0ne0i  7905  gt0ne0d  7931  lt0ne0d  7932  recexre  7996  recexgt0  7998  inelr  8002  rimul  8003  1ap0  8008  reapmul1  8013  apsqgt0  8019  msqge0  8034  mulge0  8037  recexaplem2  8060  recexap  8061  rerecclap  8136  ltm1  8242  recgt0  8246  ltmul12a  8256  lemul12a  8258  mulgt1  8259  gt0div  8266  ge0div  8267  recgt1i  8294  recreclt  8296  crap0  8353  nnge1  8380  nngt0  8382  nnrecgt0  8394  0ne1  8424  0le0  8446  neg1lt0  8465  halfge0  8565  iap0  8572  nn0ssre  8610  nn0ge0  8631  nn0nlt0  8632  nn0le0eq0  8634  0mnnnnn0  8638  elnnnn0b  8650  elnnnn0c  8651  elnnz  8693  0z  8694  elnnz1  8706  nn0lt10b  8760  recnz  8772  gtndiv  8774  fnn0ind  8795  rpge0  9078  rpnegap  9098  0nrp  9099  0ltpnf  9184  mnflt0  9186  xneg0  9225  elrege0  9326  0e0icopnf  9329  0elunit  9335  1elunit  9336  divelunit  9351  lincmb01cmp  9352  iccf1o  9353  unitssre  9354  modqelico  9669  modqmuladdim  9702  addmodid  9707  expubnd  9911  le2sq2  9929  bernneq2  9972  expnbnd  9974  expnlbnd  9975  faclbnd  10046  faclbnd3  10048  faclbnd6  10049  bcval4  10057  bcpasc  10071  reim0  10191  re0  10225  im0  10226  rei  10229  imi  10230  cj0  10231  caucvgre  10310  rennim  10331  sqrt0rlem  10332  sqrt0  10333  resqrexlemdecn  10341  resqrexlemnm  10347  resqrexlemgt0  10349  sqrt00  10369  sqrt9  10377  sqrt2gt1lt2  10378  leabs  10403  ltabs  10416  sqrtpclii  10459  max0addsup  10548  fimaxre2  10553  climge0  10607  iserige0  10625  flodddiv4  10816  gcdn0gt0  10851  nn0seqcvgd  10905  algcvgblem  10913  ialgcvga  10915  ex-gcd  11103
  Copyright terms: Public domain W3C validator