Theorem 0re 8239

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 8238	. 2 |- 1 e. RR
2		ax-rnegex 8201	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 8218	. . . . 5 |- ( ( 1 e. RR /\ x e. RR ) -> ( 1 + x ) e. RR )
4	1, 3	mpan 424	. . . 4 |- ( x e. RR -> ( 1 + x ) e. RR )
5		eleq1 2294	. . . 4 |- ( ( 1 + x ) = 0 -> ( ( 1 + x ) e. RR <-> 0 e. RR ) )
6	4, 5	syl5ibcom 155	. . 3 |- ( x e. RR -> ( ( 1 + x ) = 0 -> 0 e. RR ) )
7	6	rexlimiv 2645	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1398   e. wcel 2202   E.wrex 2512  (class class class)co 6028   RRcr 8091   0cc0 8092   1c1 8093   + caddc 8095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1re 8186  ax-addrcl 8189  ax-rnegex 8201

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2224  df-clel 2227  df-ral 2516  df-rex 2517

This theorem is referenced by:  0red  8240  0xr  8285  axmulgt0  8310  gtso  8317  0lt1  8365  ine0  8632  ltaddneg  8663  addgt0  8687  addgegt0  8688  addgtge0  8689  addge0  8690  ltaddpos  8691  ltneg  8701  leneg  8704  lt0neg1  8707  lt0neg2  8708  le0neg1  8709  le0neg2  8710  addge01  8711  suble0  8715  0le1  8720  gt0ne0i  8725  gt0ne0d  8751  lt0ne0d  8752  recexre  8817  recexgt0  8819  inelr  8823  rimul  8824  1ap0  8829  reapmul1  8834  apsqgt0  8840  msqge0  8855  mulge0  8858  recexaplem2  8891  recexap  8892  rerecclap  8969  ltm1  9085  recgt0  9089  ltmul12a  9099  lemul12a  9101  mulgt1  9102  gt0div  9109  ge0div  9110  recgt1i  9137  recreclt  9139  sup3exmid  9196  crap0  9197  nnge1  9225  nngt0  9227  nnrecgt0  9240  0ne1  9269  0le0  9291  neg1lt0  9310  halfge0  9419  iap0  9426  nn0ssre  9465  nn0ge0  9486  nn0nlt0  9487  nn0le0eq0  9489  0mnnnnn0  9493  elnnnn0b  9505  elnnnn0c  9506  elnnz  9550  0z  9551  elnnz1  9563  nn0lt10b  9621  recnz  9634  gtndiv  9636  fnn0ind  9657  rpge0  9962  rpnegap  9982  0nrp  9985  0ltpnf  10078  mnflt0  10080  xneg0  10127  xaddid1  10158  xnn0xadd0  10163  xposdif  10178  elrege0  10272  0e0icopnf  10275  0elunit  10282  1elunit  10283  divelunit  10298  lincmb01cmp  10299  lincmble  10300  iccf1o  10301  unitssre  10302  fz0to4untppr  10421  nn0p1elfzo  10484  modqelico  10659  modqmuladdim  10692  addmodid  10697  xnn0nnen  10762  expubnd  10921  le2sq2  10940  bernneq2  10986  expnbnd  10988  expnlbnd  10989  faclbnd  11066  faclbnd3  11068  faclbnd6  11069  bcval4  11077  bcpasc  11091  lsw0  11227  swrdccatin2  11376  pfxccatin12lem3  11379  reim0  11501  re0  11535  im0  11536  rei  11539  imi  11540  cj0  11541  caucvgre  11621  rennim  11642  sqrt0rlem  11643  sqrt0  11644  resqrexlemdecn  11652  resqrexlemnm  11658  resqrexlemgt0  11660  sqrt00  11680  sqrt9  11688  sqrt2gt1lt2  11689  leabs  11714  ltabs  11727  sqrtpclii  11770  max0addsup  11859  fimaxre2  11867  climge0  11965  iserge0  11983  fsum00  12103  arisum2  12140  0.999...  12162  fprodge0  12278  cos0  12371  ef01bndlem  12397  sin01bnd  12398  cos01bnd  12399  cos2bnd  12401  sin01gt0  12403  cos01gt0  12404  sincos2sgn  12407  sin4lt0  12408  absef  12411  absefib  12412  efieq1re  12413  epos  12422  flodddiv4  12577  gcdn0gt0  12629  nn0seqcvgd  12693  algcvgblem  12701  algcvga  12703  pythagtriplem12  12928  pythagtriplem13  12929  pythagtriplem14  12930  pythagtriplem16  12932  mulgnegnn  13799  ssblps  15236  ssbl  15237  xmeter  15247  cnbl0  15345  hovera  15458  hovergt0  15461  plyrecj  15574  reeff1olem  15582  pilem3  15594  pipos  15599  sinhalfpilem  15602  sincosq1sgn  15637  sincosq2sgn  15638  sinq34lt0t  15642  coseq0q4123  15645  coseq00topi  15646  coseq0negpitopi  15647  tangtx  15649  sincos4thpi  15651  sincos6thpi  15653  cosordlem  15660  cosq34lt1  15661  cos02pilt1  15662  cos0pilt1  15663  cos11  15664  ioocosf1o  15665  log1  15677  logrpap0b  15687  logdivlti  15692  rpabscxpbnd  15751  lgsval2lem  15829  lgsval4a  15841  lgsneg  15843  lgsdilem  15846  lgsdir2lem1  15847  clwwlkn0  16349  konigsberg  16434  ex-gcd  16445  repiecelem  16757  repiecele0  16758  repiecege0  16759  trilpolemclim  16768  trilpolemcl  16769  trilpolemisumle  16770  trilpolemeq1  16772  trilpolemlt1  16773  trirec0  16776  apdiff  16780  redc0  16790  reap0  16791  dceqnconst  16793  dcapnconst  16794  nconstwlpolemgt0  16797  neap0mkv  16802