Theorem 0re 8142

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

Syntax hints:   = wceq 1395   ∈ wcel 2200  ∃wrex 2509  (class class class)co 6000  ℝcr 7994  0cc0 7995  1c1 7996   + caddc 7998

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8089  ax-addrcl 8092  ax-rnegex 8104

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-ral 2513  df-rex 2514

This theorem is referenced by:  0red  8143  0xr  8189  axmulgt0  8214  gtso  8221  0lt1  8269  ine0  8536  ltaddneg  8567  addgt0  8591  addgegt0  8592  addgtge0  8593  addge0  8594  ltaddpos  8595  ltneg  8605  leneg  8608  lt0neg1  8611  lt0neg2  8612  le0neg1  8613  le0neg2  8614  addge01  8615  suble0  8619  0le1  8624  gt0ne0i  8629  gt0ne0d  8655  lt0ne0d  8656  recexre  8721  recexgt0  8723  inelr  8727  rimul  8728  1ap0  8733  reapmul1  8738  apsqgt0  8744  msqge0  8759  mulge0  8762  recexaplem2  8795  recexap  8796  rerecclap  8873  ltm1  8989  recgt0  8993  ltmul12a  9003  lemul12a  9005  mulgt1  9006  gt0div  9013  ge0div  9014  recgt1i  9041  recreclt  9043  sup3exmid  9100  crap0  9101  nnge1  9129  nngt0  9131  nnrecgt0  9144  0ne1  9173  0le0  9195  neg1lt0  9214  halfge0  9323  iap0  9330  nn0ssre  9369  nn0ge0  9390  nn0nlt0  9391  nn0le0eq0  9393  0mnnnnn0  9397  elnnnn0b  9409  elnnnn0c  9410  elnnz  9452  0z  9453  elnnz1  9465  nn0lt10b  9523  recnz  9536  gtndiv  9538  fnn0ind  9559  rpge0  9858  rpnegap  9878  0nrp  9881  0ltpnf  9974  mnflt0  9976  xneg0  10023  xaddid1  10054  xnn0xadd0  10059  xposdif  10074  elrege0  10168  0e0icopnf  10171  0elunit  10178  1elunit  10179  divelunit  10194  lincmb01cmp  10195  iccf1o  10196  unitssre  10197  fz0to4untppr  10316  modqelico  10551  modqmuladdim  10584  addmodid  10589  xnn0nnen  10654  expubnd  10813  le2sq2  10832  bernneq2  10878  expnbnd  10880  expnlbnd  10881  faclbnd  10958  faclbnd3  10960  faclbnd6  10961  bcval4  10969  bcpasc  10983  lsw0  11114  swrdccatin2  11256  pfxccatin12lem3  11259  reim0  11367  re0  11401  im0  11402  rei  11405  imi  11406  cj0  11407  caucvgre  11487  rennim  11508  sqrt0rlem  11509  sqrt0  11510  resqrexlemdecn  11518  resqrexlemnm  11524  resqrexlemgt0  11526  sqrt00  11546  sqrt9  11554  sqrt2gt1lt2  11555  leabs  11580  ltabs  11593  sqrtpclii  11636  max0addsup  11725  fimaxre2  11733  climge0  11831  iserge0  11849  fsum00  11968  arisum2  12005  0.999...  12027  fprodge0  12143  cos0  12236  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  cos2bnd  12266  sin01gt0  12268  cos01gt0  12269  sincos2sgn  12272  sin4lt0  12273  absef  12276  absefib  12277  efieq1re  12278  epos  12287  flodddiv4  12442  gcdn0gt0  12494  nn0seqcvgd  12558  algcvgblem  12566  algcvga  12568  pythagtriplem12  12793  pythagtriplem13  12794  pythagtriplem14  12795  pythagtriplem16  12797  mulgnegnn  13664  ssblps  15093  ssbl  15094  xmeter  15104  cnbl0  15202  hovera  15315  hovergt0  15318  plyrecj  15431  reeff1olem  15439  pilem3  15451  pipos  15456  sinhalfpilem  15459  sincosq1sgn  15494  sincosq2sgn  15495  sinq34lt0t  15499  coseq0q4123  15502  coseq00topi  15503  coseq0negpitopi  15504  tangtx  15506  sincos4thpi  15508  sincos6thpi  15510  cosordlem  15517  cosq34lt1  15518  cos02pilt1  15519  cos0pilt1  15520  cos11  15521  ioocosf1o  15522  log1  15534  logrpap0b  15544  logdivlti  15549  rpabscxpbnd  15608  lgsval2lem  15683  lgsval4a  15695  lgsneg  15697  lgsdilem  15700  lgsdir2lem1  15701  ex-gcd  16053  trilpolemclim  16363  trilpolemcl  16364  trilpolemisumle  16365  trilpolemeq1  16367  trilpolemlt1  16368  trirec0  16371  apdiff  16375  redc0  16384  reap0  16385  dceqnconst  16387  dcapnconst  16388  nconstwlpolemgt0  16391  neap0mkv  16396