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

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

Proof of Theorem 3re
StepHypRef Expression
1 df-3 8773 . 2  |-  3  =  ( 2  +  1 )
2 2re 8783 . . 3  |-  2  e.  RR
3 1re 7758 . . 3  |-  1  e.  RR
42, 3readdcli 7772 . 2  |-  ( 2  +  1 )  e.  RR
51, 4eqeltri 2210 1  |-  3  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1480  (class class class)co 5767   RRcr 7612   1c1 7614    + caddc 7616   2c2 8764   3c3 8765
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119  ax-1re 7707  ax-addrcl 7710
This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133  df-2 8772  df-3 8773
This theorem is referenced by:  3cn  8788  4re  8790  3ne0  8808  3ap0  8809  4pos  8810  1lt3  8884  3lt4  8885  2lt4  8886  3lt5  8889  3lt6  8894  2lt6  8895  3lt7  8900  2lt7  8901  3lt8  8907  2lt8  8908  3lt9  8915  2lt9  8916  1le3  8924  8th4div3  8932  halfpm6th  8933  3halfnz  9141  3lt10  9311  2lt10  9312  uzuzle23  9359  uz3m2nn  9361  nn01to3  9402  3rp  9440  expnass  10391  sqrt9  10813  ef01bndlem  11452  sin01bnd  11453  cos2bnd  11456  sin01gt0  11457  cos01gt0  11458  egt2lt3  11475  flodddiv4  11620  dveflem  12844  sincosq3sgn  12898  sincosq4sgn  12899  cosq23lt0  12903  coseq0q4123  12904  coseq00topi  12905  coseq0negpitopi  12906  tangtx  12908  sincos6thpi  12912  pigt3  12914  pige3  12915  cos02pilt1  12921  ex-fl  12926  ex-gcd  12932
  Copyright terms: Public domain W3C validator