Theorem 0re 7759

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 7758	. 2 |- 1 e. RR
2		ax-rnegex 7722	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 7739	. . . . 5 |- ( ( 1 e. RR /\ x e. RR ) -> ( 1 + x ) e. RR )
4	1, 3	mpan 420	. . . 4 |- ( x e. RR -> ( 1 + x ) e. RR )
5		eleq1 2200	. . . 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 2541	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1331   e. wcel 1480   E.wrex 2415  (class class class)co 5767   RRcr 7612   0cc0 7613   1c1 7614   + caddc 7616

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-1re 7707  ax-addrcl 7710  ax-rnegex 7722

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-cleq 2130  df-clel 2133  df-ral 2419  df-rex 2420

This theorem is referenced by:  0red  7760  0xr  7805  axmulgt0  7829  gtso  7836  0lt1  7882  ine0  8149  ltaddneg  8179  addgt0  8203  addgegt0  8204  addgtge0  8205  addge0  8206  ltaddpos  8207  ltneg  8217  leneg  8220  lt0neg1  8223  lt0neg2  8224  le0neg1  8225  le0neg2  8226  addge01  8227  suble0  8231  0le1  8236  gt0ne0i  8241  gt0ne0d  8267  lt0ne0d  8268  recexre  8333  recexgt0  8335  inelr  8339  rimul  8340  1ap0  8345  reapmul1  8350  apsqgt0  8356  msqge0  8371  mulge0  8374  recexaplem2  8406  recexap  8407  rerecclap  8483  ltm1  8597  recgt0  8601  ltmul12a  8611  lemul12a  8613  mulgt1  8614  gt0div  8621  ge0div  8622  recgt1i  8649  recreclt  8651  sup3exmid  8708  crap0  8709  nnge1  8736  nngt0  8738  nnrecgt0  8751  0ne1  8780  0le0  8802  neg1lt0  8821  halfge0  8929  iap0  8936  nn0ssre  8974  nn0ge0  8995  nn0nlt0  8996  nn0le0eq0  8998  0mnnnnn0  9002  elnnnn0b  9014  elnnnn0c  9015  elnnz  9057  0z  9058  elnnz1  9070  nn0lt10b  9124  recnz  9137  gtndiv  9139  fnn0ind  9160  rpge0  9447  rpnegap  9467  0nrp  9470  0ltpnf  9561  mnflt0  9563  xneg0  9607  xaddid1  9638  xnn0xadd0  9643  xposdif  9658  elrege0  9752  0e0icopnf  9755  0elunit  9762  1elunit  9763  divelunit  9778  lincmb01cmp  9779  iccf1o  9780  unitssre  9781  modqelico  10100  modqmuladdim  10133  addmodid  10138  expubnd  10343  le2sq2  10361  bernneq2  10406  expnbnd  10408  expnlbnd  10409  faclbnd  10480  faclbnd3  10482  faclbnd6  10483  bcval4  10491  bcpasc  10505  reim0  10626  re0  10660  im0  10661  rei  10664  imi  10665  cj0  10666  caucvgre  10746  rennim  10767  sqrt0rlem  10768  sqrt0  10769  resqrexlemdecn  10777  resqrexlemnm  10783  resqrexlemgt0  10785  sqrt00  10805  sqrt9  10813  sqrt2gt1lt2  10814  leabs  10839  ltabs  10852  sqrtpclii  10895  max0addsup  10984  fimaxre2  10991  climge0  11087  iserge0  11105  fsum00  11224  arisum2  11261  0.999...  11283  cos0  11426  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  cos2bnd  11456  sin01gt0  11457  cos01gt0  11458  sincos2sgn  11461  sin4lt0  11462  absef  11465  absefib  11466  efieq1re  11467  epos  11476  flodddiv4  11620  gcdn0gt0  11655  nn0seqcvgd  11711  algcvgblem  11719  algcvga  11721  ssblps  12583  ssbl  12584  xmeter  12594  cnbl0  12692  pilem3  12853  pipos  12858  sinhalfpilem  12861  sincosq1sgn  12896  sincosq2sgn  12897  sinq34lt0t  12901  coseq0q4123  12904  coseq00topi  12905  coseq0negpitopi  12906  tangtx  12908  sincos4thpi  12910  sincos6thpi  12912  cosordlem  12919  cosq34lt1  12920  cos02pilt1  12921  ex-gcd  12932  trilpolemclim  13218  trilpolemcl  13219  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223