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  8454  ine0  8722  ltaddneg  8753  addgt0  8777  addgegt0  8778  addgtge0  8779  addge0  8780  ltaddpos  8781  ltneg  8791  leneg  8794  lt0neg1  8797  lt0neg2  8798  le0neg1  8799  le0neg2  8800  addge01  8801  suble0  8805  0le1  8810  gt0ne0i  8815  gt0ne0d  8841  lt0ne0d  8842  recexre  8908  recexgt0  8910  inelr  8914  rimul  8915  1ap0  8920  reapmul1  8925  apsqgt0  8931  msqge0  8946  mulge0  8949  recexaplem2  8982  recexap  8983  rerecclap  9062  ltm1  9178  recgt0  9182  ltmul12a  9192  lemul12a  9194  mulgt1  9195  gt0div  9202  ge0div  9203  recgt1i  9230  recreclt  9232  sup3exmid  9289  crap0  9290  indfval  9301  indconst0  9304  nnge1  9329  nngt0  9331  nnrecgt0  9344  0ne1  9373  0le0  9395  neg1lt0  9414  halfge0  9525  iap0  9532  nn0ssre  9571  nn0ge0  9592  nn0nlt0  9593  nn0le0eq0  9595  0mnnnnn0  9599  elnnnn0b  9611  elnnnn0c  9612  elnnz  9658  0z  9659  elnnz1  9671  nn0lt10b  9730  recnz  9743  gtndiv  9745  fnn0ind  9766  rpge0  10077  rpnegap  10097  0nrp  10100  0ltpnf  10194  mnflt0  10196  xneg0  10243  xaddid1  10274  xnn0xadd0  10279  xposdif  10294  elrege0  10388  0e0icopnf  10391  0elunit  10398  1elunit  10399  divelunit  10414  lincmb01cmp  10415  lincmble  10416  iccf1o  10417  unitssre  10418  fz0to4untppr  10541  nn0p1elfzo  10604  modqelico  10784  modqmuladdim  10817  addmodid  10822  xnn0nnen  10887  expubnd  11046  le2sq2  11065  resq01  11108  bernneq2  11112  expnbnd  11114  expnlbnd  11115  faclbnd  11193  faclbnd3  11195  faclbnd6  11196  bcval4  11204  bcpasc  11218  lsw0  11366  swrdccatin2  11515  pfxccatin12lem3  11518  reim0  11640  re0  11675  im0  11676  rei  11679  imi  11680  cj0  11681  caucvgre  11761  rennim  11782  sqrt0rlem  11783  sqrt0  11784  resqrexlemdecn  11792  resqrexlemnm  11798  resqrexlemgt0  11800  sqrt00  11820  sqrt9  11828  sqrt2gt1lt2  11829  leabs  11854  ltabs  11868  sqrtpclii  11911  max0addsup  12000  fimaxre2  12008  climge0  12107  iserge0  12125  fsum00  12245  arisum2  12282  0.999...  12304  fprodge0  12420  cos0  12513  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  cos2bnd  12543  sin01gt0  12545  cos01gt0  12546  sincos2sgn  12549  sin4lt0  12550  absef  12553  absefib  12554  efieq1re  12555  epos  12564  flodddiv4  12719  gcdn0gt0  12771  nn0seqcvgd  12835  algcvgblem  12843  algcvga  12845  pythagtriplem12  13074  pythagtriplem13  13075  pythagtriplem14  13076  pythagtriplem16  13078  ballotfilem2  13277  ballotfilem4  13290  ballotfilemi1  13294  ballotfilemic  13299  mulgnegnn  13984  ssblps  15575  ssbl  15576  xmeter  15586  cnbl0  15684  hovera  15797  hovergt0  15800  plyrecj  15913  reeff1olem  15921  efap1p  15929  pilem3  15934  pipos  15939  sinhalfpilem  15942  sincosq1sgn  15977  sincosq2sgn  15978  sinq34lt0t  15982  coseq0q4123  15985  coseq00topi  15986  coseq0negpitopi  15987  tangtx  15989  sincos4thpi  15991  sincos6thpi  15993  cosordlem  16000  cosq34lt1  16001  cos02pilt1  16002  cos0pilt1  16003  cos11  16004  ioocosf1o  16005  log1  16017  logrpap0b  16028  logdivlti  16033  rpabscxpbnd  16095  log2tlbndlog2  16139  log2ublog2  16143  ppiqsval  16156  ppiqub  16194  bposlem4  16212  bposlem5  16213  lgsval2lem  16227  lgsval4a  16239  lgsneg  16241  lgsdilem  16244  lgsdir2lem1  16245  clwwlkn0  16747  konigsberg  16832  ex-gcd  16843  repiecelem  17172  repiecele0  17173  repiecege0  17174  trilpolemclim  17183  trilpolemcl  17184  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  trirec0  17191  apdiff  17195  redc0  17205  reap0  17206  dceqnconst  17208  dcapnconst  17209  nconstwlpolemgt0  17212  neap0mkv  17217