Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 2re | GIF version |
Description: The number 2 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
2re | ⊢ 2 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2 7973 | . 2 ⊢ 2 = (1 + 1) | |
2 | 1re 7026 | . . 3 ⊢ 1 ∈ ℝ | |
3 | 2, 2 | readdcli 7040 | . 2 ⊢ (1 + 1) ∈ ℝ |
4 | 1, 3 | eqeltri 2110 | 1 ⊢ 2 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1393 (class class class)co 5512 ℝcr 6888 1c1 6890 + caddc 6892 2c2 7964 |
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 |
This theorem is referenced by: 2cn 7986 3re 7989 2ne0 8008 2ap0 8009 3pos 8010 2lt3 8087 1lt3 8088 2lt4 8090 1lt4 8091 2lt5 8094 2lt6 8099 1lt6 8100 2lt7 8105 1lt7 8106 2lt8 8112 1lt8 8113 2lt9 8120 1lt9 8121 2lt10 8129 1lt10 8130 1le2 8133 2rene0 8135 halfre 8138 halfgt0 8140 halflt1 8142 rehalfcl 8152 halfpos2 8155 halfnneg2 8157 addltmul 8161 nominpos 8162 avglt1 8163 avglt2 8164 div4p1lem1div2 8177 nn0lele2xi 8233 nn0ge2m1nn 8242 halfnz 8336 uzuzle23 8513 uz3m2nn 8515 2rp 8588 fztpval 8945 fzo0to42pr 9076 qbtwnrelemcalc 9110 qbtwnre 9111 2tnp1ge0ge0 9143 flhalf 9144 fldiv4p1lem1div2 9147 expubnd 9311 cvg1nlemres 9584 resqrexlemover 9608 resqrexlemga 9621 sqrt4 9645 sqrt2gt1lt2 9647 abstri 9700 amgm2 9714 sqr2irrlem 9877 sqrt2re 9879 ex-fl 9895 |
Copyright terms: Public domain | W3C validator |