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 ℕ_{0}$
	3dec.b	$⊢ B \in ℕ_{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 ℕ_{0}$
2		3dec.b	$⊢ B \in ℕ_{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 ℕ$
7	6	nncni	$⊢ 10 \in ℂ$
8	1	nn0cni	$⊢ A \in ℂ$
9	7 8	mulcli	$⊢ 10 A \in ℂ$
10	2	nn0cni	$⊢ B \in ℂ$
11	7 9 10	adddii	$⊢ 10 (10 A + B) = 10 10 A + 10 B$
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 10 A = 10 10 A$
14	13	eqcomi	$⊢ 10 10 A = 10 \cdot 10 A$
15	7	sqvali	$⊢ 10^{2} = 10 \cdot 10$
16	15	eqcomi	$⊢ 10 \cdot 10 = 10^{2}$
17	16	oveq1i	$⊢ 10 \cdot 10 A = 10^{2} A$
18	14 17	eqtri	$⊢ 10 10 A = 10^{2} A$
19	18	oveq1i	$⊢ 10 10 A + 10 B = 10^{2} A + 10 B$
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 \|-

Metamath Proof Explorer

Theorem 3dec

Proof