Theorem fmtno5faclem1

Description: Lemma 1 for fmtno5fac . (Contributed by AV, 22-Jul-2021)

	Ref	Expression
Assertion	fmtno5faclem1	$$⊢6700417\cdot 4=26801668$$

Proof

Step	Hyp	Ref	Expression
1		4nn0	$$⊢4\in {\mathbb{N}}_0$$
2		6nn0	$$⊢6\in {\mathbb{N}}_0$$
3		7nn0	$$⊢7\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢67\in {\mathbb{N}}_0$$
5		0nn0	$$⊢0\in {\mathbb{N}}_0$$
6	4 5	deccl	$$⊢670\in {\mathbb{N}}_0$$
7	6 5	deccl	$$⊢6700\in {\mathbb{N}}_0$$
8	7 1	deccl	$$⊢67004\in {\mathbb{N}}_0$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10	8 9	deccl	$$⊢670041\in {\mathbb{N}}_0$$
11		eqid	$$⊢6700417=6700417$$
12		8nn0	$$⊢8\in {\mathbb{N}}_0$$
13		2nn0	$$⊢2\in {\mathbb{N}}_0$$
14	13 2	deccl	$$⊢26\in {\mathbb{N}}_0$$
15	14 12	deccl	$$⊢268\in {\mathbb{N}}_0$$
16	15 5	deccl	$$⊢2680\in {\mathbb{N}}_0$$
17	16 9	deccl	$$⊢26801\in {\mathbb{N}}_0$$
18	17 2	deccl	$$⊢268016\in {\mathbb{N}}_0$$
19		eqid	$$⊢670041=670041$$
20		eqid	$$⊢67004=67004$$
21		eqid	$$⊢6700=6700$$
22		eqid	$$⊢670=670$$
23		eqid	$$⊢67=67$$
24		6t4e24	$$⊢6\cdot 4=24$$
25		4p2e6	$$⊢4+2=6$$
26	13 1 13 24 25	decaddi	$$⊢6\cdot 4+2=26$$
27		7t4e28	$$⊢7\cdot 4=28$$
28	1 2 3 23 12 13 26 27	decmul1c	$$⊢67\cdot 4=268$$
29		4cn	$$⊢4\in ℂ$$
30	29	mul02i	$$⊢0\cdot 4=0$$
31	1 4 5 22 28 30	decmul1	$$⊢670\cdot 4=2680$$
32	1 6 5 21 31 30	decmul1	$$⊢6700\cdot 4=26800$$
33		0p1e1	$$⊢0+1=1$$
34	16 5 9 32 33	decaddi	$$⊢6700\cdot 4+1=26801$$
35		4t4e16	$$⊢4\cdot 4=16$$
36	1 7 1 20 2 9 34 35	decmul1c	$$⊢67004\cdot 4=268016$$
37	29	mullidi	$$⊢1\cdot 4=4$$
38	1 8 9 19 36 37	decmul1	$$⊢670041\cdot 4=2680164$$
39	18 1 13 38 25	decaddi	$$⊢670041\cdot 4+2=2680166$$
40	1 10 3 11 12 13 39 27	decmul1c	$$⊢6700417\cdot 4=26801668$$