Theorem 0re 8146

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 8145	. 2 |- 1 e. RR
2		ax-rnegex 8108	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 8125	. . . . 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 2292	. . . 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 2642	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1395   e. wcel 2200   E.wrex 2509  (class class class)co 6001   RRcr 7998   0cc0 7999   1c1 8000   + caddc 8002

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8093  ax-addrcl 8096  ax-rnegex 8108

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-ral 2513  df-rex 2514

This theorem is referenced by:  0red  8147  0xr  8193  axmulgt0  8218  gtso  8225  0lt1  8273  ine0  8540  ltaddneg  8571  addgt0  8595  addgegt0  8596  addgtge0  8597  addge0  8598  ltaddpos  8599  ltneg  8609  leneg  8612  lt0neg1  8615  lt0neg2  8616  le0neg1  8617  le0neg2  8618  addge01  8619  suble0  8623  0le1  8628  gt0ne0i  8633  gt0ne0d  8659  lt0ne0d  8660  recexre  8725  recexgt0  8727  inelr  8731  rimul  8732  1ap0  8737  reapmul1  8742  apsqgt0  8748  msqge0  8763  mulge0  8766  recexaplem2  8799  recexap  8800  rerecclap  8877  ltm1  8993  recgt0  8997  ltmul12a  9007  lemul12a  9009  mulgt1  9010  gt0div  9017  ge0div  9018  recgt1i  9045  recreclt  9047  sup3exmid  9104  crap0  9105  nnge1  9133  nngt0  9135  nnrecgt0  9148  0ne1  9177  0le0  9199  neg1lt0  9218  halfge0  9327  iap0  9334  nn0ssre  9373  nn0ge0  9394  nn0nlt0  9395  nn0le0eq0  9397  0mnnnnn0  9401  elnnnn0b  9413  elnnnn0c  9414  elnnz  9456  0z  9457  elnnz1  9469  nn0lt10b  9527  recnz  9540  gtndiv  9542  fnn0ind  9563  rpge0  9862  rpnegap  9882  0nrp  9885  0ltpnf  9978  mnflt0  9980  xneg0  10027  xaddid1  10058  xnn0xadd0  10063  xposdif  10078  elrege0  10172  0e0icopnf  10175  0elunit  10182  1elunit  10183  divelunit  10198  lincmb01cmp  10199  iccf1o  10200  unitssre  10201  fz0to4untppr  10320  modqelico  10556  modqmuladdim  10589  addmodid  10594  xnn0nnen  10659  expubnd  10818  le2sq2  10837  bernneq2  10883  expnbnd  10885  expnlbnd  10886  faclbnd  10963  faclbnd3  10965  faclbnd6  10966  bcval4  10974  bcpasc  10988  lsw0  11119  swrdccatin2  11261  pfxccatin12lem3  11264  reim0  11372  re0  11406  im0  11407  rei  11410  imi  11411  cj0  11412  caucvgre  11492  rennim  11513  sqrt0rlem  11514  sqrt0  11515  resqrexlemdecn  11523  resqrexlemnm  11529  resqrexlemgt0  11531  sqrt00  11551  sqrt9  11559  sqrt2gt1lt2  11560  leabs  11585  ltabs  11598  sqrtpclii  11641  max0addsup  11730  fimaxre2  11738  climge0  11836  iserge0  11854  fsum00  11973  arisum2  12010  0.999...  12032  fprodge0  12148  cos0  12241  ef01bndlem  12267  sin01bnd  12268  cos01bnd  12269  cos2bnd  12271  sin01gt0  12273  cos01gt0  12274  sincos2sgn  12277  sin4lt0  12278  absef  12281  absefib  12282  efieq1re  12283  epos  12292  flodddiv4  12447  gcdn0gt0  12499  nn0seqcvgd  12563  algcvgblem  12571  algcvga  12573  pythagtriplem12  12798  pythagtriplem13  12799  pythagtriplem14  12800  pythagtriplem16  12802  mulgnegnn  13669  ssblps  15099  ssbl  15100  xmeter  15110  cnbl0  15208  hovera  15321  hovergt0  15324  plyrecj  15437  reeff1olem  15445  pilem3  15457  pipos  15462  sinhalfpilem  15465  sincosq1sgn  15500  sincosq2sgn  15501  sinq34lt0t  15505  coseq0q4123  15508  coseq00topi  15509  coseq0negpitopi  15510  tangtx  15512  sincos4thpi  15514  sincos6thpi  15516  cosordlem  15523  cosq34lt1  15524  cos02pilt1  15525  cos0pilt1  15526  cos11  15527  ioocosf1o  15528  log1  15540  logrpap0b  15550  logdivlti  15555  rpabscxpbnd  15614  lgsval2lem  15689  lgsval4a  15701  lgsneg  15703  lgsdilem  15706  lgsdir2lem1  15707  ex-gcd  16095  trilpolemclim  16404  trilpolemcl  16405  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  trirec0  16412  apdiff  16416  redc0  16425  reap0  16426  dceqnconst  16428  dcapnconst  16429  nconstwlpolemgt0  16432  neap0mkv  16437