Theorem dfdecOLD 11495

Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 10. Obsolete version of df-dec 11494 as of 1-Aug-2021. (Contributed by Mario Carneiro, 17-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.)

Assertion

Ref	Expression
dfdecOLD	|- ; A B = ( ( 10 x. A ) + B )

Proof of Theorem dfdecOLD

Step	Hyp	Ref	Expression
1		df-dec 11494	. 2 |- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
2		9p1e10OLD 11159	. . . 4 |- ( 9 + 1 ) = 10
3	2	oveq1i 6660	. . 3 |- ( ( 9 + 1 ) x. A ) = ( 10 x. A )
4	3	oveq1i 6660	. 2 |- ( ( ( 9 + 1 ) x. A ) + B ) = ( ( 10 x. A ) + B )
5	1, 4	eqtri 2644	1 |- ; A B = ( ( 10 x. A ) + B )

Syntax hints:   = wceq 1483  (class class class)co 6650   1c1 9937   + caddc 9939   x. cmul 9941   9c9 11077   10c10 11078  ;cdc 11493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-10OLD 11087  df-dec 11494

This theorem is referenced by:  decexOLD  11499  deceq1OLD  11501  deceq2OLD  11503  decclOLD  11513  decnnclOLD  11519  dec0uOLD  11521  dec0hOLD  11523  decnncl2OLD  11526  decltOLD  11531  decltcOLD  11533  decsucOLD  11536  decleOLD  11543  decltiOLD  11548  decsuccOLD  11551  dec10pOLD  11554  decmaOLD  11565  decmacOLD  11567  decma2cOLD  11569  decaddOLD  11571  decaddcOLD  11573  decsubiOLD  11584  decmul1OLD  11586  decmul1cOLD  11588  decmul2cOLD  11590  decmul10addOLD  11594  5t5e25OLD  11640  6t6e36OLD  11647  8t6e48OLD  11660  9t11e99OLD  11672  sq10OLD  13051  3decOLD  13053  3dvdsdecOLD  15055  decsplit1OLD  15790  decsplitOLD  15791  dpfrac1OLD  29600  1t10e1p1e11OLD  41320  tgoldbachltOLD  41710