Theorem 0re 8072

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 8071	. 2 |- 1 e. RR
2		ax-rnegex 8034	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 8051	. . . . 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 2268	. . . 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 2617	. 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 2176   E.wrex 2485  (class class class)co 5944   RRcr 7924   0cc0 7925   1c1 7926   + caddc 7928

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-1re 8019  ax-addrcl 8022  ax-rnegex 8034

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-cleq 2198  df-clel 2201  df-ral 2489  df-rex 2490

This theorem is referenced by:  0red  8073  0xr  8119  axmulgt0  8144  gtso  8151  0lt1  8199  ine0  8466  ltaddneg  8497  addgt0  8521  addgegt0  8522  addgtge0  8523  addge0  8524  ltaddpos  8525  ltneg  8535  leneg  8538  lt0neg1  8541  lt0neg2  8542  le0neg1  8543  le0neg2  8544  addge01  8545  suble0  8549  0le1  8554  gt0ne0i  8559  gt0ne0d  8585  lt0ne0d  8586  recexre  8651  recexgt0  8653  inelr  8657  rimul  8658  1ap0  8663  reapmul1  8668  apsqgt0  8674  msqge0  8689  mulge0  8692  recexaplem2  8725  recexap  8726  rerecclap  8803  ltm1  8919  recgt0  8923  ltmul12a  8933  lemul12a  8935  mulgt1  8936  gt0div  8943  ge0div  8944  recgt1i  8971  recreclt  8973  sup3exmid  9030  crap0  9031  nnge1  9059  nngt0  9061  nnrecgt0  9074  0ne1  9103  0le0  9125  neg1lt0  9144  halfge0  9253  iap0  9260  nn0ssre  9299  nn0ge0  9320  nn0nlt0  9321  nn0le0eq0  9323  0mnnnnn0  9327  elnnnn0b  9339  elnnnn0c  9340  elnnz  9382  0z  9383  elnnz1  9395  nn0lt10b  9453  recnz  9466  gtndiv  9468  fnn0ind  9489  rpge0  9788  rpnegap  9808  0nrp  9811  0ltpnf  9904  mnflt0  9906  xneg0  9953  xaddid1  9984  xnn0xadd0  9989  xposdif  10004  elrege0  10098  0e0icopnf  10101  0elunit  10108  1elunit  10109  divelunit  10124  lincmb01cmp  10125  iccf1o  10126  unitssre  10127  fz0to4untppr  10246  modqelico  10479  modqmuladdim  10512  addmodid  10517  xnn0nnen  10582  expubnd  10741  le2sq2  10760  bernneq2  10806  expnbnd  10808  expnlbnd  10809  faclbnd  10886  faclbnd3  10888  faclbnd6  10889  bcval4  10897  bcpasc  10911  lsw0  11041  reim0  11172  re0  11206  im0  11207  rei  11210  imi  11211  cj0  11212  caucvgre  11292  rennim  11313  sqrt0rlem  11314  sqrt0  11315  resqrexlemdecn  11323  resqrexlemnm  11329  resqrexlemgt0  11331  sqrt00  11351  sqrt9  11359  sqrt2gt1lt2  11360  leabs  11385  ltabs  11398  sqrtpclii  11441  max0addsup  11530  fimaxre2  11538  climge0  11636  iserge0  11654  fsum00  11773  arisum2  11810  0.999...  11832  fprodge0  11948  cos0  12041  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  cos2bnd  12071  sin01gt0  12073  cos01gt0  12074  sincos2sgn  12077  sin4lt0  12078  absef  12081  absefib  12082  efieq1re  12083  epos  12092  flodddiv4  12247  gcdn0gt0  12299  nn0seqcvgd  12363  algcvgblem  12371  algcvga  12373  pythagtriplem12  12598  pythagtriplem13  12599  pythagtriplem14  12600  pythagtriplem16  12602  mulgnegnn  13468  ssblps  14897  ssbl  14898  xmeter  14908  cnbl0  15006  hovera  15119  hovergt0  15122  plyrecj  15235  reeff1olem  15243  pilem3  15255  pipos  15260  sinhalfpilem  15263  sincosq1sgn  15298  sincosq2sgn  15299  sinq34lt0t  15303  coseq0q4123  15306  coseq00topi  15307  coseq0negpitopi  15308  tangtx  15310  sincos4thpi  15312  sincos6thpi  15314  cosordlem  15321  cosq34lt1  15322  cos02pilt1  15323  cos0pilt1  15324  cos11  15325  ioocosf1o  15326  log1  15338  logrpap0b  15348  logdivlti  15353  rpabscxpbnd  15412  lgsval2lem  15487  lgsval4a  15499  lgsneg  15501  lgsdilem  15504  lgsdir2lem1  15505  ex-gcd  15671  trilpolemclim  15979  trilpolemcl  15980  trilpolemisumle  15981  trilpolemeq1  15983  trilpolemlt1  15984  trirec0  15987  apdiff  15991  redc0  16000  reap0  16001  dceqnconst  16003  dcapnconst  16004  nconstwlpolemgt0  16007  neap0mkv  16012