Theorem 0re 7920

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 7919	. 2 |- 1 e. RR
2		ax-rnegex 7883	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 7900	. . . . 5 |- ( ( 1 e. RR /\ x e. RR ) -> ( 1 + x ) e. RR )
4	1, 3	mpan 422	. . . 4 |- ( x e. RR -> ( 1 + x ) e. RR )
5		eleq1 2233	. . . 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 2581	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1348   e. wcel 2141   E.wrex 2449  (class class class)co 5853   RRcr 7773   0cc0 7774   1c1 7775   + caddc 7777

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1re 7868  ax-addrcl 7871  ax-rnegex 7883

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-cleq 2163  df-clel 2166  df-ral 2453  df-rex 2454

This theorem is referenced by:  0red  7921  0xr  7966  axmulgt0  7991  gtso  7998  0lt1  8046  ine0  8313  ltaddneg  8343  addgt0  8367  addgegt0  8368  addgtge0  8369  addge0  8370  ltaddpos  8371  ltneg  8381  leneg  8384  lt0neg1  8387  lt0neg2  8388  le0neg1  8389  le0neg2  8390  addge01  8391  suble0  8395  0le1  8400  gt0ne0i  8405  gt0ne0d  8431  lt0ne0d  8432  recexre  8497  recexgt0  8499  inelr  8503  rimul  8504  1ap0  8509  reapmul1  8514  apsqgt0  8520  msqge0  8535  mulge0  8538  recexaplem2  8570  recexap  8571  rerecclap  8647  ltm1  8762  recgt0  8766  ltmul12a  8776  lemul12a  8778  mulgt1  8779  gt0div  8786  ge0div  8787  recgt1i  8814  recreclt  8816  sup3exmid  8873  crap0  8874  nnge1  8901  nngt0  8903  nnrecgt0  8916  0ne1  8945  0le0  8967  neg1lt0  8986  halfge0  9094  iap0  9101  nn0ssre  9139  nn0ge0  9160  nn0nlt0  9161  nn0le0eq0  9163  0mnnnnn0  9167  elnnnn0b  9179  elnnnn0c  9180  elnnz  9222  0z  9223  elnnz1  9235  nn0lt10b  9292  recnz  9305  gtndiv  9307  fnn0ind  9328  rpge0  9623  rpnegap  9643  0nrp  9646  0ltpnf  9739  mnflt0  9741  xneg0  9788  xaddid1  9819  xnn0xadd0  9824  xposdif  9839  elrege0  9933  0e0icopnf  9936  0elunit  9943  1elunit  9944  divelunit  9959  lincmb01cmp  9960  iccf1o  9961  unitssre  9962  fz0to4untppr  10080  modqelico  10290  modqmuladdim  10323  addmodid  10328  expubnd  10533  le2sq2  10551  bernneq2  10597  expnbnd  10599  expnlbnd  10600  faclbnd  10675  faclbnd3  10677  faclbnd6  10678  bcval4  10686  bcpasc  10700  reim0  10825  re0  10859  im0  10860  rei  10863  imi  10864  cj0  10865  caucvgre  10945  rennim  10966  sqrt0rlem  10967  sqrt0  10968  resqrexlemdecn  10976  resqrexlemnm  10982  resqrexlemgt0  10984  sqrt00  11004  sqrt9  11012  sqrt2gt1lt2  11013  leabs  11038  ltabs  11051  sqrtpclii  11094  max0addsup  11183  fimaxre2  11190  climge0  11288  iserge0  11306  fsum00  11425  arisum2  11462  0.999...  11484  fprodge0  11600  cos0  11693  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  cos2bnd  11723  sin01gt0  11724  cos01gt0  11725  sincos2sgn  11728  sin4lt0  11729  absef  11732  absefib  11733  efieq1re  11734  epos  11743  flodddiv4  11893  gcdn0gt0  11933  nn0seqcvgd  11995  algcvgblem  12003  algcvga  12005  pythagtriplem12  12229  pythagtriplem13  12230  pythagtriplem14  12231  pythagtriplem16  12233  ssblps  13219  ssbl  13220  xmeter  13230  cnbl0  13328  reeff1olem  13486  pilem3  13498  pipos  13503  sinhalfpilem  13506  sincosq1sgn  13541  sincosq2sgn  13542  sinq34lt0t  13546  coseq0q4123  13549  coseq00topi  13550  coseq0negpitopi  13551  tangtx  13553  sincos4thpi  13555  sincos6thpi  13557  cosordlem  13564  cosq34lt1  13565  cos02pilt1  13566  cos0pilt1  13567  cos11  13568  ioocosf1o  13569  log1  13581  logrpap0b  13591  logdivlti  13596  rpabscxpbnd  13653  lgsval2lem  13705  lgsval4a  13717  lgsneg  13719  lgsdilem  13722  lgsdir2lem1  13723  ex-gcd  13766  trilpolemclim  14068  trilpolemcl  14069  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  trirec0  14076  apdiff  14080  redc0  14089  reap0  14090  dceqnconst  14091  dcapnconst  14092  nconstwlpolemgt0  14095