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

Theorem 2re 8750
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 8739 . 2  |-  2  =  ( 1  +  1 )
2 1re 7729 . . 3  |-  1  e.  RR
32, 2readdcli 7743 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2188 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1463  (class class class)co 5740   RRcr 7583   1c1 7585    + caddc 7587   2c2 8731
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097  ax-1re 7678  ax-addrcl 7681
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111  df-2 8739
This theorem is referenced by:  2cn  8751  3re  8754  2ne0  8772  2ap0  8773  3pos  8774  2lt3  8844  1lt3  8845  2lt4  8847  1lt4  8848  2lt5  8851  2lt6  8856  1lt6  8857  2lt7  8862  1lt7  8863  2lt8  8869  1lt8  8870  2lt9  8877  1lt9  8878  1ap2  8881  1le2  8882  2rene0  8884  halfre  8887  halfgt0  8889  halflt1  8891  rehalfcl  8901  halfpos2  8904  halfnneg2  8906  addltmul  8910  nominpos  8911  avglt1  8912  avglt2  8913  div4p1lem1div2  8927  nn0lele2xi  8982  nn0ge2m1nn  8991  halfnz  9101  3halfnz  9102  2lt10  9273  1lt10  9274  uzuzle23  9318  uz3m2nn  9320  2rp  9398  xleaddadd  9621  fztpval  9814  fzo0to42pr  9948  qbtwnrelemcalc  9984  qbtwnre  9985  2tnp1ge0ge0  10025  flhalf  10026  fldiv4p1lem1div2  10029  mulp1mod1  10089  expubnd  10301  nn0opthlem2d  10418  faclbnd2  10439  4bc2eq6  10471  cvg1nlemres  10708  resqrexlemover  10733  resqrexlemga  10746  sqrt4  10770  sqrt2gt1lt2  10772  abstri  10827  amgm2  10841  maxabslemlub  10930  maxltsup  10941  bdtrilem  10961  efcllemp  11274  efcllem  11275  ege2le3  11287  ef01bndlem  11373  cos01bnd  11375  cos2bnd  11377  cos01gt0  11379  sin02gt0  11380  sincos2sgn  11382  sin4lt0  11383  eirraplem  11390  egt2lt3  11393  epos  11394  ene1  11398  eap1  11399  oexpneg  11481  oddge22np1  11485  evennn02n  11486  evennn2n  11487  nn0ehalf  11507  nno  11510  nn0o  11511  nn0oddm1d2  11513  nnoddm1d2  11514  flodddiv4t2lthalf  11541  6gcd4e2  11590  ncoprmgcdne1b  11677  3lcm2e6  11745  sqrt2irrlem  11746  sqrt2re  11748  sqrt2irraplemnn  11763  sqrt2irrap  11764  plusgndxnmulrndx  11978  bl2in  12478  ex-fl  12771  sin24declemx24  13073  sin24declemy01  13074  sin24declemsub  13075  sin24declemlt  13076
  Copyright terms: Public domain W3C validator