Theorem 0re 7027

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 7026	. 2 |- 1 e. RR
2		ax-rnegex 6993	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 7007	. . . . 5 |- ( ( 1 e. RR /\ x e. RR ) -> ( 1 + x ) e. RR )
4	1, 3	mpan 400	. . . 4 |- ( x e. RR -> ( 1 + x ) e. RR )
5		eleq1 2100	. . . 4 |- ( ( 1 + x ) = 0 -> ( ( 1 + x ) e. RR <-> 0 e. RR ) )
6	4, 5	syl5ibcom 144	. . 3 |- ( x e. RR -> ( ( 1 + x ) = 0 -> 0 e. RR ) )
7	6	rexlimiv 2427	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1243   e. wcel 1393   E.wrex 2307  (class class class)co 5512   RRcr 6888   0cc0 6889   1c1 6890   + caddc 6892

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-1re 6978  ax-addrcl 6981  ax-rnegex 6993

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-cleq 2033  df-clel 2036  df-ral 2311  df-rex 2312

This theorem is referenced by:  0red  7028  0xr  7072  axmulgt0  7091  gtso  7097  0lt1  7141  ine0  7391  addgt0  7443  addgegt0  7444  addgtge0  7445  addge0  7446  ltaddpos  7447  ltneg  7457  leneg  7460  lt0neg1  7463  lt0neg2  7464  le0neg1  7465  le0neg2  7466  addge01  7467  suble0  7471  0le1  7476  gt0ne0i  7478  gt0ne0d  7504  lt0ne0d  7505  recexre  7569  recexgt0  7571  inelr  7575  rimul  7576  1ap0  7581  reapmul1  7586  apsqgt0  7592  msqge0  7607  mulge0  7610  recexaplem2  7633  recexap  7634  rerecclap  7706  ltm1  7812  recgt0  7816  ltmul12a  7826  lemul12a  7828  mulgt1  7829  gt0div  7836  ge0div  7837  recgt1i  7864  recreclt  7866  crap0  7910  nnge1  7937  nngt0  7939  nnrecgt0  7951  0ne1  7982  0le0  8005  neg1lt0  8025  halfge0  8141  iap0  8148  nn0ssre  8185  nn0ge0  8207  nn0nlt0  8208  nn0le0eq0  8210  0mnnnnn0  8214  elnnnn0b  8226  elnnnn0c  8227  elnnz  8255  0z  8256  elnnz1  8268  nn0lt10b  8321  recnz  8333  gtndiv  8335  fnn0ind  8354  rpge0  8595  rpnegap  8615  0nrp  8616  0ltpnf  8703  mnflt0  8705  xneg0  8744  elrege0  8845  0e0icopnf  8848  0elunit  8854  1elunit  8855  divelunit  8870  lincmb01cmp  8871  iccf1o  8872  unitssre  8873  modqelico  9176  expubnd  9311  le2sq2  9329  bernneq2  9370  expnbnd  9372  expnlbnd  9373  reim0  9461  re0  9495  im0  9496  rei  9499  imi  9500  cj0  9501  caucvgre  9580  rennim  9600  sqrt0rlem  9601  sqrt0  9602  resqrexlemdecn  9610  resqrexlemnm  9616  resqrexlemgt0  9618  sqrt00  9638  sqrt9  9646  sqrt2gt1lt2  9647  leabs  9672  ltabs  9683  sqrtpclii  9726  climge0  9845  iserige0  9863  nn0seqcvgd  9880  algcvgblem  9888  ialgcvga  9890