Theorem 0re 8332

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 8331	. 2 ⊢ 1 ∈ ℝ
2		ax-rnegex 8294	. 2 ⊢ (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3		readdcl 8311	. . . . 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 6088  ℝcr 8184  0cc0 8185  1c1 8186   + caddc 8188

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 8279  ax-addrcl 8282  ax-rnegex 8294

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  8333  0xr  8378  axmulgt0  8403  gtso  8410  0lt1  8460  ine0  8728  ltaddneg  8759  addgt0  8783  addgegt0  8784  addgtge0  8785  addge0  8786  ltaddpos  8787  ltneg  8797  leneg  8800  lt0neg1  8803  lt0neg2  8804  le0neg1  8805  le0neg2  8806  addge01  8807  suble0  8811  0le1  8816  gt0ne0i  8821  gt0ne0d  8847  lt0ne0d  8848  recexre  8914  recexgt0  8916  inelr  8920  rimul  8921  1ap0  8926  reapmul1  8931  apsqgt0  8937  msqge0  8952  mulge0  8955  recexaplem2  8988  recexap  8989  rerecclap  9068  ltm1  9184  recgt0  9188  ltmul12a  9198  lemul12a  9200  mulgt1  9201  gt0div  9208  ge0div  9209  recgt1i  9236  recreclt  9238  sup3exmid  9295  crap0  9296  indfval  9308  indconst0  9311  nnge1  9336  nngt0  9338  nnrecgt0  9351  0ne1  9380  0le0  9402  neg1lt0  9421  halfge0  9532  iap0  9539  nn0ssre  9578  nn0ge0  9599  nn0nlt0  9600  nn0le0eq0  9602  0mnnnnn0  9606  elnnnn0b  9618  elnnnn0c  9619  elnnz  9665  0z  9666  elnnz1  9678  nn0lt10b  9737  recnz  9750  gtndiv  9752  fnn0ind  9773  rpge0  10084  rpnegap  10104  0nrp  10107  0ltpnf  10201  mnflt0  10203  xneg0  10250  xaddid1  10281  xnn0xadd0  10286  xposdif  10301  elrege0  10395  0e0icopnf  10398  0elunit  10405  1elunit  10406  divelunit  10421  lincmb01cmp  10422  lincmble  10423  iccf1o  10424  unitssre  10425  fz0to4untppr  10548  nn0p1elfzo  10611  modqelico  10792  modqmuladdim  10825  addmodid  10830  xnn0nnen  10895  expubnd  11054  le2sq2  11073  resq01  11116  bernneq2  11120  expnbnd  11122  expnlbnd  11123  faclbnd  11201  faclbnd3  11203  faclbnd6  11204  bcval4  11212  bcpasc  11226  lsw0  11374  swrdccatin2  11523  pfxccatin12lem3  11526  reim0  11648  re0  11683  im0  11684  rei  11687  imi  11688  cj0  11689  caucvgre  11769  rennim  11790  sqrt0rlem  11791  sqrt0  11792  resqrexlemdecn  11800  resqrexlemnm  11806  resqrexlemgt0  11808  sqrt00  11828  sqrt9  11836  sqrt2gt1lt2  11837  leabs  11862  ltabs  11876  sqrtpclii  11919  max0addsup  12008  fimaxre2  12016  climge0  12116  iserge0  12134  fsum00  12254  arisum2  12291  0.999...  12313  fprodge0  12429  cos0  12522  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  cos2bnd  12552  sin01gt0  12554  cos01gt0  12555  sincos2sgn  12558  sin4lt0  12559  absef  12562  absefib  12563  efieq1re  12564  epos  12573  flodddiv4  12728  gcdn0gt0  12780  nn0seqcvgd  12844  algcvgblem  12852  algcvga  12854  pythagtriplem12  13083  pythagtriplem13  13084  pythagtriplem14  13085  pythagtriplem16  13087  ballotfilem2  13286  ballotfilem4  13299  ballotfilemi1  13303  ballotfilemic  13308  mulgnegnn  13994  ssblps  15651  ssbl  15652  xmeter  15662  cnbl0  15760  hovera  15873  hovergt0  15876  plyrecj  15989  reeff1olem  15997  efap1p  16005  pilem3  16010  pipos  16015  sinhalfpilem  16018  sincosq1sgn  16053  sincosq2sgn  16054  sinq34lt0t  16058  coseq0q4123  16061  coseq00topi  16062  coseq0negpitopi  16063  tangtx  16065  sincos4thpi  16067  sincos6thpi  16069  cosordlem  16077  cosq34lt1  16078  cos02pilt1  16079  cos0pilt1  16080  cos11  16081  ioocosf1o  16082  log1  16095  logrpap0b  16106  logdivlti  16111  rpabscxpbnd  16175  log2tlbndlog2  16220  log2ublog2  16224  efnnfsumcl  16239  ppiqsval  16240  efchtqdvds  16265  ppiqub  16293  chtqleppi  16294  bposlem4  16314  bposlem5  16315  bposlem7  16317  bposlem8  16318  bposlem9  16319  lgsval2lem  16334  lgsval4a  16346  lgsneg  16348  lgsdilem  16351  lgsdir2lem1  16352  clwwlkn0  16854  konigsberg  16939  ex-gcd  16950  repiecelem  17280  repiecele0  17281  repiecege0  17282  trilpolemclim  17292  trilpolemcl  17293  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  trirec0  17300  apdiff  17304  redc0  17314  reap0  17315  dceqnconst  17317  dcapnconst  17318  nconstwlpolemgt0  17321  neap0mkv  17326