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

Theorem 0re 6825
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 6824 . 2 1
2 ax-rnegex 6792 . 2 (1 ℝ → x ℝ (1 + x) = 0)
3 readdcl 6805 . . . . 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 6710  0cc0 6711  1c1 6712   + caddc 6714
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 6777  ax-addrcl 6780  ax-rnegex 6792
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  6826  0xr  6869  axmulgt0  6888  gtso  6894  0lt1  6938  ine0  7187  addgt0  7238  addgegt0  7239  addgtge0  7240  addge0  7241  ltaddpos  7242  ltneg  7252  leneg  7255  lt0neg1  7258  lt0neg2  7259  le0neg1  7260  le0neg2  7261  addge01  7262  suble0  7266  0le1  7271  gt0ne0i  7273  gt0ne0d  7299  lt0ne0d  7300  recexre  7362  recexgt0  7364  inelr  7368  rimul  7369  1ap0  7374  reapmul1  7379  apsqgt0  7385  msqge0  7400  mulge0  7403  recexaplem2  7415  recexap  7416  rerecclap  7488  ltm1  7593  recgt0  7597  ltmul12a  7607  lemul12a  7609  mulgt1  7610  gt0div  7617  ge0div  7618  recgt1i  7645  recreclt  7647  crap0  7691  nnge1  7718  nngt0  7720  nnrecgt0  7732  0ne1  7762  0le0  7785  neg1lt0  7803  iap0  7925  nn0ssre  7961  nn0ge0  7983  nn0nlt0  7984  nn0le0eq0  7986  0mnnnnn0  7990  elnnnn0b  8002  elnnnn0c  8003  elnnz  8031  0z  8032  elnnz1  8044  nn0lt10b  8097  recnz  8109  gtndiv  8111  fnn0ind  8130  rpge0  8370  rpnegap  8390  0nrp  8391  0ltpnf  8473  mnflt0  8475  xneg0  8514  elrege0  8615  0e0icopnf  8618  0elunit  8624  1elunit  8625  divelunit  8640  lincmb01cmp  8641  iccf1o  8642  unitssre  8643  expubnd  8965  le2sq2  8982  bernneq2  9023  expnbnd  9025  expnlbnd  9026  reim0  9089  re0  9123  im0  9124  rei  9127  imi  9128  cj0  9129  rennim  9211  sqrt0rlem  9212  sqrt0  9213  sqrt9  9218
  Copyright terms: Public domain W3C validator