Theorem fmtno5lem3

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

	Ref	Expression
Assertion	fmtno5lem3	$$⊢65536\cdot 3=196608$$

Proof

Step	Hyp	Ref	Expression
1		3nn0	$$⊢3\in {\mathbb{N}}_0$$
2		6nn0	$$⊢6\in {\mathbb{N}}_0$$
3		5nn0	$$⊢5\in {\mathbb{N}}_0$$
4	2 3	deccl	$$⊢65\in {\mathbb{N}}_0$$
5	4 3	deccl	$$⊢655\in {\mathbb{N}}_0$$
6	5 1	deccl	$$⊢6553\in {\mathbb{N}}_0$$
7		eqid	$$⊢65536=65536$$
8		8nn0	$$⊢8\in {\mathbb{N}}_0$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10		9nn0	$$⊢9\in {\mathbb{N}}_0$$
11	9 10	deccl	$$⊢19\in {\mathbb{N}}_0$$
12	11 2	deccl	$$⊢196\in {\mathbb{N}}_0$$
13	12 3	deccl	$$⊢1965\in {\mathbb{N}}_0$$
14		5p1e6	$$⊢5+1=6$$
15		eqid	$$⊢1965=1965$$
16	12 3 14 15	decsuc	$$⊢1965+1=1966$$
17		eqid	$$⊢6553=6553$$
18		eqid	$$⊢655=655$$
19		eqid	$$⊢65=65$$
20		8p1e9	$$⊢8+1=9$$
21		6t3e18	$$⊢6\cdot 3=18$$
22	9 8 20 21	decsuc	$$⊢6\cdot 3+1=19$$
23		5t3e15	$$⊢5\cdot 3=15$$
24	1 2 3 19 3 9 22 23	decmul1c	$$⊢65\cdot 3=195$$
25	11 3 14 24	decsuc	$$⊢65\cdot 3+1=196$$
26	1 4 3 18 3 9 25 23	decmul1c	$$⊢655\cdot 3=1965$$
27		3t3e9	$$⊢3\cdot 3=9$$
28	1 5 1 17 26 27	decmul1	$$⊢6553\cdot 3=19659$$
29	13 16 28	decsucc	$$⊢6553\cdot 3+1=19660$$
30	1 6 2 7 8 9 29 21	decmul1c	$$⊢65536\cdot 3=196608$$