Theorem 0re 8071

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

Syntax hints:   = wceq 1372   ∈ wcel 2175  ∃wrex 2484  (class class class)co 5943  ℝcr 7923  0cc0 7924  1c1 7925   + caddc 7927

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-1re 8018  ax-addrcl 8021  ax-rnegex 8033

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-cleq 2197  df-clel 2200  df-ral 2488  df-rex 2489

This theorem is referenced by:  0red  8072  0xr  8118  axmulgt0  8143  gtso  8150  0lt1  8198  ine0  8465  ltaddneg  8496  addgt0  8520  addgegt0  8521  addgtge0  8522  addge0  8523  ltaddpos  8524  ltneg  8534  leneg  8537  lt0neg1  8540  lt0neg2  8541  le0neg1  8542  le0neg2  8543  addge01  8544  suble0  8548  0le1  8553  gt0ne0i  8558  gt0ne0d  8584  lt0ne0d  8585  recexre  8650  recexgt0  8652  inelr  8656  rimul  8657  1ap0  8662  reapmul1  8667  apsqgt0  8673  msqge0  8688  mulge0  8691  recexaplem2  8724  recexap  8725  rerecclap  8802  ltm1  8918  recgt0  8922  ltmul12a  8932  lemul12a  8934  mulgt1  8935  gt0div  8942  ge0div  8943  recgt1i  8970  recreclt  8972  sup3exmid  9029  crap0  9030  nnge1  9058  nngt0  9060  nnrecgt0  9073  0ne1  9102  0le0  9124  neg1lt0  9143  halfge0  9252  iap0  9259  nn0ssre  9298  nn0ge0  9319  nn0nlt0  9320  nn0le0eq0  9322  0mnnnnn0  9326  elnnnn0b  9338  elnnnn0c  9339  elnnz  9381  0z  9382  elnnz1  9394  nn0lt10b  9452  recnz  9465  gtndiv  9467  fnn0ind  9488  rpge0  9787  rpnegap  9807  0nrp  9810  0ltpnf  9903  mnflt0  9905  xneg0  9952  xaddid1  9983  xnn0xadd0  9988  xposdif  10003  elrege0  10097  0e0icopnf  10100  0elunit  10107  1elunit  10108  divelunit  10123  lincmb01cmp  10124  iccf1o  10125  unitssre  10126  fz0to4untppr  10245  modqelico  10477  modqmuladdim  10510  addmodid  10515  xnn0nnen  10580  expubnd  10739  le2sq2  10758  bernneq2  10804  expnbnd  10806  expnlbnd  10807  faclbnd  10884  faclbnd3  10886  faclbnd6  10887  bcval4  10895  bcpasc  10909  lsw0  11039  reim0  11143  re0  11177  im0  11178  rei  11181  imi  11182  cj0  11183  caucvgre  11263  rennim  11284  sqrt0rlem  11285  sqrt0  11286  resqrexlemdecn  11294  resqrexlemnm  11300  resqrexlemgt0  11302  sqrt00  11322  sqrt9  11330  sqrt2gt1lt2  11331  leabs  11356  ltabs  11369  sqrtpclii  11412  max0addsup  11501  fimaxre2  11509  climge0  11607  iserge0  11625  fsum00  11744  arisum2  11781  0.999...  11803  fprodge0  11919  cos0  12012  ef01bndlem  12038  sin01bnd  12039  cos01bnd  12040  cos2bnd  12042  sin01gt0  12044  cos01gt0  12045  sincos2sgn  12048  sin4lt0  12049  absef  12052  absefib  12053  efieq1re  12054  epos  12063  flodddiv4  12218  gcdn0gt0  12270  nn0seqcvgd  12334  algcvgblem  12342  algcvga  12344  pythagtriplem12  12569  pythagtriplem13  12570  pythagtriplem14  12571  pythagtriplem16  12573  mulgnegnn  13439  ssblps  14868  ssbl  14869  xmeter  14879  cnbl0  14977  hovera  15090  hovergt0  15093  plyrecj  15206  reeff1olem  15214  pilem3  15226  pipos  15231  sinhalfpilem  15234  sincosq1sgn  15269  sincosq2sgn  15270  sinq34lt0t  15274  coseq0q4123  15277  coseq00topi  15278  coseq0negpitopi  15279  tangtx  15281  sincos4thpi  15283  sincos6thpi  15285  cosordlem  15292  cosq34lt1  15293  cos02pilt1  15294  cos0pilt1  15295  cos11  15296  ioocosf1o  15297  log1  15309  logrpap0b  15319  logdivlti  15324  rpabscxpbnd  15383  lgsval2lem  15458  lgsval4a  15470  lgsneg  15472  lgsdilem  15475  lgsdir2lem1  15476  ex-gcd  15629  trilpolemclim  15937  trilpolemcl  15938  trilpolemisumle  15939  trilpolemeq1  15941  trilpolemlt1  15942  trirec0  15945  apdiff  15949  redc0  15958  reap0  15959  dceqnconst  15961  dcapnconst  15962  nconstwlpolemgt0  15965  neap0mkv  15970