Theorem 0re 7957

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 7956	. 2 |- 1 e. RR
2		ax-rnegex 7920	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 7937	. . . . 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 2240	. . . 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 2588	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1353   e. wcel 2148   E.wrex 2456  (class class class)co 5875   RRcr 7810   0cc0 7811   1c1 7812   + caddc 7814

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7905  ax-addrcl 7908  ax-rnegex 7920

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-cleq 2170  df-clel 2173  df-ral 2460  df-rex 2461

This theorem is referenced by:  0red  7958  0xr  8004  axmulgt0  8029  gtso  8036  0lt1  8084  ine0  8351  ltaddneg  8381  addgt0  8405  addgegt0  8406  addgtge0  8407  addge0  8408  ltaddpos  8409  ltneg  8419  leneg  8422  lt0neg1  8425  lt0neg2  8426  le0neg1  8427  le0neg2  8428  addge01  8429  suble0  8433  0le1  8438  gt0ne0i  8443  gt0ne0d  8469  lt0ne0d  8470  recexre  8535  recexgt0  8537  inelr  8541  rimul  8542  1ap0  8547  reapmul1  8552  apsqgt0  8558  msqge0  8573  mulge0  8576  recexaplem2  8609  recexap  8610  rerecclap  8687  ltm1  8803  recgt0  8807  ltmul12a  8817  lemul12a  8819  mulgt1  8820  gt0div  8827  ge0div  8828  recgt1i  8855  recreclt  8857  sup3exmid  8914  crap0  8915  nnge1  8942  nngt0  8944  nnrecgt0  8957  0ne1  8986  0le0  9008  neg1lt0  9027  halfge0  9135  iap0  9142  nn0ssre  9180  nn0ge0  9201  nn0nlt0  9202  nn0le0eq0  9204  0mnnnnn0  9208  elnnnn0b  9220  elnnnn0c  9221  elnnz  9263  0z  9264  elnnz1  9276  nn0lt10b  9333  recnz  9346  gtndiv  9348  fnn0ind  9369  rpge0  9666  rpnegap  9686  0nrp  9689  0ltpnf  9782  mnflt0  9784  xneg0  9831  xaddid1  9862  xnn0xadd0  9867  xposdif  9882  elrege0  9976  0e0icopnf  9979  0elunit  9986  1elunit  9987  divelunit  10002  lincmb01cmp  10003  iccf1o  10004  unitssre  10005  fz0to4untppr  10124  modqelico  10334  modqmuladdim  10367  addmodid  10372  expubnd  10577  le2sq2  10596  bernneq2  10642  expnbnd  10644  expnlbnd  10645  faclbnd  10721  faclbnd3  10723  faclbnd6  10724  bcval4  10732  bcpasc  10746  reim0  10870  re0  10904  im0  10905  rei  10908  imi  10909  cj0  10910  caucvgre  10990  rennim  11011  sqrt0rlem  11012  sqrt0  11013  resqrexlemdecn  11021  resqrexlemnm  11027  resqrexlemgt0  11029  sqrt00  11049  sqrt9  11057  sqrt2gt1lt2  11058  leabs  11083  ltabs  11096  sqrtpclii  11139  max0addsup  11228  fimaxre2  11235  climge0  11333  iserge0  11351  fsum00  11470  arisum2  11507  0.999...  11529  fprodge0  11645  cos0  11738  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  cos2bnd  11768  sin01gt0  11769  cos01gt0  11770  sincos2sgn  11773  sin4lt0  11774  absef  11777  absefib  11778  efieq1re  11779  epos  11788  flodddiv4  11939  gcdn0gt0  11979  nn0seqcvgd  12041  algcvgblem  12049  algcvga  12051  pythagtriplem12  12275  pythagtriplem13  12276  pythagtriplem14  12277  pythagtriplem16  12279  mulgnegnn  12993  ssblps  13928  ssbl  13929  xmeter  13939  cnbl0  14037  reeff1olem  14195  pilem3  14207  pipos  14212  sinhalfpilem  14215  sincosq1sgn  14250  sincosq2sgn  14251  sinq34lt0t  14255  coseq0q4123  14258  coseq00topi  14259  coseq0negpitopi  14260  tangtx  14262  sincos4thpi  14264  sincos6thpi  14266  cosordlem  14273  cosq34lt1  14274  cos02pilt1  14275  cos0pilt1  14276  cos11  14277  ioocosf1o  14278  log1  14290  logrpap0b  14300  logdivlti  14305  rpabscxpbnd  14362  lgsval2lem  14414  lgsval4a  14426  lgsneg  14428  lgsdilem  14431  lgsdir2lem1  14432  ex-gcd  14486  trilpolemclim  14787  trilpolemcl  14788  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  trirec0  14795  apdiff  14799  redc0  14808  reap0  14809  dceqnconst  14810  dcapnconst  14811  nconstwlpolemgt0  14814  neap0mkv  14819