This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )