![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-5 | Structured version Visualization version GIF version |
Description: Define the number 5. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-5 | ⊢ 5 = (4 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c5 12274 | . 2 class 5 | |
2 | c4 12273 | . . 3 class 4 | |
3 | c1 11113 | . . 3 class 1 | |
4 | caddc 11115 | . . 3 class + | |
5 | 2, 3, 4 | co 7405 | . 2 class (4 + 1) |
6 | 1, 5 | wceq 1533 | 1 wff 5 = (4 + 1) |
Colors of variables: wff setvar class |
This definition is referenced by: 5nn 12302 5re 12303 5cn 12304 5pos 12325 5m1e4 12346 4p1e5 12362 3p2e5 12367 4p2e6 12369 4lt5 12393 5p5e10 12752 6p5e11 12754 7p5e12 12758 8p5e13 12764 8p7e15 12766 9p5e14 12771 9p6e15 12772 5t5e25 12784 6t5e30 12788 7t5e35 12793 8t5e40 12799 9t5e45 12806 fldiv4p1lem1div2 13806 ef01bndlem 16134 prm23lt5 16756 5prm 17051 lt6abl 19815 log2ublem3 26835 ppiublem2 27091 bclbnd 27168 bposlem6 27177 bposlem9 27180 lgsdir2lem3 27215 2lgslem3c 27286 2lgsoddprmlem3c 27300 ex-exp 30212 ex-fac 30213 ex-bc 30214 3lexlogpow5ineq5 41442 aks4d1p1p7 41456 rmydioph 42336 expdiophlem2 42344 stoweidlem13 45306 fmtno5 46802 fmtnofac1 46815 31prm 46842 5odd 46955 sbgoldbo 47032 ackval50 47664 |
Copyright terms: Public domain | W3C validator |