Theorem 0re 7956

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 7955	. 2 |- 1 e. RR
2		ax-rnegex 7919	. 2 |- ( 1 e. RR -> E. x e. RR ( 1 + x ) = 0 )
3		readdcl 7936	. . . . 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 2240	. . . 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 2588	. 2 |- ( E. x e. RR ( 1 + x ) = 0 -> 0 e. RR )
8	1, 2, 7	mp2b 8	1 |- 0 e. RR

Syntax hints:   = wceq 1353   e. wcel 2148   E.wrex 2456  (class class class)co 5874   RRcr 7809   0cc0 7810   1c1 7811   + caddc 7813

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7904  ax-addrcl 7907  ax-rnegex 7919

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-cleq 2170  df-clel 2173  df-ral 2460  df-rex 2461

This theorem is referenced by:  0red  7957  0xr  8002  axmulgt0  8027  gtso  8034  0lt1  8082  ine0  8349  ltaddneg  8379  addgt0  8403  addgegt0  8404  addgtge0  8405  addge0  8406  ltaddpos  8407  ltneg  8417  leneg  8420  lt0neg1  8423  lt0neg2  8424  le0neg1  8425  le0neg2  8426  addge01  8427  suble0  8431  0le1  8436  gt0ne0i  8441  gt0ne0d  8467  lt0ne0d  8468  recexre  8533  recexgt0  8535  inelr  8539  rimul  8540  1ap0  8545  reapmul1  8550  apsqgt0  8556  msqge0  8571  mulge0  8574  recexaplem2  8607  recexap  8608  rerecclap  8685  ltm1  8801  recgt0  8805  ltmul12a  8815  lemul12a  8817  mulgt1  8818  gt0div  8825  ge0div  8826  recgt1i  8853  recreclt  8855  sup3exmid  8912  crap0  8913  nnge1  8940  nngt0  8942  nnrecgt0  8955  0ne1  8984  0le0  9006  neg1lt0  9025  halfge0  9133  iap0  9140  nn0ssre  9178  nn0ge0  9199  nn0nlt0  9200  nn0le0eq0  9202  0mnnnnn0  9206  elnnnn0b  9218  elnnnn0c  9219  elnnz  9261  0z  9262  elnnz1  9274  nn0lt10b  9331  recnz  9344  gtndiv  9346  fnn0ind  9367  rpge0  9664  rpnegap  9684  0nrp  9687  0ltpnf  9780  mnflt0  9782  xneg0  9829  xaddid1  9860  xnn0xadd0  9865  xposdif  9880  elrege0  9974  0e0icopnf  9977  0elunit  9984  1elunit  9985  divelunit  10000  lincmb01cmp  10001  iccf1o  10002  unitssre  10003  fz0to4untppr  10121  modqelico  10331  modqmuladdim  10364  addmodid  10369  expubnd  10574  le2sq2  10592  bernneq2  10638  expnbnd  10640  expnlbnd  10641  faclbnd  10716  faclbnd3  10718  faclbnd6  10719  bcval4  10727  bcpasc  10741  reim0  10865  re0  10899  im0  10900  rei  10903  imi  10904  cj0  10905  caucvgre  10985  rennim  11006  sqrt0rlem  11007  sqrt0  11008  resqrexlemdecn  11016  resqrexlemnm  11022  resqrexlemgt0  11024  sqrt00  11044  sqrt9  11052  sqrt2gt1lt2  11053  leabs  11078  ltabs  11091  sqrtpclii  11134  max0addsup  11223  fimaxre2  11230  climge0  11328  iserge0  11346  fsum00  11465  arisum2  11502  0.999...  11524  fprodge0  11640  cos0  11733  ef01bndlem  11759  sin01bnd  11760  cos01bnd  11761  cos2bnd  11763  sin01gt0  11764  cos01gt0  11765  sincos2sgn  11768  sin4lt0  11769  absef  11772  absefib  11773  efieq1re  11774  epos  11783  flodddiv4  11933  gcdn0gt0  11973  nn0seqcvgd  12035  algcvgblem  12043  algcvga  12045  pythagtriplem12  12269  pythagtriplem13  12270  pythagtriplem14  12271  pythagtriplem16  12273  mulgnegnn  12987  ssblps  13856  ssbl  13857  xmeter  13867  cnbl0  13965  reeff1olem  14123  pilem3  14135  pipos  14140  sinhalfpilem  14143  sincosq1sgn  14178  sincosq2sgn  14179  sinq34lt0t  14183  coseq0q4123  14186  coseq00topi  14187  coseq0negpitopi  14188  tangtx  14190  sincos4thpi  14192  sincos6thpi  14194  cosordlem  14201  cosq34lt1  14202  cos02pilt1  14203  cos0pilt1  14204  cos11  14205  ioocosf1o  14206  log1  14218  logrpap0b  14228  logdivlti  14233  rpabscxpbnd  14290  lgsval2lem  14342  lgsval4a  14354  lgsneg  14356  lgsdilem  14359  lgsdir2lem1  14360  ex-gcd  14403  trilpolemclim  14704  trilpolemcl  14705  trilpolemisumle  14706  trilpolemeq1  14708  trilpolemlt1  14709  trirec0  14712  apdiff  14716  redc0  14725  reap0  14726  dceqnconst  14727  dcapnconst  14728  nconstwlpolemgt0  14731  neap0mkv  14736