Theorem 0re 8327

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

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209   E.wrex 2529  (class class class)co 6085   RRcr 8179   0cc0 8180   1c1 8181   + caddc 8183

This proof depends on 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 8274  ax-addrcl 8277  ax-rnegex 8289

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

This theorem is used by:  0red  8328  0xr  8373  axmulgt0  8398  gtso  8405  0lt1  8455  ine0  8723  ltaddneg  8754  addgt0  8778  addgegt0  8779  addgtge0  8780  addge0  8781  ltaddpos  8782  ltneg  8792  leneg  8795  lt0neg1  8798  lt0neg2  8799  le0neg1  8800  le0neg2  8801  addge01  8802  suble0  8806  0le1  8811  gt0ne0i  8816  gt0ne0d  8842  lt0ne0d  8843  recexre  8909  recexgt0  8911  inelr  8915  rimul  8916  1ap0  8921  reapmul1  8926  apsqgt0  8932  msqge0  8947  mulge0  8950  recexaplem2  8983  recexap  8984  rerecclap  9063  ltm1  9179  recgt0  9183  ltmul12a  9193  lemul12a  9195  mulgt1  9196  gt0div  9203  ge0div  9204  recgt1i  9231  recreclt  9233  sup3exmid  9290  crap0  9291  indfval  9302  indconst0  9305  nnge1  9330  nngt0  9332  nnrecgt0  9345  0ne1  9374  0le0  9396  neg1lt0  9415  halfge0  9526  iap0  9533  nn0ssre  9572  nn0ge0  9593  nn0nlt0  9594  nn0le0eq0  9596  0mnnnnn0  9600  elnnnn0b  9612  elnnnn0c  9613  elnnz  9659  0z  9660  elnnz1  9672  nn0lt10b  9731  recnz  9744  gtndiv  9746  fnn0ind  9767  rpge0  10078  rpnegap  10098  0nrp  10101  0ltpnf  10195  mnflt0  10197  xneg0  10244  xaddid1  10275  xnn0xadd0  10280  xposdif  10295  elrege0  10389  0e0icopnf  10392  0elunit  10399  1elunit  10400  divelunit  10415  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  unitssre  10419  fz0to4untppr  10542  nn0p1elfzo  10605  modqelico  10786  modqmuladdim  10819  addmodid  10824  xnn0nnen  10889  expubnd  11048  le2sq2  11067  resq01  11110  bernneq2  11114  expnbnd  11116  expnlbnd  11117  faclbnd  11195  faclbnd3  11197  faclbnd6  11198  bcval4  11206  bcpasc  11220  lsw0  11368  swrdccatin2  11517  pfxccatin12lem3  11520  reim0  11642  re0  11677  im0  11678  rei  11681  imi  11682  cj0  11683  caucvgre  11763  rennim  11784  sqrt0rlem  11785  sqrt0  11786  resqrexlemdecn  11794  resqrexlemnm  11800  resqrexlemgt0  11802  sqrt00  11822  sqrt9  11830  sqrt2gt1lt2  11831  leabs  11856  ltabs  11870  sqrtpclii  11913  max0addsup  12002  fimaxre2  12010  climge0  12110  iserge0  12128  fsum00  12248  arisum2  12285  0.999...  12307  fprodge0  12423  cos0  12516  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  cos2bnd  12546  sin01gt0  12548  cos01gt0  12549  sincos2sgn  12552  sin4lt0  12553  absef  12556  absefib  12557  efieq1re  12558  epos  12567  flodddiv4  12722  gcdn0gt0  12774  nn0seqcvgd  12838  algcvgblem  12846  algcvga  12848  pythagtriplem12  13077  pythagtriplem13  13078  pythagtriplem14  13079  pythagtriplem16  13081  ballotfilem2  13280  ballotfilem4  13293  ballotfilemi1  13297  ballotfilemic  13302  mulgnegnn  13988  ssblps  15617  ssbl  15618  xmeter  15628  cnbl0  15726  hovera  15839  hovergt0  15842  plyrecj  15955  reeff1olem  15963  efap1p  15971  pilem3  15976  pipos  15981  sinhalfpilem  15984  sincosq1sgn  16019  sincosq2sgn  16020  sinq34lt0t  16024  coseq0q4123  16027  coseq00topi  16028  coseq0negpitopi  16029  tangtx  16031  sincos4thpi  16033  sincos6thpi  16035  cosordlem  16042  cosq34lt1  16043  cos02pilt1  16044  cos0pilt1  16045  cos11  16046  ioocosf1o  16047  log1  16059  logrpap0b  16070  logdivlti  16075  rpabscxpbnd  16137  log2tlbndlog2  16181  log2ublog2  16185  efnnfsumcl  16200  ppiqsval  16201  efchtqdvds  16226  ppiqub  16254  chtqleppi  16255  bposlem4  16275  bposlem5  16276  bposlem7  16278  bposlem8  16279  bposlem9  16280  lgsval2lem  16295  lgsval4a  16307  lgsneg  16309  lgsdilem  16312  lgsdir2lem1  16313  clwwlkn0  16815  konigsberg  16900  ex-gcd  16911  repiecelem  17240  repiecele0  17241  repiecege0  17242  trilpolemclim  17252  trilpolemcl  17253  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  trirec0  17260  apdiff  17264  redc0  17274  reap0  17275  dceqnconst  17277  dcapnconst  17278  nconstwlpolemgt0  17281  neap0mkv  17286