Theorem dfdec10

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)

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

Proof

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