Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 4re | GIF version |
Description: The number 4 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
4re | ⊢ 4 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-4 8749 | . 2 ⊢ 4 = (3 + 1) | |
2 | 3re 8762 | . . 3 ⊢ 3 ∈ ℝ | |
3 | 1re 7733 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7747 | . 2 ⊢ (3 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 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 |