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

Theorem 2re 8420
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 8409 . 2 2 = (1 + 1)
2 1re 7424 . . 3 1 ∈ ℝ
32, 2readdcli 7438 . 2 (1 + 1) ∈ ℝ
41, 3eqeltri 2157 1 2 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1436  (class class class)co 5607  cr 7286  1c1 7288   + caddc 7290  2c2 8400
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067  ax-1re 7376  ax-addrcl 7379
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081  df-2 8409
This theorem is referenced by:  2cn  8421  3re  8424  2ne0  8442  2ap0  8443  3pos  8444  2lt3  8513  1lt3  8514  2lt4  8516  1lt4  8517  2lt5  8520  2lt6  8525  1lt6  8526  2lt7  8531  1lt7  8532  2lt8  8538  1lt8  8539  2lt9  8546  1lt9  8547  1le2  8550  2rene0  8552  halfre  8555  halfgt0  8557  halflt1  8559  rehalfcl  8569  halfpos2  8572  halfnneg2  8574  addltmul  8578  nominpos  8579  avglt1  8580  avglt2  8581  div4p1lem1div2  8595  nn0lele2xi  8650  nn0ge2m1nn  8659  halfnz  8768  3halfnz  8769  2lt10  8939  1lt10  8940  uzuzle23  8984  uz3m2nn  8986  2rp  9064  fztpval  9420  fzo0to42pr  9552  qbtwnrelemcalc  9588  qbtwnre  9589  2tnp1ge0ge0  9629  flhalf  9630  fldiv4p1lem1div2  9633  mulp1mod1  9693  expubnd  9903  nn0opthlem2d  10018  faclbnd2  10039  4bc2eq6  10071  cvg1nlemres  10306  resqrexlemover  10331  resqrexlemga  10344  sqrt4  10368  sqrt2gt1lt2  10370  abstri  10425  amgm2  10439  maxabslemlub  10528  maxltsup  10539  oexpneg  10744  oddge22np1  10748  evennn02n  10749  evennn2n  10750  nn0ehalf  10770  nno  10773  nn0o  10774  nn0oddm1d2  10776  nnoddm1d2  10777  flodddiv4t2lthalf  10804  6gcd4e2  10851  ncoprmgcdne1b  10938  3lcm2e6  11006  sqrt2irrlem  11007  sqrt2re  11009  sqrt2irraplemnn  11024  sqrt2irrap  11025  ex-fl  11083
  Copyright terms: Public domain W3C validator