Theorem 0re 8026

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 8025	. 2 |- 1 e. RR
2		ax-rnegex 7988	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 8005	. . . . 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 2259	. . . 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 2608	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1364   e. wcel 2167   E.wrex 2476  (class class class)co 5922   RRcr 7878   0cc0 7879   1c1 7880   + caddc 7882

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7973  ax-addrcl 7976  ax-rnegex 7988

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-cleq 2189  df-clel 2192  df-ral 2480  df-rex 2481

This theorem is referenced by:  0red  8027  0xr  8073  axmulgt0  8098  gtso  8105  0lt1  8153  ine0  8420  ltaddneg  8451  addgt0  8475  addgegt0  8476  addgtge0  8477  addge0  8478  ltaddpos  8479  ltneg  8489  leneg  8492  lt0neg1  8495  lt0neg2  8496  le0neg1  8497  le0neg2  8498  addge01  8499  suble0  8503  0le1  8508  gt0ne0i  8513  gt0ne0d  8539  lt0ne0d  8540  recexre  8605  recexgt0  8607  inelr  8611  rimul  8612  1ap0  8617  reapmul1  8622  apsqgt0  8628  msqge0  8643  mulge0  8646  recexaplem2  8679  recexap  8680  rerecclap  8757  ltm1  8873  recgt0  8877  ltmul12a  8887  lemul12a  8889  mulgt1  8890  gt0div  8897  ge0div  8898  recgt1i  8925  recreclt  8927  sup3exmid  8984  crap0  8985  nnge1  9013  nngt0  9015  nnrecgt0  9028  0ne1  9057  0le0  9079  neg1lt0  9098  halfge0  9207  iap0  9214  nn0ssre  9253  nn0ge0  9274  nn0nlt0  9275  nn0le0eq0  9277  0mnnnnn0  9281  elnnnn0b  9293  elnnnn0c  9294  elnnz  9336  0z  9337  elnnz1  9349  nn0lt10b  9406  recnz  9419  gtndiv  9421  fnn0ind  9442  rpge0  9741  rpnegap  9761  0nrp  9764  0ltpnf  9857  mnflt0  9859  xneg0  9906  xaddid1  9937  xnn0xadd0  9942  xposdif  9957  elrege0  10051  0e0icopnf  10054  0elunit  10061  1elunit  10062  divelunit  10077  lincmb01cmp  10078  iccf1o  10079  unitssre  10080  fz0to4untppr  10199  modqelico  10426  modqmuladdim  10459  addmodid  10464  xnn0nnen  10529  expubnd  10688  le2sq2  10707  bernneq2  10753  expnbnd  10755  expnlbnd  10756  faclbnd  10833  faclbnd3  10835  faclbnd6  10836  bcval4  10844  bcpasc  10858  reim0  11026  re0  11060  im0  11061  rei  11064  imi  11065  cj0  11066  caucvgre  11146  rennim  11167  sqrt0rlem  11168  sqrt0  11169  resqrexlemdecn  11177  resqrexlemnm  11183  resqrexlemgt0  11185  sqrt00  11205  sqrt9  11213  sqrt2gt1lt2  11214  leabs  11239  ltabs  11252  sqrtpclii  11295  max0addsup  11384  fimaxre2  11392  climge0  11490  iserge0  11508  fsum00  11627  arisum2  11664  0.999...  11686  fprodge0  11802  cos0  11895  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  cos2bnd  11925  sin01gt0  11927  cos01gt0  11928  sincos2sgn  11931  sin4lt0  11932  absef  11935  absefib  11936  efieq1re  11937  epos  11946  flodddiv4  12101  gcdn0gt0  12145  nn0seqcvgd  12209  algcvgblem  12217  algcvga  12219  pythagtriplem12  12444  pythagtriplem13  12445  pythagtriplem14  12446  pythagtriplem16  12448  mulgnegnn  13262  ssblps  14661  ssbl  14662  xmeter  14672  cnbl0  14770  hovera  14883  hovergt0  14886  plyrecj  14999  reeff1olem  15007  pilem3  15019  pipos  15024  sinhalfpilem  15027  sincosq1sgn  15062  sincosq2sgn  15063  sinq34lt0t  15067  coseq0q4123  15070  coseq00topi  15071  coseq0negpitopi  15072  tangtx  15074  sincos4thpi  15076  sincos6thpi  15078  cosordlem  15085  cosq34lt1  15086  cos02pilt1  15087  cos0pilt1  15088  cos11  15089  ioocosf1o  15090  log1  15102  logrpap0b  15112  logdivlti  15117  rpabscxpbnd  15176  lgsval2lem  15251  lgsval4a  15263  lgsneg  15265  lgsdilem  15268  lgsdir2lem1  15269  ex-gcd  15377  trilpolemclim  15680  trilpolemcl  15681  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  trirec0  15688  apdiff  15692  redc0  15701  reap0  15702  dceqnconst  15704  dcapnconst  15705  nconstwlpolemgt0  15708  neap0mkv  15713