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  8269  axmulgt0  8294  gtso  8301  0lt1  8349  ine0  8616  ltaddneg  8647  addgt0  8671  addgegt0  8672  addgtge0  8673  addge0  8674  ltaddpos  8675  ltneg  8685  leneg  8688  lt0neg1  8691  lt0neg2  8692  le0neg1  8693  le0neg2  8694  addge01  8695  suble0  8699  0le1  8704  gt0ne0i  8709  gt0ne0d  8735  lt0ne0d  8736  recexre  8801  recexgt0  8803  inelr  8807  rimul  8808  1ap0  8813  reapmul1  8818  apsqgt0  8824  msqge0  8839  mulge0  8842  recexaplem2  8875  recexap  8876  rerecclap  8953  ltm1  9069  recgt0  9073  ltmul12a  9083  lemul12a  9085  mulgt1  9086  gt0div  9093  ge0div  9094  recgt1i  9121  recreclt  9123  sup3exmid  9180  crap0  9181  nnge1  9209  nngt0  9211  nnrecgt0  9224  0ne1  9253  0le0  9275  neg1lt0  9294  halfge0  9403  iap0  9410  nn0ssre  9449  nn0ge0  9470  nn0nlt0  9471  nn0le0eq0  9473  0mnnnnn0  9477  elnnnn0b  9489  elnnnn0c  9490  elnnz  9534  0z  9535  elnnz1  9547  nn0lt10b  9605  recnz  9618  gtndiv  9620  fnn0ind  9641  rpge0  9946  rpnegap  9966  0nrp  9969  0ltpnf  10062  mnflt0  10064  xneg0  10111  xaddid1  10142  xnn0xadd0  10147  xposdif  10162  elrege0  10256  0e0icopnf  10259  0elunit  10266  1elunit  10267  divelunit  10282  lincmb01cmp  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