Theorem fmtno5lem2

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

	Ref	Expression
Assertion	fmtno5lem2	$$⊢65536\cdot 5=327680$$

Proof

Step	Hyp	Ref	Expression
1		5nn0	$$⊢5\in {\mathbb{N}}_0$$
2		6nn0	$$⊢6\in {\mathbb{N}}_0$$
3	2 1	deccl	$$⊢65\in {\mathbb{N}}_0$$
4	3 1	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		0nn0	$$⊢0\in {\mathbb{N}}_0$$
9		2nn0	$$⊢2\in {\mathbb{N}}_0$$
10	5 9	deccl	$$⊢32\in {\mathbb{N}}_0$$
11		7nn0	$$⊢7\in {\mathbb{N}}_0$$
12	10 11	deccl	$$⊢327\in {\mathbb{N}}_0$$
13	12 2	deccl	$$⊢3276\in {\mathbb{N}}_0$$
14		eqid	$$⊢6553=6553$$
15		1nn0	$$⊢1\in {\mathbb{N}}_0$$
16		5p1e6	$$⊢5+1=6$$
17		eqid	$$⊢655=655$$
18		eqid	$$⊢65=65$$
19		6t5e30	$$⊢6\cdot 5=30$$
20		2cn	$$⊢2\in ℂ$$
21	20	addlidi	$$⊢0+2=2$$
22	5 8 9 19 21	decaddi	$$⊢6\cdot 5+2=32$$
23		5t5e25	$$⊢5\cdot 5=25$$
24	1 2 1 18 1 9 22 23	decmul1c	$$⊢65\cdot 5=325$$
25		5p2e7	$$⊢5+2=7$$
26	10 1 9 24 25	decaddi	$$⊢65\cdot 5+2=327$$
27	1 3 1 17 1 9 26 23	decmul1c	$$⊢655\cdot 5=3275$$
28	12 1 16 27	decsuc	$$⊢655\cdot 5+1=3276$$
29		5cn	$$⊢5\in ℂ$$
30		3cn	$$⊢3\in ℂ$$
31		5t3e15	$$⊢5\cdot 3=15$$
32	29 30 31	mulcomli	$$⊢3\cdot 5=15$$
33	1 4 5 14 1 15 28 32	decmul1c	$$⊢6553\cdot 5=32765$$
34		5p3e8	$$⊢5+3=8$$
35	13 1 5 33 34	decaddi	$$⊢6553\cdot 5+3=32768$$
36	1 6 2 7 8 5 35 19	decmul1c	$$⊢65536\cdot 5=327680$$