Theorem fmtno5faclem2

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

	Ref	Expression
Assertion	fmtno5faclem2	$$⊢6700417\cdot 6=40202502$$

Proof

Step	Hyp	Ref	Expression
1		6nn0	$$⊢6\in {\mathbb{N}}_0$$
2		7nn0	$$⊢7\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢67\in {\mathbb{N}}_0$$
4		0nn0	$$⊢0\in {\mathbb{N}}_0$$
5	3 4	deccl	$$⊢670\in {\mathbb{N}}_0$$
6	5 4	deccl	$$⊢6700\in {\mathbb{N}}_0$$
7		4nn0	$$⊢4\in {\mathbb{N}}_0$$
8	6 7	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		2nn0	$$⊢2\in {\mathbb{N}}_0$$
13	7 4	deccl	$$⊢40\in {\mathbb{N}}_0$$
14	13 12	deccl	$$⊢402\in {\mathbb{N}}_0$$
15	14 4	deccl	$$⊢4020\in {\mathbb{N}}_0$$
16	15 12	deccl	$$⊢40202\in {\mathbb{N}}_0$$
17	16 7	deccl	$$⊢402024\in {\mathbb{N}}_0$$
18		eqid	$$⊢670041=670041$$
19		eqid	$$⊢67004=67004$$
20		eqid	$$⊢6700=6700$$
21		eqid	$$⊢670=670$$
22		eqid	$$⊢67=67$$
23		3nn0	$$⊢3\in {\mathbb{N}}_0$$
24		6t6e36	$$⊢6\cdot 6=36$$
25		3p1e4	$$⊢3+1=4$$
26		6p4e10	$$⊢6+4=10$$
27	23 1 7 24 25 26	decaddci2	$$⊢6\cdot 6+4=40$$
28		7t6e42	$$⊢7\cdot 6=42$$
29	1 1 2 22 12 7 27 28	decmul1c	$$⊢67\cdot 6=402$$
30		6cn	$$⊢6\in ℂ$$
31	30	mul02i	$$⊢0\cdot 6=0$$
32	1 3 4 21 29 31	decmul1	$$⊢670\cdot 6=4020$$
33	1 5 4 20 32 31	decmul1	$$⊢6700\cdot 6=40200$$
34		2cn	$$⊢2\in ℂ$$
35	34	addid2i	$$⊢0+2=2$$
36	15 4 12 33 35	decaddi	$$⊢6700\cdot 6+2=40202$$
37		4cn	$$⊢4\in ℂ$$
38		6t4e24	$$⊢6\cdot 4=24$$
39	30 37 38	mulcomli	$$⊢4\cdot 6=24$$
40	1 6 7 19 7 12 36 39	decmul1c	$$⊢67004\cdot 6=402024$$
41	30	mulid2i	$$⊢1\cdot 6=6$$
42	1 8 9 18 40 41	decmul1	$$⊢670041\cdot 6=4020246$$
43		eqid	$$⊢402024=402024$$
44		4p1e5	$$⊢4+1=5$$
45	16 7 9 43 44	decaddi	$$⊢402024+1=402025$$
46	17 1 7 42 45 26	decaddci2	$$⊢670041\cdot 6+4=4020250$$
47	1 10 2 11 12 7 46 28	decmul1c	$$⊢6700417\cdot 6=40202502$$