Theorem 0re 8092

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

Syntax hints:   = wceq 1373   ∈ wcel 2177  ∃wrex 2486  (class class class)co 5957  ℝcr 7944  0cc0 7945  1c1 7946   + caddc 7948

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-1re 8039  ax-addrcl 8042  ax-rnegex 8054

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-cleq 2199  df-clel 2202  df-ral 2490  df-rex 2491

This theorem is referenced by:  0red  8093  0xr  8139  axmulgt0  8164  gtso  8171  0lt1  8219  ine0  8486  ltaddneg  8517  addgt0  8541  addgegt0  8542  addgtge0  8543  addge0  8544  ltaddpos  8545  ltneg  8555  leneg  8558  lt0neg1  8561  lt0neg2  8562  le0neg1  8563  le0neg2  8564  addge01  8565  suble0  8569  0le1  8574  gt0ne0i  8579  gt0ne0d  8605  lt0ne0d  8606  recexre  8671  recexgt0  8673  inelr  8677  rimul  8678  1ap0  8683  reapmul1  8688  apsqgt0  8694  msqge0  8709  mulge0  8712  recexaplem2  8745  recexap  8746  rerecclap  8823  ltm1  8939  recgt0  8943  ltmul12a  8953  lemul12a  8955  mulgt1  8956  gt0div  8963  ge0div  8964  recgt1i  8991  recreclt  8993  sup3exmid  9050  crap0  9051  nnge1  9079  nngt0  9081  nnrecgt0  9094  0ne1  9123  0le0  9145  neg1lt0  9164  halfge0  9273  iap0  9280  nn0ssre  9319  nn0ge0  9340  nn0nlt0  9341  nn0le0eq0  9343  0mnnnnn0  9347  elnnnn0b  9359  elnnnn0c  9360  elnnz  9402  0z  9403  elnnz1  9415  nn0lt10b  9473  recnz  9486  gtndiv  9488  fnn0ind  9509  rpge0  9808  rpnegap  9828  0nrp  9831  0ltpnf  9924  mnflt0  9926  xneg0  9973  xaddid1  10004  xnn0xadd0  10009  xposdif  10024  elrege0  10118  0e0icopnf  10121  0elunit  10128  1elunit  10129  divelunit  10144  lincmb01cmp  10145  iccf1o  10146  unitssre  10147  fz0to4untppr  10266  modqelico  10501  modqmuladdim  10534  addmodid  10539  xnn0nnen  10604  expubnd  10763  le2sq2  10782  bernneq2  10828  expnbnd  10830  expnlbnd  10831  faclbnd  10908  faclbnd3  10910  faclbnd6  10911  bcval4  10919  bcpasc  10933  lsw0  11063  reim0  11247  re0  11281  im0  11282  rei  11285  imi  11286  cj0  11287  caucvgre  11367  rennim  11388  sqrt0rlem  11389  sqrt0  11390  resqrexlemdecn  11398  resqrexlemnm  11404  resqrexlemgt0  11406  sqrt00  11426  sqrt9  11434  sqrt2gt1lt2  11435  leabs  11460  ltabs  11473  sqrtpclii  11516  max0addsup  11605  fimaxre2  11613  climge0  11711  iserge0  11729  fsum00  11848  arisum2  11885  0.999...  11907  fprodge0  12023  cos0  12116  ef01bndlem  12142  sin01bnd  12143  cos01bnd  12144  cos2bnd  12146  sin01gt0  12148  cos01gt0  12149  sincos2sgn  12152  sin4lt0  12153  absef  12156  absefib  12157  efieq1re  12158  epos  12167  flodddiv4  12322  gcdn0gt0  12374  nn0seqcvgd  12438  algcvgblem  12446  algcvga  12448  pythagtriplem12  12673  pythagtriplem13  12674  pythagtriplem14  12675  pythagtriplem16  12677  mulgnegnn  13543  ssblps  14972  ssbl  14973  xmeter  14983  cnbl0  15081  hovera  15194  hovergt0  15197  plyrecj  15310  reeff1olem  15318  pilem3  15330  pipos  15335  sinhalfpilem  15338  sincosq1sgn  15373  sincosq2sgn  15374  sinq34lt0t  15378  coseq0q4123  15381  coseq00topi  15382  coseq0negpitopi  15383  tangtx  15385  sincos4thpi  15387  sincos6thpi  15389  cosordlem  15396  cosq34lt1  15397  cos02pilt1  15398  cos0pilt1  15399  cos11  15400  ioocosf1o  15401  log1  15413  logrpap0b  15423  logdivlti  15428  rpabscxpbnd  15487  lgsval2lem  15562  lgsval4a  15574  lgsneg  15576  lgsdilem  15579  lgsdir2lem1  15580  ex-gcd  15806  trilpolemclim  16116  trilpolemcl  16117  trilpolemisumle  16118  trilpolemeq1  16120  trilpolemlt1  16121  trirec0  16124  apdiff  16128  redc0  16137  reap0  16138  dceqnconst  16140  dcapnconst  16141  nconstwlpolemgt0  16144  neap0mkv  16149