Theorem 0re 8169

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

Syntax hints:   = wceq 1395   ∈ wcel 2200  ∃wrex 2509  (class class class)co 6013  ℝcr 8021  0cc0 8022  1c1 8023   + caddc 8025

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8116  ax-addrcl 8119  ax-rnegex 8131

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-ral 2513  df-rex 2514

This theorem is referenced by:  0red  8170  0xr  8216  axmulgt0  8241  gtso  8248  0lt1  8296  ine0  8563  ltaddneg  8594  addgt0  8618  addgegt0  8619  addgtge0  8620  addge0  8621  ltaddpos  8622  ltneg  8632  leneg  8635  lt0neg1  8638  lt0neg2  8639  le0neg1  8640  le0neg2  8641  addge01  8642  suble0  8646  0le1  8651  gt0ne0i  8656  gt0ne0d  8682  lt0ne0d  8683  recexre  8748  recexgt0  8750  inelr  8754  rimul  8755  1ap0  8760  reapmul1  8765  apsqgt0  8771  msqge0  8786  mulge0  8789  recexaplem2  8822  recexap  8823  rerecclap  8900  ltm1  9016  recgt0  9020  ltmul12a  9030  lemul12a  9032  mulgt1  9033  gt0div  9040  ge0div  9041  recgt1i  9068  recreclt  9070  sup3exmid  9127  crap0  9128  nnge1  9156  nngt0  9158  nnrecgt0  9171  0ne1  9200  0le0  9222  neg1lt0  9241  halfge0  9350  iap0  9357  nn0ssre  9396  nn0ge0  9417  nn0nlt0  9418  nn0le0eq0  9420  0mnnnnn0  9424  elnnnn0b  9436  elnnnn0c  9437  elnnz  9479  0z  9480  elnnz1  9492  nn0lt10b  9550  recnz  9563  gtndiv  9565  fnn0ind  9586  rpge0  9891  rpnegap  9911  0nrp  9914  0ltpnf  10007  mnflt0  10009  xneg0  10056  xaddid1  10087  xnn0xadd0  10092  xposdif  10107  elrege0  10201  0e0icopnf  10204  0elunit  10211  1elunit  10212  divelunit  10227  lincmb01cmp  10228  iccf1o  10229  unitssre  10230  fz0to4untppr  10349  modqelico  10586  modqmuladdim  10619  addmodid  10624  xnn0nnen  10689  expubnd  10848  le2sq2  10867  bernneq2  10913  expnbnd  10915  expnlbnd  10916  faclbnd  10993  faclbnd3  10995  faclbnd6  10996  bcval4  11004  bcpasc  11018  lsw0  11151  swrdccatin2  11300  pfxccatin12lem3  11303  reim0  11412  re0  11446  im0  11447  rei  11450  imi  11451  cj0  11452  caucvgre  11532  rennim  11553  sqrt0rlem  11554  sqrt0  11555  resqrexlemdecn  11563  resqrexlemnm  11569  resqrexlemgt0  11571  sqrt00  11591  sqrt9  11599  sqrt2gt1lt2  11600  leabs  11625  ltabs  11638  sqrtpclii  11681  max0addsup  11770  fimaxre2  11778  climge0  11876  iserge0  11894  fsum00  12013  arisum2  12050  0.999...  12072  fprodge0  12188  cos0  12281  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  cos2bnd  12311  sin01gt0  12313  cos01gt0  12314  sincos2sgn  12317  sin4lt0  12318  absef  12321  absefib  12322  efieq1re  12323  epos  12332  flodddiv4  12487  gcdn0gt0  12539  nn0seqcvgd  12603  algcvgblem  12611  algcvga  12613  pythagtriplem12  12838  pythagtriplem13  12839  pythagtriplem14  12840  pythagtriplem16  12842  mulgnegnn  13709  ssblps  15139  ssbl  15140  xmeter  15150  cnbl0  15248  hovera  15361  hovergt0  15364  plyrecj  15477  reeff1olem  15485  pilem3  15497  pipos  15502  sinhalfpilem  15505  sincosq1sgn  15540  sincosq2sgn  15541  sinq34lt0t  15545  coseq0q4123  15548  coseq00topi  15549  coseq0negpitopi  15550  tangtx  15552  sincos4thpi  15554  sincos6thpi  15556  cosordlem  15563  cosq34lt1  15564  cos02pilt1  15565  cos0pilt1  15566  cos11  15567  ioocosf1o  15568  log1  15580  logrpap0b  15590  logdivlti  15595  rpabscxpbnd  15654  lgsval2lem  15729  lgsval4a  15741  lgsneg  15743  lgsdilem  15746  lgsdir2lem1  15747  clwwlkn0  16203  ex-gcd  16263  trilpolemclim  16576  trilpolemcl  16577  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  trirec0  16584  apdiff  16588  redc0  16597  reap0  16598  dceqnconst  16600  dcapnconst  16601  nconstwlpolemgt0  16604  neap0mkv  16609