Theorem 0re 8157

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 8156	. 2 |- 1 e. RR
2		ax-rnegex 8119	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 8136	. . . . 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 2292	. . . 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 2642	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1395   e. wcel 2200   E.wrex 2509  (class class class)co 6007   RRcr 8009   0cc0 8010   1c1 8011   + caddc 8013

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8104  ax-addrcl 8107  ax-rnegex 8119

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-ral 2513  df-rex 2514

This theorem is referenced by:  0red  8158  0xr  8204  axmulgt0  8229  gtso  8236  0lt1  8284  ine0  8551  ltaddneg  8582  addgt0  8606  addgegt0  8607  addgtge0  8608  addge0  8609  ltaddpos  8610  ltneg  8620  leneg  8623  lt0neg1  8626  lt0neg2  8627  le0neg1  8628  le0neg2  8629  addge01  8630  suble0  8634  0le1  8639  gt0ne0i  8644  gt0ne0d  8670  lt0ne0d  8671  recexre  8736  recexgt0  8738  inelr  8742  rimul  8743  1ap0  8748  reapmul1  8753  apsqgt0  8759  msqge0  8774  mulge0  8777  recexaplem2  8810  recexap  8811  rerecclap  8888  ltm1  9004  recgt0  9008  ltmul12a  9018  lemul12a  9020  mulgt1  9021  gt0div  9028  ge0div  9029  recgt1i  9056  recreclt  9058  sup3exmid  9115  crap0  9116  nnge1  9144  nngt0  9146  nnrecgt0  9159  0ne1  9188  0le0  9210  neg1lt0  9229  halfge0  9338  iap0  9345  nn0ssre  9384  nn0ge0  9405  nn0nlt0  9406  nn0le0eq0  9408  0mnnnnn0  9412  elnnnn0b  9424  elnnnn0c  9425  elnnz  9467  0z  9468  elnnz1  9480  nn0lt10b  9538  recnz  9551  gtndiv  9553  fnn0ind  9574  rpge0  9874  rpnegap  9894  0nrp  9897  0ltpnf  9990  mnflt0  9992  xneg0  10039  xaddid1  10070  xnn0xadd0  10075  xposdif  10090  elrege0  10184  0e0icopnf  10187  0elunit  10194  1elunit  10195  divelunit  10210  lincmb01cmp  10211  iccf1o  10212  unitssre  10213  fz0to4untppr  10332  modqelico  10568  modqmuladdim  10601  addmodid  10606  xnn0nnen  10671  expubnd  10830  le2sq2  10849  bernneq2  10895  expnbnd  10897  expnlbnd  10898  faclbnd  10975  faclbnd3  10977  faclbnd6  10978  bcval4  10986  bcpasc  11000  lsw0  11132  swrdccatin2  11277  pfxccatin12lem3  11280  reim0  11388  re0  11422  im0  11423  rei  11426  imi  11427  cj0  11428  caucvgre  11508  rennim  11529  sqrt0rlem  11530  sqrt0  11531  resqrexlemdecn  11539  resqrexlemnm  11545  resqrexlemgt0  11547  sqrt00  11567  sqrt9  11575  sqrt2gt1lt2  11576  leabs  11601  ltabs  11614  sqrtpclii  11657  max0addsup  11746  fimaxre2  11754  climge0  11852  iserge0  11870  fsum00  11989  arisum2  12026  0.999...  12048  fprodge0  12164  cos0  12257  ef01bndlem  12283  sin01bnd  12284  cos01bnd  12285  cos2bnd  12287  sin01gt0  12289  cos01gt0  12290  sincos2sgn  12293  sin4lt0  12294  absef  12297  absefib  12298  efieq1re  12299  epos  12308  flodddiv4  12463  gcdn0gt0  12515  nn0seqcvgd  12579  algcvgblem  12587  algcvga  12589  pythagtriplem12  12814  pythagtriplem13  12815  pythagtriplem14  12816  pythagtriplem16  12818  mulgnegnn  13685  ssblps  15115  ssbl  15116  xmeter  15126  cnbl0  15224  hovera  15337  hovergt0  15340  plyrecj  15453  reeff1olem  15461  pilem3  15473  pipos  15478  sinhalfpilem  15481  sincosq1sgn  15516  sincosq2sgn  15517  sinq34lt0t  15521  coseq0q4123  15524  coseq00topi  15525  coseq0negpitopi  15526  tangtx  15528  sincos4thpi  15530  sincos6thpi  15532  cosordlem  15539  cosq34lt1  15540  cos02pilt1  15541  cos0pilt1  15542  cos11  15543  ioocosf1o  15544  log1  15556  logrpap0b  15566  logdivlti  15571  rpabscxpbnd  15630  lgsval2lem  15705  lgsval4a  15717  lgsneg  15719  lgsdilem  15722  lgsdir2lem1  15723  clwwlkn0  16151  ex-gcd  16178  trilpolemclim  16492  trilpolemcl  16493  trilpolemisumle  16494  trilpolemeq1  16496  trilpolemlt1  16497  trirec0  16500  apdiff  16504  redc0  16513  reap0  16514  dceqnconst  16516  dcapnconst  16517  nconstwlpolemgt0  16520  neap0mkv  16525