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

Theorem 4re 8754
Description: The number 4 is real. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
4re 4 ∈ ℝ

Proof of Theorem 4re
StepHypRef Expression
1 df-4 8738 . 2 4 = (3 + 1)
2 3re 8751 . . 3 3 ∈ ℝ
3 1re 7729 . . 3 1 ∈ ℝ
42, 3readdcli 7743 . 2 (3 + 1) ∈ ℝ
51, 4eqeltri 2188 1 4 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1463  (class class class)co 5740  cr 7583  1c1 7585   + caddc 7587  3c3 8729  4c4 8730
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097  ax-1re 7678  ax-addrcl 7681
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111  df-2 8736  df-3 8737  df-4 8738
This theorem is referenced by:  4cn  8755  5re  8756  4ne0  8775  4ap0  8776  5pos  8777  2lt4  8844  1lt4  8845  4lt5  8846  3lt5  8847  2lt5  8848  1lt5  8849  4lt6  8851  3lt6  8852  4lt7  8857  3lt7  8858  4lt8  8864  3lt8  8865  4lt9  8872  3lt9  8873  8th4div3  8890  div4p1lem1div2  8924  4lt10  9268  3lt10  9269  fzo0to42pr  9937  fldiv4p1lem1div2  10018  faclbnd2  10428  4bc2eq6  10460  resqrexlemover  10722  resqrexlemcalc1  10726  resqrexlemcalc2  10727  resqrexlemcalc3  10728  resqrexlemnm  10730  resqrexlemga  10735  sqrt2gt1lt2  10761  amgm2  10830  ef01bndlem  11362  sin01bnd  11363  cos01bnd  11364  cos2bnd  11366  flodddiv4  11527  dveflem  12729
  Copyright terms: Public domain W3C validator