![]() |
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 8481 | . 2 ⊢ 4 = (3 + 1) | |
2 | 3re 8494 | . . 3 ⊢ 3 ∈ ℝ | |
3 | 1re 7485 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7499 | . 2 ⊢ (3 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2160 | 1 ⊢ 4 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1438 (class class class)co 5652 ℝcr 7347 1c1 7349 + caddc 7351 3c3 8472 4c4 8473 |
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 1381 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-4 1445 ax-17 1464 ax-ial 1472 ax-ext 2070 ax-1re 7437 ax-addrcl 7440 |
This theorem depends on definitions: df-bi 115 df-cleq 2081 df-clel 2084 df-2 8479 df-3 8480 df-4 8481 |
This theorem is referenced by: 4cn 8498 5re 8499 4ne0 8518 4ap0 8519 5pos 8520 2lt4 8587 1lt4 8588 4lt5 8589 3lt5 8590 2lt5 8591 1lt5 8592 4lt6 8594 3lt6 8595 4lt7 8600 3lt7 8601 4lt8 8607 3lt8 8608 4lt9 8615 3lt9 8616 8th4div3 8633 div4p1lem1div2 8667 4lt10 9010 3lt10 9011 fzo0to42pr 9627 fldiv4p1lem1div2 9708 faclbnd2 10146 4bc2eq6 10178 resqrexlemover 10439 resqrexlemcalc1 10443 resqrexlemcalc2 10444 resqrexlemcalc3 10445 resqrexlemnm 10447 resqrexlemga 10452 sqrt2gt1lt2 10478 amgm2 10547 ef01bndlem 11043 sin01bnd 11044 cos01bnd 11045 cos2bnd 11047 flodddiv4 11208 |
Copyright terms: Public domain | W3C validator |