Theorem 0re 8157

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

Syntax hints:   = wceq 1395   ∈ wcel 2200  ∃wrex 2509  (class class class)co 6007  ℝcr 8009  0cc0 8010  1c1 8011   + caddc 8013

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8104  ax-addrcl 8107  ax-rnegex 8119

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-ral 2513  df-rex 2514

This theorem is referenced by:  0red  8158  0xr  8204  axmulgt0  8229  gtso  8236  0lt1  8284  ine0  8551  ltaddneg  8582  addgt0  8606  addgegt0  8607  addgtge0  8608  addge0  8609  ltaddpos  8610  ltneg  8620  leneg  8623  lt0neg1  8626  lt0neg2  8627  le0neg1  8628  le0neg2  8629  addge01  8630  suble0  8634  0le1  8639  gt0ne0i  8644  gt0ne0d  8670  lt0ne0d  8671  recexre  8736  recexgt0  8738  inelr  8742  rimul  8743  1ap0  8748  reapmul1  8753  apsqgt0  8759  msqge0  8774  mulge0  8777  recexaplem2  8810  recexap  8811  rerecclap  8888  ltm1  9004  recgt0  9008  ltmul12a  9018  lemul12a  9020  mulgt1  9021  gt0div  9028  ge0div  9029  recgt1i  9056  recreclt  9058  sup3exmid  9115  crap0  9116  nnge1  9144  nngt0  9146  nnrecgt0  9159  0ne1  9188  0le0  9210  neg1lt0  9229  halfge0  9338  iap0  9345  nn0ssre  9384  nn0ge0  9405  nn0nlt0  9406  nn0le0eq0  9408  0mnnnnn0  9412  elnnnn0b  9424  elnnnn0c  9425  elnnz  9467  0z  9468  elnnz1  9480  nn0lt10b  9538  recnz  9551  gtndiv  9553  fnn0ind  9574  rpge0  9874  rpnegap  9894  0nrp  9897  0ltpnf  9990  mnflt0  9992  xneg0  10039  xaddid1  10070  xnn0xadd0  10075  xposdif  10090  elrege0  10184  0e0icopnf  10187  0elunit  10194  1elunit  10195  divelunit  10210  lincmb01cmp  10211  iccf1o  10212  unitssre  10213  fz0to4untppr  10332  modqelico  10568  modqmuladdim  10601  addmodid  10606  xnn0nnen  10671  expubnd  10830  le2sq2  10849  bernneq2  10895  expnbnd  10897  expnlbnd  10898  faclbnd  10975  faclbnd3  10977  faclbnd6  10978  bcval4  10986  bcpasc  11000  lsw0  11132  swrdccatin2  11276  pfxccatin12lem3  11279  reim0  11387  re0  11421  im0  11422  rei  11425  imi  11426  cj0  11427  caucvgre  11507  rennim  11528  sqrt0rlem  11529  sqrt0  11530  resqrexlemdecn  11538  resqrexlemnm  11544  resqrexlemgt0  11546  sqrt00  11566  sqrt9  11574  sqrt2gt1lt2  11575  leabs  11600  ltabs  11613  sqrtpclii  11656  max0addsup  11745  fimaxre2  11753  climge0  11851  iserge0  11869  fsum00  11988  arisum2  12025  0.999...  12047  fprodge0  12163  cos0  12256  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  cos2bnd  12286  sin01gt0  12288  cos01gt0  12289  sincos2sgn  12292  sin4lt0  12293  absef  12296  absefib  12297  efieq1re  12298  epos  12307  flodddiv4  12462  gcdn0gt0  12514  nn0seqcvgd  12578  algcvgblem  12586  algcvga  12588  pythagtriplem12  12813  pythagtriplem13  12814  pythagtriplem14  12815  pythagtriplem16  12817  mulgnegnn  13684  ssblps  15114  ssbl  15115  xmeter  15125  cnbl0  15223  hovera  15336  hovergt0  15339  plyrecj  15452  reeff1olem  15460  pilem3  15472  pipos  15477  sinhalfpilem  15480  sincosq1sgn  15515  sincosq2sgn  15516  sinq34lt0t  15520  coseq0q4123  15523  coseq00topi  15524  coseq0negpitopi  15525  tangtx  15527  sincos4thpi  15529  sincos6thpi  15531  cosordlem  15538  cosq34lt1  15539  cos02pilt1  15540  cos0pilt1  15541  cos11  15542  ioocosf1o  15543  log1  15555  logrpap0b  15565  logdivlti  15570  rpabscxpbnd  15629  lgsval2lem  15704  lgsval4a  15716  lgsneg  15718  lgsdilem  15721  lgsdir2lem1  15722  ex-gcd  16150  trilpolemclim  16464  trilpolemcl  16465  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  trirec0  16472  apdiff  16476  redc0  16485  reap0  16486  dceqnconst  16488  dcapnconst  16489  nconstwlpolemgt0  16492  neap0mkv  16497