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

Theorem dfdecOLD 11371
Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. Obsolete version of df-dec 11370 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 11370 . 2 𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
2 9p1e10OLD 11036 . . . 4 (9 + 1) = 10
32oveq1i 6559 . . 3 ((9 + 1) · 𝐴) = (10 · 𝐴)
43oveq1i 6559 . 2 (((9 + 1) · 𝐴) + 𝐵) = ((10 · 𝐴) + 𝐵)
51, 4eqtri 2632 1 𝐴𝐵 = ((10 · 𝐴) + 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  (class class class)co 6549  1c1 9816   + caddc 9818   · cmul 9820  9c9 10954  10c10 10955  cdc 11369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-10OLD 10964  df-dec 11370
This theorem is referenced by:  decexOLD  11375  deceq1OLD  11377  deceq2OLD  11379  decclOLD  11389  decnnclOLD  11395  dec0uOLD  11397  dec0hOLD  11399  decnncl2OLD  11402  decltOLD  11407  decltcOLD  11409  decsucOLD  11412  decleOLD  11419  decltiOLD  11424  decsuccOLD  11427  dec10pOLD  11430  decmaOLD  11441  decmacOLD  11443  decma2cOLD  11445  decaddOLD  11447  decaddcOLD  11449  decsubiOLD  11460  decmul1OLD  11462  decmul1cOLD  11464  decmul2cOLD  11466  decmul10addOLD  11470  5t5e25OLD  11516  6t6e36OLD  11523  8t6e48OLD  11536  9t11e99OLD  11548  sq10OLD  12913  3decOLD  12915  3dvdsdecOLD  14893  decsplit1OLD  15628  decsplitOLD  15629  1t10e1p1e11OLD  39938  tgoldbachltOLD  40237  dpfrac1OLD  42313
  Copyright terms: Public domain W3C validator