Theorem 3dec

Description: A "decimal constructor" which is used to build up "decimal integers" or "numeric terms" in base 10 with 3 "digits". (Contributed by AV, 14-Jun-2021) (Revised by AV, 1-Aug-2021)

	Ref	Expression
Hypotheses	3dec.a	$$⊢A\in {\mathbb{N}}_0$$
	3dec.b	$$⊢B\in {\mathbb{N}}_0$$
Assertion	3dec	Could not format assertion : No typesetting found for |- ; ; A B C = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		3dec.a	$$⊢A\in {\mathbb{N}}_0$$
2		3dec.b	$$⊢B\in {\mathbb{N}}_0$$
3		dfdec10	Could not format ; ; A B C = ( ( ; 1 0 x. ; A B ) + C ) : No typesetting found for |- ; ; A B C = ( ( ; 1 0 x. ; A B ) + C ) with typecode |-
4		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for |- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode |-
5	4	oveq2i	Could not format ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) : No typesetting found for |- ( ; 1 0 x. ; A B ) = ( ; 1 0 x. ( ( ; 1 0 x. A ) + B ) ) with typecode |-
6		10nn	$$⊢10\in \mathbb{N}$$
7	6	nncni	$$⊢10\in ℂ$$
8	1	nn0cni	$$⊢A\in ℂ$$
9	7 8	mulcli	$$⊢10A\in ℂ$$
10	2	nn0cni	$$⊢B\in ℂ$$
11	7 9 10	adddii	$$⊢10\left(10A+B\right)=1010A+10B$$
12	5 11	eqtri	Could not format ( ; 1 0 x. ; A B ) = ( ( ; 1 0 x. ( ; 1 0 x. A ) ) + ( ; 1 0 x. B ) ) : No typesetting found for |- ( ; 1 0 x. ; A B ) = ( ( ; 1 0 x. ( ; 1 0 x. A ) ) + ( ; 1 0 x. B ) ) with typecode |-
13	7 7 8	mulassi	$$⊢10\cdot 10A=1010A$$
14	13	eqcomi	$$⊢1010A=10\cdot 10A$$
15	7	sqvali	$$⊢{10}^2=10\cdot 10$$
16	15	eqcomi	$$⊢10\cdot 10={10}^2$$
17	16	oveq1i	$$⊢10\cdot 10A={10}^{2}A$$
18	14 17	eqtri	$$⊢1010A={10}^{2}A$$
19	18	oveq1i	$$⊢1010A+10B={10}^{2}A+10B$$
20	12 19	eqtri	Could not format ( ; 1 0 x. ; A B ) = ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) : No typesetting found for |- ( ; 1 0 x. ; A B ) = ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) with typecode |-
21	20	oveq1i	Could not format ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C ) : No typesetting found for |- ( ( ; 1 0 x. ; A B ) + C ) = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C ) with typecode |-
22	3 21	eqtri	Could not format ; ; A B C = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C ) : No typesetting found for |- ; ; A B C = ( ( ( ( ; 1 0 ^ 2 ) x. A ) + ( ; 1 0 x. B ) ) + C ) with typecode |-