Theorem 257prm

Description: 257 is a prime number (thefourth Fermat prime). (Contributed by AV, 15-Jun-2021)

	Ref	Expression
Assertion	257prm	$$⊢257\in \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$$⊢2\in {\mathbb{N}}_0$$
2		5nn0	$$⊢5\in {\mathbb{N}}_0$$
3	1 2	deccl	$$⊢25\in {\mathbb{N}}_0$$
4		7nn	$$⊢7\in \mathbb{N}$$
5	3 4	decnncl	$$⊢257\in \mathbb{N}$$
6		8nn0	$$⊢8\in {\mathbb{N}}_0$$
7		4nn0	$$⊢4\in {\mathbb{N}}_0$$
8		7nn0	$$⊢7\in {\mathbb{N}}_0$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10		2lt8	$$⊢2<8$$
11		5lt10	$$⊢5<10$$
12		7lt10	$$⊢7<10$$
13	1 6 2 7 8 9 10 11 12	3decltc	$$⊢257<841$$
14		5nn	$$⊢5\in \mathbb{N}$$
15	1 14	decnncl	$$⊢25\in \mathbb{N}$$
16		1lt10	$$⊢1<10$$
17	15 8 9 16	declti	$$⊢1<257$$
18		3nn0	$$⊢3\in {\mathbb{N}}_0$$
19		3t2e6	$$⊢3\cdot 2=6$$
20		df-7	$$⊢7=6+1$$
21	3 18 19 20	dec2dvds	$$⊢\neg 2\parallel 257$$
22		3nn	$$⊢3\in \mathbb{N}$$
23		2nn	$$⊢2\in \mathbb{N}$$
24		3cn	$$⊢3\in ℂ$$
25	24	mulid1i	$$⊢3\cdot 1=3$$
26	25	oveq1i	$$⊢3\cdot 1+2=3+2$$
27		3p2e5	$$⊢3+2=5$$
28	26 27	eqtri	$$⊢3\cdot 1+2=5$$
29		2lt3	$$⊢2<3$$
30	22 9 23 28 29	ndvdsi	$$⊢\neg 3\parallel 5$$
31	1 2 8	3dvds2dec	$$⊢3\parallel 257\leftrightarrow 3\parallel \left(2+5+7\right)$$
32		5cn	$$⊢5\in ℂ$$
33		2cn	$$⊢2\in ℂ$$
34		5p2e7	$$⊢5+2=7$$
35	32 33 34	addcomli	$$⊢2+5=7$$
36	35	oveq1i	$$⊢2+5+7=7+7$$
37		7p7e14	$$⊢7+7=14$$
38	36 37	eqtri	$$⊢2+5+7=14$$
39	38	breq2i	$$⊢3\parallel \left(2+5+7\right)\leftrightarrow 3\parallel 14$$
40	9 7	3dvdsdec	$$⊢3\parallel 14\leftrightarrow 3\parallel \left(1+4\right)$$
41		4cn	$$⊢4\in ℂ$$
42		ax-1cn	$$⊢1\in ℂ$$
43		4p1e5	$$⊢4+1=5$$
44	41 42 43	addcomli	$$⊢1+4=5$$
45	44	breq2i	$$⊢3\parallel \left(1+4\right)\leftrightarrow 3\parallel 5$$
46	40 45	bitri	$$⊢3\parallel 14\leftrightarrow 3\parallel 5$$
47	31 39 46	3bitri	$$⊢3\parallel 257\leftrightarrow 3\parallel 5$$
48	30 47	mtbir	$$⊢\neg 3\parallel 257$$
49		2lt5	$$⊢2<5$$
50	3 23 49 34	dec5dvds2	$$⊢\neg 5\parallel 257$$
51		6nn0	$$⊢6\in {\mathbb{N}}_0$$
52	18 51	deccl	$$⊢36\in {\mathbb{N}}_0$$
53		eqid	$$⊢36=36$$
54		7t3e21	$$⊢7\cdot 3=21$$
55	1 9 7 54 44	decaddi	$$⊢7\cdot 3+4=25$$
56		7t6e42	$$⊢7\cdot 6=42$$
57	8 18 51 53 1 7 55 56	decmul2c	$$⊢7\cdot 36=252$$
58	3 1 2 57 35	decaddi	$$⊢7\cdot 36+5=257$$
59		5lt7	$$⊢5<7$$
60	4 52 14 58 59	ndvdsi	$$⊢\neg 7\parallel 257$$
61		1nn	$$⊢1\in \mathbb{N}$$
62	9 61	decnncl	$$⊢11\in \mathbb{N}$$
63	1 18	deccl	$$⊢23\in {\mathbb{N}}_0$$
64		4nn	$$⊢4\in \mathbb{N}$$
65	9 9	deccl	$$⊢11\in {\mathbb{N}}_0$$
66		eqid	$$⊢23=23$$
67	65	nn0cni	$$⊢11\in ℂ$$
68	67 33	mulcomi	$$⊢11\cdot 2=2\cdot 11$$
69	68	oveq1i	$$⊢11\cdot 2+3=2\cdot 11+3$$
70	1	11multnc	$$⊢2\cdot 11=22$$
71	24 33 27	addcomli	$$⊢2+3=5$$
72	1 1 18 70 71	decaddi	$$⊢2\cdot 11+3=25$$
73	69 72	eqtri	$$⊢11\cdot 2+3=25$$
74	18	11multnc	$$⊢3\cdot 11=33$$
75	24 67 74	mulcomli	$$⊢11\cdot 3=33$$
76	65 1 18 66 18 18 73 75	decmul2c	$$⊢11\cdot 23=253$$
77		4p3e7	$$⊢4+3=7$$
78	41 24 77	addcomli	$$⊢3+4=7$$
79	3 18 7 76 78	decaddi	$$⊢11\cdot 23+4=257$$
80		4lt10	$$⊢4<10$$
81	61 9 7 80	declti	$$⊢4<11$$
82	62 63 64 79 81	ndvdsi	$$⊢\neg 11\parallel 257$$
83	9 22	decnncl	$$⊢13\in \mathbb{N}$$
84		9nn0	$$⊢9\in {\mathbb{N}}_0$$
85	9 84	deccl	$$⊢19\in {\mathbb{N}}_0$$
86		10nn	$$⊢10\in \mathbb{N}$$
87	9 18	deccl	$$⊢13\in {\mathbb{N}}_0$$
88	87	nn0cni	$$⊢13\in ℂ$$
89	85	nn0cni	$$⊢19\in ℂ$$
90	88 89	mulcomi	$$⊢13\cdot 19=19\cdot 13$$
91	90	oveq1i	$$⊢13\cdot 19+10=19\cdot 13+10$$
92		0nn0	$$⊢0\in {\mathbb{N}}_0$$
93		eqid	$$⊢19=19$$
94		eqid	$$⊢10=10$$
95	88	mulid2i	$$⊢1\cdot 13=13$$
96		1p1e2	$$⊢1+1=2$$
97		eqid	$$⊢11=11$$
98	9 9 96 97	decsuc	$$⊢11+1=12$$
99	67 42 98	addcomli	$$⊢1+11=12$$
100	9 18 9 1 95 99 96 27	decadd	$$⊢1\cdot 13+1+11=25$$
101		eqid	$$⊢13=13$$
102		9cn	$$⊢9\in ℂ$$
103	102	mulid1i	$$⊢9\cdot 1=9$$
104	103	oveq1i	$$⊢9\cdot 1+2=9+2$$
105		9p2e11	$$⊢9+2=11$$
106	104 105	eqtri	$$⊢9\cdot 1+2=11$$
107		9t3e27	$$⊢9\cdot 3=27$$
108	84 9 18 101 8 1 106 107	decmul2c	$$⊢9\cdot 13=117$$
109	108	oveq1i	$$⊢9\cdot 13+0=117+0$$
110	65 8	deccl	$$⊢117\in {\mathbb{N}}_0$$
111	110	nn0cni	$$⊢117\in ℂ$$
112	111	addid1i	$$⊢117+0=117$$
113	109 112	eqtri	$$⊢9\cdot 13+0=117$$
114	9 84 9 92 93 94 87 8 65 100 113	decmac	$$⊢19\cdot 13+10=257$$
115	91 114	eqtri	$$⊢13\cdot 19+10=257$$
116		3pos	$$⊢0<3$$
117	9 92 22 116	declt	$$⊢10<13$$
118	83 85 86 115 117	ndvdsi	$$⊢\neg 13\parallel 257$$
119	9 4	decnncl	$$⊢17\in \mathbb{N}$$
120	9 2	deccl	$$⊢15\in {\mathbb{N}}_0$$
121	9 8	deccl	$$⊢17\in {\mathbb{N}}_0$$
122		eqid	$$⊢15=15$$
123	121	nn0cni	$$⊢17\in ℂ$$
124	123	mulid1i	$$⊢17\cdot 1=17$$
125		8cn	$$⊢8\in ℂ$$
126		7cn	$$⊢7\in ℂ$$
127		8p7e15	$$⊢8+7=15$$
128	125 126 127	addcomli	$$⊢7+8=15$$
129	9 8 6 124 96 2 128	decaddci	$$⊢17\cdot 1+8=25$$
130		eqid	$$⊢17=17$$
131	32	mulid2i	$$⊢1\cdot 5=5$$
132	131	oveq1i	$$⊢1\cdot 5+3=5+3$$
133		5p3e8	$$⊢5+3=8$$
134	132 133	eqtri	$$⊢1\cdot 5+3=8$$
135		7t5e35	$$⊢7\cdot 5=35$$
136	2 9 8 130 2 18 134 135	decmul1c	$$⊢17\cdot 5=85$$
137	121 9 2 122 2 6 129 136	decmul2c	$$⊢17\cdot 15=255$$
138	3 2 1 137 34	decaddi	$$⊢17\cdot 15+2=257$$
139		2lt10	$$⊢2<10$$
140	61 8 1 139	declti	$$⊢2<17$$
141	119 120 23 138 140	ndvdsi	$$⊢\neg 17\parallel 257$$
142		9nn	$$⊢9\in \mathbb{N}$$
143	9 142	decnncl	$$⊢19\in \mathbb{N}$$
144		9pos	$$⊢0<9$$
145	9 92 142 144	declt	$$⊢10<19$$
146	143 87 86 114 145	ndvdsi	$$⊢\neg 19\parallel 257$$
147	1 22	decnncl	$$⊢23\in \mathbb{N}$$
148	65 1 18 66 18 18 72 74	decmul1c	$$⊢23\cdot 11=253$$
149	3 18 7 148 78	decaddi	$$⊢23\cdot 11+4=257$$
150	23 18 7 80	declti	$$⊢4<23$$
151	147 65 64 149 150	ndvdsi	$$⊢\neg 23\parallel 257$$
152	5 13 17 21 48 50 60 82 118 141 146 151	prmlem2	$$⊢257\in \mathbb{P}$$