Theorem dfdec10 9325

Description: Version of the definition of the "decimal constructor" using ; 1 0 instead of the symbol 10. Of course, this statement cannot be used as definition, because it uses the "decimal constructor". (Contributed by AV, 1-Aug-2021.)

Assertion

Ref	Expression
dfdec10	|- ; A B = ( (; 1 0 x. A ) + B )

Proof of Theorem dfdec10

Step	Hyp	Ref	Expression
1		df-dec 9323	. 2 |- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
2		9p1e10 9324	. . . 4 |- ( 9 + 1 ) = ; 1 0
3	2	oveq1i 5852	. . 3 |- ( ( 9 + 1 ) x. A ) = (; 1 0 x. A )
4	3	oveq1i 5852	. 2 |- ( ( ( 9 + 1 ) x. A ) + B ) = ( (; 1 0 x. A ) + B )
5	1, 4	eqtri 2186	1 |- ; A B = ( (; 1 0 x. A ) + B )

Syntax hints:   = wceq 1343  (class class class)co 5842   0cc0 7753   1c1 7754   + caddc 7756   x. cmul 7758   9c9 8915  ;cdc 9322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-sep 4100  ax-cnex 7844  ax-resscn 7845  ax-1cn 7846  ax-1re 7847  ax-icn 7848  ax-addcl 7849  ax-addrcl 7850  ax-mulcl 7851  ax-mulcom 7854  ax-addass 7855  ax-mulass 7856  ax-distr 7857  ax-1rid 7860  ax-0id 7861  ax-cnre 7864

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-rex 2450  df-rab 2453  df-v 2728  df-un 3120  df-in 3122  df-ss 3129  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-int 3825  df-br 3983  df-iota 5153  df-fv 5196  df-ov 5845  df-inn 8858  df-2 8916  df-3 8917  df-4 8918  df-5 8919  df-6 8920  df-7 8921  df-8 8922  df-9 8923  df-dec 9323

This theorem is referenced by:  decnncl  9341  dec0u  9342  dec0h  9343  decnncl2  9345  declt  9349  decltc  9350  decsuc  9352  decle  9355  declti  9359  decsucc  9362  dec10p  9364  decma  9372  decmac  9373  decma2c  9374  decadd  9375  decaddc  9376  decsubi  9384  decmul1  9385  decmul1c  9386  decmul2c  9387  decmul10add  9390  5t5e25  9424  6t6e36  9429  8t6e48  9440  9t11e99  9451  3dec  10627  3dvdsdec  11802