Theorem 0re 7899

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

Step	Hyp	Ref	Expression
1		1re 7898	. 2 |- 1 e. RR
2		ax-rnegex 7862	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 7879	. . . . 5 |- ( ( 1 e. RR /\ x e. RR ) -> ( 1 + x ) e. RR )
4	1, 3	mpan 421	. . . 4 |- ( x e. RR -> ( 1 + x ) e. RR )
5		eleq1 2229	. . . 4 |- ( ( 1 + x ) = 0 -> ( ( 1 + x ) e. RR <-> 0 e. RR ) )
6	4, 5	syl5ibcom 154	. . 3 |- ( x e. RR -> ( ( 1 + x ) = 0 -> 0 e. RR ) )
7	6	rexlimiv 2577	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1343   e. wcel 2136   E.wrex 2445  (class class class)co 5842   RRcr 7752   0cc0 7753   1c1 7754   + caddc 7756

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-1re 7847  ax-addrcl 7850  ax-rnegex 7862

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-cleq 2158  df-clel 2161  df-ral 2449  df-rex 2450

This theorem is referenced by:  0red  7900  0xr  7945  axmulgt0  7970  gtso  7977  0lt1  8025  ine0  8292  ltaddneg  8322  addgt0  8346  addgegt0  8347  addgtge0  8348  addge0  8349  ltaddpos  8350  ltneg  8360  leneg  8363  lt0neg1  8366  lt0neg2  8367  le0neg1  8368  le0neg2  8369  addge01  8370  suble0  8374  0le1  8379  gt0ne0i  8384  gt0ne0d  8410  lt0ne0d  8411  recexre  8476  recexgt0  8478  inelr  8482  rimul  8483  1ap0  8488  reapmul1  8493  apsqgt0  8499  msqge0  8514  mulge0  8517  recexaplem2  8549  recexap  8550  rerecclap  8626  ltm1  8741  recgt0  8745  ltmul12a  8755  lemul12a  8757  mulgt1  8758  gt0div  8765  ge0div  8766  recgt1i  8793  recreclt  8795  sup3exmid  8852  crap0  8853  nnge1  8880  nngt0  8882  nnrecgt0  8895  0ne1  8924  0le0  8946  neg1lt0  8965  halfge0  9073  iap0  9080  nn0ssre  9118  nn0ge0  9139  nn0nlt0  9140  nn0le0eq0  9142  0mnnnnn0  9146  elnnnn0b  9158  elnnnn0c  9159  elnnz  9201  0z  9202  elnnz1  9214  nn0lt10b  9271  recnz  9284  gtndiv  9286  fnn0ind  9307  rpge0  9602  rpnegap  9622  0nrp  9625  0ltpnf  9718  mnflt0  9720  xneg0  9767  xaddid1  9798  xnn0xadd0  9803  xposdif  9818  elrege0  9912  0e0icopnf  9915  0elunit  9922  1elunit  9923  divelunit  9938  lincmb01cmp  9939  iccf1o  9940  unitssre  9941  fz0to4untppr  10059  modqelico  10269  modqmuladdim  10302  addmodid  10307  expubnd  10512  le2sq2  10530  bernneq2  10576  expnbnd  10578  expnlbnd  10579  faclbnd  10654  faclbnd3  10656  faclbnd6  10657  bcval4  10665  bcpasc  10679  reim0  10803  re0  10837  im0  10838  rei  10841  imi  10842  cj0  10843  caucvgre  10923  rennim  10944  sqrt0rlem  10945  sqrt0  10946  resqrexlemdecn  10954  resqrexlemnm  10960  resqrexlemgt0  10962  sqrt00  10982  sqrt9  10990  sqrt2gt1lt2  10991  leabs  11016  ltabs  11029  sqrtpclii  11072  max0addsup  11161  fimaxre2  11168  climge0  11266  iserge0  11284  fsum00  11403  arisum2  11440  0.999...  11462  fprodge0  11578  cos0  11671  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  cos2bnd  11701  sin01gt0  11702  cos01gt0  11703  sincos2sgn  11706  sin4lt0  11707  absef  11710  absefib  11711  efieq1re  11712  epos  11721  flodddiv4  11871  gcdn0gt0  11911  nn0seqcvgd  11973  algcvgblem  11981  algcvga  11983  pythagtriplem12  12207  pythagtriplem13  12208  pythagtriplem14  12209  pythagtriplem16  12211  ssblps  13065  ssbl  13066  xmeter  13076  cnbl0  13174  reeff1olem  13332  pilem3  13344  pipos  13349  sinhalfpilem  13352  sincosq1sgn  13387  sincosq2sgn  13388  sinq34lt0t  13392  coseq0q4123  13395  coseq00topi  13396  coseq0negpitopi  13397  tangtx  13399  sincos4thpi  13401  sincos6thpi  13403  cosordlem  13410  cosq34lt1  13411  cos02pilt1  13412  cos0pilt1  13413  cos11  13414  ioocosf1o  13415  log1  13427  logrpap0b  13437  logdivlti  13442  rpabscxpbnd  13499  lgsval2lem  13551  lgsval4a  13563  lgsneg  13565  lgsdilem  13568  lgsdir2lem1  13569  ex-gcd  13612  trilpolemclim  13915  trilpolemcl  13916  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  trirec0  13923  apdiff  13927  redc0  13936  reap0  13937  dceqnconst  13938  dcapnconst  13939  nconstwlpolemgt0  13942