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	Could not format assertion : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-dec	Could not format ; A B = ( ( ( 9 + 1 ) x. A ) + B ) : No typesetting found for |- ; A B = ( ( ( 9 + 1 ) x. A ) + B ) with typecode |-
2		9p1e10	$$⊢9+1=10$$
3	2	oveq1i	$$⊢\left(9+1\right)A=10A$$
4	3	oveq1i	$$⊢\left(9+1\right)A+B=10A+B$$
5	1 4	eqtri	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-