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 8805 | . 2 ⊢ 4 = (3 + 1) | |
2 | 3re 8818 | . . 3 ⊢ 3 ∈ ℝ | |
3 | 1re 7789 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7803 | . 2 ⊢ (3 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2213 | 1 ⊢ 4 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1481 (class class class)co 5782 ℝcr 7643 1c1 7645 + caddc 7647 3c3 8796 4c4 8797 |
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 7738 ax-addrcl 7741 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-clel 2136 df-2 8803 df-3 8804 df-4 8805 |
This theorem is referenced by: 4cn 8822 5re 8823 4ne0 8842 4ap0 8843 5pos 8844 2lt4 8917 1lt4 8918 4lt5 8919 3lt5 8920 2lt5 8921 1lt5 8922 4lt6 8924 3lt6 8925 4lt7 8930 3lt7 8931 4lt8 8937 3lt8 8938 4lt9 8945 3lt9 8946 8th4div3 8963 div4p1lem1div2 8997 4lt10 9341 3lt10 9342 eluz4eluz2 9389 fzo0to42pr 10028 fldiv4p1lem1div2 10109 faclbnd2 10520 4bc2eq6 10552 resqrexlemover 10814 resqrexlemcalc1 10818 resqrexlemcalc2 10819 resqrexlemcalc3 10820 resqrexlemnm 10822 resqrexlemga 10827 sqrt2gt1lt2 10853 amgm2 10922 ef01bndlem 11499 sin01bnd 11500 cos01bnd 11501 cos2bnd 11503 flodddiv4 11667 dveflem 12895 sin0pilem2 12911 sinhalfpilem 12920 sincosq1lem 12954 coseq0negpitopi 12965 tangtx 12967 sincos4thpi 12969 pigt3 12973 |
Copyright terms: Public domain | W3C validator |