Theorem 0re 8316

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 8315	. 2 |- 1 e. RR
2		ax-rnegex 8278	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 8295	. . . . 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

Syntax hints:   = wceq 1402   e. wcel 2209   E.wrex 2529  (class class class)co 6075   RRcr 8168   0cc0 8169   1c1 8170   + caddc 8172

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 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 8263  ax-addrcl 8266  ax-rnegex 8278

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

This theorem is referenced by:  0red  8317  0xr  8362  axmulgt0  8387  gtso  8394  0lt1  8443  ine0  8711  ltaddneg  8742  addgt0  8766  addgegt0  8767  addgtge0  8768  addge0  8769  ltaddpos  8770  ltneg  8780  leneg  8783  lt0neg1  8786  lt0neg2  8787  le0neg1  8788  le0neg2  8789  addge01  8790  suble0  8794  0le1  8799  gt0ne0i  8804  gt0ne0d  8830  lt0ne0d  8831  recexre  8896  recexgt0  8898  inelr  8902  rimul  8903  1ap0  8908  reapmul1  8913  apsqgt0  8919  msqge0  8934  mulge0  8937  recexaplem2  8970  recexap  8971  rerecclap  9050  ltm1  9166  recgt0  9170  ltmul12a  9180  lemul12a  9182  mulgt1  9183  gt0div  9190  ge0div  9191  recgt1i  9218  recreclt  9220  sup3exmid  9277  crap0  9278  nnge1  9306  nngt0  9308  nnrecgt0  9321  0ne1  9350  0le0  9372  neg1lt0  9391  halfge0  9500  iap0  9507  nn0ssre  9546  nn0ge0  9567  nn0nlt0  9568  nn0le0eq0  9570  0mnnnnn0  9574  elnnnn0b  9586  elnnnn0c  9587  elnnz  9633  0z  9634  elnnz1  9646  nn0lt10b  9705  recnz  9718  gtndiv  9720  fnn0ind  9741  rpge0  10046  rpnegap  10066  0nrp  10069  0ltpnf  10163  mnflt0  10165  xneg0  10212  xaddid1  10243  xnn0xadd0  10248  xposdif  10263  elrege0  10357  0e0icopnf  10360  0elunit  10367  1elunit  10368  divelunit  10383  lincmb01cmp  10384  lincmble  10385  iccf1o  10386  unitssre  10387  fz0to4untppr  10509  nn0p1elfzo  10572  modqelico  10749  modqmuladdim  10782  addmodid  10787  xnn0nnen  10852  expubnd  11011  le2sq2  11030  resq01  11073  bernneq2  11077  expnbnd  11079  expnlbnd  11080  faclbnd  11157  faclbnd3  11159  faclbnd6  11160  bcval4  11168  bcpasc  11182  lsw0  11330  swrdccatin2  11479  pfxccatin12lem3  11482  reim0  11604  re0  11639  im0  11640  rei  11643  imi  11644  cj0  11645  caucvgre  11725  rennim  11746  sqrt0rlem  11747  sqrt0  11748  resqrexlemdecn  11756  resqrexlemnm  11762  resqrexlemgt0  11764  sqrt00  11784  sqrt9  11792  sqrt2gt1lt2  11793  leabs  11818  ltabs  11831  sqrtpclii  11874  max0addsup  11963  fimaxre2  11971  climge0  12069  iserge0  12087  fsum00  12207  arisum2  12244  0.999...  12266  fprodge0  12382  cos0  12475  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  cos2bnd  12505  sin01gt0  12507  cos01gt0  12508  sincos2sgn  12511  sin4lt0  12512  absef  12515  absefib  12516  efieq1re  12517  epos  12526  flodddiv4  12681  gcdn0gt0  12733  nn0seqcvgd  12797  algcvgblem  12805  algcvga  12807  pythagtriplem12  13032  pythagtriplem13  13033  pythagtriplem14  13034  pythagtriplem16  13036  ballotfilem2  13206  ballotfilem4  13219  ballotfilemi1  13223  ballotfilemic  13228  mulgnegnn  13912  ssblps  15449  ssbl  15450  xmeter  15460  cnbl0  15558  hovera  15671  hovergt0  15674  plyrecj  15787  reeff1olem  15795  pilem3  15807  pipos  15812  sinhalfpilem  15815  sincosq1sgn  15850  sincosq2sgn  15851  sinq34lt0t  15855  coseq0q4123  15858  coseq00topi  15859  coseq0negpitopi  15860  tangtx  15862  sincos4thpi  15864  sincos6thpi  15866  cosordlem  15873  cosq34lt1  15874  cos02pilt1  15875  cos0pilt1  15876  cos11  15877  ioocosf1o  15878  log1  15890  logrpap0b  15900  logdivlti  15905  rpabscxpbnd  15965  lgsval2lem  16043  lgsval4a  16055  lgsneg  16057  lgsdilem  16060  lgsdir2lem1  16061  clwwlkn0  16563  konigsberg  16648  ex-gcd  16659  repiecelem  16979  repiecele0  16980  repiecege0  16981  trilpolemclim  16990  trilpolemcl  16991  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  trirec0  16998  apdiff  17002  redc0  17012  reap0  17013  dceqnconst  17015  dcapnconst  17016  nconstwlpolemgt0  17019  neap0mkv  17024