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

Metamath Proof Explorer

Definition df-dec

Description: Define the "decimal constructor", which is used to build up "decimal integers" or "numeric terms" in base 1 0 . For example, ( ; ; ; 1 0 0 0 + ; ; ; 2 0 0 0 ) = ; ; ; 3 0 0 0 1kp2ke3k . (Contributed by Mario Carneiro, 17-Apr-2015) (Revised by AV, 1-Aug-2021)

		Ref	Expression
	Assertion	df-dec	Could not format assertion : No typesetting found for \|- ; A B = ( ( ( 9 + 1 ) x. A ) + B ) with typecode \|-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cB	$class B$
2	0 1	cdc	Could not format ; A B : No typesetting found for class ; A B with typecode class
3		c9	$class 9$
4		caddc	$class +$
5		c1	$class 1$
6	3 5 4	co	$class (9 + 1)$
7		cmul	$class \times$
8	6 0 7	co	$class (9 + 1) A$
9	8 1 4	co	$class ((9 + 1) A + B)$
10	2 9	wceq	Could not format ; A B = ( ( ( 9 + 1 ) x. A ) + B ) : No typesetting found for wff ; A B = ( ( ( 9 + 1 ) x. A ) + B ) with typecode wff