Theorem 0re 8332

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 8331	. 2 |- 1 e. RR
2		ax-rnegex 8294	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 8311	. . . . 5 |- ( ( 1 e. RR /\ x e. RR ) -> ( 1 + x ) e. RR )
4	1, 3	mpan 428	. . . 4 |- ( x e. RR -> ( 1 + x ) e. RR )
5		eleq1 2301	. . . 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 2662	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209   E.wrex 2529  (class class class)co 6088   RRcr 8184   0cc0 8185   1c1 8186   + caddc 8188

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8279  ax-addrcl 8282  ax-rnegex 8294

This proof depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-ral 2533  df-rex 2534

This theorem is used by:  0red  8333  0xr  8378  axmulgt0  8403  gtso  8410  0lt1  8460  ine0  8728  ltaddneg  8759  addgt0  8783  addgegt0  8784  addgtge0  8785  addge0  8786  ltaddpos  8787  ltneg  8797  leneg  8800  lt0neg1  8803  lt0neg2  8804  le0neg1  8805  le0neg2  8806  addge01  8807  suble0  8811  0le1  8816  gt0ne0i  8821  gt0ne0d  8847  lt0ne0d  8848  recexre  8914  recexgt0  8916  inelr  8920  rimul  8921  1ap0  8926  reapmul1  8931  apsqgt0  8937  msqge0  8952  mulge0  8955  recexaplem2  8988  recexap  8989  rerecclap  9068  ltm1  9184  recgt0  9188  ltmul12a  9198  lemul12a  9200  mulgt1  9201  gt0div  9208  ge0div  9209  recgt1i  9236  recreclt  9238  sup3exmid  9295  crap0  9296  indfval  9308  indconst0  9311  nnge1  9336  nngt0  9338  nnrecgt0  9351  0ne1  9380  0le0  9402  neg1lt0  9421  halfge0  9532  iap0  9539  nn0ssre  9578  nn0ge0  9599  nn0nlt0  9600  nn0le0eq0  9602  0mnnnnn0  9606  elnnnn0b  9618  elnnnn0c  9619  elnnz  9663  0z  9664  elnnz1  9676  nn0lt10b  9735  recnz  9749  gtndiv  9751  fnn0ind  9772  rpge0  10083  rpnegap  10103  0nrp  10106  0ltpnf  10200  mnflt0  10202  xneg0  10249  xaddid1  10280  xnn0xadd0  10285  xposdif  10300  elrege0  10394  0e0icopnf  10397  0elunit  10404  1elunit  10405  divelunit  10420  lincmb01cmp  10421  lincmble  10422  iccf1o  10423  unitssre  10424  fz0to4untppr  10547  nn0p1elfzo  10610  modqelico  10791  modqmuladdim  10824  addmodid  10829  xnn0nnen  10894  expubnd  11053  le2sq2  11072  resq01  11115  bernneq2  11119  expnbnd  11121  expnlbnd  11122  faclbnd  11200  faclbnd3  11202  faclbnd6  11203  bcval4  11211  bcpasc  11225  lsw0  11373  swrdccatin2  11522  pfxccatin12lem3  11525  reim0  11647  re0  11682  im0  11683  rei  11686  imi  11687  cj0  11688  caucvgre  11768  rennim  11789  sqrt0rlem  11790  sqrt0  11791  resqrexlemdecn  11799  resqrexlemnm  11805  resqrexlemgt0  11807  sqrt00  11827  sqrt9  11835  sqrt2gt1lt2  11836  leabs  11861  ltabs  11875  sqrtpclii  11918  max0addsup  12007  fimaxre2  12015  climge0  12115  iserge0  12133  fsum00  12253  arisum2  12290  0.999...  12312  fprodge0  12428  cos0  12521  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  cos2bnd  12551  sin01gt0  12553  cos01gt0  12554  sincos2sgn  12557  sin4lt0  12558  absef  12561  absefib  12562  efieq1re  12563  epos  12572  flodddiv4  12727  gcdn0gt0  12779  nn0seqcvgd  12843  algcvgblem  12851  algcvga  12853  pythagtriplem12  13082  pythagtriplem13  13083  pythagtriplem14  13084  pythagtriplem16  13086  ballotfilem2  13285  ballotfilem4  13298  ballotfilemi1  13302  ballotfilemic  13307  mulgnegnn  13993  ssblps  15668  ssbl  15669  xmeter  15679  cnbl0  15777  hovera  15890  hovergt0  15893  plyrecj  16006  reeff1olem  16014  efap1p  16022  pilem3  16027  pipos  16032  sinhalfpilem  16035  sincosq1sgn  16070  sincosq2sgn  16071  sinq34lt0t  16075  coseq0q4123  16078  coseq00topi  16079  coseq0negpitopi  16080  tangtx  16082  sincos4thpi  16084  sincos6thpi  16086  cosordlem  16094  cosq34lt1  16095  cos02pilt1  16096  cos0pilt1  16097  cos11  16098  ioocosf1o  16099  log1  16112  logrpap0b  16123  logdivlti  16128  rpabscxpbnd  16192  log2tlbndlog2  16237  log2ublog2  16241  efnnfsumcl  16256  ppiqsval  16257  efchtqdvds  16282  ppiqub  16310  chtqleppi  16311  bposlem4  16331  bposlem5  16332  bposlem7  16334  bposlem8  16335  bposlem9  16336  lgsval2lem  16351  lgsval4a  16363  lgsneg  16365  lgsdilem  16368  lgsdir2lem1  16369  clwwlkn0  16871  konigsberg  16956  ex-gcd  16967  repiecelem  17297  repiecele0  17298  repiecege0  17299  trilpolemclim  17309  trilpolemcl  17310  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  trirec0  17317  apdiff  17321  redc0  17331  reap0  17332  dceqnconst  17334  dcapnconst  17335  nconstwlpolemgt0  17338  neap0mkv  17343