Theorem 0re 8179

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

Syntax hints:   = wceq 1397   ∈ wcel 2202  ∃wrex 2511  (class class class)co 6018  ℝcr 8031  0cc0 8032  1c1 8033   + caddc 8035

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8126  ax-addrcl 8129  ax-rnegex 8141

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-cleq 2224  df-clel 2227  df-ral 2515  df-rex 2516

This theorem is referenced by:  0red  8180  0xr  8226  axmulgt0  8251  gtso  8258  0lt1  8306  ine0  8573  ltaddneg  8604  addgt0  8628  addgegt0  8629  addgtge0  8630  addge0  8631  ltaddpos  8632  ltneg  8642  leneg  8645  lt0neg1  8648  lt0neg2  8649  le0neg1  8650  le0neg2  8651  addge01  8652  suble0  8656  0le1  8661  gt0ne0i  8666  gt0ne0d  8692  lt0ne0d  8693  recexre  8758  recexgt0  8760  inelr  8764  rimul  8765  1ap0  8770  reapmul1  8775  apsqgt0  8781  msqge0  8796  mulge0  8799  recexaplem2  8832  recexap  8833  rerecclap  8910  ltm1  9026  recgt0  9030  ltmul12a  9040  lemul12a  9042  mulgt1  9043  gt0div  9050  ge0div  9051  recgt1i  9078  recreclt  9080  sup3exmid  9137  crap0  9138  nnge1  9166  nngt0  9168  nnrecgt0  9181  0ne1  9210  0le0  9232  neg1lt0  9251  halfge0  9360  iap0  9367  nn0ssre  9406  nn0ge0  9427  nn0nlt0  9428  nn0le0eq0  9430  0mnnnnn0  9434  elnnnn0b  9446  elnnnn0c  9447  elnnz  9489  0z  9490  elnnz1  9502  nn0lt10b  9560  recnz  9573  gtndiv  9575  fnn0ind  9596  rpge0  9901  rpnegap  9921  0nrp  9924  0ltpnf  10017  mnflt0  10019  xneg0  10066  xaddid1  10097  xnn0xadd0  10102  xposdif  10117  elrege0  10211  0e0icopnf  10214  0elunit  10221  1elunit  10222  divelunit  10237  lincmb01cmp  10238  iccf1o  10239  unitssre  10240  fz0to4untppr  10359  nn0p1elfzo  10422  modqelico  10597  modqmuladdim  10630  addmodid  10635  xnn0nnen  10700  expubnd  10859  le2sq2  10878  bernneq2  10924  expnbnd  10926  expnlbnd  10927  faclbnd  11004  faclbnd3  11006  faclbnd6  11007  bcval4  11015  bcpasc  11029  lsw0  11165  swrdccatin2  11314  pfxccatin12lem3  11317  reim0  11439  re0  11473  im0  11474  rei  11477  imi  11478  cj0  11479  caucvgre  11559  rennim  11580  sqrt0rlem  11581  sqrt0  11582  resqrexlemdecn  11590  resqrexlemnm  11596  resqrexlemgt0  11598  sqrt00  11618  sqrt9  11626  sqrt2gt1lt2  11627  leabs  11652  ltabs  11665  sqrtpclii  11708  max0addsup  11797  fimaxre2  11805  climge0  11903  iserge0  11921  fsum00  12041  arisum2  12078  0.999...  12100  fprodge0  12216  cos0  12309  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  cos2bnd  12339  sin01gt0  12341  cos01gt0  12342  sincos2sgn  12345  sin4lt0  12346  absef  12349  absefib  12350  efieq1re  12351  epos  12360  flodddiv4  12515  gcdn0gt0  12567  nn0seqcvgd  12631  algcvgblem  12639  algcvga  12641  pythagtriplem12  12866  pythagtriplem13  12867  pythagtriplem14  12868  pythagtriplem16  12870  mulgnegnn  13737  ssblps  15168  ssbl  15169  xmeter  15179  cnbl0  15277  hovera  15390  hovergt0  15393  plyrecj  15506  reeff1olem  15514  pilem3  15526  pipos  15531  sinhalfpilem  15534  sincosq1sgn  15569  sincosq2sgn  15570  sinq34lt0t  15574  coseq0q4123  15577  coseq00topi  15578  coseq0negpitopi  15579  tangtx  15581  sincos4thpi  15583  sincos6thpi  15585  cosordlem  15592  cosq34lt1  15593  cos02pilt1  15594  cos0pilt1  15595  cos11  15596  ioocosf1o  15597  log1  15609  logrpap0b  15619  logdivlti  15624  rpabscxpbnd  15683  lgsval2lem  15758  lgsval4a  15770  lgsneg  15772  lgsdilem  15775  lgsdir2lem1  15776  clwwlkn0  16278  konigsberg  16363  ex-gcd  16374  trilpolemclim  16691  trilpolemcl  16692  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  trirec0  16699  apdiff  16703  redc0  16713  reap0  16714  dceqnconst  16716  dcapnconst  16717  nconstwlpolemgt0  16720  neap0mkv  16725