Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 4re | Unicode version |
Description: The number 4 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
4re |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-4 8100 | . 2 | |
2 | 3re 8113 | . . 3 | |
3 | 1re 7118 | . . 3 | |
4 | 2, 3 | readdcli 7132 | . 2 |
5 | 1, 4 | eqeltri 2151 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1433 (class class class)co 5532 cr 6980 c1 6982 caddc 6984 c3 8090 c4 8091 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 ax-ie1 1422 ax-ie2 1423 ax-4 1440 ax-17 1459 ax-ial 1467 ax-ext 2063 ax-1re 7070 ax-addrcl 7073 |
This theorem depends on definitions: df-bi 115 df-cleq 2074 df-clel 2077 df-2 8098 df-3 8099 df-4 8100 |
This theorem is referenced by: 4cn 8117 5re 8118 4ne0 8137 4ap0 8138 5pos 8139 2lt4 8205 1lt4 8206 4lt5 8207 3lt5 8208 2lt5 8209 1lt5 8210 4lt6 8212 3lt6 8213 4lt7 8218 3lt7 8219 4lt8 8225 3lt8 8226 4lt9 8233 3lt9 8234 8th4div3 8250 div4p1lem1div2 8284 4lt10 8612 3lt10 8613 fzo0to42pr 9229 fldiv4p1lem1div2 9307 faclbnd2 9669 4bc2eq6 9701 resqrexlemover 9896 resqrexlemcalc1 9900 resqrexlemcalc2 9901 resqrexlemcalc3 9902 resqrexlemnm 9904 resqrexlemga 9909 sqrt2gt1lt2 9935 amgm2 10004 flodddiv4 10334 |
Copyright terms: Public domain | W3C validator |