Theorem 0re 8274

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

Syntax hints:   = wceq 1398   ∈ wcel 2203  ∃wrex 2521  (class class class)co 6050  ℝcr 8126  0cc0 8127  1c1 8128   + caddc 8130

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 2214  ax-1re 8221  ax-addrcl 8224  ax-rnegex 8236

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2225  df-clel 2228  df-ral 2525  df-rex 2526

This theorem is referenced by:  0red  8275  0xr  8320  axmulgt0  8345  gtso  8352  0lt1  8400  ine0  8667  ltaddneg  8698  addgt0  8722  addgegt0  8723  addgtge0  8724  addge0  8725  ltaddpos  8726  ltneg  8736  leneg  8739  lt0neg1  8742  lt0neg2  8743  le0neg1  8744  le0neg2  8745  addge01  8746  suble0  8750  0le1  8755  gt0ne0i  8760  gt0ne0d  8786  lt0ne0d  8787  recexre  8852  recexgt0  8854  inelr  8858  rimul  8859  1ap0  8864  reapmul1  8869  apsqgt0  8875  msqge0  8890  mulge0  8893  recexaplem2  8926  recexap  8927  rerecclap  9004  ltm1  9120  recgt0  9124  ltmul12a  9134  lemul12a  9136  mulgt1  9137  gt0div  9144  ge0div  9145  recgt1i  9172  recreclt  9174  sup3exmid  9231  crap0  9232  nnge1  9260  nngt0  9262  nnrecgt0  9275  0ne1  9304  0le0  9326  neg1lt0  9345  halfge0  9454  iap0  9461  nn0ssre  9500  nn0ge0  9521  nn0nlt0  9522  nn0le0eq0  9524  0mnnnnn0  9528  elnnnn0b  9540  elnnnn0c  9541  elnnz  9587  0z  9588  elnnz1  9600  nn0lt10b  9658  recnz  9671  gtndiv  9673  fnn0ind  9694  rpge0  9999  rpnegap  10019  0nrp  10022  0ltpnf  10115  mnflt0  10117  xneg0  10164  xaddid1  10195  xnn0xadd0  10200  xposdif  10215  elrege0  10309  0e0icopnf  10312  0elunit  10319  1elunit  10320  divelunit  10335  lincmb01cmp  10336  lincmble  10337  iccf1o  10338  unitssre  10339  fz0to4untppr  10458  nn0p1elfzo  10521  modqelico  10696  modqmuladdim  10729  addmodid  10734  xnn0nnen  10799  expubnd  10958  le2sq2  10977  bernneq2  11023  expnbnd  11025  expnlbnd  11026  faclbnd  11103  faclbnd3  11105  faclbnd6  11106  bcval4  11114  bcpasc  11128  lsw0  11272  swrdccatin2  11421  pfxccatin12lem3  11424  reim0  11546  re0  11580  im0  11581  rei  11584  imi  11585  cj0  11586  caucvgre  11666  rennim  11687  sqrt0rlem  11688  sqrt0  11689  resqrexlemdecn  11697  resqrexlemnm  11703  resqrexlemgt0  11705  sqrt00  11725  sqrt9  11733  sqrt2gt1lt2  11734  leabs  11759  ltabs  11772  sqrtpclii  11815  max0addsup  11904  fimaxre2  11912  climge0  12010  iserge0  12028  fsum00  12148  arisum2  12185  0.999...  12207  fprodge0  12323  cos0  12416  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  cos2bnd  12446  sin01gt0  12448  cos01gt0  12449  sincos2sgn  12452  sin4lt0  12453  absef  12456  absefib  12457  efieq1re  12458  epos  12467  flodddiv4  12622  gcdn0gt0  12674  nn0seqcvgd  12738  algcvgblem  12746  algcvga  12748  pythagtriplem12  12973  pythagtriplem13  12974  pythagtriplem14  12975  pythagtriplem16  12977  ballotfilem2  13142  mulgnegnn  13849  ssblps  15290  ssbl  15291  xmeter  15301  cnbl0  15399  hovera  15512  hovergt0  15515  plyrecj  15628  reeff1olem  15636  pilem3  15648  pipos  15653  sinhalfpilem  15656  sincosq1sgn  15691  sincosq2sgn  15692  sinq34lt0t  15696  coseq0q4123  15699  coseq00topi  15700  coseq0negpitopi  15701  tangtx  15703  sincos4thpi  15705  sincos6thpi  15707  cosordlem  15714  cosq34lt1  15715  cos02pilt1  15716  cos0pilt1  15717  cos11  15718  ioocosf1o  15719  log1  15731  logrpap0b  15741  logdivlti  15746  rpabscxpbnd  15805  lgsval2lem  15883  lgsval4a  15895  lgsneg  15897  lgsdilem  15900  lgsdir2lem1  15901  clwwlkn0  16403  konigsberg  16488  ex-gcd  16499  repiecelem  16809  repiecele0  16810  repiecege0  16811  trilpolemclim  16820  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  trirec0  16828  apdiff  16832  redc0  16842  reap0  16843  dceqnconst  16846  dcapnconst  16847  nconstwlpolemgt0  16850  neap0mkv  16855