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	⊢ ; 𝐴 𝐵 = ( ( ; 1 0 · 𝐴 ) + 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-dec	⊢ ; 𝐴 𝐵 = ( ( ( 9 + 1 ) · 𝐴 ) + 𝐵 )
2		9p1e10	⊢ ( 9 + 1 ) = ; 1 0
3	2	oveq1i	⊢ ( ( 9 + 1 ) · 𝐴 ) = ( ; 1 0 · 𝐴 )
4	3	oveq1i	⊢ ( ( ( 9 + 1 ) · 𝐴 ) + 𝐵 ) = ( ( ; 1 0 · 𝐴 ) + 𝐵 )
5	1 4	eqtri	⊢ ; 𝐴 𝐵 = ( ( ; 1 0 · 𝐴 ) + 𝐵 )