Theorem 0re 7907

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 7906	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 7870	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 7887	. . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
4	1, 3	mpan 422	. . . 4 ⊢ (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5		eleq1 2233	. . . 4 ⊢ ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 154	. . 3 ⊢ (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
7	6	rexlimiv 2581	. 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
8	1, 2, 7	mp2b 8	1 ⊢ 0 ∈ ℝ

Syntax hints:   = wceq 1348   ∈ wcel 2141  ∃wrex 2449  (class class class)co 5850  ℝcr 7760  0cc0 7761  1c1 7762   + caddc 7764

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528  ax-ext 2152  ax-1re 7855  ax-addrcl 7858  ax-rnegex 7870

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-cleq 2163  df-clel 2166  df-ral 2453  df-rex 2454

This theorem is referenced by:  0red  7908  0xr  7953  axmulgt0  7978  gtso  7985  0lt1  8033  ine0  8300  ltaddneg  8330  addgt0  8354  addgegt0  8355  addgtge0  8356  addge0  8357  ltaddpos  8358  ltneg  8368  leneg  8371  lt0neg1  8374  lt0neg2  8375  le0neg1  8376  le0neg2  8377  addge01  8378  suble0  8382  0le1  8387  gt0ne0i  8392  gt0ne0d  8418  lt0ne0d  8419  recexre  8484  recexgt0  8486  inelr  8490  rimul  8491  1ap0  8496  reapmul1  8501  apsqgt0  8507  msqge0  8522  mulge0  8525  recexaplem2  8557  recexap  8558  rerecclap  8634  ltm1  8749  recgt0  8753  ltmul12a  8763  lemul12a  8765  mulgt1  8766  gt0div  8773  ge0div  8774  recgt1i  8801  recreclt  8803  sup3exmid  8860  crap0  8861  nnge1  8888  nngt0  8890  nnrecgt0  8903  0ne1  8932  0le0  8954  neg1lt0  8973  halfge0  9081  iap0  9088  nn0ssre  9126  nn0ge0  9147  nn0nlt0  9148  nn0le0eq0  9150  0mnnnnn0  9154  elnnnn0b  9166  elnnnn0c  9167  elnnz  9209  0z  9210  elnnz1  9222  nn0lt10b  9279  recnz  9292  gtndiv  9294  fnn0ind  9315  rpge0  9610  rpnegap  9630  0nrp  9633  0ltpnf  9726  mnflt0  9728  xneg0  9775  xaddid1  9806  xnn0xadd0  9811  xposdif  9826  elrege0  9920  0e0icopnf  9923  0elunit  9930  1elunit  9931  divelunit  9946  lincmb01cmp  9947  iccf1o  9948  unitssre  9949  fz0to4untppr  10067  modqelico  10277  modqmuladdim  10310  addmodid  10315  expubnd  10520  le2sq2  10538  bernneq2  10584  expnbnd  10586  expnlbnd  10587  faclbnd  10662  faclbnd3  10664  faclbnd6  10665  bcval4  10673  bcpasc  10687  reim0  10812  re0  10846  im0  10847  rei  10850  imi  10851  cj0  10852  caucvgre  10932  rennim  10953  sqrt0rlem  10954  sqrt0  10955  resqrexlemdecn  10963  resqrexlemnm  10969  resqrexlemgt0  10971  sqrt00  10991  sqrt9  10999  sqrt2gt1lt2  11000  leabs  11025  ltabs  11038  sqrtpclii  11081  max0addsup  11170  fimaxre2  11177  climge0  11275  iserge0  11293  fsum00  11412  arisum2  11449  0.999...  11471  fprodge0  11587  cos0  11680  ef01bndlem  11706  sin01bnd  11707  cos01bnd  11708  cos2bnd  11710  sin01gt0  11711  cos01gt0  11712  sincos2sgn  11715  sin4lt0  11716  absef  11719  absefib  11720  efieq1re  11721  epos  11730  flodddiv4  11880  gcdn0gt0  11920  nn0seqcvgd  11982  algcvgblem  11990  algcvga  11992  pythagtriplem12  12216  pythagtriplem13  12217  pythagtriplem14  12218  pythagtriplem16  12220  ssblps  13178  ssbl  13179  xmeter  13189  cnbl0  13287  reeff1olem  13445  pilem3  13457  pipos  13462  sinhalfpilem  13465  sincosq1sgn  13500  sincosq2sgn  13501  sinq34lt0t  13505  coseq0q4123  13508  coseq00topi  13509  coseq0negpitopi  13510  tangtx  13512  sincos4thpi  13514  sincos6thpi  13516  cosordlem  13523  cosq34lt1  13524  cos02pilt1  13525  cos0pilt1  13526  cos11  13527  ioocosf1o  13528  log1  13540  logrpap0b  13550  logdivlti  13555  rpabscxpbnd  13612  lgsval2lem  13664  lgsval4a  13676  lgsneg  13678  lgsdilem  13681  lgsdir2lem1  13682  ex-gcd  13725  trilpolemclim  14028  trilpolemcl  14029  trilpolemisumle  14030  trilpolemeq1  14032  trilpolemlt1  14033  trirec0  14036  apdiff  14040  redc0  14049  reap0  14050  dceqnconst  14051  dcapnconst  14052  nconstwlpolemgt0  14055