Theorem 0re 7974

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 ∈ ℝ

Proof of Theorem 0re

Step	Hyp	Ref	Expression
1		1re 7973	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 7937	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 7954	. . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
4	1, 3	mpan 424	. . . 4 ⊢ (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5		eleq1 2251	. . . 4 ⊢ ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 155	. . 3 ⊢ (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
7	6	rexlimiv 2600	. 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
8	1, 2, 7	mp2b 8	1 ⊢ 0 ∈ ℝ

Syntax hints:   = wceq 1363   ∈ wcel 2159  ∃wrex 2468  (class class class)co 5890  ℝcr 7827  0cc0 7828  1c1 7829   + caddc 7831

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-i5r 1545  ax-ext 2170  ax-1re 7922  ax-addrcl 7925  ax-rnegex 7937

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-cleq 2181  df-clel 2184  df-ral 2472  df-rex 2473

This theorem is referenced by:  0red  7975  0xr  8021  axmulgt0  8046  gtso  8053  0lt1  8101  ine0  8368  ltaddneg  8398  addgt0  8422  addgegt0  8423  addgtge0  8424  addge0  8425  ltaddpos  8426  ltneg  8436  leneg  8439  lt0neg1  8442  lt0neg2  8443  le0neg1  8444  le0neg2  8445  addge01  8446  suble0  8450  0le1  8455  gt0ne0i  8460  gt0ne0d  8486  lt0ne0d  8487  recexre  8552  recexgt0  8554  inelr  8558  rimul  8559  1ap0  8564  reapmul1  8569  apsqgt0  8575  msqge0  8590  mulge0  8593  recexaplem2  8626  recexap  8627  rerecclap  8704  ltm1  8820  recgt0  8824  ltmul12a  8834  lemul12a  8836  mulgt1  8837  gt0div  8844  ge0div  8845  recgt1i  8872  recreclt  8874  sup3exmid  8931  crap0  8932  nnge1  8959  nngt0  8961  nnrecgt0  8974  0ne1  9003  0le0  9025  neg1lt0  9044  halfge0  9152  iap0  9159  nn0ssre  9197  nn0ge0  9218  nn0nlt0  9219  nn0le0eq0  9221  0mnnnnn0  9225  elnnnn0b  9237  elnnnn0c  9238  elnnz  9280  0z  9281  elnnz1  9293  nn0lt10b  9350  recnz  9363  gtndiv  9365  fnn0ind  9386  rpge0  9683  rpnegap  9703  0nrp  9706  0ltpnf  9799  mnflt0  9801  xneg0  9848  xaddid1  9879  xnn0xadd0  9884  xposdif  9899  elrege0  9993  0e0icopnf  9996  0elunit  10003  1elunit  10004  divelunit  10019  lincmb01cmp  10020  iccf1o  10021  unitssre  10022  fz0to4untppr  10141  modqelico  10351  modqmuladdim  10384  addmodid  10389  expubnd  10594  le2sq2  10613  bernneq2  10659  expnbnd  10661  expnlbnd  10662  faclbnd  10738  faclbnd3  10740  faclbnd6  10741  bcval4  10749  bcpasc  10763  reim0  10887  re0  10921  im0  10922  rei  10925  imi  10926  cj0  10927  caucvgre  11007  rennim  11028  sqrt0rlem  11029  sqrt0  11030  resqrexlemdecn  11038  resqrexlemnm  11044  resqrexlemgt0  11046  sqrt00  11066  sqrt9  11074  sqrt2gt1lt2  11075  leabs  11100  ltabs  11113  sqrtpclii  11156  max0addsup  11245  fimaxre2  11252  climge0  11350  iserge0  11368  fsum00  11487  arisum2  11524  0.999...  11546  fprodge0  11662  cos0  11755  ef01bndlem  11781  sin01bnd  11782  cos01bnd  11783  cos2bnd  11785  sin01gt0  11786  cos01gt0  11787  sincos2sgn  11790  sin4lt0  11791  absef  11794  absefib  11795  efieq1re  11796  epos  11805  flodddiv4  11956  gcdn0gt0  11996  nn0seqcvgd  12058  algcvgblem  12066  algcvga  12068  pythagtriplem12  12292  pythagtriplem13  12293  pythagtriplem14  12294  pythagtriplem16  12296  mulgnegnn  13037  ssblps  14308  ssbl  14309  xmeter  14319  cnbl0  14417  reeff1olem  14575  pilem3  14587  pipos  14592  sinhalfpilem  14595  sincosq1sgn  14630  sincosq2sgn  14631  sinq34lt0t  14635  coseq0q4123  14638  coseq00topi  14639  coseq0negpitopi  14640  tangtx  14642  sincos4thpi  14644  sincos6thpi  14646  cosordlem  14653  cosq34lt1  14654  cos02pilt1  14655  cos0pilt1  14656  cos11  14657  ioocosf1o  14658  log1  14670  logrpap0b  14680  logdivlti  14685  rpabscxpbnd  14742  lgsval2lem  14794  lgsval4a  14806  lgsneg  14808  lgsdilem  14811  lgsdir2lem1  14812  ex-gcd  14866  trilpolemclim  15168  trilpolemcl  15169  trilpolemisumle  15170  trilpolemeq1  15172  trilpolemlt1  15173  trirec0  15176  apdiff  15180  redc0  15189  reap0  15190  dceqnconst  15192  dcapnconst  15193  nconstwlpolemgt0  15196  neap0mkv  15201