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 7975 | . 2 ⊢ 4 = (3 + 1) | |
2 | 3re 7989 | . . 3 ⊢ 3 ∈ ℝ | |
3 | 1re 7026 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7040 | . 2 ⊢ (3 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2110 | 1 ⊢ 4 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1393 (class class class)co 5512 ℝcr 6888 1c1 6890 + caddc 6892 3c3 7965 4c4 7966 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-ext 2022 ax-1re 6978 ax-addrcl 6981 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 df-clel 2036 df-2 7973 df-3 7974 df-4 7975 |
This theorem is referenced by: 4cn 7993 5re 7994 4ne0 8014 4ap0 8015 5pos 8016 2lt4 8090 1lt4 8091 4lt5 8092 3lt5 8093 2lt5 8094 1lt5 8095 4lt6 8097 3lt6 8098 4lt7 8103 3lt7 8104 4lt8 8110 3lt8 8111 4lt9 8118 3lt9 8119 4lt10 8127 3lt10 8128 8th4div3 8144 div4p1lem1div2 8177 fzo0to42pr 9076 fldiv4p1lem1div2 9147 resqrexlemover 9608 resqrexlemcalc1 9612 resqrexlemcalc2 9613 resqrexlemcalc3 9614 resqrexlemnm 9616 resqrexlemga 9621 sqrt2gt1lt2 9647 amgm2 9714 |
Copyright terms: Public domain | W3C validator |