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

Theorem 3re 8250
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 8236 . 2  |-  3  =  ( 2  +  1 )
2 2re 8246 . . 3  |-  2  e.  RR
3 1re 7250 . . 3  |-  1  e.  RR
42, 3readdcli 7264 . 2  |-  ( 2  +  1 )  e.  RR
51, 4eqeltri 2155 1  |-  3  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1434  (class class class)co 5564   RRcr 7112   1c1 7114    + caddc 7116   2c2 8226   3c3 8227
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 2065  ax-1re 7202  ax-addrcl 7205
This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-clel 2079  df-2 8235  df-3 8236
This theorem is referenced by:  3cn  8251  4re  8253  3ne0  8271  3ap0  8272  4pos  8273  1lt3  8340  3lt4  8341  2lt4  8342  3lt5  8345  3lt6  8350  2lt6  8351  3lt7  8356  2lt7  8357  3lt8  8363  2lt8  8364  3lt9  8371  2lt9  8372  1le3  8379  8th4div3  8387  halfpm6th  8388  3halfnz  8595  3lt10  8764  2lt10  8765  uzuzle23  8810  uz3m2nn  8812  nn01to3  8853  expnass  9747  sqrt9  10153  flodddiv4  10559  ex-fl  10841  ex-gcd  10846
  Copyright terms: Public domain W3C validator