Theorem 0re 8045

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

Syntax hints:   = wceq 1364   ∈ wcel 2167  ∃wrex 2476  (class class class)co 5925  ℝcr 7897  0cc0 7898  1c1 7899   + caddc 7901

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7992  ax-addrcl 7995  ax-rnegex 8007

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-cleq 2189  df-clel 2192  df-ral 2480  df-rex 2481

This theorem is referenced by:  0red  8046  0xr  8092  axmulgt0  8117  gtso  8124  0lt1  8172  ine0  8439  ltaddneg  8470  addgt0  8494  addgegt0  8495  addgtge0  8496  addge0  8497  ltaddpos  8498  ltneg  8508  leneg  8511  lt0neg1  8514  lt0neg2  8515  le0neg1  8516  le0neg2  8517  addge01  8518  suble0  8522  0le1  8527  gt0ne0i  8532  gt0ne0d  8558  lt0ne0d  8559  recexre  8624  recexgt0  8626  inelr  8630  rimul  8631  1ap0  8636  reapmul1  8641  apsqgt0  8647  msqge0  8662  mulge0  8665  recexaplem2  8698  recexap  8699  rerecclap  8776  ltm1  8892  recgt0  8896  ltmul12a  8906  lemul12a  8908  mulgt1  8909  gt0div  8916  ge0div  8917  recgt1i  8944  recreclt  8946  sup3exmid  9003  crap0  9004  nnge1  9032  nngt0  9034  nnrecgt0  9047  0ne1  9076  0le0  9098  neg1lt0  9117  halfge0  9226  iap0  9233  nn0ssre  9272  nn0ge0  9293  nn0nlt0  9294  nn0le0eq0  9296  0mnnnnn0  9300  elnnnn0b  9312  elnnnn0c  9313  elnnz  9355  0z  9356  elnnz1  9368  nn0lt10b  9425  recnz  9438  gtndiv  9440  fnn0ind  9461  rpge0  9760  rpnegap  9780  0nrp  9783  0ltpnf  9876  mnflt0  9878  xneg0  9925  xaddid1  9956  xnn0xadd0  9961  xposdif  9976  elrege0  10070  0e0icopnf  10073  0elunit  10080  1elunit  10081  divelunit  10096  lincmb01cmp  10097  iccf1o  10098  unitssre  10099  fz0to4untppr  10218  modqelico  10445  modqmuladdim  10478  addmodid  10483  xnn0nnen  10548  expubnd  10707  le2sq2  10726  bernneq2  10772  expnbnd  10774  expnlbnd  10775  faclbnd  10852  faclbnd3  10854  faclbnd6  10855  bcval4  10863  bcpasc  10877  reim0  11045  re0  11079  im0  11080  rei  11083  imi  11084  cj0  11085  caucvgre  11165  rennim  11186  sqrt0rlem  11187  sqrt0  11188  resqrexlemdecn  11196  resqrexlemnm  11202  resqrexlemgt0  11204  sqrt00  11224  sqrt9  11232  sqrt2gt1lt2  11233  leabs  11258  ltabs  11271  sqrtpclii  11314  max0addsup  11403  fimaxre2  11411  climge0  11509  iserge0  11527  fsum00  11646  arisum2  11683  0.999...  11705  fprodge0  11821  cos0  11914  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  cos2bnd  11944  sin01gt0  11946  cos01gt0  11947  sincos2sgn  11950  sin4lt0  11951  absef  11954  absefib  11955  efieq1re  11956  epos  11965  flodddiv4  12120  gcdn0gt0  12172  nn0seqcvgd  12236  algcvgblem  12244  algcvga  12246  pythagtriplem12  12471  pythagtriplem13  12472  pythagtriplem14  12473  pythagtriplem16  12475  mulgnegnn  13340  ssblps  14769  ssbl  14770  xmeter  14780  cnbl0  14878  hovera  14991  hovergt0  14994  plyrecj  15107  reeff1olem  15115  pilem3  15127  pipos  15132  sinhalfpilem  15135  sincosq1sgn  15170  sincosq2sgn  15171  sinq34lt0t  15175  coseq0q4123  15178  coseq00topi  15179  coseq0negpitopi  15180  tangtx  15182  sincos4thpi  15184  sincos6thpi  15186  cosordlem  15193  cosq34lt1  15194  cos02pilt1  15195  cos0pilt1  15196  cos11  15197  ioocosf1o  15198  log1  15210  logrpap0b  15220  logdivlti  15225  rpabscxpbnd  15284  lgsval2lem  15359  lgsval4a  15371  lgsneg  15373  lgsdilem  15376  lgsdir2lem1  15377  ex-gcd  15485  trilpolemclim  15793  trilpolemcl  15794  trilpolemisumle  15795  trilpolemeq1  15797  trilpolemlt1  15798  trirec0  15801  apdiff  15805  redc0  15814  reap0  15815  dceqnconst  15817  dcapnconst  15818  nconstwlpolemgt0  15821  neap0mkv  15826