Theorem fmtno5fac

Description: The factorisation of the 5 th Fermat number, see remark in ApostolNT p. 7. (Contributed by AV, 22-Jul-2021)

	Ref	Expression
Assertion	fmtno5fac	$$⊢\mathrm{FermatNo}\left(5\right)=6700417\cdot 641$$

Proof

Step	Hyp	Ref	Expression
1		4nn0	$$⊢4\in {\mathbb{N}}_0$$
2		2nn0	$$⊢2\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢42\in {\mathbb{N}}_0$$
4		8nn0	$$⊢8\in {\mathbb{N}}_0$$
5	3 4	deccl	$$⊢428\in {\mathbb{N}}_0$$
6	5 4	deccl	$$⊢4288\in {\mathbb{N}}_0$$
7	6 2	deccl	$$⊢42882\in {\mathbb{N}}_0$$
8		6nn0	$$⊢6\in {\mathbb{N}}_0$$
9	7 8	deccl	$$⊢428826\in {\mathbb{N}}_0$$
10	9 8	deccl	$$⊢4288266\in {\mathbb{N}}_0$$
11	10 4	deccl	$$⊢42882668\in {\mathbb{N}}_0$$
12	11 4	deccl	$$⊢428826688\in {\mathbb{N}}_0$$
13		0nn0	$$⊢0\in {\mathbb{N}}_0$$
14		7nn0	$$⊢7\in {\mathbb{N}}_0$$
15	8 14	deccl	$$⊢67\in {\mathbb{N}}_0$$
16	15 13	deccl	$$⊢670\in {\mathbb{N}}_0$$
17	16 13	deccl	$$⊢6700\in {\mathbb{N}}_0$$
18	17 1	deccl	$$⊢67004\in {\mathbb{N}}_0$$
19		1nn0	$$⊢1\in {\mathbb{N}}_0$$
20	18 19	deccl	$$⊢670041\in {\mathbb{N}}_0$$
21		fmtno5faclem3	$$⊢402025020+26801668=428826688$$
22	21	deceq1i	Could not format ; ( ; ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 0 + ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8 ) 0 = ; ; ; ; ; ; ; ; ; 4 2 8 8 2 6 6 8 8 0 : No typesetting found for |- ; ( ; ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 0 + ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8 ) 0 = ; ; ; ; ; ; ; ; ; 4 2 8 8 2 6 6 8 8 0 with typecode |-
23		eqid	$$⊢6700417=6700417$$
24		eqid	$$⊢428826688=428826688$$
25		eqid	$$⊢670041=670041$$
26		eqid	$$⊢42882668=42882668$$
27		eqid	$$⊢67004=67004$$
28		9nn0	$$⊢9\in {\mathbb{N}}_0$$
29	3 28	deccl	$$⊢429\in {\mathbb{N}}_0$$
30	29 1	deccl	$$⊢4294\in {\mathbb{N}}_0$$
31	30 28	deccl	$$⊢42949\in {\mathbb{N}}_0$$
32	31 8	deccl	$$⊢429496\in {\mathbb{N}}_0$$
33		6p1e7	$$⊢6+1=7$$
34		eqid	$$⊢4288266=4288266$$
35		eqid	$$⊢6700=6700$$
36		eqid	$$⊢428826=428826$$
37		eqid	$$⊢670=670$$
38		eqid	$$⊢42882=42882$$
39		eqid	$$⊢67=67$$
40		eqid	$$⊢4288=4288$$
41		8p1e9	$$⊢8+1=9$$
42		eqid	$$⊢428=428$$
43	3 4 41 42	decsuc	$$⊢428+1=429$$
44		8p6e14	$$⊢8+6=14$$
45	5 4 8 40 43 1 44	decaddci	$$⊢4288+6=4294$$
46		7cn	$$⊢7\in ℂ$$
47		2cn	$$⊢2\in ℂ$$
48		7p2e9	$$⊢7+2=9$$
49	46 47 48	addcomli	$$⊢2+7=9$$
50	6 2 8 14 38 39 45 49	decadd	$$⊢42882+67=42949$$
51		6cn	$$⊢6\in ℂ$$
52	51	addridi	$$⊢6+0=6$$
53	7 8 15 13 36 37 50 52	decadd	$$⊢428826+670=429496$$
54	9 8 16 13 34 35 53 52	decadd	$$⊢4288266+6700=4294966$$
55	32 8 33 54	decsuc	$$⊢4288266+6700+1=4294967$$
56		8p4e12	$$⊢8+4=12$$
57	10 4 17 1 26 27 55 2 56	decaddc	$$⊢42882668+67004=42949672$$
58	11 4 18 19 24 25 57 41	decadd	$$⊢428826688+670041=429496729$$
59	46	addlidi	$$⊢0+7=7$$
60	12 13 20 14 22 23 58 59	decadd	Could not format ( ; ( ; ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 0 + ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8 ) 0 + ; ; ; ; ; ; 6 7 0 0 4 1 7 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 7 : No typesetting found for |- ( ; ( ; ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 0 + ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8 ) 0 + ; ; ; ; ; ; 6 7 0 0 4 1 7 ) = ; ; ; ; ; ; ; ; ; 4 2 9 4 9 6 7 2 9 7 with typecode |-
61	8 1	deccl	$$⊢64\in {\mathbb{N}}_0$$
62	20 14	deccl	$$⊢6700417\in {\mathbb{N}}_0$$
63		fmtno5faclem2	$$⊢6700417\cdot 6=40202502$$
64	63	eqcomi	$$⊢40202502=6700417\cdot 6$$
65		fmtno5faclem1	$$⊢6700417\cdot 4=26801668$$
66	65	eqcomi	$$⊢26801668=6700417\cdot 4$$
67	8 1 62 64 66	decmul10add	$$⊢6700417\cdot 64=402025020+26801668$$
68	67	eqcomi	$$⊢402025020+26801668=6700417\cdot 64$$
69	62	nn0cni	$$⊢6700417\in ℂ$$
70	69	mulridi	$$⊢6700417\cdot 1=6700417$$
71	70	eqcomi	$$⊢6700417=6700417\cdot 1$$
72	61 19 62 68 71	decmul10add	Could not format ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. ; ; 6 4 1 ) = ( ; ( ; ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 0 + ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8 ) 0 + ; ; ; ; ; ; 6 7 0 0 4 1 7 ) : No typesetting found for |- ( ; ; ; ; ; ; 6 7 0 0 4 1 7 x. ; ; 6 4 1 ) = ( ; ( ; ; ; ; ; ; ; ; 4 0 2 0 2 5 0 2 0 + ; ; ; ; ; ; ; 2 6 8 0 1 6 6 8 ) 0 + ; ; ; ; ; ; 6 7 0 0 4 1 7 ) with typecode |-
73		fmtno5	$$⊢\mathrm{FermatNo}\left(5\right)=4294967297$$
74	60 72 73	3eqtr4ri	$$⊢\mathrm{FermatNo}\left(5\right)=6700417\cdot 641$$