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

Theorem 2re 8176
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 8165 . 2  |-  2  =  ( 1  +  1 )
2 1re 7180 . . 3  |-  1  e.  RR
32, 2readdcli 7194 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2152 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1434  (class class class)co 5543   RRcr 7042   1c1 7044    + caddc 7046   2c2 8156
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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064  ax-1re 7132  ax-addrcl 7135
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078  df-2 8165
This theorem is referenced by:  2cn  8177  3re  8180  2ne0  8198  2ap0  8199  3pos  8200  2lt3  8269  1lt3  8270  2lt4  8272  1lt4  8273  2lt5  8276  2lt6  8281  1lt6  8282  2lt7  8287  1lt7  8288  2lt8  8294  1lt8  8295  2lt9  8302  1lt9  8303  1le2  8306  2rene0  8308  halfre  8311  halfgt0  8313  halflt1  8315  rehalfcl  8325  halfpos2  8328  halfnneg2  8330  addltmul  8334  nominpos  8335  avglt1  8336  avglt2  8337  div4p1lem1div2  8351  nn0lele2xi  8406  nn0ge2m1nn  8415  halfnz  8524  3halfnz  8525  2lt10  8695  1lt10  8696  uzuzle23  8740  uz3m2nn  8742  2rp  8820  fztpval  9176  fzo0to42pr  9306  qbtwnrelemcalc  9342  qbtwnre  9343  2tnp1ge0ge0  9383  flhalf  9384  fldiv4p1lem1div2  9387  mulp1mod1  9447  expubnd  9630  nn0opthlem2d  9745  faclbnd2  9766  4bc2eq6  9798  cvg1nlemres  10009  resqrexlemover  10034  resqrexlemga  10047  sqrt4  10071  sqrt2gt1lt2  10073  abstri  10128  amgm2  10142  maxabslemlub  10231  maxltsup  10242  oexpneg  10421  oddge22np1  10425  evennn02n  10426  evennn2n  10427  nn0ehalf  10447  nno  10450  nn0o  10451  nn0oddm1d2  10453  nnoddm1d2  10454  flodddiv4t2lthalf  10481  6gcd4e2  10528  ncoprmgcdne1b  10615  3lcm2e6  10683  sqrt2irrlem  10684  sqrt2re  10686  sqrt2irraplemnn  10701  sqrt2irrap  10702  ex-fl  10714
  Copyright terms: Public domain W3C validator