Theorem 0re 7119

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 7118	. 2 |- 1 e. RR
2		ax-rnegex 7085	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 7099	. . . . 5 |- ( ( 1 e. RR /\ x e. RR ) -> ( 1 + x ) e. RR )
4	1, 3	mpan 414	. . . 4 |- ( x e. RR -> ( 1 + x ) e. RR )
5		eleq1 2141	. . . 4 |- ( ( 1 + x ) = 0 -> ( ( 1 + x ) e. RR <-> 0 e. RR ) )
6	4, 5	syl5ibcom 153	. . 3 |- ( x e. RR -> ( ( 1 + x ) = 0 -> 0 e. RR ) )
7	6	rexlimiv 2471	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1284   e. wcel 1433   E.wrex 2349  (class class class)co 5532   RRcr 6980   0cc0 6981   1c1 6982   + caddc 6984

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-1re 7070  ax-addrcl 7073  ax-rnegex 7085

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-cleq 2074  df-clel 2077  df-ral 2353  df-rex 2354

This theorem is referenced by:  0red  7120  0xr  7165  axmulgt0  7184  gtso  7190  0lt1  7236  ine0  7498  ltaddneg  7528  addgt0  7552  addgegt0  7553  addgtge0  7554  addge0  7555  ltaddpos  7556  ltneg  7566  leneg  7569  lt0neg1  7572  lt0neg2  7573  le0neg1  7574  le0neg2  7575  addge01  7576  suble0  7580  0le1  7585  gt0ne0i  7587  gt0ne0d  7613  lt0ne0d  7614  recexre  7678  recexgt0  7680  inelr  7684  rimul  7685  1ap0  7690  reapmul1  7695  apsqgt0  7701  msqge0  7716  mulge0  7719  recexaplem2  7742  recexap  7743  rerecclap  7818  ltm1  7924  recgt0  7928  ltmul12a  7938  lemul12a  7940  mulgt1  7941  gt0div  7948  ge0div  7949  recgt1i  7976  recreclt  7978  crap0  8035  nnge1  8062  nngt0  8064  nnrecgt0  8076  0ne1  8106  0le0  8128  neg1lt0  8147  halfge0  8247  iap0  8254  nn0ssre  8292  nn0ge0  8313  nn0nlt0  8314  nn0le0eq0  8316  0mnnnnn0  8320  elnnnn0b  8332  elnnnn0c  8333  elnnz  8361  0z  8362  elnnz1  8374  nn0lt10b  8428  recnz  8440  gtndiv  8442  fnn0ind  8463  rpge0  8746  rpnegap  8766  0nrp  8767  0ltpnf  8857  mnflt0  8859  xneg0  8898  elrege0  8999  0e0icopnf  9002  0elunit  9008  1elunit  9009  divelunit  9024  lincmb01cmp  9025  iccf1o  9026  unitssre  9027  modqelico  9336  modqmuladdim  9369  addmodid  9374  expubnd  9533  le2sq2  9551  bernneq2  9594  expnbnd  9596  expnlbnd  9597  faclbnd  9668  faclbnd3  9670  faclbnd6  9671  bcval4  9679  bcpasc  9693  reim0  9748  re0  9782  im0  9783  rei  9786  imi  9787  cj0  9788  caucvgre  9867  rennim  9888  sqrt0rlem  9889  sqrt0  9890  resqrexlemdecn  9898  resqrexlemnm  9904  resqrexlemgt0  9906  sqrt00  9926  sqrt9  9934  sqrt2gt1lt2  9935  leabs  9960  ltabs  9973  sqrtpclii  10016  max0addsup  10105  fimaxre2  10109  climge0  10163  iserige0  10181  flodddiv4  10334  gcdn0gt0  10369  nn0seqcvgd  10423  algcvgblem  10431  ialgcvga  10433  ex-gcd  10568