Theorem 0re 8178

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 8177	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 8140	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 8157	. . . . 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 2644	. 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
8	1, 2, 7	mp2b 8	1 ⊢ 0 ∈ ℝ

Syntax hints:   = wceq 1397   ∈ wcel 2202  ∃wrex 2511  (class class class)co 6017  ℝcr 8030  0cc0 8031  1c1 8032   + caddc 8034

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583  ax-ext 2213  ax-1re 8125  ax-addrcl 8128  ax-rnegex 8140

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

This theorem is referenced by:  0red  8179  0xr  8225  axmulgt0  8250  gtso  8257  0lt1  8305  ine0  8572  ltaddneg  8603  addgt0  8627  addgegt0  8628  addgtge0  8629  addge0  8630  ltaddpos  8631  ltneg  8641  leneg  8644  lt0neg1  8647  lt0neg2  8648  le0neg1  8649  le0neg2  8650  addge01  8651  suble0  8655  0le1  8660  gt0ne0i  8665  gt0ne0d  8691  lt0ne0d  8692  recexre  8757  recexgt0  8759  inelr  8763  rimul  8764  1ap0  8769  reapmul1  8774  apsqgt0  8780  msqge0  8795  mulge0  8798  recexaplem2  8831  recexap  8832  rerecclap  8909  ltm1  9025  recgt0  9029  ltmul12a  9039  lemul12a  9041  mulgt1  9042  gt0div  9049  ge0div  9050  recgt1i  9077  recreclt  9079  sup3exmid  9136  crap0  9137  nnge1  9165  nngt0  9167  nnrecgt0  9180  0ne1  9209  0le0  9231  neg1lt0  9250  halfge0  9359  iap0  9366  nn0ssre  9405  nn0ge0  9426  nn0nlt0  9427  nn0le0eq0  9429  0mnnnnn0  9433  elnnnn0b  9445  elnnnn0c  9446  elnnz  9488  0z  9489  elnnz1  9501  nn0lt10b  9559  recnz  9572  gtndiv  9574  fnn0ind  9595  rpge0  9900  rpnegap  9920  0nrp  9923  0ltpnf  10016  mnflt0  10018  xneg0  10065  xaddid1  10096  xnn0xadd0  10101  xposdif  10116  elrege0  10210  0e0icopnf  10213  0elunit  10220  1elunit  10221  divelunit  10236  lincmb01cmp  10237  iccf1o  10238  unitssre  10239  fz0to4untppr  10358  modqelico  10595  modqmuladdim  10628  addmodid  10633  xnn0nnen  10698  expubnd  10857  le2sq2  10876  bernneq2  10922  expnbnd  10924  expnlbnd  10925  faclbnd  11002  faclbnd3  11004  faclbnd6  11005  bcval4  11013  bcpasc  11027  lsw0  11160  swrdccatin2  11309  pfxccatin12lem3  11312  reim0  11421  re0  11455  im0  11456  rei  11459  imi  11460  cj0  11461  caucvgre  11541  rennim  11562  sqrt0rlem  11563  sqrt0  11564  resqrexlemdecn  11572  resqrexlemnm  11578  resqrexlemgt0  11580  sqrt00  11600  sqrt9  11608  sqrt2gt1lt2  11609  leabs  11634  ltabs  11647  sqrtpclii  11690  max0addsup  11779  fimaxre2  11787  climge0  11885  iserge0  11903  fsum00  12022  arisum2  12059  0.999...  12081  fprodge0  12197  cos0  12290  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  cos2bnd  12320  sin01gt0  12322  cos01gt0  12323  sincos2sgn  12326  sin4lt0  12327  absef  12330  absefib  12331  efieq1re  12332  epos  12341  flodddiv4  12496  gcdn0gt0  12548  nn0seqcvgd  12612  algcvgblem  12620  algcvga  12622  pythagtriplem12  12847  pythagtriplem13  12848  pythagtriplem14  12849  pythagtriplem16  12851  mulgnegnn  13718  ssblps  15148  ssbl  15149  xmeter  15159  cnbl0  15257  hovera  15370  hovergt0  15373  plyrecj  15486  reeff1olem  15494  pilem3  15506  pipos  15511  sinhalfpilem  15514  sincosq1sgn  15549  sincosq2sgn  15550  sinq34lt0t  15554  coseq0q4123  15557  coseq00topi  15558  coseq0negpitopi  15559  tangtx  15561  sincos4thpi  15563  sincos6thpi  15565  cosordlem  15572  cosq34lt1  15573  cos02pilt1  15574  cos0pilt1  15575  cos11  15576  ioocosf1o  15577  log1  15589  logrpap0b  15599  logdivlti  15604  rpabscxpbnd  15663  lgsval2lem  15738  lgsval4a  15750  lgsneg  15752  lgsdilem  15755  lgsdir2lem1  15756  clwwlkn0  16258  ex-gcd  16327  trilpolemclim  16640  trilpolemcl  16641  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  trirec0  16648  apdiff  16652  redc0  16661  reap0  16662  dceqnconst  16664  dcapnconst  16665  nconstwlpolemgt0  16668  neap0mkv  16673