Theorem 0re 8028

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

Syntax hints:   = wceq 1364   ∈ wcel 2167  ∃wrex 2476  (class class class)co 5923  ℝcr 7880  0cc0 7881  1c1 7882   + caddc 7884

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7975  ax-addrcl 7978  ax-rnegex 7990

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-cleq 2189  df-clel 2192  df-ral 2480  df-rex 2481

This theorem is referenced by:  0red  8029  0xr  8075  axmulgt0  8100  gtso  8107  0lt1  8155  ine0  8422  ltaddneg  8453  addgt0  8477  addgegt0  8478  addgtge0  8479  addge0  8480  ltaddpos  8481  ltneg  8491  leneg  8494  lt0neg1  8497  lt0neg2  8498  le0neg1  8499  le0neg2  8500  addge01  8501  suble0  8505  0le1  8510  gt0ne0i  8515  gt0ne0d  8541  lt0ne0d  8542  recexre  8607  recexgt0  8609  inelr  8613  rimul  8614  1ap0  8619  reapmul1  8624  apsqgt0  8630  msqge0  8645  mulge0  8648  recexaplem2  8681  recexap  8682  rerecclap  8759  ltm1  8875  recgt0  8879  ltmul12a  8889  lemul12a  8891  mulgt1  8892  gt0div  8899  ge0div  8900  recgt1i  8927  recreclt  8929  sup3exmid  8986  crap0  8987  nnge1  9015  nngt0  9017  nnrecgt0  9030  0ne1  9059  0le0  9081  neg1lt0  9100  halfge0  9209  iap0  9216  nn0ssre  9255  nn0ge0  9276  nn0nlt0  9277  nn0le0eq0  9279  0mnnnnn0  9283  elnnnn0b  9295  elnnnn0c  9296  elnnz  9338  0z  9339  elnnz1  9351  nn0lt10b  9408  recnz  9421  gtndiv  9423  fnn0ind  9444  rpge0  9743  rpnegap  9763  0nrp  9766  0ltpnf  9859  mnflt0  9861  xneg0  9908  xaddid1  9939  xnn0xadd0  9944  xposdif  9959  elrege0  10053  0e0icopnf  10056  0elunit  10063  1elunit  10064  divelunit  10079  lincmb01cmp  10080  iccf1o  10081  unitssre  10082  fz0to4untppr  10201  modqelico  10428  modqmuladdim  10461  addmodid  10466  xnn0nnen  10531  expubnd  10690  le2sq2  10709  bernneq2  10755  expnbnd  10757  expnlbnd  10758  faclbnd  10835  faclbnd3  10837  faclbnd6  10838  bcval4  10846  bcpasc  10860  reim0  11028  re0  11062  im0  11063  rei  11066  imi  11067  cj0  11068  caucvgre  11148  rennim  11169  sqrt0rlem  11170  sqrt0  11171  resqrexlemdecn  11179  resqrexlemnm  11185  resqrexlemgt0  11187  sqrt00  11207  sqrt9  11215  sqrt2gt1lt2  11216  leabs  11241  ltabs  11254  sqrtpclii  11297  max0addsup  11386  fimaxre2  11394  climge0  11492  iserge0  11510  fsum00  11629  arisum2  11666  0.999...  11688  fprodge0  11804  cos0  11897  ef01bndlem  11923  sin01bnd  11924  cos01bnd  11925  cos2bnd  11927  sin01gt0  11929  cos01gt0  11930  sincos2sgn  11933  sin4lt0  11934  absef  11937  absefib  11938  efieq1re  11939  epos  11948  flodddiv4  12103  gcdn0gt0  12155  nn0seqcvgd  12219  algcvgblem  12227  algcvga  12229  pythagtriplem12  12454  pythagtriplem13  12455  pythagtriplem14  12456  pythagtriplem16  12458  mulgnegnn  13272  ssblps  14671  ssbl  14672  xmeter  14682  cnbl0  14780  hovera  14893  hovergt0  14896  plyrecj  15009  reeff1olem  15017  pilem3  15029  pipos  15034  sinhalfpilem  15037  sincosq1sgn  15072  sincosq2sgn  15073  sinq34lt0t  15077  coseq0q4123  15080  coseq00topi  15081  coseq0negpitopi  15082  tangtx  15084  sincos4thpi  15086  sincos6thpi  15088  cosordlem  15095  cosq34lt1  15096  cos02pilt1  15097  cos0pilt1  15098  cos11  15099  ioocosf1o  15100  log1  15112  logrpap0b  15122  logdivlti  15127  rpabscxpbnd  15186  lgsval2lem  15261  lgsval4a  15273  lgsneg  15275  lgsdilem  15278  lgsdir2lem1  15279  ex-gcd  15387  trilpolemclim  15690  trilpolemcl  15691  trilpolemisumle  15692  trilpolemeq1  15694  trilpolemlt1  15695  trirec0  15698  apdiff  15702  redc0  15711  reap0  15712  dceqnconst  15714  dcapnconst  15715  nconstwlpolemgt0  15718  neap0mkv  15723