Theorem 0re 7181

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 7180	. 2 |- 1 e. RR
2		ax-rnegex 7147	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 7161	. . . . 5 |- ( ( 1 e. RR /\ x e. RR ) -> ( 1 + x ) e. RR )
4	1, 3	mpan 415	. . . 4 |- ( x e. RR -> ( 1 + x ) e. RR )
5		eleq1 2142	. . . 4 |- ( ( 1 + x ) = 0 -> ( ( 1 + x ) e. RR <-> 0 e. RR ) )
6	4, 5	syl5ibcom 153	. . 3 |- ( x e. RR -> ( ( 1 + x ) = 0 -> 0 e. RR ) )
7	6	rexlimiv 2472	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1285   e. wcel 1434   E.wrex 2350  (class class class)co 5543   RRcr 7042   0cc0 7043   1c1 7044   + caddc 7046

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-1re 7132  ax-addrcl 7135  ax-rnegex 7147

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-cleq 2075  df-clel 2078  df-ral 2354  df-rex 2355

This theorem is referenced by:  0red  7182  0xr  7227  axmulgt0  7251  gtso  7257  0lt1  7303  ine0  7565  ltaddneg  7595  addgt0  7619  addgegt0  7620  addgtge0  7621  addge0  7622  ltaddpos  7623  ltneg  7633  leneg  7636  lt0neg1  7639  lt0neg2  7640  le0neg1  7641  le0neg2  7642  addge01  7643  suble0  7647  0le1  7652  gt0ne0i  7654  gt0ne0d  7680  lt0ne0d  7681  recexre  7745  recexgt0  7747  inelr  7751  rimul  7752  1ap0  7757  reapmul1  7762  apsqgt0  7768  msqge0  7783  mulge0  7786  recexaplem2  7809  recexap  7810  rerecclap  7885  ltm1  7991  recgt0  7995  ltmul12a  8005  lemul12a  8007  mulgt1  8008  gt0div  8015  ge0div  8016  recgt1i  8043  recreclt  8045  crap0  8102  nnge1  8129  nngt0  8131  nnrecgt0  8143  0ne1  8173  0le0  8195  neg1lt0  8214  halfge0  8314  iap0  8321  nn0ssre  8359  nn0ge0  8380  nn0nlt0  8381  nn0le0eq0  8383  0mnnnnn0  8387  elnnnn0b  8399  elnnnn0c  8400  elnnz  8442  0z  8443  elnnz1  8455  nn0lt10b  8509  recnz  8521  gtndiv  8523  fnn0ind  8544  rpge0  8827  rpnegap  8847  0nrp  8848  0ltpnf  8933  mnflt0  8935  xneg0  8974  elrege0  9075  0e0icopnf  9078  0elunit  9084  1elunit  9085  divelunit  9100  lincmb01cmp  9101  iccf1o  9102  unitssre  9103  modqelico  9416  modqmuladdim  9449  addmodid  9454  expubnd  9630  le2sq2  9648  bernneq2  9691  expnbnd  9693  expnlbnd  9694  faclbnd  9765  faclbnd3  9767  faclbnd6  9768  bcval4  9776  bcpasc  9790  reim0  9886  re0  9920  im0  9921  rei  9924  imi  9925  cj0  9926  caucvgre  10005  rennim  10026  sqrt0rlem  10027  sqrt0  10028  resqrexlemdecn  10036  resqrexlemnm  10042  resqrexlemgt0  10044  sqrt00  10064  sqrt9  10072  sqrt2gt1lt2  10073  leabs  10098  ltabs  10111  sqrtpclii  10154  max0addsup  10243  fimaxre2  10247  climge0  10301  iserige0  10319  flodddiv4  10478  gcdn0gt0  10513  nn0seqcvgd  10567  algcvgblem  10575  ialgcvga  10577  ex-gcd  10719