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

Theorem 4re 8765
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 8749 . 2 4 = (3 + 1)
2 3re 8762 . . 3 3 ∈ ℝ
3 1re 7733 . . 3 1 ∈ ℝ
42, 3readdcli 7747 . 2 (3 + 1) ∈ ℝ
51, 4eqeltri 2190 1 4 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1465  (class class class)co 5742  cr 7587  1c1 7589   + caddc 7591  3c3 8740  4c4 8741
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  df-4 8749
This theorem is referenced by:  4cn  8766  5re  8767  4ne0  8786  4ap0  8787  5pos  8788  2lt4  8861  1lt4  8862  4lt5  8863  3lt5  8864  2lt5  8865  1lt5  8866  4lt6  8868  3lt6  8869  4lt7  8874  3lt7  8875  4lt8  8881  3lt8  8882  4lt9  8889  3lt9  8890  8th4div3  8907  div4p1lem1div2  8941  4lt10  9285  3lt10  9286  fzo0to42pr  9965  fldiv4p1lem1div2  10046  faclbnd2  10456  4bc2eq6  10488  resqrexlemover  10750  resqrexlemcalc1  10754  resqrexlemcalc2  10755  resqrexlemcalc3  10756  resqrexlemnm  10758  resqrexlemga  10763  sqrt2gt1lt2  10789  amgm2  10858  ef01bndlem  11390  sin01bnd  11391  cos01bnd  11392  cos2bnd  11394  flodddiv4  11558  dveflem  12782  sin0pilem2  12790  sinhalfpilem  12799  sincosq1lem  12833  coseq0negpitopi  12844  tangtx  12846  sincos4thpi  12848  pigt3  12852
  Copyright terms: Public domain W3C validator