Theorem 0re 8107

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 8106	. 2 |- 1 e. RR
2		ax-rnegex 8069	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 8086	. . . . 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 2270	. . . 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 2619	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1373   e. wcel 2178   E.wrex 2487  (class class class)co 5967   RRcr 7959   0cc0 7960   1c1 7961   + caddc 7963

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-1re 8054  ax-addrcl 8057  ax-rnegex 8069

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-cleq 2200  df-clel 2203  df-ral 2491  df-rex 2492

This theorem is referenced by:  0red  8108  0xr  8154  axmulgt0  8179  gtso  8186  0lt1  8234  ine0  8501  ltaddneg  8532  addgt0  8556  addgegt0  8557  addgtge0  8558  addge0  8559  ltaddpos  8560  ltneg  8570  leneg  8573  lt0neg1  8576  lt0neg2  8577  le0neg1  8578  le0neg2  8579  addge01  8580  suble0  8584  0le1  8589  gt0ne0i  8594  gt0ne0d  8620  lt0ne0d  8621  recexre  8686  recexgt0  8688  inelr  8692  rimul  8693  1ap0  8698  reapmul1  8703  apsqgt0  8709  msqge0  8724  mulge0  8727  recexaplem2  8760  recexap  8761  rerecclap  8838  ltm1  8954  recgt0  8958  ltmul12a  8968  lemul12a  8970  mulgt1  8971  gt0div  8978  ge0div  8979  recgt1i  9006  recreclt  9008  sup3exmid  9065  crap0  9066  nnge1  9094  nngt0  9096  nnrecgt0  9109  0ne1  9138  0le0  9160  neg1lt0  9179  halfge0  9288  iap0  9295  nn0ssre  9334  nn0ge0  9355  nn0nlt0  9356  nn0le0eq0  9358  0mnnnnn0  9362  elnnnn0b  9374  elnnnn0c  9375  elnnz  9417  0z  9418  elnnz1  9430  nn0lt10b  9488  recnz  9501  gtndiv  9503  fnn0ind  9524  rpge0  9823  rpnegap  9843  0nrp  9846  0ltpnf  9939  mnflt0  9941  xneg0  9988  xaddid1  10019  xnn0xadd0  10024  xposdif  10039  elrege0  10133  0e0icopnf  10136  0elunit  10143  1elunit  10144  divelunit  10159  lincmb01cmp  10160  iccf1o  10161  unitssre  10162  fz0to4untppr  10281  modqelico  10516  modqmuladdim  10549  addmodid  10554  xnn0nnen  10619  expubnd  10778  le2sq2  10797  bernneq2  10843  expnbnd  10845  expnlbnd  10846  faclbnd  10923  faclbnd3  10925  faclbnd6  10926  bcval4  10934  bcpasc  10948  lsw0  11078  swrdccatin2  11220  pfxccatin12lem3  11223  reim0  11287  re0  11321  im0  11322  rei  11325  imi  11326  cj0  11327  caucvgre  11407  rennim  11428  sqrt0rlem  11429  sqrt0  11430  resqrexlemdecn  11438  resqrexlemnm  11444  resqrexlemgt0  11446  sqrt00  11466  sqrt9  11474  sqrt2gt1lt2  11475  leabs  11500  ltabs  11513  sqrtpclii  11556  max0addsup  11645  fimaxre2  11653  climge0  11751  iserge0  11769  fsum00  11888  arisum2  11925  0.999...  11947  fprodge0  12063  cos0  12156  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  cos2bnd  12186  sin01gt0  12188  cos01gt0  12189  sincos2sgn  12192  sin4lt0  12193  absef  12196  absefib  12197  efieq1re  12198  epos  12207  flodddiv4  12362  gcdn0gt0  12414  nn0seqcvgd  12478  algcvgblem  12486  algcvga  12488  pythagtriplem12  12713  pythagtriplem13  12714  pythagtriplem14  12715  pythagtriplem16  12717  mulgnegnn  13583  ssblps  15012  ssbl  15013  xmeter  15023  cnbl0  15121  hovera  15234  hovergt0  15237  plyrecj  15350  reeff1olem  15358  pilem3  15370  pipos  15375  sinhalfpilem  15378  sincosq1sgn  15413  sincosq2sgn  15414  sinq34lt0t  15418  coseq0q4123  15421  coseq00topi  15422  coseq0negpitopi  15423  tangtx  15425  sincos4thpi  15427  sincos6thpi  15429  cosordlem  15436  cosq34lt1  15437  cos02pilt1  15438  cos0pilt1  15439  cos11  15440  ioocosf1o  15441  log1  15453  logrpap0b  15463  logdivlti  15468  rpabscxpbnd  15527  lgsval2lem  15602  lgsval4a  15614  lgsneg  15616  lgsdilem  15619  lgsdir2lem1  15620  ex-gcd  15867  trilpolemclim  16177  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  trirec0  16185  apdiff  16189  redc0  16198  reap0  16199  dceqnconst  16201  dcapnconst  16202  nconstwlpolemgt0  16205  neap0mkv  16210