Theorem fmtno4nprmfac193

Description: 193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021)

	Ref	Expression
Assertion	fmtno4nprmfac193	$$⊢\neg 193\parallel \mathrm{FermatNo}\left(4\right)$$

Proof

Step	Hyp	Ref	Expression
1		1nn0	$$⊢1\in {\mathbb{N}}_0$$
2		9nn0	$$⊢9\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢19\in {\mathbb{N}}_0$$
4		3nn	$$⊢3\in \mathbb{N}$$
5	3 4	decnncl	$$⊢193\in \mathbb{N}$$
6		3nn0	$$⊢3\in {\mathbb{N}}_0$$
7	6 6	deccl	$$⊢33\in {\mathbb{N}}_0$$
8	7 2	deccl	$$⊢339\in {\mathbb{N}}_0$$
9		1nn	$$⊢1\in \mathbb{N}$$
10	1 9	decnncl	$$⊢11\in \mathbb{N}$$
11	10	decnncl2	$$⊢110\in \mathbb{N}$$
12		6nn0	$$⊢6\in {\mathbb{N}}_0$$
13		5nn0	$$⊢5\in {\mathbb{N}}_0$$
14	12 13	deccl	$$⊢65\in {\mathbb{N}}_0$$
15		4nn0	$$⊢4\in {\mathbb{N}}_0$$
16	14 15	deccl	$$⊢654\in {\mathbb{N}}_0$$
17		2nn0	$$⊢2\in {\mathbb{N}}_0$$
18	16 17	deccl	$$⊢6542\in {\mathbb{N}}_0$$
19		7nn0	$$⊢7\in {\mathbb{N}}_0$$
20	1 1	deccl	$$⊢11\in {\mathbb{N}}_0$$
21		0nn0	$$⊢0\in {\mathbb{N}}_0$$
22	3 6	deccl	$$⊢193\in {\mathbb{N}}_0$$
23		eqid	$$⊢339=339$$
24	1 19	deccl	$$⊢17\in {\mathbb{N}}_0$$
25	24 6	deccl	$$⊢173\in {\mathbb{N}}_0$$
26		eqid	$$⊢33=33$$
27		eqid	$$⊢173=173$$
28		8nn0	$$⊢8\in {\mathbb{N}}_0$$
29	13 28	deccl	$$⊢58\in {\mathbb{N}}_0$$
30	13 19	deccl	$$⊢57\in {\mathbb{N}}_0$$
31		eqid	$$⊢193=193$$
32		eqid	$$⊢19=19$$
33		3cn	$$⊢3\in ℂ$$
34	33	mulid2i	$$⊢1\cdot 3=3$$
35	34	oveq1i	$$⊢1\cdot 3+2=3+2$$
36		3p2e5	$$⊢3+2=5$$
37	35 36	eqtri	$$⊢1\cdot 3+2=5$$
38		9t3e27	$$⊢9\cdot 3=27$$
39	6 1 2 32 19 17 37 38	decmul1c	$$⊢19\cdot 3=57$$
40		3t3e9	$$⊢3\cdot 3=9$$
41	6 3 6 31 39 40	decmul1	$$⊢193\cdot 3=579$$
42		eqid	$$⊢17=17$$
43		eqid	$$⊢58=58$$
44		5cn	$$⊢5\in ℂ$$
45		ax-1cn	$$⊢1\in ℂ$$
46		5p1e6	$$⊢5+1=6$$
47	44 45 46	addcomli	$$⊢1+5=6$$
48	47	oveq1i	$$⊢1+5+1=6+1$$
49		6p1e7	$$⊢6+1=7$$
50	48 49	eqtri	$$⊢1+5+1=7$$
51		8cn	$$⊢8\in ℂ$$
52		7cn	$$⊢7\in ℂ$$
53		8p7e15	$$⊢8+7=15$$
54	51 52 53	addcomli	$$⊢7+8=15$$
55	1 19 13 28 42 43 50 13 54	decaddc	$$⊢17+58=75$$
56		4p1e5	$$⊢4+1=5$$
57		eqid	$$⊢57=57$$
58		7p7e14	$$⊢7+7=14$$
59	13 19 19 57 46 15 58	decaddci	$$⊢57+7=64$$
60	12 15 56 59	decsuc	$$⊢57+7+1=65$$
61		9p5e14	$$⊢9+5=14$$
62	30 2 19 13 41 55 60 15 61	decaddc	$$⊢193\cdot 3+17+58=654$$
63		7p1e8	$$⊢7+1=8$$
64	13 19 63 57	decsuc	$$⊢57+1=58$$
65		9p3e12	$$⊢9+3=12$$
66	30 2 6 41 64 17 65	decaddci	$$⊢193\cdot 3+3=582$$
67	6 6 24 6 26 27 22 17 29 62 66	decma2c	$$⊢193\cdot 33+173=6542$$
68		9cn	$$⊢9\in ℂ$$
69	68	mulid2i	$$⊢1\cdot 9=9$$
70	69	oveq1i	$$⊢1\cdot 9+8=9+8$$
71		9p8e17	$$⊢9+8=17$$
72	70 71	eqtri	$$⊢1\cdot 9+8=17$$
73		9t9e81	$$⊢9\cdot 9=81$$
74	2 1 2 32 1 28 72 73	decmul1c	$$⊢19\cdot 9=171$$
75		1p2e3	$$⊢1+2=3$$
76	24 1 17 74 75	decaddi	$$⊢19\cdot 9+2=173$$
77	68 33 38	mulcomli	$$⊢3\cdot 9=27$$
78	2 3 6 31 19 17 76 77	decmul1c	$$⊢193\cdot 9=1737$$
79	22 7 2 23 19 25 67 78	decmul2c	$$⊢193\cdot 339=65427$$
80		eqid	$$⊢110=110$$
81		eqid	$$⊢6542=6542$$
82		eqid	$$⊢11=11$$
83		eqid	$$⊢654=654$$
84	14 15 56 83	decsuc	$$⊢654+1=655$$
85		2p1e3	$$⊢2+1=3$$
86	16 17 1 1 81 82 84 85	decadd	$$⊢6542+11=6553$$
87	52	addid1i	$$⊢7+0=7$$
88	18 19 20 21 79 80 86 87	decadd	$$⊢193\cdot 339+110=65537$$
89		10pos	$$⊢0<10$$
90		9nn	$$⊢9\in \mathbb{N}$$
91		1lt9	$$⊢1<9$$
92	1 1 90 91	declt	$$⊢11<19$$
93	20 3 21 6 89 92	decltc	$$⊢110<193$$
94	5 8 11 88 93	ndvdsi	$$⊢\neg 193\parallel 65537$$
95		fmtno4	$$⊢\mathrm{FermatNo}\left(4\right)=65537$$
96	95	breq2i	$$⊢193\parallel \mathrm{FermatNo}\left(4\right)\leftrightarrow 193\parallel 65537$$
97	94 96	mtbir	$$⊢\neg 193\parallel \mathrm{FermatNo}\left(4\right)$$