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

Theorem 2re 8812
Description: The number 2 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
2re 2 ∈ ℝ

Proof of Theorem 2re
StepHypRef Expression
1 df-2 8801 . 2 2 = (1 + 1)
2 1re 7787 . . 3 1 ∈ ℝ
32, 2readdcli 7801 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2213 1 2 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1481  (class class class)co 5780  cr 7641  1c1 7643   + caddc 7645  2c2 8793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122  ax-1re 7736  ax-addrcl 7739
This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136  df-2 8801
This theorem is referenced by:  2cn  8813  3re  8816  2ne0  8834  2ap0  8835  3pos  8836  2lt3  8912  1lt3  8913  2lt4  8915  1lt4  8916  2lt5  8919  2lt6  8924  1lt6  8925  2lt7  8930  1lt7  8931  2lt8  8937  1lt8  8938  2lt9  8945  1lt9  8946  1ap2  8949  1le2  8950  2rene0  8952  halfre  8955  halfgt0  8957  halflt1  8959  rehalfcl  8969  halfpos2  8972  halfnneg2  8974  addltmul  8978  nominpos  8979  avglt1  8980  avglt2  8981  div4p1lem1div2  8995  nn0lele2xi  9050  nn0ge2m1nn  9059  halfnz  9169  3halfnz  9170  2lt10  9341  1lt10  9342  eluz4eluz2  9387  uzuzle23  9391  uz3m2nn  9393  2rp  9473  xleaddadd  9698  fztpval  9892  fzo0to42pr  10026  qbtwnrelemcalc  10062  qbtwnre  10063  2tnp1ge0ge0  10103  flhalf  10104  fldiv4p1lem1div2  10107  mulp1mod1  10167  expubnd  10379  nn0opthlem2d  10497  faclbnd2  10518  4bc2eq6  10550  cvg1nlemres  10787  resqrexlemover  10812  resqrexlemga  10825  sqrt4  10849  sqrt2gt1lt2  10851  abstri  10906  amgm2  10920  maxabslemlub  11009  maxltsup  11020  bdtrilem  11040  efcllemp  11394  efcllem  11395  ege2le3  11407  ef01bndlem  11492  cos01bnd  11494  cos2bnd  11496  cos01gt0  11498  sin02gt0  11499  sincos2sgn  11501  sin4lt0  11502  cos12dec  11503  eirraplem  11512  egt2lt3  11515  epos  11516  ene1  11520  eap1  11521  oexpneg  11603  oddge22np1  11607  evennn02n  11608  evennn2n  11609  nn0ehalf  11629  nno  11632  nn0o  11633  nn0oddm1d2  11635  nnoddm1d2  11636  flodddiv4t2lthalf  11663  6gcd4e2  11712  ncoprmgcdne1b  11799  3lcm2e6  11867  sqrt2irrlem  11868  sqrt2re  11870  sqrt2irraplemnn  11886  sqrt2irrap  11887  plusgndxnmulrndx  12104  bl2in  12604  reeff1o  12895  cosz12  12902  sin0pilem1  12903  sin0pilem2  12904  pilem3  12905  pipos  12910  sinhalfpilem  12913  sincosq1lem  12947  sincosq4sgn  12951  sinq12gt0  12952  cosq23lt0  12955  coseq00topi  12957  coseq0negpitopi  12958  tangtx  12960  sincos4thpi  12962  tan4thpi  12963  sincos6thpi  12964  cosordlem  12971  cosq34lt1  12972  cos02pilt1  12973  cos0pilt1  12974  2logb9irr  13089  2logb3irr  13091  2logb9irrALT  13092  sqrt2cxp2logb9e3  13093  2logb9irrap  13095  ex-fl  13101  taupi  13423
  Copyright terms: Public domain W3C validator