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

Theorem 3re 8762
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 8748 . 2  |-  3  =  ( 2  +  1 )
2 2re 8758 . . 3  |-  2  e.  RR
3 1re 7733 . . 3  |-  1  e.  RR
42, 3readdcli 7747 . 2  |-  ( 2  +  1 )  e.  RR
51, 4eqeltri 2190 1  |-  3  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   3c3 8740
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  df-3 8748
This theorem is referenced by:  3cn  8763  4re  8765  3ne0  8783  3ap0  8784  4pos  8785  1lt3  8859  3lt4  8860  2lt4  8861  3lt5  8864  3lt6  8869  2lt6  8870  3lt7  8875  2lt7  8876  3lt8  8882  2lt8  8883  3lt9  8890  2lt9  8891  1le3  8899  8th4div3  8907  halfpm6th  8908  3halfnz  9116  3lt10  9286  2lt10  9287  uzuzle23  9334  uz3m2nn  9336  nn01to3  9377  3rp  9415  expnass  10366  sqrt9  10788  ef01bndlem  11390  sin01bnd  11391  cos2bnd  11394  sin01gt0  11395  cos01gt0  11396  egt2lt3  11413  flodddiv4  11558  dveflem  12782  sincosq3sgn  12836  sincosq4sgn  12837  cosq23lt0  12841  coseq0q4123  12842  coseq00topi  12843  coseq0negpitopi  12844  tangtx  12846  sincos6thpi  12850  pigt3  12852  pige3  12853  cos02pilt1  12859  ex-fl  12864  ex-gcd  12870
  Copyright terms: Public domain W3C validator