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

Theorem dfdecOLD 11707
Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. Obsolete version of df-dec 11706 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 11706 . 2 𝐴𝐵 = (((9 + 1) · 𝐴) + 𝐵)
2 9p1e10OLD 11371 . . . 4 (9 + 1) = 10
32oveq1i 6824 . . 3 ((9 + 1) · 𝐴) = (10 · 𝐴)
43oveq1i 6824 . 2 (((9 + 1) · 𝐴) + 𝐵) = ((10 · 𝐴) + 𝐵)
51, 4eqtri 2782 1 𝐴𝐵 = ((10 · 𝐴) + 𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  (class class class)co 6814  1c1 10149   + caddc 10151   · cmul 10153  9c9 11289  10c10 11290  cdc 11705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817  df-10OLD 11299  df-dec 11706
This theorem is referenced by:  decexOLD  11711  deceq1OLD  11713  deceq2OLD  11715  decclOLD  11725  decnnclOLD  11731  dec0uOLD  11733  dec0hOLD  11735  decnncl2OLD  11738  decltOLD  11743  decltcOLD  11745  decsucOLD  11748  decleOLD  11755  decltiOLD  11760  decsuccOLD  11763  dec10pOLD  11766  decmaOLD  11777  decmacOLD  11779  decma2cOLD  11781  decaddOLD  11783  decaddcOLD  11785  decsubiOLD  11796  decmul1OLD  11798  decmul1cOLD  11800  decmul2cOLD  11802  decmul10addOLD  11806  5t5e25OLD  11852  6t6e36OLD  11859  8t6e48OLD  11872  9t11e99OLD  11884  sq10OLD  13265  3decOLD  13267  3dvdsdecOLD  15277  decsplit1OLD  16012  decsplitOLD  16013  dpfrac1OLD  29930  1t10e1p1e11OLD  41848  tgoldbachltOLD  42238
  Copyright terms: Public domain W3C validator