![]() |
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 8544 | . 2 ⊢ 4 = (3 + 1) | |
2 | 3re 8557 | . . 3 ⊢ 3 ∈ ℝ | |
3 | 1re 7548 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 7562 | . 2 ⊢ (3 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2161 | 1 ⊢ 4 ∈ ℝ |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1439 (class class class)co 5666 ℝcr 7410 1c1 7412 + caddc 7414 3c3 8535 4c4 8536 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1382 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 ax-17 1465 ax-ial 1473 ax-ext 2071 ax-1re 7500 ax-addrcl 7503 |
This theorem depends on definitions: df-bi 116 df-cleq 2082 df-clel 2085 df-2 8542 df-3 8543 df-4 8544 |
This theorem is referenced by: 4cn 8561 5re 8562 4ne0 8581 4ap0 8582 5pos 8583 2lt4 8650 1lt4 8651 4lt5 8652 3lt5 8653 2lt5 8654 1lt5 8655 4lt6 8657 3lt6 8658 4lt7 8663 3lt7 8664 4lt8 8670 3lt8 8671 4lt9 8678 3lt9 8679 8th4div3 8696 div4p1lem1div2 8730 4lt10 9073 3lt10 9074 fzo0to42pr 9692 fldiv4p1lem1div2 9773 faclbnd2 10211 4bc2eq6 10243 resqrexlemover 10504 resqrexlemcalc1 10508 resqrexlemcalc2 10509 resqrexlemcalc3 10510 resqrexlemnm 10512 resqrexlemga 10517 sqrt2gt1lt2 10543 amgm2 10612 ef01bndlem 11108 sin01bnd 11109 cos01bnd 11110 cos2bnd 11112 flodddiv4 11273 |
Copyright terms: Public domain | W3C validator |