Theorem fmtno5faclem3

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

	Ref	Expression
Assertion	fmtno5faclem3	$$⊢402025020+26801668=428826688$$

Proof

Step	Hyp	Ref	Expression
1		4nn0	$$⊢4\in {\mathbb{N}}_0$$
2		0nn0	$$⊢0\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢40\in {\mathbb{N}}_0$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5	3 4	deccl	$$⊢402\in {\mathbb{N}}_0$$
6	5 2	deccl	$$⊢4020\in {\mathbb{N}}_0$$
7	6 4	deccl	$$⊢40202\in {\mathbb{N}}_0$$
8		5nn0	$$⊢5\in {\mathbb{N}}_0$$
9	7 8	deccl	$$⊢402025\in {\mathbb{N}}_0$$
10	9 2	deccl	$$⊢4020250\in {\mathbb{N}}_0$$
11	10 4	deccl	$$⊢40202502\in {\mathbb{N}}_0$$
12		6nn0	$$⊢6\in {\mathbb{N}}_0$$
13	4 12	deccl	$$⊢26\in {\mathbb{N}}_0$$
14		8nn0	$$⊢8\in {\mathbb{N}}_0$$
15	13 14	deccl	$$⊢268\in {\mathbb{N}}_0$$
16	15 2	deccl	$$⊢2680\in {\mathbb{N}}_0$$
17		1nn0	$$⊢1\in {\mathbb{N}}_0$$
18	16 17	deccl	$$⊢26801\in {\mathbb{N}}_0$$
19	18 12	deccl	$$⊢268016\in {\mathbb{N}}_0$$
20	19 12	deccl	$$⊢2680166\in {\mathbb{N}}_0$$
21		eqid	$$⊢402025020=402025020$$
22		eqid	$$⊢26801668=26801668$$
23		eqid	$$⊢40202502=40202502$$
24		eqid	$$⊢2680166=2680166$$
25		eqid	$$⊢4020250=4020250$$
26		eqid	$$⊢268016=268016$$
27		eqid	$$⊢402025=402025$$
28		eqid	$$⊢26801=26801$$
29		eqid	$$⊢40202=40202$$
30		eqid	$$⊢2680=2680$$
31		eqid	$$⊢4020=4020$$
32		eqid	$$⊢268=268$$
33		eqid	$$⊢402=402$$
34		eqid	$$⊢26=26$$
35		eqid	$$⊢40=40$$
36		2cn	$$⊢2\in ℂ$$
37	36	addid2i	$$⊢0+2=2$$
38	1 2 4 35 37	decaddi	$$⊢40+2=42$$
39		6cn	$$⊢6\in ℂ$$
40		6p2e8	$$⊢6+2=8$$
41	39 36 40	addcomli	$$⊢2+6=8$$
42	3 4 4 12 33 34 38 41	decadd	$$⊢402+26=428$$
43		8cn	$$⊢8\in ℂ$$
44	43	addid2i	$$⊢0+8=8$$
45	5 2 13 14 31 32 42 44	decadd	$$⊢4020+268=4288$$
46	36	addid1i	$$⊢2+0=2$$
47	6 4 15 2 29 30 45 46	decadd	$$⊢40202+2680=42882$$
48		5p1e6	$$⊢5+1=6$$
49	7 8 16 17 27 28 47 48	decadd	$$⊢402025+26801=428826$$
50	39	addid2i	$$⊢0+6=6$$
51	9 2 18 12 25 26 49 50	decadd	$$⊢4020250+268016=4288266$$
52	10 4 19 12 23 24 51 41	decadd	$$⊢40202502+2680166=42882668$$
53	11 2 20 14 21 22 52 44	decadd	$$⊢402025020+26801668=428826688$$