Theorem 0re 8021

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 8020	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 7983	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 8000	. . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
4	1, 3	mpan 424	. . . 4 ⊢ (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5		eleq1 2256	. . . 4 ⊢ ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 155	. . 3 ⊢ (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
7	6	rexlimiv 2605	. 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
8	1, 2, 7	mp2b 8	1 ⊢ 0 ∈ ℝ

Syntax hints:   = wceq 1364   ∈ wcel 2164  ∃wrex 2473  (class class class)co 5919  ℝcr 7873  0cc0 7874  1c1 7875   + caddc 7877

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546  ax-ext 2175  ax-1re 7968  ax-addrcl 7971  ax-rnegex 7983

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-cleq 2186  df-clel 2189  df-ral 2477  df-rex 2478

This theorem is referenced by:  0red  8022  0xr  8068  axmulgt0  8093  gtso  8100  0lt1  8148  ine0  8415  ltaddneg  8445  addgt0  8469  addgegt0  8470  addgtge0  8471  addge0  8472  ltaddpos  8473  ltneg  8483  leneg  8486  lt0neg1  8489  lt0neg2  8490  le0neg1  8491  le0neg2  8492  addge01  8493  suble0  8497  0le1  8502  gt0ne0i  8507  gt0ne0d  8533  lt0ne0d  8534  recexre  8599  recexgt0  8601  inelr  8605  rimul  8606  1ap0  8611  reapmul1  8616  apsqgt0  8622  msqge0  8637  mulge0  8640  recexaplem2  8673  recexap  8674  rerecclap  8751  ltm1  8867  recgt0  8871  ltmul12a  8881  lemul12a  8883  mulgt1  8884  gt0div  8891  ge0div  8892  recgt1i  8919  recreclt  8921  sup3exmid  8978  crap0  8979  nnge1  9007  nngt0  9009  nnrecgt0  9022  0ne1  9051  0le0  9073  neg1lt0  9092  halfge0  9201  iap0  9208  nn0ssre  9247  nn0ge0  9268  nn0nlt0  9269  nn0le0eq0  9271  0mnnnnn0  9275  elnnnn0b  9287  elnnnn0c  9288  elnnz  9330  0z  9331  elnnz1  9343  nn0lt10b  9400  recnz  9413  gtndiv  9415  fnn0ind  9436  rpge0  9735  rpnegap  9755  0nrp  9758  0ltpnf  9851  mnflt0  9853  xneg0  9900  xaddid1  9931  xnn0xadd0  9936  xposdif  9951  elrege0  10045  0e0icopnf  10048  0elunit  10055  1elunit  10056  divelunit  10071  lincmb01cmp  10072  iccf1o  10073  unitssre  10074  fz0to4untppr  10193  modqelico  10408  modqmuladdim  10441  addmodid  10446  xnn0nnen  10511  expubnd  10670  le2sq2  10689  bernneq2  10735  expnbnd  10737  expnlbnd  10738  faclbnd  10815  faclbnd3  10817  faclbnd6  10818  bcval4  10826  bcpasc  10840  reim0  11008  re0  11042  im0  11043  rei  11046  imi  11047  cj0  11048  caucvgre  11128  rennim  11149  sqrt0rlem  11150  sqrt0  11151  resqrexlemdecn  11159  resqrexlemnm  11165  resqrexlemgt0  11167  sqrt00  11187  sqrt9  11195  sqrt2gt1lt2  11196  leabs  11221  ltabs  11234  sqrtpclii  11277  max0addsup  11366  fimaxre2  11373  climge0  11471  iserge0  11489  fsum00  11608  arisum2  11645  0.999...  11667  fprodge0  11783  cos0  11876  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  cos2bnd  11906  sin01gt0  11908  cos01gt0  11909  sincos2sgn  11912  sin4lt0  11913  absef  11916  absefib  11917  efieq1re  11918  epos  11927  flodddiv4  12078  gcdn0gt0  12118  nn0seqcvgd  12182  algcvgblem  12190  algcvga  12192  pythagtriplem12  12416  pythagtriplem13  12417  pythagtriplem14  12418  pythagtriplem16  12420  mulgnegnn  13205  ssblps  14604  ssbl  14605  xmeter  14615  cnbl0  14713  hovera  14826  hovergt0  14829  plyrecj  14941  reeff1olem  14947  pilem3  14959  pipos  14964  sinhalfpilem  14967  sincosq1sgn  15002  sincosq2sgn  15003  sinq34lt0t  15007  coseq0q4123  15010  coseq00topi  15011  coseq0negpitopi  15012  tangtx  15014  sincos4thpi  15016  sincos6thpi  15018  cosordlem  15025  cosq34lt1  15026  cos02pilt1  15027  cos0pilt1  15028  cos11  15029  ioocosf1o  15030  log1  15042  logrpap0b  15052  logdivlti  15057  rpabscxpbnd  15114  lgsval2lem  15167  lgsval4a  15179  lgsneg  15181  lgsdilem  15184  lgsdir2lem1  15185  ex-gcd  15293  trilpolemclim  15596  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  trirec0  15604  apdiff  15608  redc0  15617  reap0  15618  dceqnconst  15620  dcapnconst  15621  nconstwlpolemgt0  15624  neap0mkv  15629