Theorem 0re 8222

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 8221	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 8184	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 8201	. . . . 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 2645	. 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
8	1, 2, 7	mp2b 8	1 ⊢ 0 ∈ ℝ

Syntax hints:   = wceq 1398   ∈ wcel 2202  ∃wrex 2512  (class class class)co 6028  ℝcr 8074  0cc0 8075  1c1 8076   + caddc 8078

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584  ax-ext 2213  ax-1re 8169  ax-addrcl 8172  ax-rnegex 8184

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

This theorem is referenced by:  0red  8223  0xr  8268  axmulgt0  8293  gtso  8300  0lt1  8348  ine0  8615  ltaddneg  8646  addgt0  8670  addgegt0  8671  addgtge0  8672  addge0  8673  ltaddpos  8674  ltneg  8684  leneg  8687  lt0neg1  8690  lt0neg2  8691  le0neg1  8692  le0neg2  8693  addge01  8694  suble0  8698  0le1  8703  gt0ne0i  8708  gt0ne0d  8734  lt0ne0d  8735  recexre  8800  recexgt0  8802  inelr  8806  rimul  8807  1ap0  8812  reapmul1  8817  apsqgt0  8823  msqge0  8838  mulge0  8841  recexaplem2  8874  recexap  8875  rerecclap  8952  ltm1  9068  recgt0  9072  ltmul12a  9082  lemul12a  9084  mulgt1  9085  gt0div  9092  ge0div  9093  recgt1i  9120  recreclt  9122  sup3exmid  9179  crap0  9180  nnge1  9208  nngt0  9210  nnrecgt0  9223  0ne1  9252  0le0  9274  neg1lt0  9293  halfge0  9402  iap0  9409  nn0ssre  9448  nn0ge0  9469  nn0nlt0  9470  nn0le0eq0  9472  0mnnnnn0  9476  elnnnn0b  9488  elnnnn0c  9489  elnnz  9533  0z  9534  elnnz1  9546  nn0lt10b  9604  recnz  9617  gtndiv  9619  fnn0ind  9640  rpge0  9945  rpnegap  9965  0nrp  9968  0ltpnf  10061  mnflt0  10063  xneg0  10110  xaddid1  10141  xnn0xadd0  10146  xposdif  10161  elrege0  10255  0e0icopnf  10258  0elunit  10265  1elunit  10266  divelunit  10281  lincmb01cmp  10282  lincmble  10283  iccf1o  10284  unitssre  10285  fz0to4untppr  10404  nn0p1elfzo  10467  modqelico  10642  modqmuladdim  10675  addmodid  10680  xnn0nnen  10745  expubnd  10904  le2sq2  10923  bernneq2  10969  expnbnd  10971  expnlbnd  10972  faclbnd  11049  faclbnd3  11051  faclbnd6  11052  bcval4  11060  bcpasc  11074  lsw0  11210  swrdccatin2  11359  pfxccatin12lem3  11362  reim0  11484  re0  11518  im0  11519  rei  11522  imi  11523  cj0  11524  caucvgre  11604  rennim  11625  sqrt0rlem  11626  sqrt0  11627  resqrexlemdecn  11635  resqrexlemnm  11641  resqrexlemgt0  11643  sqrt00  11663  sqrt9  11671  sqrt2gt1lt2  11672  leabs  11697  ltabs  11710  sqrtpclii  11753  max0addsup  11842  fimaxre2  11850  climge0  11948  iserge0  11966  fsum00  12086  arisum2  12123  0.999...  12145  fprodge0  12261  cos0  12354  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  cos2bnd  12384  sin01gt0  12386  cos01gt0  12387  sincos2sgn  12390  sin4lt0  12391  absef  12394  absefib  12395  efieq1re  12396  epos  12405  flodddiv4  12560  gcdn0gt0  12612  nn0seqcvgd  12676  algcvgblem  12684  algcvga  12686  pythagtriplem12  12911  pythagtriplem13  12912  pythagtriplem14  12913  pythagtriplem16  12915  mulgnegnn  13782  ssblps  15219  ssbl  15220  xmeter  15230  cnbl0  15328  hovera  15441  hovergt0  15444  plyrecj  15557  reeff1olem  15565  pilem3  15577  pipos  15582  sinhalfpilem  15585  sincosq1sgn  15620  sincosq2sgn  15621  sinq34lt0t  15625  coseq0q4123  15628  coseq00topi  15629  coseq0negpitopi  15630  tangtx  15632  sincos4thpi  15634  sincos6thpi  15636  cosordlem  15643  cosq34lt1  15644  cos02pilt1  15645  cos0pilt1  15646  cos11  15647  ioocosf1o  15648  log1  15660  logrpap0b  15670  logdivlti  15675  rpabscxpbnd  15734  lgsval2lem  15812  lgsval4a  15824  lgsneg  15826  lgsdilem  15829  lgsdir2lem1  15830  clwwlkn0  16332  konigsberg  16417  ex-gcd  16428  repiecelem  16740  repiecele0  16741  repiecege0  16742  trilpolemclim  16751  trilpolemcl  16752  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  trirec0  16759  apdiff  16763  redc0  16773  reap0  16774  dceqnconst  16776  dcapnconst  16777  nconstwlpolemgt0  16780  neap0mkv  16785