Theorem 0re 7687

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 7686	. 2 |- 1 e. RR
2		ax-rnegex 7651	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 7667	. . . . 5 |- ( ( 1 e. RR /\ x e. RR ) -> ( 1 + x ) e. RR )
4	1, 3	mpan 418	. . . 4 |- ( x e. RR -> ( 1 + x ) e. RR )
5		eleq1 2177	. . . 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 2517	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1314   e. wcel 1463   E.wrex 2391  (class class class)co 5728   RRcr 7543   0cc0 7544   1c1 7545   + caddc 7547

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-1re 7636  ax-addrcl 7639  ax-rnegex 7651

This theorem depends on definitions:  df-bi 116  df-nf 1420  df-cleq 2108  df-clel 2111  df-ral 2395  df-rex 2396

This theorem is referenced by:  0red  7688  0xr  7733  axmulgt0  7757  gtso  7763  0lt1  7809  ine0  8072  ltaddneg  8102  addgt0  8126  addgegt0  8127  addgtge0  8128  addge0  8129  ltaddpos  8130  ltneg  8140  leneg  8143  lt0neg1  8146  lt0neg2  8147  le0neg1  8148  le0neg2  8149  addge01  8150  suble0  8154  0le1  8159  gt0ne0i  8164  gt0ne0d  8190  lt0ne0d  8191  recexre  8255  recexgt0  8257  inelr  8261  rimul  8262  1ap0  8267  reapmul1  8272  apsqgt0  8278  msqge0  8293  mulge0  8296  recexaplem2  8323  recexap  8324  rerecclap  8400  ltm1  8511  recgt0  8515  ltmul12a  8525  lemul12a  8527  mulgt1  8528  gt0div  8535  ge0div  8536  recgt1i  8563  recreclt  8565  sup3exmid  8622  crap0  8623  nnge1  8650  nngt0  8652  nnrecgt0  8665  0ne1  8694  0le0  8716  neg1lt0  8735  halfge0  8837  iap0  8844  nn0ssre  8882  nn0ge0  8903  nn0nlt0  8904  nn0le0eq0  8906  0mnnnnn0  8910  elnnnn0b  8922  elnnnn0c  8923  elnnz  8965  0z  8966  elnnz1  8978  nn0lt10b  9032  recnz  9045  gtndiv  9047  fnn0ind  9068  rpge0  9352  rpnegap  9372  0nrp  9373  0ltpnf  9458  mnflt0  9460  xneg0  9504  xaddid1  9535  xnn0xadd0  9540  xposdif  9555  elrege0  9649  0e0icopnf  9652  0elunit  9659  1elunit  9660  divelunit  9675  lincmb01cmp  9676  iccf1o  9677  unitssre  9678  modqelico  9997  modqmuladdim  10030  addmodid  10035  expubnd  10240  le2sq2  10258  bernneq2  10303  expnbnd  10305  expnlbnd  10306  faclbnd  10377  faclbnd3  10379  faclbnd6  10380  bcval4  10388  bcpasc  10402  reim0  10523  re0  10557  im0  10558  rei  10561  imi  10562  cj0  10563  caucvgre  10642  rennim  10663  sqrt0rlem  10664  sqrt0  10665  resqrexlemdecn  10673  resqrexlemnm  10679  resqrexlemgt0  10681  sqrt00  10701  sqrt9  10709  sqrt2gt1lt2  10710  leabs  10735  ltabs  10748  sqrtpclii  10791  max0addsup  10880  fimaxre2  10887  climge0  10983  iserge0  11001  fsum00  11120  arisum2  11157  0.999...  11179  cos0  11285  ef01bndlem  11311  sin01bnd  11312  cos01bnd  11313  cos2bnd  11315  sin01gt0  11316  cos01gt0  11317  sincos2sgn  11320  sin4lt0  11321  absef  11323  absefib  11324  efieq1re  11325  epos  11332  flodddiv4  11476  gcdn0gt0  11511  nn0seqcvgd  11565  algcvgblem  11573  algcvga  11575  ssblps  12411  ssbl  12412  xmeter  12422  cnbl0  12520  ex-gcd  12630  trilpolemclim  12913  trilpolemcl  12914  trilpolemisumle  12915  trilpolemeq1  12917  trilpolemlt1  12918