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

Theorem dfdecOLD 11329
Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. Obsolete version of df-dec 11328 as of 1-Aug-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
dfdecOLD 𝐴𝐵 = ((10 · 𝐴) + 𝐵)

Proof of Theorem dfdecOLD
StepHypRef Expression
1 df-dec 11328 . 2 𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
2 9p1e10OLD 11008 . . . 4 (9 + 1) = 10
32oveq1i 6536 . . 3 ((9 + 1) · 𝐴) = (10 · 𝐴)
43oveq1i 6536 . 2 (((9 + 1) · 𝐴) + 𝐵) = ((10 · 𝐴) + 𝐵)
51, 4eqtri 2631 1 𝐴𝐵 = ((10 · 𝐴) + 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  (class class class)co 6526  1c1 9793   + caddc 9795   · cmul 9797  9c9 10926  10c10 10927  cdc 11327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5753  df-fv 5797  df-ov 6529  df-10OLD 10936  df-dec 11328
This theorem is referenced by:  decexOLD  11333  deceq1OLD  11335  deceq2OLD  11337  decclOLD  11347  decnnclOLD  11353  dec0uOLD  11355  dec0hOLD  11357  decnncl2OLD  11360  decltOLD  11365  decltcOLD  11367  decsucOLD  11370  decleOLD  11377  decltiOLD  11382  decsuccOLD  11385  dec10pOLD  11388  decmaOLD  11399  decmacOLD  11401  decma2cOLD  11403  decaddOLD  11405  decaddcOLD  11407  decsubiOLD  11418  decmul1OLD  11420  decmul1cOLD  11422  decmul2cOLD  11424  decmul10addOLD  11428  5t5e25OLD  11474  6t6e36OLD  11481  8t6e48OLD  11494  9t11e99OLD  11506  sq10OLD  12870  3decOLD  12872  3dvdsdecOLD  14841  decsplit1OLD  15576  decsplitOLD  15577  1t10e1p1e11OLD  39722  tgoldbachltOLD  40021  dpfrac1OLD  42255
  Copyright terms: Public domain W3C validator