decmul10add

Description: A multiplication of a number and a numeral expressed as addition with first summand as multiple of 10. (Contributed by AV, 22-Jul-2021) (Revised by AV, 6-Sep-2021)

	Ref	Expression
Hypotheses	decmul10add.1	$⊢ A \in ℕ_{0}$
	decmul10add.2	$⊢ B \in ℕ_{0}$
	decmul10add.3	$⊢ M \in ℕ_{0}$
	decmul10add.4	$⊢ E = M A$
	decmul10add.5	$⊢ F = M B$
Assertion	decmul10add	Could not format assertion : No typesetting found for \|- ( M x. ; A B ) = ( ; E 0 + F ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		decmul10add.1	$⊢ A \in ℕ_{0}$
2		decmul10add.2	$⊢ B \in ℕ_{0}$
3		decmul10add.3	$⊢ M \in ℕ_{0}$
4		decmul10add.4	$⊢ E = M A$
5		decmul10add.5	$⊢ F = M B$
6		dfdec10	Could not format ; A B = ( ( ; 1 0 x. A ) + B ) : No typesetting found for \|- ; A B = ( ( ; 1 0 x. A ) + B ) with typecode \|-
7	6	oveq2i	Could not format ( M x. ; A B ) = ( M x. ( ( ; 1 0 x. A ) + B ) ) : No typesetting found for \|- ( M x. ; A B ) = ( M x. ( ( ; 1 0 x. A ) + B ) ) with typecode \|-
8	3	nn0cni	$⊢ M \in ℂ$
9		10nn0	$⊢ 10 \in ℕ_{0}$
10	9 1	nn0mulcli	$⊢ 10 A \in ℕ_{0}$
11	10	nn0cni	$⊢ 10 A \in ℂ$
12	2	nn0cni	$⊢ B \in ℂ$
13	8 11 12	adddii	$⊢ M (10 A + B) = M 10 A + M B$
14	9	nn0cni	$⊢ 10 \in ℂ$
15	1	nn0cni	$⊢ A \in ℂ$
16	8 14 15	mul12i	$⊢ M 10 A = 10 M A$
17	3 1	nn0mulcli	$⊢ M A \in ℕ_{0}$
18	17	dec0u	Could not format ( ; 1 0 x. ( M x. A ) ) = ; ( M x. A ) 0 : No typesetting found for \|- ( ; 1 0 x. ( M x. A ) ) = ; ( M x. A ) 0 with typecode \|-
19	4	eqcomi	$⊢ M A = E$
20	19	deceq1i	Could not format ; ( M x. A ) 0 = ; E 0 : No typesetting found for \|- ; ( M x. A ) 0 = ; E 0 with typecode \|-
21	16 18 20	3eqtri	Could not format ( M x. ( ; 1 0 x. A ) ) = ; E 0 : No typesetting found for \|- ( M x. ( ; 1 0 x. A ) ) = ; E 0 with typecode \|-
22	5	eqcomi	$⊢ M B = F$
23	21 22	oveq12i	Could not format ( ( M x. ( ; 1 0 x. A ) ) + ( M x. B ) ) = ( ; E 0 + F ) : No typesetting found for \|- ( ( M x. ( ; 1 0 x. A ) ) + ( M x. B ) ) = ( ; E 0 + F ) with typecode \|-
24	7 13 23	3eqtri	Could not format ( M x. ; A B ) = ( ; E 0 + F ) : No typesetting found for \|- ( M x. ; A B ) = ( ; E 0 + F ) with typecode \|-

Metamath Proof Explorer

Theorem decmul10add

Proof