MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-5 Structured version   Visualization version   GIF version

Definition df-5 12282
Description: Define the number 5. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-5 5 = (4 + 1)

Detailed syntax breakdown of Definition df-5
StepHypRef Expression
1 c5 12274 . 2 class 5
2 c4 12273 . . 3 class 4
3 c1 11113 . . 3 class 1
4 caddc 11115 . . 3 class +
52, 3, 4co 7405 . 2 class (4 + 1)
61, 5wceq 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