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	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	$⊢ (9 + 1) A = 10 A$
4	3	oveq1i	$⊢ (9 + 1) A + B = 10 A + 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 \|-