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

Theorem 0re 7734
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 7733 . 2  |-  1  e.  RR
2 ax-rnegex 7697 . 2  |-  ( 1  e.  RR  ->  E. x  e.  RR  ( 1  +  x )  =  0 )
3 readdcl 7714 . . . . 5  |-  ( ( 1  e.  RR  /\  x  e.  RR )  ->  ( 1  +  x
)  e.  RR )
41, 3mpan 420 . . . 4  |-  ( x  e.  RR  ->  (
1  +  x )  e.  RR )
5 eleq1 2180 . . . 4  |-  ( ( 1  +  x )  =  0  ->  (
( 1  +  x
)  e.  RR  <->  0  e.  RR ) )
64, 5syl5ibcom 154 . . 3  |-  ( x  e.  RR  ->  (
( 1  +  x
)  =  0  -> 
0  e.  RR ) )
76rexlimiv 2520 . 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 1316    e. wcel 1465   E.wrex 2394  (class class class)co 5742   RRcr 7587   0cc0 7588   1c1 7589    + caddc 7591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-1re 7682  ax-addrcl 7685  ax-rnegex 7697
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-cleq 2110  df-clel 2113  df-ral 2398  df-rex 2399
This theorem is referenced by:  0red  7735  0xr  7780  axmulgt0  7804  gtso  7811  0lt1  7857  ine0  8124  ltaddneg  8154  addgt0  8178  addgegt0  8179  addgtge0  8180  addge0  8181  ltaddpos  8182  ltneg  8192  leneg  8195  lt0neg1  8198  lt0neg2  8199  le0neg1  8200  le0neg2  8201  addge01  8202  suble0  8206  0le1  8211  gt0ne0i  8216  gt0ne0d  8242  lt0ne0d  8243  recexre  8307  recexgt0  8309  inelr  8313  rimul  8314  1ap0  8319  reapmul1  8324  apsqgt0  8330  msqge0  8345  mulge0  8348  recexaplem2  8380  recexap  8381  rerecclap  8457  ltm1  8568  recgt0  8572  ltmul12a  8582  lemul12a  8584  mulgt1  8585  gt0div  8592  ge0div  8593  recgt1i  8620  recreclt  8622  sup3exmid  8679  crap0  8680  nnge1  8707  nngt0  8709  nnrecgt0  8722  0ne1  8751  0le0  8773  neg1lt0  8792  halfge0  8894  iap0  8901  nn0ssre  8939  nn0ge0  8960  nn0nlt0  8961  nn0le0eq0  8963  0mnnnnn0  8967  elnnnn0b  8979  elnnnn0c  8980  elnnz  9022  0z  9023  elnnz1  9035  nn0lt10b  9089  recnz  9102  gtndiv  9104  fnn0ind  9125  rpge0  9409  rpnegap  9429  0nrp  9432  0ltpnf  9523  mnflt0  9525  xneg0  9569  xaddid1  9600  xnn0xadd0  9605  xposdif  9620  elrege0  9714  0e0icopnf  9717  0elunit  9724  1elunit  9725  divelunit  9740  lincmb01cmp  9741  iccf1o  9742  unitssre  9743  modqelico  10062  modqmuladdim  10095  addmodid  10100  expubnd  10305  le2sq2  10323  bernneq2  10368  expnbnd  10370  expnlbnd  10371  faclbnd  10442  faclbnd3  10444  faclbnd6  10445  bcval4  10453  bcpasc  10467  reim0  10588  re0  10622  im0  10623  rei  10626  imi  10627  cj0  10628  caucvgre  10708  rennim  10729  sqrt0rlem  10730  sqrt0  10731  resqrexlemdecn  10739  resqrexlemnm  10745  resqrexlemgt0  10747  sqrt00  10767  sqrt9  10775  sqrt2gt1lt2  10776  leabs  10801  ltabs  10814  sqrtpclii  10857  max0addsup  10946  fimaxre2  10953  climge0  11049  iserge0  11067  fsum00  11186  arisum2  11223  0.999...  11245  cos0  11351  ef01bndlem  11377  sin01bnd  11378  cos01bnd  11379  cos2bnd  11381  sin01gt0  11382  cos01gt0  11383  sincos2sgn  11386  sin4lt0  11387  absef  11390  absefib  11391  efieq1re  11392  epos  11399  flodddiv4  11543  gcdn0gt0  11578  nn0seqcvgd  11634  algcvgblem  11642  algcvga  11644  ssblps  12505  ssbl  12506  xmeter  12516  cnbl0  12614  pilem3  12775  pipos  12780  sinhalfpilem  12783  sincosq1sgn  12818  sincosq2sgn  12819  sinq34lt0t  12823  coseq0q4123  12826  coseq00topi  12827  coseq0negpitopi  12828  ex-gcd  12839  trilpolemclim  13125  trilpolemcl  13126  trilpolemisumle  13127  trilpolemeq1  13129  trilpolemlt1  13130
  Copyright terms: Public domain W3C validator