ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0re Unicode 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  e.  RR

Proof of Theorem 0re
StepHypRef Expression
1 1re 7431 . 2  |-  1  e.  RR
2 ax-rnegex 7398 . 2  |-  ( 1  e.  RR  ->  E. x  e.  RR  ( 1  +  x )  =  0 )
3 readdcl 7412 . . . . 5  |-  ( ( 1  e.  RR  /\  x  e.  RR )  ->  ( 1  +  x
)  e.  RR )
41, 3mpan 415 . . . 4  |-  ( x  e.  RR  ->  (
1  +  x )  e.  RR )
5 eleq1 2147 . . . 4  |-  ( ( 1  +  x )  =  0  ->  (
( 1  +  x
)  e.  RR  <->  0  e.  RR ) )
64, 5syl5ibcom 153 . . 3  |-  ( x  e.  RR  ->  (
( 1  +  x
)  =  0  -> 
0  e.  RR ) )
76rexlimiv 2479 . 2  |-  ( E. x  e.  RR  (
1  +  x )  =  0  ->  0  e.  RR )
81, 2, 7mp2b 8 1  |-  0  e.  RR
Colors of variables: wff set class
Syntax hints:    = wceq 1287    e. wcel 1436   E.wrex 2356  (class class class)co 5613   RRcr 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  9910  le2sq2  9928  bernneq2  9971  expnbnd  9973  expnlbnd  9974  faclbnd  10045  faclbnd3  10047  faclbnd6  10048  bcval4  10056  bcpasc  10070  reim0  10190  re0  10224  im0  10225  rei  10228  imi  10229  cj0  10230  caucvgre  10309  rennim  10330  sqrt0rlem  10331  sqrt0  10332  resqrexlemdecn  10340  resqrexlemnm  10346  resqrexlemgt0  10348  sqrt00  10368  sqrt9  10376  sqrt2gt1lt2  10377  leabs  10402  ltabs  10415  sqrtpclii  10458  max0addsup  10547  fimaxre2  10551  climge0  10605  iserige0  10623  flodddiv4  10809  gcdn0gt0  10844  nn0seqcvgd  10898  algcvgblem  10906  ialgcvga  10908  ex-gcd  11096
  Copyright terms: Public domain W3C validator