Theorem 0re 7766

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 7765	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 7729	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 7746	. . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
4	1, 3	mpan 420	. . . 4 ⊢ (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5		eleq1 2202	. . . 4 ⊢ ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 154	. . 3 ⊢ (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
7	6	rexlimiv 2543	. 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
8	1, 2, 7	mp2b 8	1 ⊢ 0 ∈ ℝ

Syntax hints:   = wceq 1331   ∈ wcel 1480  ∃wrex 2417  (class class class)co 5774  ℝcr 7619  0cc0 7620  1c1 7621   + caddc 7623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-1re 7714  ax-addrcl 7717  ax-rnegex 7729

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-cleq 2132  df-clel 2135  df-ral 2421  df-rex 2422

This theorem is referenced by:  0red  7767  0xr  7812  axmulgt0  7836  gtso  7843  0lt1  7889  ine0  8156  ltaddneg  8186  addgt0  8210  addgegt0  8211  addgtge0  8212  addge0  8213  ltaddpos  8214  ltneg  8224  leneg  8227  lt0neg1  8230  lt0neg2  8231  le0neg1  8232  le0neg2  8233  addge01  8234  suble0  8238  0le1  8243  gt0ne0i  8248  gt0ne0d  8274  lt0ne0d  8275  recexre  8340  recexgt0  8342  inelr  8346  rimul  8347  1ap0  8352  reapmul1  8357  apsqgt0  8363  msqge0  8378  mulge0  8381  recexaplem2  8413  recexap  8414  rerecclap  8490  ltm1  8604  recgt0  8608  ltmul12a  8618  lemul12a  8620  mulgt1  8621  gt0div  8628  ge0div  8629  recgt1i  8656  recreclt  8658  sup3exmid  8715  crap0  8716  nnge1  8743  nngt0  8745  nnrecgt0  8758  0ne1  8787  0le0  8809  neg1lt0  8828  halfge0  8936  iap0  8943  nn0ssre  8981  nn0ge0  9002  nn0nlt0  9003  nn0le0eq0  9005  0mnnnnn0  9009  elnnnn0b  9021  elnnnn0c  9022  elnnz  9064  0z  9065  elnnz1  9077  nn0lt10b  9131  recnz  9144  gtndiv  9146  fnn0ind  9167  rpge0  9454  rpnegap  9474  0nrp  9477  0ltpnf  9568  mnflt0  9570  xneg0  9614  xaddid1  9645  xnn0xadd0  9650  xposdif  9665  elrege0  9759  0e0icopnf  9762  0elunit  9769  1elunit  9770  divelunit  9785  lincmb01cmp  9786  iccf1o  9787  unitssre  9788  modqelico  10107  modqmuladdim  10140  addmodid  10145  expubnd  10350  le2sq2  10368  bernneq2  10413  expnbnd  10415  expnlbnd  10416  faclbnd  10487  faclbnd3  10489  faclbnd6  10490  bcval4  10498  bcpasc  10512  reim0  10633  re0  10667  im0  10668  rei  10671  imi  10672  cj0  10673  caucvgre  10753  rennim  10774  sqrt0rlem  10775  sqrt0  10776  resqrexlemdecn  10784  resqrexlemnm  10790  resqrexlemgt0  10792  sqrt00  10812  sqrt9  10820  sqrt2gt1lt2  10821  leabs  10846  ltabs  10859  sqrtpclii  10902  max0addsup  10991  fimaxre2  10998  climge0  11094  iserge0  11112  fsum00  11231  arisum2  11268  0.999...  11290  cos0  11437  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  cos2bnd  11467  sin01gt0  11468  cos01gt0  11469  sincos2sgn  11472  sin4lt0  11473  absef  11476  absefib  11477  efieq1re  11478  epos  11487  flodddiv4  11631  gcdn0gt0  11666  nn0seqcvgd  11722  algcvgblem  11730  algcvga  11732  ssblps  12594  ssbl  12595  xmeter  12605  cnbl0  12703  pilem3  12864  pipos  12869  sinhalfpilem  12872  sincosq1sgn  12907  sincosq2sgn  12908  sinq34lt0t  12912  coseq0q4123  12915  coseq00topi  12916  coseq0negpitopi  12917  tangtx  12919  sincos4thpi  12921  sincos6thpi  12923  cosordlem  12930  cosq34lt1  12931  cos02pilt1  12932  ex-gcd  12943  trilpolemclim  13229  trilpolemcl  13230  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234