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

Theorem 0re 7008
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 7007 . 2 1 ∈ ℝ
2 ax-rnegex 6974 . 2 (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3 readdcl 6988 . . . . 5 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
41, 3mpan 400 . . . 4 (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5 eleq1 2100 . . . 4 ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 144 . . 3 (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
76rexlimiv 2424 . 2 (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
81, 2, 7mp2b 8 1 0 ∈ ℝ
Colors of variables: wff set class
Syntax hints:   = wceq 1243  wcel 1393  wrex 2304  (class class class)co 5499  cr 6869  0cc0 6870  1c1 6871   + caddc 6873
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-1re 6959  ax-addrcl 6962  ax-rnegex 6974
This theorem depends on definitions:  df-bi 110  df-nf 1350  df-cleq 2033  df-clel 2036  df-ral 2308  df-rex 2309
This theorem is referenced by:  0red  7009  0xr  7052  axmulgt0  7071  gtso  7077  0lt1  7121  ine0  7370  addgt0  7421  addgegt0  7422  addgtge0  7423  addge0  7424  ltaddpos  7425  ltneg  7435  leneg  7438  lt0neg1  7441  lt0neg2  7442  le0neg1  7443  le0neg2  7444  addge01  7445  suble0  7449  0le1  7454  gt0ne0i  7456  gt0ne0d  7482  lt0ne0d  7483  recexre  7545  recexgt0  7547  inelr  7551  rimul  7552  1ap0  7557  reapmul1  7562  apsqgt0  7568  msqge0  7583  mulge0  7586  recexaplem2  7609  recexap  7610  rerecclap  7682  ltm1  7788  recgt0  7792  ltmul12a  7802  lemul12a  7804  mulgt1  7805  gt0div  7812  ge0div  7813  recgt1i  7840  recreclt  7842  crap0  7886  nnge1  7913  nngt0  7915  nnrecgt0  7927  0ne1  7958  0le0  7981  neg1lt0  7999  iap0  8121  nn0ssre  8157  nn0ge0  8179  nn0nlt0  8180  nn0le0eq0  8182  0mnnnnn0  8186  elnnnn0b  8198  elnnnn0c  8199  elnnz  8227  0z  8228  elnnz1  8240  nn0lt10b  8293  recnz  8305  gtndiv  8307  fnn0ind  8326  rpge0  8566  rpnegap  8586  0nrp  8587  0ltpnf  8670  mnflt0  8672  xneg0  8711  elrege0  8812  0e0icopnf  8815  0elunit  8821  1elunit  8822  divelunit  8837  lincmb01cmp  8838  iccf1o  8839  unitssre  8840  expubnd  9189  le2sq2  9207  bernneq2  9248  expnbnd  9250  expnlbnd  9251  reim0  9339  re0  9373  im0  9374  rei  9377  imi  9378  cj0  9379  caucvgre  9458  rennim  9478  sqrt0rlem  9479  sqrt0  9480  resqrexlemdecn  9488  resqrexlemnm  9494  resqrexlemgt0  9496  sqrt00  9516  sqrt9  9524  sqrt2gt1lt2  9525  leabs  9550  ltabs  9561  sqrtpclii  9604  climge0  9722  iserige0  9740  nn0seqcvgd  9757  algcvgblem  9765  ialgcvga  9767
  Copyright terms: Public domain W3C validator