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

Theorem 2re 8758
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 8747 . 2  |-  2  =  ( 1  +  1 )
2 1re 7733 . . 3  |-  1  e.  RR
32, 2readdcli 7747 . 2  |-  ( 1  +  1 )  e.  RR
41, 3eqeltri 2190 1  |-  2  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1465  (class class class)co 5742   RRcr 7587   1c1 7589    + caddc 7591   2c2 8739
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099  ax-1re 7682  ax-addrcl 7685
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113  df-2 8747
This theorem is referenced by:  2cn  8759  3re  8762  2ne0  8780  2ap0  8781  3pos  8782  2lt3  8858  1lt3  8859  2lt4  8861  1lt4  8862  2lt5  8865  2lt6  8870  1lt6  8871  2lt7  8876  1lt7  8877  2lt8  8883  1lt8  8884  2lt9  8891  1lt9  8892  1ap2  8895  1le2  8896  2rene0  8898  halfre  8901  halfgt0  8903  halflt1  8905  rehalfcl  8915  halfpos2  8918  halfnneg2  8920  addltmul  8924  nominpos  8925  avglt1  8926  avglt2  8927  div4p1lem1div2  8941  nn0lele2xi  8996  nn0ge2m1nn  9005  halfnz  9115  3halfnz  9116  2lt10  9287  1lt10  9288  uzuzle23  9334  uz3m2nn  9336  2rp  9414  xleaddadd  9638  fztpval  9831  fzo0to42pr  9965  qbtwnrelemcalc  10001  qbtwnre  10002  2tnp1ge0ge0  10042  flhalf  10043  fldiv4p1lem1div2  10046  mulp1mod1  10106  expubnd  10318  nn0opthlem2d  10435  faclbnd2  10456  4bc2eq6  10488  cvg1nlemres  10725  resqrexlemover  10750  resqrexlemga  10763  sqrt4  10787  sqrt2gt1lt2  10789  abstri  10844  amgm2  10858  maxabslemlub  10947  maxltsup  10958  bdtrilem  10978  efcllemp  11291  efcllem  11292  ege2le3  11304  ef01bndlem  11390  cos01bnd  11392  cos2bnd  11394  cos01gt0  11396  sin02gt0  11397  sincos2sgn  11399  sin4lt0  11400  cos12dec  11401  eirraplem  11410  egt2lt3  11413  epos  11414  ene1  11418  eap1  11419  oexpneg  11501  oddge22np1  11505  evennn02n  11506  evennn2n  11507  nn0ehalf  11527  nno  11530  nn0o  11531  nn0oddm1d2  11533  nnoddm1d2  11534  flodddiv4t2lthalf  11561  6gcd4e2  11610  ncoprmgcdne1b  11697  3lcm2e6  11765  sqrt2irrlem  11766  sqrt2re  11768  sqrt2irraplemnn  11784  sqrt2irrap  11785  plusgndxnmulrndx  11999  bl2in  12499  cosz12  12788  sin0pilem1  12789  sin0pilem2  12790  pilem3  12791  pipos  12796  sinhalfpilem  12799  sincosq1lem  12833  sincosq4sgn  12837  sinq12gt0  12838  cosq23lt0  12841  coseq00topi  12843  coseq0negpitopi  12844  tangtx  12846  sincos4thpi  12848  tan4thpi  12849  sincos6thpi  12850  cosordlem  12857  cosq34lt1  12858  cos02pilt1  12859  ex-fl  12864  taupi  13166
  Copyright terms: Public domain W3C validator