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

Theorem 0re 6805
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 6804 . 2 1
2 ax-rnegex 6772 . 2 (1 ℝ → x ℝ (1 + x) = 0)
3 readdcl 6785 . . . . 5 ((1 x ℝ) → (1 + x) ℝ)
41, 3mpan 400 . . . 4 (x ℝ → (1 + x) ℝ)
5 eleq1 2097 . . . 4 ((1 + x) = 0 → ((1 + x) ℝ ↔ 0 ℝ))
64, 5syl5ibcom 144 . . 3 (x ℝ → ((1 + x) = 0 → 0 ℝ))
76rexlimiv 2421 . 2 (x ℝ (1 + x) = 0 → 0 ℝ)
81, 2, 7mp2b 8 1 0
Colors of variables: wff set class
Syntax hints:   = wceq 1242   wcel 1390  wrex 2301  (class class class)co 5455  cr 6690  0cc0 6691  1c1 6692   + caddc 6694
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-1re 6757  ax-addrcl 6760  ax-rnegex 6772
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-cleq 2030  df-clel 2033  df-ral 2305  df-rex 2306
This theorem is referenced by:  0red  6806  0xr  6849  axmulgt0  6868  gtso  6874  0lt1  6918  ine0  7167  addgt0  7218  addgegt0  7219  addgtge0  7220  addge0  7221  ltaddpos  7222  ltneg  7232  leneg  7235  lt0neg1  7238  lt0neg2  7239  le0neg1  7240  le0neg2  7241  addge01  7242  suble0  7246  0le1  7251  gt0ne0i  7253  gt0ne0d  7279  lt0ne0d  7280  recexre  7342  recexgt0  7344  inelr  7348  rimul  7349  1ap0  7354  reapmul1  7359  apsqgt0  7365  msqge0  7380  mulge0  7383  recexaplem2  7395  recexap  7396  rerecclap  7468  ltm1  7573  recgt0  7577  ltmul12a  7587  lemul12a  7589  mulgt1  7590  gt0div  7597  ge0div  7598  recgt1i  7625  recreclt  7627  crap0  7671  nnge1  7698  nngt0  7700  nnrecgt0  7712  0ne1  7742  0le0  7765  neg1lt0  7783  iap0  7905  nn0ssre  7941  nn0ge0  7963  nn0nlt0  7964  nn0le0eq0  7966  0mnnnnn0  7970  elnnnn0b  7982  elnnnn0c  7983  elnnz  8011  0z  8012  elnnz1  8024  nn0lt10b  8077  recnz  8089  gtndiv  8091  fnn0ind  8110  rpge0  8350  rpnegap  8370  0nrp  8371  0ltpnf  8453  mnflt0  8455  xneg0  8494  elrege0  8595  0e0icopnf  8598  0elunit  8604  1elunit  8605  divelunit  8620  lincmb01cmp  8621  iccf1o  8622  unitssre  8623  expubnd  8945  le2sq2  8962  bernneq2  9003  expnbnd  9005  expnlbnd  9006  reim0  9069  re0  9103  im0  9104  rei  9107  imi  9108  cj0  9109  rennim  9191  sqrt0rlem  9192  sqrt0  9193  sqrt9  9198
  Copyright terms: Public domain W3C validator