Theorem 257prm

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

	Ref	Expression
Assertion	257prm	|- ; ; 2 5 7 e. Prime

Proof

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