Theorem 0re 8019

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 8018	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 7981	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 7998	. . . . 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 5918  ℝcr 7871  0cc0 7872  1c1 7873   + caddc 7875

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 7966  ax-addrcl 7969  ax-rnegex 7981

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  8020  0xr  8066  axmulgt0  8091  gtso  8098  0lt1  8146  ine0  8413  ltaddneg  8443  addgt0  8467  addgegt0  8468  addgtge0  8469  addge0  8470  ltaddpos  8471  ltneg  8481  leneg  8484  lt0neg1  8487  lt0neg2  8488  le0neg1  8489  le0neg2  8490  addge01  8491  suble0  8495  0le1  8500  gt0ne0i  8505  gt0ne0d  8531  lt0ne0d  8532  recexre  8597  recexgt0  8599  inelr  8603  rimul  8604  1ap0  8609  reapmul1  8614  apsqgt0  8620  msqge0  8635  mulge0  8638  recexaplem2  8671  recexap  8672  rerecclap  8749  ltm1  8865  recgt0  8869  ltmul12a  8879  lemul12a  8881  mulgt1  8882  gt0div  8889  ge0div  8890  recgt1i  8917  recreclt  8919  sup3exmid  8976  crap0  8977  nnge1  9005  nngt0  9007  nnrecgt0  9020  0ne1  9049  0le0  9071  neg1lt0  9090  halfge0  9198  iap0  9205  nn0ssre  9244  nn0ge0  9265  nn0nlt0  9266  nn0le0eq0  9268  0mnnnnn0  9272  elnnnn0b  9284  elnnnn0c  9285  elnnz  9327  0z  9328  elnnz1  9340  nn0lt10b  9397  recnz  9410  gtndiv  9412  fnn0ind  9433  rpge0  9732  rpnegap  9752  0nrp  9755  0ltpnf  9848  mnflt0  9850  xneg0  9897  xaddid1  9928  xnn0xadd0  9933  xposdif  9948  elrege0  10042  0e0icopnf  10045  0elunit  10052  1elunit  10053  divelunit  10068  lincmb01cmp  10069  iccf1o  10070  unitssre  10071  fz0to4untppr  10190  modqelico  10405  modqmuladdim  10438  addmodid  10443  xnn0nnen  10508  expubnd  10667  le2sq2  10686  bernneq2  10732  expnbnd  10734  expnlbnd  10735  faclbnd  10812  faclbnd3  10814  faclbnd6  10815  bcval4  10823  bcpasc  10837  reim0  11005  re0  11039  im0  11040  rei  11043  imi  11044  cj0  11045  caucvgre  11125  rennim  11146  sqrt0rlem  11147  sqrt0  11148  resqrexlemdecn  11156  resqrexlemnm  11162  resqrexlemgt0  11164  sqrt00  11184  sqrt9  11192  sqrt2gt1lt2  11193  leabs  11218  ltabs  11231  sqrtpclii  11274  max0addsup  11363  fimaxre2  11370  climge0  11468  iserge0  11486  fsum00  11605  arisum2  11642  0.999...  11664  fprodge0  11780  cos0  11873  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  cos2bnd  11903  sin01gt0  11905  cos01gt0  11906  sincos2sgn  11909  sin4lt0  11910  absef  11913  absefib  11914  efieq1re  11915  epos  11924  flodddiv4  12075  gcdn0gt0  12115  nn0seqcvgd  12179  algcvgblem  12187  algcvga  12189  pythagtriplem12  12413  pythagtriplem13  12414  pythagtriplem14  12415  pythagtriplem16  12417  mulgnegnn  13202  ssblps  14593  ssbl  14594  xmeter  14604  cnbl0  14702  hovera  14801  hovergt0  14804  reeff1olem  14906  pilem3  14918  pipos  14923  sinhalfpilem  14926  sincosq1sgn  14961  sincosq2sgn  14962  sinq34lt0t  14966  coseq0q4123  14969  coseq00topi  14970  coseq0negpitopi  14971  tangtx  14973  sincos4thpi  14975  sincos6thpi  14977  cosordlem  14984  cosq34lt1  14985  cos02pilt1  14986  cos0pilt1  14987  cos11  14988  ioocosf1o  14989  log1  15001  logrpap0b  15011  logdivlti  15016  rpabscxpbnd  15073  lgsval2lem  15126  lgsval4a  15138  lgsneg  15140  lgsdilem  15143  lgsdir2lem1  15144  ex-gcd  15223  trilpolemclim  15526  trilpolemcl  15527  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  trirec0  15534  apdiff  15538  redc0  15547  reap0  15548  dceqnconst  15550  dcapnconst  15551  nconstwlpolemgt0  15554  neap0mkv  15559