Theorem 0re 8071

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

Syntax hints:   = wceq 1372   ∈ wcel 2175  ∃wrex 2484  (class class class)co 5943  ℝcr 7923  0cc0 7924  1c1 7925   + caddc 7927

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-1re 8018  ax-addrcl 8021  ax-rnegex 8033

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-cleq 2197  df-clel 2200  df-ral 2488  df-rex 2489

This theorem is referenced by:  0red  8072  0xr  8118  axmulgt0  8143  gtso  8150  0lt1  8198  ine0  8465  ltaddneg  8496  addgt0  8520  addgegt0  8521  addgtge0  8522  addge0  8523  ltaddpos  8524  ltneg  8534  leneg  8537  lt0neg1  8540  lt0neg2  8541  le0neg1  8542  le0neg2  8543  addge01  8544  suble0  8548  0le1  8553  gt0ne0i  8558  gt0ne0d  8584  lt0ne0d  8585  recexre  8650  recexgt0  8652  inelr  8656  rimul  8657  1ap0  8662  reapmul1  8667  apsqgt0  8673  msqge0  8688  mulge0  8691  recexaplem2  8724  recexap  8725  rerecclap  8802  ltm1  8918  recgt0  8922  ltmul12a  8932  lemul12a  8934  mulgt1  8935  gt0div  8942  ge0div  8943  recgt1i  8970  recreclt  8972  sup3exmid  9029  crap0  9030  nnge1  9058  nngt0  9060  nnrecgt0  9073  0ne1  9102  0le0  9124  neg1lt0  9143  halfge0  9252  iap0  9259  nn0ssre  9298  nn0ge0  9319  nn0nlt0  9320  nn0le0eq0  9322  0mnnnnn0  9326  elnnnn0b  9338  elnnnn0c  9339  elnnz  9381  0z  9382  elnnz1  9394  nn0lt10b  9452  recnz  9465  gtndiv  9467  fnn0ind  9488  rpge0  9787  rpnegap  9807  0nrp  9810  0ltpnf  9903  mnflt0  9905  xneg0  9952  xaddid1  9983  xnn0xadd0  9988  xposdif  10003  elrege0  10097  0e0icopnf  10100  0elunit  10107  1elunit  10108  divelunit  10123  lincmb01cmp  10124  iccf1o  10125  unitssre  10126  fz0to4untppr  10245  modqelico  10477  modqmuladdim  10510  addmodid  10515  xnn0nnen  10580  expubnd  10739  le2sq2  10758  bernneq2  10804  expnbnd  10806  expnlbnd  10807  faclbnd  10884  faclbnd3  10886  faclbnd6  10887  bcval4  10895  bcpasc  10909  lsw0  11039  reim0  11114  re0  11148  im0  11149  rei  11152  imi  11153  cj0  11154  caucvgre  11234  rennim  11255  sqrt0rlem  11256  sqrt0  11257  resqrexlemdecn  11265  resqrexlemnm  11271  resqrexlemgt0  11273  sqrt00  11293  sqrt9  11301  sqrt2gt1lt2  11302  leabs  11327  ltabs  11340  sqrtpclii  11383  max0addsup  11472  fimaxre2  11480  climge0  11578  iserge0  11596  fsum00  11715  arisum2  11752  0.999...  11774  fprodge0  11890  cos0  11983  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  cos2bnd  12013  sin01gt0  12015  cos01gt0  12016  sincos2sgn  12019  sin4lt0  12020  absef  12023  absefib  12024  efieq1re  12025  epos  12034  flodddiv4  12189  gcdn0gt0  12241  nn0seqcvgd  12305  algcvgblem  12313  algcvga  12315  pythagtriplem12  12540  pythagtriplem13  12541  pythagtriplem14  12542  pythagtriplem16  12544  mulgnegnn  13410  ssblps  14839  ssbl  14840  xmeter  14850  cnbl0  14948  hovera  15061  hovergt0  15064  plyrecj  15177  reeff1olem  15185  pilem3  15197  pipos  15202  sinhalfpilem  15205  sincosq1sgn  15240  sincosq2sgn  15241  sinq34lt0t  15245  coseq0q4123  15248  coseq00topi  15249  coseq0negpitopi  15250  tangtx  15252  sincos4thpi  15254  sincos6thpi  15256  cosordlem  15263  cosq34lt1  15264  cos02pilt1  15265  cos0pilt1  15266  cos11  15267  ioocosf1o  15268  log1  15280  logrpap0b  15290  logdivlti  15295  rpabscxpbnd  15354  lgsval2lem  15429  lgsval4a  15441  lgsneg  15443  lgsdilem  15446  lgsdir2lem1  15447  ex-gcd  15600  trilpolemclim  15908  trilpolemcl  15909  trilpolemisumle  15910  trilpolemeq1  15912  trilpolemlt1  15913  trirec0  15916  apdiff  15920  redc0  15929  reap0  15930  dceqnconst  15932  dcapnconst  15933  nconstwlpolemgt0  15936  neap0mkv  15941