Theorem 0re 7890

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 7889	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 7853	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 7870	. . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
4	1, 3	mpan 421	. . . 4 ⊢ (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5		eleq1 2227	. . . 4 ⊢ ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 154	. . 3 ⊢ (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
7	6	rexlimiv 2575	. 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
8	1, 2, 7	mp2b 8	1 ⊢ 0 ∈ ℝ

Syntax hints:   = wceq 1342   ∈ wcel 2135  ∃wrex 2443  (class class class)co 5836  ℝcr 7743  0cc0 7744  1c1 7745   + caddc 7747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-i5r 1522  ax-ext 2146  ax-1re 7838  ax-addrcl 7841  ax-rnegex 7853

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-cleq 2157  df-clel 2160  df-ral 2447  df-rex 2448

This theorem is referenced by:  0red  7891  0xr  7936  axmulgt0  7961  gtso  7968  0lt1  8016  ine0  8283  ltaddneg  8313  addgt0  8337  addgegt0  8338  addgtge0  8339  addge0  8340  ltaddpos  8341  ltneg  8351  leneg  8354  lt0neg1  8357  lt0neg2  8358  le0neg1  8359  le0neg2  8360  addge01  8361  suble0  8365  0le1  8370  gt0ne0i  8375  gt0ne0d  8401  lt0ne0d  8402  recexre  8467  recexgt0  8469  inelr  8473  rimul  8474  1ap0  8479  reapmul1  8484  apsqgt0  8490  msqge0  8505  mulge0  8508  recexaplem2  8540  recexap  8541  rerecclap  8617  ltm1  8732  recgt0  8736  ltmul12a  8746  lemul12a  8748  mulgt1  8749  gt0div  8756  ge0div  8757  recgt1i  8784  recreclt  8786  sup3exmid  8843  crap0  8844  nnge1  8871  nngt0  8873  nnrecgt0  8886  0ne1  8915  0le0  8937  neg1lt0  8956  halfge0  9064  iap0  9071  nn0ssre  9109  nn0ge0  9130  nn0nlt0  9131  nn0le0eq0  9133  0mnnnnn0  9137  elnnnn0b  9149  elnnnn0c  9150  elnnz  9192  0z  9193  elnnz1  9205  nn0lt10b  9262  recnz  9275  gtndiv  9277  fnn0ind  9298  rpge0  9593  rpnegap  9613  0nrp  9616  0ltpnf  9709  mnflt0  9711  xneg0  9758  xaddid1  9789  xnn0xadd0  9794  xposdif  9809  elrege0  9903  0e0icopnf  9906  0elunit  9913  1elunit  9914  divelunit  9929  lincmb01cmp  9930  iccf1o  9931  unitssre  9932  fz0to4untppr  10049  modqelico  10259  modqmuladdim  10292  addmodid  10297  expubnd  10502  le2sq2  10520  bernneq2  10565  expnbnd  10567  expnlbnd  10568  faclbnd  10643  faclbnd3  10645  faclbnd6  10646  bcval4  10654  bcpasc  10668  reim0  10789  re0  10823  im0  10824  rei  10827  imi  10828  cj0  10829  caucvgre  10909  rennim  10930  sqrt0rlem  10931  sqrt0  10932  resqrexlemdecn  10940  resqrexlemnm  10946  resqrexlemgt0  10948  sqrt00  10968  sqrt9  10976  sqrt2gt1lt2  10977  leabs  11002  ltabs  11015  sqrtpclii  11058  max0addsup  11147  fimaxre2  11154  climge0  11252  iserge0  11270  fsum00  11389  arisum2  11426  0.999...  11448  fprodge0  11564  cos0  11657  ef01bndlem  11683  sin01bnd  11684  cos01bnd  11685  cos2bnd  11687  sin01gt0  11688  cos01gt0  11689  sincos2sgn  11692  sin4lt0  11693  absef  11696  absefib  11697  efieq1re  11698  epos  11707  flodddiv4  11856  gcdn0gt0  11896  nn0seqcvgd  11952  algcvgblem  11960  algcvga  11962  pythagtriplem12  12184  pythagtriplem13  12185  pythagtriplem14  12186  pythagtriplem16  12188  ssblps  12966  ssbl  12967  xmeter  12977  cnbl0  13075  reeff1olem  13233  pilem3  13245  pipos  13250  sinhalfpilem  13253  sincosq1sgn  13288  sincosq2sgn  13289  sinq34lt0t  13293  coseq0q4123  13296  coseq00topi  13297  coseq0negpitopi  13298  tangtx  13300  sincos4thpi  13302  sincos6thpi  13304  cosordlem  13311  cosq34lt1  13312  cos02pilt1  13313  cos0pilt1  13314  cos11  13315  ioocosf1o  13316  log1  13328  logrpap0b  13338  logdivlti  13343  rpabscxpbnd  13400  ex-gcd  13449  trilpolemclim  13749  trilpolemcl  13750  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  trirec0  13757  apdiff  13761  redc0  13770  reap0  13771  dceqnconst  13772  dcapnconst  13773  nconstwlpolemgt0  13776