Theorem 0re 7959

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

Syntax hints:   = wceq 1353   ∈ wcel 2148  ∃wrex 2456  (class class class)co 5877  ℝcr 7812  0cc0 7813  1c1 7814   + caddc 7816

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7907  ax-addrcl 7910  ax-rnegex 7922

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-cleq 2170  df-clel 2173  df-ral 2460  df-rex 2461

This theorem is referenced by:  0red  7960  0xr  8006  axmulgt0  8031  gtso  8038  0lt1  8086  ine0  8353  ltaddneg  8383  addgt0  8407  addgegt0  8408  addgtge0  8409  addge0  8410  ltaddpos  8411  ltneg  8421  leneg  8424  lt0neg1  8427  lt0neg2  8428  le0neg1  8429  le0neg2  8430  addge01  8431  suble0  8435  0le1  8440  gt0ne0i  8445  gt0ne0d  8471  lt0ne0d  8472  recexre  8537  recexgt0  8539  inelr  8543  rimul  8544  1ap0  8549  reapmul1  8554  apsqgt0  8560  msqge0  8575  mulge0  8578  recexaplem2  8611  recexap  8612  rerecclap  8689  ltm1  8805  recgt0  8809  ltmul12a  8819  lemul12a  8821  mulgt1  8822  gt0div  8829  ge0div  8830  recgt1i  8857  recreclt  8859  sup3exmid  8916  crap0  8917  nnge1  8944  nngt0  8946  nnrecgt0  8959  0ne1  8988  0le0  9010  neg1lt0  9029  halfge0  9137  iap0  9144  nn0ssre  9182  nn0ge0  9203  nn0nlt0  9204  nn0le0eq0  9206  0mnnnnn0  9210  elnnnn0b  9222  elnnnn0c  9223  elnnz  9265  0z  9266  elnnz1  9278  nn0lt10b  9335  recnz  9348  gtndiv  9350  fnn0ind  9371  rpge0  9668  rpnegap  9688  0nrp  9691  0ltpnf  9784  mnflt0  9786  xneg0  9833  xaddid1  9864  xnn0xadd0  9869  xposdif  9884  elrege0  9978  0e0icopnf  9981  0elunit  9988  1elunit  9989  divelunit  10004  lincmb01cmp  10005  iccf1o  10006  unitssre  10007  fz0to4untppr  10126  modqelico  10336  modqmuladdim  10369  addmodid  10374  expubnd  10579  le2sq2  10598  bernneq2  10644  expnbnd  10646  expnlbnd  10647  faclbnd  10723  faclbnd3  10725  faclbnd6  10726  bcval4  10734  bcpasc  10748  reim0  10872  re0  10906  im0  10907  rei  10910  imi  10911  cj0  10912  caucvgre  10992  rennim  11013  sqrt0rlem  11014  sqrt0  11015  resqrexlemdecn  11023  resqrexlemnm  11029  resqrexlemgt0  11031  sqrt00  11051  sqrt9  11059  sqrt2gt1lt2  11060  leabs  11085  ltabs  11098  sqrtpclii  11141  max0addsup  11230  fimaxre2  11237  climge0  11335  iserge0  11353  fsum00  11472  arisum2  11509  0.999...  11531  fprodge0  11647  cos0  11740  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  cos2bnd  11770  sin01gt0  11771  cos01gt0  11772  sincos2sgn  11775  sin4lt0  11776  absef  11779  absefib  11780  efieq1re  11781  epos  11790  flodddiv4  11941  gcdn0gt0  11981  nn0seqcvgd  12043  algcvgblem  12051  algcvga  12053  pythagtriplem12  12277  pythagtriplem13  12278  pythagtriplem14  12279  pythagtriplem16  12281  mulgnegnn  12998  ssblps  13964  ssbl  13965  xmeter  13975  cnbl0  14073  reeff1olem  14231  pilem3  14243  pipos  14248  sinhalfpilem  14251  sincosq1sgn  14286  sincosq2sgn  14287  sinq34lt0t  14291  coseq0q4123  14294  coseq00topi  14295  coseq0negpitopi  14296  tangtx  14298  sincos4thpi  14300  sincos6thpi  14302  cosordlem  14309  cosq34lt1  14310  cos02pilt1  14311  cos0pilt1  14312  cos11  14313  ioocosf1o  14314  log1  14326  logrpap0b  14336  logdivlti  14341  rpabscxpbnd  14398  lgsval2lem  14450  lgsval4a  14462  lgsneg  14464  lgsdilem  14467  lgsdir2lem1  14468  ex-gcd  14522  trilpolemclim  14823  trilpolemcl  14824  trilpolemisumle  14825  trilpolemeq1  14827  trilpolemlt1  14828  trirec0  14831  apdiff  14835  redc0  14844  reap0  14845  dceqnconst  14846  dcapnconst  14847  nconstwlpolemgt0  14850  neap0mkv  14855