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

Theorem 2re 8463
Description: The number 2 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
2re  |-  2  e.  RR

Proof of Theorem 2re
StepHypRef Expression
1 df-2 8452 . 2  |-  2  =  ( 1  +  1 )
2 1re 7466 . . 3  |-  1  e.  RR
32, 2readdcli 7480 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2160 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1438  (class class class)co 5634   RRcr 7328   1c1 7330    + caddc 7332   2c2 8444
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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1re 7418  ax-addrcl 7421
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084  df-2 8452
This theorem is referenced by:  2cn  8464  3re  8467  2ne0  8485  2ap0  8486  3pos  8487  2lt3  8556  1lt3  8557  2lt4  8559  1lt4  8560  2lt5  8563  2lt6  8568  1lt6  8569  2lt7  8574  1lt7  8575  2lt8  8581  1lt8  8582  2lt9  8589  1lt9  8590  1ap2  8593  1le2  8594  2rene0  8596  halfre  8599  halfgt0  8601  halflt1  8603  rehalfcl  8613  halfpos2  8616  halfnneg2  8618  addltmul  8622  nominpos  8623  avglt1  8624  avglt2  8625  div4p1lem1div2  8639  nn0lele2xi  8694  nn0ge2m1nn  8703  halfnz  8812  3halfnz  8813  2lt10  8983  1lt10  8984  uzuzle23  9028  uz3m2nn  9030  2rp  9108  fztpval  9464  fzo0to42pr  9596  qbtwnrelemcalc  9632  qbtwnre  9633  2tnp1ge0ge0  9673  flhalf  9674  fldiv4p1lem1div2  9677  mulp1mod1  9737  expubnd  9977  nn0opthlem2d  10094  faclbnd2  10115  4bc2eq6  10147  cvg1nlemres  10383  resqrexlemover  10408  resqrexlemga  10421  sqrt4  10445  sqrt2gt1lt2  10447  abstri  10502  amgm2  10516  maxabslemlub  10605  maxltsup  10616  oexpneg  10970  oddge22np1  10974  evennn02n  10975  evennn2n  10976  nn0ehalf  10996  nno  10999  nn0o  11000  nn0oddm1d2  11002  nnoddm1d2  11003  flodddiv4t2lthalf  11030  6gcd4e2  11077  ncoprmgcdne1b  11164  3lcm2e6  11232  sqrt2irrlem  11233  sqrt2re  11235  sqrt2irraplemnn  11250  sqrt2irrap  11251  ex-fl  11309
  Copyright terms: Public domain W3C validator