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

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

Proof of Theorem 4re
StepHypRef Expression
1 df-4 8804 . 2  |-  4  =  ( 3  +  1 )
2 3re 8817 . . 3  |-  3  e.  RR
3 1re 7788 . . 3  |-  1  e.  RR
42, 3readdcli 7802 . 2  |-  ( 3  +  1 )  e.  RR
51, 4eqeltri 2213 1  |-  4  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1481  (class class class)co 5781   RRcr 7642   1c1 7644    + caddc 7646   3c3 8795   4c4 8796
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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122  ax-1re 7737  ax-addrcl 7740
This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136  df-2 8802  df-3 8803  df-4 8804
This theorem is referenced by:  4cn  8821  5re  8822  4ne0  8841  4ap0  8842  5pos  8843  2lt4  8916  1lt4  8917  4lt5  8918  3lt5  8919  2lt5  8920  1lt5  8921  4lt6  8923  3lt6  8924  4lt7  8929  3lt7  8930  4lt8  8936  3lt8  8937  4lt9  8944  3lt9  8945  8th4div3  8962  div4p1lem1div2  8996  4lt10  9340  3lt10  9341  eluz4eluz2  9388  fzo0to42pr  10027  fldiv4p1lem1div2  10108  faclbnd2  10519  4bc2eq6  10551  resqrexlemover  10813  resqrexlemcalc1  10817  resqrexlemcalc2  10818  resqrexlemcalc3  10819  resqrexlemnm  10821  resqrexlemga  10826  sqrt2gt1lt2  10852  amgm2  10921  ef01bndlem  11497  sin01bnd  11498  cos01bnd  11499  cos2bnd  11501  flodddiv4  11665  dveflem  12893  sin0pilem2  12909  sinhalfpilem  12918  sincosq1lem  12952  coseq0negpitopi  12963  tangtx  12965  sincos4thpi  12967  pigt3  12971
  Copyright terms: Public domain W3C validator