Theorem 0re 8074

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 8073	. 2 |- 1 e. RR
2		ax-rnegex 8036	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 8053	. . . . 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 2268	. . . 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 2617	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1373   e. wcel 2176   E.wrex 2485  (class class class)co 5946   RRcr 7926   0cc0 7927   1c1 7928   + caddc 7930

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558  ax-ext 2187  ax-1re 8021  ax-addrcl 8024  ax-rnegex 8036

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-cleq 2198  df-clel 2201  df-ral 2489  df-rex 2490

This theorem is referenced by:  0red  8075  0xr  8121  axmulgt0  8146  gtso  8153  0lt1  8201  ine0  8468  ltaddneg  8499  addgt0  8523  addgegt0  8524  addgtge0  8525  addge0  8526  ltaddpos  8527  ltneg  8537  leneg  8540  lt0neg1  8543  lt0neg2  8544  le0neg1  8545  le0neg2  8546  addge01  8547  suble0  8551  0le1  8556  gt0ne0i  8561  gt0ne0d  8587  lt0ne0d  8588  recexre  8653  recexgt0  8655  inelr  8659  rimul  8660  1ap0  8665  reapmul1  8670  apsqgt0  8676  msqge0  8691  mulge0  8694  recexaplem2  8727  recexap  8728  rerecclap  8805  ltm1  8921  recgt0  8925  ltmul12a  8935  lemul12a  8937  mulgt1  8938  gt0div  8945  ge0div  8946  recgt1i  8973  recreclt  8975  sup3exmid  9032  crap0  9033  nnge1  9061  nngt0  9063  nnrecgt0  9076  0ne1  9105  0le0  9127  neg1lt0  9146  halfge0  9255  iap0  9262  nn0ssre  9301  nn0ge0  9322  nn0nlt0  9323  nn0le0eq0  9325  0mnnnnn0  9329  elnnnn0b  9341  elnnnn0c  9342  elnnz  9384  0z  9385  elnnz1  9397  nn0lt10b  9455  recnz  9468  gtndiv  9470  fnn0ind  9491  rpge0  9790  rpnegap  9810  0nrp  9813  0ltpnf  9906  mnflt0  9908  xneg0  9955  xaddid1  9986  xnn0xadd0  9991  xposdif  10006  elrege0  10100  0e0icopnf  10103  0elunit  10110  1elunit  10111  divelunit  10126  lincmb01cmp  10127  iccf1o  10128  unitssre  10129  fz0to4untppr  10248  modqelico  10481  modqmuladdim  10514  addmodid  10519  xnn0nnen  10584  expubnd  10743  le2sq2  10762  bernneq2  10808  expnbnd  10810  expnlbnd  10811  faclbnd  10888  faclbnd3  10890  faclbnd6  10891  bcval4  10899  bcpasc  10913  lsw0  11043  reim0  11205  re0  11239  im0  11240  rei  11243  imi  11244  cj0  11245  caucvgre  11325  rennim  11346  sqrt0rlem  11347  sqrt0  11348  resqrexlemdecn  11356  resqrexlemnm  11362  resqrexlemgt0  11364  sqrt00  11384  sqrt9  11392  sqrt2gt1lt2  11393  leabs  11418  ltabs  11431  sqrtpclii  11474  max0addsup  11563  fimaxre2  11571  climge0  11669  iserge0  11687  fsum00  11806  arisum2  11843  0.999...  11865  fprodge0  11981  cos0  12074  ef01bndlem  12100  sin01bnd  12101  cos01bnd  12102  cos2bnd  12104  sin01gt0  12106  cos01gt0  12107  sincos2sgn  12110  sin4lt0  12111  absef  12114  absefib  12115  efieq1re  12116  epos  12125  flodddiv4  12280  gcdn0gt0  12332  nn0seqcvgd  12396  algcvgblem  12404  algcvga  12406  pythagtriplem12  12631  pythagtriplem13  12632  pythagtriplem14  12633  pythagtriplem16  12635  mulgnegnn  13501  ssblps  14930  ssbl  14931  xmeter  14941  cnbl0  15039  hovera  15152  hovergt0  15155  plyrecj  15268  reeff1olem  15276  pilem3  15288  pipos  15293  sinhalfpilem  15296  sincosq1sgn  15331  sincosq2sgn  15332  sinq34lt0t  15336  coseq0q4123  15339  coseq00topi  15340  coseq0negpitopi  15341  tangtx  15343  sincos4thpi  15345  sincos6thpi  15347  cosordlem  15354  cosq34lt1  15355  cos02pilt1  15356  cos0pilt1  15357  cos11  15358  ioocosf1o  15359  log1  15371  logrpap0b  15381  logdivlti  15386  rpabscxpbnd  15445  lgsval2lem  15520  lgsval4a  15532  lgsneg  15534  lgsdilem  15537  lgsdir2lem1  15538  ex-gcd  15704  trilpolemclim  16012  trilpolemcl  16013  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  trirec0  16020  apdiff  16024  redc0  16033  reap0  16034  dceqnconst  16036  dcapnconst  16037  nconstwlpolemgt0  16040  neap0mkv  16045