ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0re GIF version

Theorem 0re 7055
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
StepHypRef Expression
1 1re 7054 . 2 1 ∈ ℝ
2 ax-rnegex 7021 . 2 (1 ∈ ℝ → ∃𝑥 ∈ ℝ (1 + 𝑥) = 0)
3 readdcl 7035 . . . . 5 ((1 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (1 + 𝑥) ∈ ℝ)
41, 3mpan 408 . . . 4 (𝑥 ∈ ℝ → (1 + 𝑥) ∈ ℝ)
5 eleq1 2114 . . . 4 ((1 + 𝑥) = 0 → ((1 + 𝑥) ∈ ℝ ↔ 0 ∈ ℝ))
64, 5syl5ibcom 148 . . 3 (𝑥 ∈ ℝ → ((1 + 𝑥) = 0 → 0 ∈ ℝ))
76rexlimiv 2442 . 2 (∃𝑥 ∈ ℝ (1 + 𝑥) = 0 → 0 ∈ ℝ)
81, 2, 7mp2b 8 1 0 ∈ ℝ
Colors of variables: wff set class
Syntax hints:   = wceq 1257  wcel 1407  wrex 2322  (class class class)co 5537  cr 6916  0cc0 6917  1c1 6918   + caddc 6920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1350  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-4 1414  ax-17 1433  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-1re 7006  ax-addrcl 7009  ax-rnegex 7021
This theorem depends on definitions:  df-bi 114  df-nf 1364  df-cleq 2047  df-clel 2050  df-ral 2326  df-rex 2327
This theorem is referenced by:  0red  7056  0xr  7101  axmulgt0  7120  gtso  7126  0lt1  7172  ine0  7433  ltaddneg  7463  addgt0  7487  addgegt0  7488  addgtge0  7489  addge0  7490  ltaddpos  7491  ltneg  7501  leneg  7504  lt0neg1  7507  lt0neg2  7508  le0neg1  7509  le0neg2  7510  addge01  7511  suble0  7515  0le1  7520  gt0ne0i  7522  gt0ne0d  7548  lt0ne0d  7549  recexre  7613  recexgt0  7615  inelr  7619  rimul  7620  1ap0  7625  reapmul1  7630  apsqgt0  7636  msqge0  7651  mulge0  7654  recexaplem2  7677  recexap  7678  rerecclap  7751  ltm1  7857  recgt0  7861  ltmul12a  7871  lemul12a  7873  mulgt1  7874  gt0div  7881  ge0div  7882  recgt1i  7909  recreclt  7911  crap0  7956  nnge1  7983  nngt0  7985  nnrecgt0  7997  0ne1  8027  0le0  8049  neg1lt0  8068  halfge0  8168  iap0  8175  nn0ssre  8213  nn0ge0  8234  nn0nlt0  8235  nn0le0eq0  8237  0mnnnnn0  8241  elnnnn0b  8253  elnnnn0c  8254  elnnz  8282  0z  8283  elnnz1  8295  nn0lt10b  8349  recnz  8361  gtndiv  8363  fnn0ind  8383  rpge0  8663  rpnegap  8683  0nrp  8684  0ltpnf  8774  mnflt0  8776  xneg0  8815  elrege0  8916  0e0icopnf  8919  0elunit  8925  1elunit  8926  divelunit  8941  lincmb01cmp  8942  iccf1o  8943  unitssre  8944  modqelico  9249  modqmuladdim  9282  addmodid  9287  expubnd  9442  le2sq2  9460  bernneq2  9502  expnbnd  9504  expnlbnd  9505  faclbnd  9573  faclbnd3  9575  faclbnd6  9576  bcval4  9584  bcpasc  9598  reim0  9653  re0  9687  im0  9688  rei  9691  imi  9692  cj0  9693  caucvgre  9772  rennim  9792  sqrt0rlem  9793  sqrt0  9794  resqrexlemdecn  9802  resqrexlemnm  9808  resqrexlemgt0  9810  sqrt00  9830  sqrt9  9838  sqrt2gt1lt2  9839  leabs  9864  ltabs  9877  sqrtpclii  9920  climge0  10039  iserige0  10057  nn0seqcvgd  10206  algcvgblem  10214  ialgcvga  10216
  Copyright terms: Public domain W3C validator