Theorem 0re 8326

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 8325	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 8288	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 8305	. . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
4	1, 3	mpan 428	. . . 4 ⊢ (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5		eleq1 2301	. . . 4 ⊢ ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
6	4, 5	syl5ibcom 155	. . 3 ⊢ (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
7	6	rexlimiv 2662	. 2 ⊢ (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
8	1, 2, 7	mp2b 8	1 ⊢ 0 ∈ ℝ

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209  ∃wrex 2529  (class class class)co 6085  ℝcr 8178  0cc0 8179  1c1 8180   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8273  ax-addrcl 8276  ax-rnegex 8288

This proof depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-ral 2533  df-rex 2534

This theorem is used by:  0red  8327  0xr  8372  axmulgt0  8397  gtso  8404  0lt1  8453  ine0  8721  ltaddneg  8752  addgt0  8776  addgegt0  8777  addgtge0  8778  addge0  8779  ltaddpos  8780  ltneg  8790  leneg  8793  lt0neg1  8796  lt0neg2  8797  le0neg1  8798  le0neg2  8799  addge01  8800  suble0  8804  0le1  8809  gt0ne0i  8814  gt0ne0d  8840  lt0ne0d  8841  recexre  8906  recexgt0  8908  inelr  8912  rimul  8913  1ap0  8918  reapmul1  8923  apsqgt0  8929  msqge0  8944  mulge0  8947  recexaplem2  8980  recexap  8981  rerecclap  9060  ltm1  9176  recgt0  9180  ltmul12a  9190  lemul12a  9192  mulgt1  9193  gt0div  9200  ge0div  9201  recgt1i  9228  recreclt  9230  sup3exmid  9287  crap0  9288  indfval  9299  indconst0  9302  nnge1  9327  nngt0  9329  nnrecgt0  9342  0ne1  9371  0le0  9393  neg1lt0  9412  halfge0  9521  iap0  9528  nn0ssre  9567  nn0ge0  9588  nn0nlt0  9589  nn0le0eq0  9591  0mnnnnn0  9595  elnnnn0b  9607  elnnnn0c  9608  elnnz  9654  0z  9655  elnnz1  9667  nn0lt10b  9726  recnz  9739  gtndiv  9741  fnn0ind  9762  rpge0  10067  rpnegap  10087  0nrp  10090  0ltpnf  10184  mnflt0  10186  xneg0  10233  xaddid1  10264  xnn0xadd0  10269  xposdif  10284  elrege0  10378  0e0icopnf  10381  0elunit  10388  1elunit  10389  divelunit  10404  lincmb01cmp  10405  lincmble  10406  iccf1o  10407  unitssre  10408  fz0to4untppr  10531  nn0p1elfzo  10594  modqelico  10771  modqmuladdim  10804  addmodid  10809  xnn0nnen  10874  expubnd  11033  le2sq2  11052  resq01  11095  bernneq2  11099  expnbnd  11101  expnlbnd  11102  faclbnd  11179  faclbnd3  11181  faclbnd6  11182  bcval4  11190  bcpasc  11204  lsw0  11352  swrdccatin2  11501  pfxccatin12lem3  11504  reim0  11626  re0  11661  im0  11662  rei  11665  imi  11666  cj0  11667  caucvgre  11747  rennim  11768  sqrt0rlem  11769  sqrt0  11770  resqrexlemdecn  11778  resqrexlemnm  11784  resqrexlemgt0  11786  sqrt00  11806  sqrt9  11814  sqrt2gt1lt2  11815  leabs  11840  ltabs  11853  sqrtpclii  11896  max0addsup  11985  fimaxre2  11993  climge0  12091  iserge0  12109  fsum00  12229  arisum2  12266  0.999...  12288  fprodge0  12404  cos0  12497  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  cos2bnd  12527  sin01gt0  12529  cos01gt0  12530  sincos2sgn  12533  sin4lt0  12534  absef  12537  absefib  12538  efieq1re  12539  epos  12548  flodddiv4  12703  gcdn0gt0  12755  nn0seqcvgd  12819  algcvgblem  12827  algcvga  12829  pythagtriplem12  13054  pythagtriplem13  13055  pythagtriplem14  13056  pythagtriplem16  13058  ballotfilem2  13228  ballotfilem4  13241  ballotfilemi1  13245  ballotfilemic  13250  mulgnegnn  13935  ssblps  15526  ssbl  15527  xmeter  15537  cnbl0  15635  hovera  15748  hovergt0  15751  plyrecj  15864  reeff1olem  15872  pilem3  15884  pipos  15889  sinhalfpilem  15892  sincosq1sgn  15927  sincosq2sgn  15928  sinq34lt0t  15932  coseq0q4123  15935  coseq00topi  15936  coseq0negpitopi  15937  tangtx  15939  sincos4thpi  15941  sincos6thpi  15943  cosordlem  15950  cosq34lt1  15951  cos02pilt1  15952  cos0pilt1  15953  cos11  15954  ioocosf1o  15955  log1  15967  logrpap0b  15977  logdivlti  15982  rpabscxpbnd  16042  log2tlbndlog2  16082  log2ublog2  16086  lgsval2lem  16129  lgsval4a  16141  lgsneg  16143  lgsdilem  16146  lgsdir2lem1  16147  clwwlkn0  16649  konigsberg  16734  ex-gcd  16745  repiecelem  17074  repiecele0  17075  repiecege0  17076  trilpolemclim  17085  trilpolemcl  17086  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  trirec0  17093  apdiff  17097  redc0  17107  reap0  17108  dceqnconst  17110  dcapnconst  17111  nconstwlpolemgt0  17114  neap0mkv  17119