Theorem 0re 7638

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 7637	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 7604	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 7618	. . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
4	1, 3	mpan 418	. . . 4 ⊢ (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5		eleq1 2162	. . . 4 ⊢ ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 154	. . 3 ⊢ (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
7	6	rexlimiv 2502	. 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
8	1, 2, 7	mp2b 8	1 ⊢ 0 ∈ ℝ

Syntax hints:   = wceq 1299   ∈ wcel 1448  ∃wrex 2376  (class class class)co 5706  ℝcr 7499  0cc0 7500  1c1 7501   + caddc 7503

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-1re 7589  ax-addrcl 7592  ax-rnegex 7604

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-cleq 2093  df-clel 2096  df-ral 2380  df-rex 2381

This theorem is referenced by:  0red  7639  0xr  7684  axmulgt0  7708  gtso  7714  0lt1  7760  ine0  8023  ltaddneg  8053  addgt0  8077  addgegt0  8078  addgtge0  8079  addge0  8080  ltaddpos  8081  ltneg  8091  leneg  8094  lt0neg1  8097  lt0neg2  8098  le0neg1  8099  le0neg2  8100  addge01  8101  suble0  8105  0le1  8110  gt0ne0i  8115  gt0ne0d  8141  lt0ne0d  8142  recexre  8206  recexgt0  8208  inelr  8212  rimul  8213  1ap0  8218  reapmul1  8223  apsqgt0  8229  msqge0  8244  mulge0  8247  recexaplem2  8274  recexap  8275  rerecclap  8351  ltm1  8462  recgt0  8466  ltmul12a  8476  lemul12a  8478  mulgt1  8479  gt0div  8486  ge0div  8487  recgt1i  8514  recreclt  8516  sup3exmid  8573  crap0  8574  nnge1  8601  nngt0  8603  nnrecgt0  8616  0ne1  8645  0le0  8667  neg1lt0  8686  halfge0  8788  iap0  8795  nn0ssre  8833  nn0ge0  8854  nn0nlt0  8855  nn0le0eq0  8857  0mnnnnn0  8861  elnnnn0b  8873  elnnnn0c  8874  elnnz  8916  0z  8917  elnnz1  8929  nn0lt10b  8983  recnz  8996  gtndiv  8998  fnn0ind  9019  rpge0  9303  rpnegap  9323  0nrp  9324  0ltpnf  9409  mnflt0  9411  xneg0  9455  xaddid1  9486  xnn0xadd0  9491  xposdif  9506  elrege0  9600  0e0icopnf  9603  0elunit  9610  1elunit  9611  divelunit  9626  lincmb01cmp  9627  iccf1o  9628  unitssre  9629  modqelico  9948  modqmuladdim  9981  addmodid  9986  expubnd  10191  le2sq2  10209  bernneq2  10254  expnbnd  10256  expnlbnd  10257  faclbnd  10328  faclbnd3  10330  faclbnd6  10331  bcval4  10339  bcpasc  10353  reim0  10474  re0  10508  im0  10509  rei  10512  imi  10513  cj0  10514  caucvgre  10593  rennim  10614  sqrt0rlem  10615  sqrt0  10616  resqrexlemdecn  10624  resqrexlemnm  10630  resqrexlemgt0  10632  sqrt00  10652  sqrt9  10660  sqrt2gt1lt2  10661  leabs  10686  ltabs  10699  sqrtpclii  10742  max0addsup  10831  fimaxre2  10837  climge0  10933  iserge0  10951  fsum00  11070  arisum2  11107  0.999...  11129  cos0  11235  ef01bndlem  11261  sin01bnd  11262  cos01bnd  11263  cos2bnd  11265  sin01gt0  11266  cos01gt0  11267  sincos2sgn  11270  sin4lt0  11271  absef  11273  absefib  11274  efieq1re  11275  epos  11282  flodddiv4  11426  gcdn0gt0  11461  nn0seqcvgd  11515  algcvgblem  11523  algcvga  11525  ssblps  12353  ssbl  12354  xmeter  12364  cnbl0  12456  ex-gcd  12546  trilpolemclim  12813  trilpolemcl  12814  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818