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

Theorem 3re 8431
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 8417 . 2  |-  3  =  ( 2  +  1 )
2 2re 8427 . . 3  |-  2  e.  RR
3 1re 7431 . . 3  |-  1  e.  RR
42, 3readdcli 7445 . 2  |-  ( 2  +  1 )  e.  RR
51, 4eqeltri 2157 1  |-  3  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1436  (class class class)co 5613   RRcr 7293   1c1 7295    + caddc 7297   2c2 8407   3c3 8408
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067  ax-1re 7383  ax-addrcl 7386
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081  df-2 8416  df-3 8417
This theorem is referenced by:  3cn  8432  4re  8434  3ne0  8452  3ap0  8453  4pos  8454  1lt3  8521  3lt4  8522  2lt4  8523  3lt5  8526  3lt6  8531  2lt6  8532  3lt7  8537  2lt7  8538  3lt8  8544  2lt8  8545  3lt9  8552  2lt9  8553  1le3  8560  8th4div3  8568  halfpm6th  8569  3halfnz  8776  3lt10  8945  2lt10  8946  uzuzle23  8991  uz3m2nn  8993  nn01to3  9034  expnass  9957  sqrt9  10376  flodddiv4  10809  ex-fl  11091  ex-gcd  11096
  Copyright terms: Public domain W3C validator