Theorem 0re 8290

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 8289	. 2 |- 1 e. RR
2		ax-rnegex 8252	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 8269	. . . . 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 2297	. . . 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 2656	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1398   e. wcel 2205   E.wrex 2523  (class class class)co 6058   RRcr 8142   0cc0 8143   1c1 8144   + caddc 8146

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1re 8237  ax-addrcl 8240  ax-rnegex 8252

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2227  df-clel 2230  df-ral 2527  df-rex 2528

This theorem is referenced by:  0red  8291  0xr  8336  axmulgt0  8361  gtso  8368  0lt1  8416  ine0  8684  ltaddneg  8715  addgt0  8739  addgegt0  8740  addgtge0  8741  addge0  8742  ltaddpos  8743  ltneg  8753  leneg  8756  lt0neg1  8759  lt0neg2  8760  le0neg1  8761  le0neg2  8762  addge01  8763  suble0  8767  0le1  8772  gt0ne0i  8777  gt0ne0d  8803  lt0ne0d  8804  recexre  8869  recexgt0  8871  inelr  8875  rimul  8876  1ap0  8881  reapmul1  8886  apsqgt0  8892  msqge0  8907  mulge0  8910  recexaplem2  8943  recexap  8944  rerecclap  9021  ltm1  9137  recgt0  9141  ltmul12a  9151  lemul12a  9153  mulgt1  9154  gt0div  9161  ge0div  9162  recgt1i  9189  recreclt  9191  sup3exmid  9248  crap0  9249  nnge1  9277  nngt0  9279  nnrecgt0  9292  0ne1  9321  0le0  9343  neg1lt0  9362  halfge0  9471  iap0  9478  nn0ssre  9517  nn0ge0  9538  nn0nlt0  9539  nn0le0eq0  9541  0mnnnnn0  9545  elnnnn0b  9557  elnnnn0c  9558  elnnz  9604  0z  9605  elnnz1  9617  nn0lt10b  9676  recnz  9689  gtndiv  9691  fnn0ind  9712  rpge0  10017  rpnegap  10037  0nrp  10040  0ltpnf  10134  mnflt0  10136  xneg0  10183  xaddid1  10214  xnn0xadd0  10219  xposdif  10234  elrege0  10328  0e0icopnf  10331  0elunit  10338  1elunit  10339  divelunit  10354  lincmb01cmp  10355  lincmble  10356  iccf1o  10357  unitssre  10358  fz0to4untppr  10480  nn0p1elfzo  10543  modqelico  10720  modqmuladdim  10753  addmodid  10758  xnn0nnen  10823  expubnd  10982  le2sq2  11001  resq01  11044  bernneq2  11048  expnbnd  11050  expnlbnd  11051  faclbnd  11128  faclbnd3  11130  faclbnd6  11131  bcval4  11139  bcpasc  11153  lsw0  11297  swrdccatin2  11446  pfxccatin12lem3  11449  reim0  11571  re0  11605  im0  11606  rei  11609  imi  11610  cj0  11611  caucvgre  11691  rennim  11712  sqrt0rlem  11713  sqrt0  11714  resqrexlemdecn  11722  resqrexlemnm  11728  resqrexlemgt0  11730  sqrt00  11750  sqrt9  11758  sqrt2gt1lt2  11759  leabs  11784  ltabs  11797  sqrtpclii  11840  max0addsup  11929  fimaxre2  11937  climge0  12035  iserge0  12053  fsum00  12173  arisum2  12210  0.999...  12232  fprodge0  12348  cos0  12441  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  cos2bnd  12471  sin01gt0  12473  cos01gt0  12474  sincos2sgn  12477  sin4lt0  12478  absef  12481  absefib  12482  efieq1re  12483  epos  12492  flodddiv4  12647  gcdn0gt0  12699  nn0seqcvgd  12763  algcvgblem  12771  algcvga  12773  pythagtriplem12  12998  pythagtriplem13  12999  pythagtriplem14  13000  pythagtriplem16  13002  ballotfilem2  13172  ballotfilem4  13185  ballotfilemi1  13189  ballotfilemic  13194  mulgnegnn  13885  ssblps  15416  ssbl  15417  xmeter  15427  cnbl0  15525  hovera  15638  hovergt0  15641  plyrecj  15754  reeff1olem  15762  pilem3  15774  pipos  15779  sinhalfpilem  15782  sincosq1sgn  15817  sincosq2sgn  15818  sinq34lt0t  15822  coseq0q4123  15825  coseq00topi  15826  coseq0negpitopi  15827  tangtx  15829  sincos4thpi  15831  sincos6thpi  15833  cosordlem  15840  cosq34lt1  15841  cos02pilt1  15842  cos0pilt1  15843  cos11  15844  ioocosf1o  15845  log1  15857  logrpap0b  15867  logdivlti  15872  rpabscxpbnd  15931  lgsval2lem  16009  lgsval4a  16021  lgsneg  16023  lgsdilem  16026  lgsdir2lem1  16027  clwwlkn0  16529  konigsberg  16614  ex-gcd  16625  repiecelem  16935  repiecele0  16936  repiecege0  16937  trilpolemclim  16946  trilpolemcl  16947  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  trirec0  16954  apdiff  16958  redc0  16968  reap0  16969  dceqnconst  16972  dcapnconst  16973  nconstwlpolemgt0  16976  neap0mkv  16981