Theorem dfdec10 9542

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 9540	. 2 |- ; A B = ( ( ( 9 + 1 ) x. A ) + B )
2		9p1e10 9541	. . . 4 |- ( 9 + 1 ) = ; 1 0
3	2	oveq1i 5977	. . 3 |- ( ( 9 + 1 ) x. A ) = (; 1 0 x. A )
4	3	oveq1i 5977	. 2 |- ( ( ( 9 + 1 ) x. A ) + B ) = ( (; 1 0 x. A ) + B )
5	1, 4	eqtri 2228	1 |- ; A B = ( (; 1 0 x. A ) + B )

Syntax hints:   = wceq 1373  (class class class)co 5967   0cc0 7960   1c1 7961   + caddc 7963   x. cmul 7965   9c9 9129  ;cdc 9539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-sep 4178  ax-cnex 8051  ax-resscn 8052  ax-1cn 8053  ax-1re 8054  ax-icn 8055  ax-addcl 8056  ax-addrcl 8057  ax-mulcl 8058  ax-mulcom 8061  ax-addass 8062  ax-mulass 8063  ax-distr 8064  ax-1rid 8067  ax-0id 8068  ax-cnre 8071

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491  df-rex 2492  df-rab 2495  df-v 2778  df-un 3178  df-in 3180  df-ss 3187  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-int 3900  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970  df-inn 9072  df-2 9130  df-3 9131  df-4 9132  df-5 9133  df-6 9134  df-7 9135  df-8 9136  df-9 9137  df-dec 9540

This theorem is referenced by:  decnncl  9558  dec0u  9559  dec0h  9560  decnncl2  9562  declt  9566  decltc  9567  decsuc  9569  decle  9572  declti  9576  decsucc  9579  dec10p  9581  decma  9589  decmac  9590  decma2c  9591  decadd  9592  decaddc  9593  decsubi  9601  decmul1  9602  decmul1c  9603  decmul2c  9604  decmul10add  9607  5t5e25  9641  6t6e36  9646  8t6e48  9657  9t11e99  9668  3dec  10896  3dvdsdec  12291  dec2dvds  12849  dec5dvds  12850  dec5nprm  12852  dec2nprm  12853  decsplit1  12866  decsplit  12867