Theorem fmtno5lem1

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

	Ref	Expression
Assertion	fmtno5lem1	$$⊢65536\cdot 6=393216$$

Proof

Step	Hyp	Ref	Expression
1		6nn0	$$⊢6\in {\mathbb{N}}_0$$
2		5nn0	$$⊢5\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢65\in {\mathbb{N}}_0$$
4	3 2	deccl	$$⊢655\in {\mathbb{N}}_0$$
5		3nn0	$$⊢3\in {\mathbb{N}}_0$$
6	4 5	deccl	$$⊢6553\in {\mathbb{N}}_0$$
7		eqid	$$⊢65536=65536$$
8		9nn0	$$⊢9\in {\mathbb{N}}_0$$
9	5 8	deccl	$$⊢39\in {\mathbb{N}}_0$$
10	9 5	deccl	$$⊢393\in {\mathbb{N}}_0$$
11		1nn0	$$⊢1\in {\mathbb{N}}_0$$
12	10 11	deccl	$$⊢3931\in {\mathbb{N}}_0$$
13		8nn0	$$⊢8\in {\mathbb{N}}_0$$
14		eqid	$$⊢6553=6553$$
15		0nn0	$$⊢0\in {\mathbb{N}}_0$$
16		0p1e1	$$⊢0+1=1$$
17		eqid	$$⊢655=655$$
18		eqid	$$⊢65=65$$
19		6t6e36	$$⊢6\cdot 6=36$$
20		6p3e9	$$⊢6+3=9$$
21	5 1 5 19 20	decaddi	$$⊢6\cdot 6+3=39$$
22		6cn	$$⊢6\in ℂ$$
23		5cn	$$⊢5\in ℂ$$
24		6t5e30	$$⊢6\cdot 5=30$$
25	22 23 24	mulcomli	$$⊢5\cdot 6=30$$
26	1 1 2 18 15 5 21 25	decmul1c	$$⊢65\cdot 6=390$$
27		3cn	$$⊢3\in ℂ$$
28	27	addid2i	$$⊢0+3=3$$
29	9 15 5 26 28	decaddi	$$⊢65\cdot 6+3=393$$
30	1 3 2 17 15 5 29 25	decmul1c	$$⊢655\cdot 6=3930$$
31	10 15 16 30	decsuc	$$⊢655\cdot 6+1=3931$$
32		6t3e18	$$⊢6\cdot 3=18$$
33	22 27 32	mulcomli	$$⊢3\cdot 6=18$$
34	1 4 5 14 13 11 31 33	decmul1c	$$⊢6553\cdot 6=39318$$
35		1p1e2	$$⊢1+1=2$$
36		eqid	$$⊢3931=3931$$
37	10 11 35 36	decsuc	$$⊢3931+1=3932$$
38		8p3e11	$$⊢8+3=11$$
39	12 13 5 34 37 11 38	decaddci	$$⊢6553\cdot 6+3=39321$$
40	1 6 1 7 1 5 39 19	decmul1c	$$⊢65536\cdot 6=393216$$