prime_five_hundred_twenty_one

Proof neighborhood

Direct dependencies

Direct dependents

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

1. 0001have hn0 : ~(2 * (11 * 22) + 37 = 0)
2. 0002intro hzero
3. 0003have htail_zero : 37 = 0
4. 0004specialize add_eq_zero_right (2 * (11 * 22))
5. 0005specialize add_eq_zero_right 37
6. 0006apply add_eq_zero_right
7. 0007exact hzero
8. 0008apply PA1
9. 0009exact htail_zero
10. 0010have hn1 : ~(2 * (11 * 22) + 37 = 1)
11. 0011intro hone
12. 0012have htail_le_one : exists k. k + 37 = 1
13. 0013exists 2 * (11 * 22)
14. 0014exact hone
15. 0015have hone_lt_tail : exists k. k + S 1 = 37
16. 0016exists 35
17. 0017norm_num
18. 0018specialize le_not_lt 37
19. 0019specialize le_not_lt 1
20. 0020apply le_not_lt
21. 0021exact htail_le_one
22. 0022exact hone_lt_tail
23. 0023have hsquare : exists bpr_gap_bb8cert_prime_five_hundred_twenty_one_square. bpr_gap_bb8cert_prime_five_hundred_twenty_one_square + S (2 * (11 * 22) + 37) = S 22 * S 22
24. 0024exists 7
25. 0025have hvalue : 2 * (11 * 22) + 37 = 23 * 22 + 15
26. 0026symm
27. 0027have hcoeff : 23 = 2 * 11 + 1
28. 0028norm_num
29. 0029rewrite hcoeff
30. 0030trans ((2 * 11) * 22 + 1 * 22) + 15
31. 0031congr
32. 0032apply add_mul
33. 0033refl
34. 0034trans (2 * (11 * 22) + 22) + 15
35. 0035congr
36. 0036congr
37. 0037apply mul_assoc
38. 0038apply one_mul
39. 0039refl
40. 0040trans 2 * (11 * 22) + (22 + 15)
41. 0041apply add_assoc
42. 0042trans 2 * (11 * 22) + 37
43. 0043congr
44. 0044refl
45. 0045norm_num
46. 0046refl
47. 0047rewrite hvalue
48. 0048trans 23 * 22 + 23
49. 0049rewrite <- PA4
50. 0050trans 23 * 22 + (7 + S 15)
51. 0051trans (7 + 23 * 22) + S 15
52. 0052symm
53. 0053apply add_assoc
54. 0054trans (23 * 22 + 7) + S 15
55. 0055congr
56. 0056apply add_comm
57. 0057refl
58. 0058apply add_assoc
59. 0059congr
60. 0060refl
61. 0061norm_num
62. 0062symm
63. 0063apply PA6
64. 0064specialize prime_of_no_small_prime_divisor_below_square 22
65. 0065specialize prime_of_no_small_prime_divisor_below_square (2 * (11 * 22) + 37)
66. 0066apply prime_of_no_small_prime_divisor_below_square
67. 0067exact hn0
68. 0068exact hn1
69. 0069exact hsquare
70. 0070intro p
71. 0071intro hp
72. 0072intro hp_bound
73. 0073intro hdivides
74. 0074have hbound_22 : exists k. k + 22 = 22
75. 0075exists 0
76. 0076norm_num
77. 0077have hp_22 : exists k. k + p = 22
78. 0078specialize le_trans p
79. 0079specialize le_trans 22
80. 0080specialize le_trans 22
81. 0081apply le_trans
82. 0082exact hp_bound
83. 0083exact hbound_22
84. 0084have hcases : p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19)))))))
85. 0085specialize prime_le_twenty_two_cases p
86. 0086apply prime_le_twenty_two_cases
87. 0087exact hp
88. 0088exact hp_22
89. 0089cases hcases
90. 0090rewrite hcases_left at hdivides
91. 0091specialize nonzero_remainder_not_multiple 2
92. 0092specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
93. 0093specialize nonzero_remainder_not_multiple (2 * (11 * 11 + 0) + 18)
94. 0094specialize nonzero_remainder_not_multiple 1
95. 0095apply nonzero_remainder_not_multiple
96. 0096specialize double_scaled_remainder_lift 2
97. 0097specialize double_scaled_remainder_lift 22
98. 0098specialize double_scaled_remainder_lift 11
99. 0099specialize double_scaled_remainder_lift 0
100. 0100specialize double_scaled_remainder_lift 0
101. 0101specialize double_scaled_remainder_lift 0
102. 0102specialize double_scaled_remainder_lift 18
103. 0103specialize double_scaled_remainder_lift 1
104. 0104apply double_scaled_remainder_lift
105. 0105norm_num
106. 0106norm_num
107. 0107norm_num
108. 0108intro hrem_2_zero
109. 0109apply PA1
110. 0110exact hrem_2_zero
111. 0111exists 0
112. 0112norm_num
113. 0113exact hdivides
114. 0114cases hcases_right
115. 0115rewrite hcases_right_left at hdivides
116. 0116specialize nonzero_remainder_not_multiple 3
117. 0117specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
118. 0118specialize nonzero_remainder_not_multiple (2 * (11 * 7 + 3) + 13)
119. 0119specialize nonzero_remainder_not_multiple 2
120. 0120apply nonzero_remainder_not_multiple
121. 0121specialize double_scaled_remainder_lift 3
122. 0122specialize double_scaled_remainder_lift 22
123. 0123specialize double_scaled_remainder_lift 7
124. 0124specialize double_scaled_remainder_lift 1
125. 0125specialize double_scaled_remainder_lift 3
126. 0126specialize double_scaled_remainder_lift 2
127. 0127specialize double_scaled_remainder_lift 13
128. 0128specialize double_scaled_remainder_lift 2
129. 0129apply double_scaled_remainder_lift
130. 0130norm_num
131. 0131norm_num
132. 0132norm_num
133. 0133intro hrem_3_zero
134. 0134apply PA1
135. 0135exact hrem_3_zero
136. 0136exists 0
137. 0137norm_num
138. 0138exact hdivides
139. 0139cases hcases_right_right
140. 0140rewrite hcases_right_right_left at hdivides
141. 0141specialize nonzero_remainder_not_multiple 5
142. 0142specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
143. 0143specialize nonzero_remainder_not_multiple (2 * (11 * 4 + 4) + 8)
144. 0144specialize nonzero_remainder_not_multiple 1
145. 0145apply nonzero_remainder_not_multiple
146. 0146specialize double_scaled_remainder_lift 5
147. 0147specialize double_scaled_remainder_lift 22
148. 0148specialize double_scaled_remainder_lift 4
149. 0149specialize double_scaled_remainder_lift 2
150. 0150specialize double_scaled_remainder_lift 4
151. 0151specialize double_scaled_remainder_lift 2
152. 0152specialize double_scaled_remainder_lift 8
153. 0153specialize double_scaled_remainder_lift 1
154. 0154apply double_scaled_remainder_lift
155. 0155norm_num
156. 0156norm_num
157. 0157norm_num
158. 0158intro hrem_5_zero
159. 0159apply PA1
160. 0160exact hrem_5_zero
161. 0161exists 3
162. 0162norm_num
163. 0163exact hdivides
164. 0164cases hcases_right_right_right
165. 0165rewrite hcases_right_right_right_left at hdivides
166. 0166specialize nonzero_remainder_not_multiple 7
167. 0167specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
168. 0168specialize nonzero_remainder_not_multiple (2 * (11 * 3 + 1) + 6)
169. 0169specialize nonzero_remainder_not_multiple 3
170. 0170apply nonzero_remainder_not_multiple
171. 0171specialize double_scaled_remainder_lift 7
172. 0172specialize double_scaled_remainder_lift 22
173. 0173specialize double_scaled_remainder_lift 3
174. 0174specialize double_scaled_remainder_lift 1
175. 0175specialize double_scaled_remainder_lift 1
176. 0176specialize double_scaled_remainder_lift 4
177. 0177specialize double_scaled_remainder_lift 6
178. 0178specialize double_scaled_remainder_lift 3
179. 0179apply double_scaled_remainder_lift
180. 0180norm_num
181. 0181norm_num
182. 0182norm_num
183. 0183intro hrem_7_zero
184. 0184apply PA1
185. 0185exact hrem_7_zero
186. 0186exists 3
187. 0187norm_num
188. 0188exact hdivides
189. 0189cases hcases_right_right_right_right
190. 0190rewrite hcases_right_right_right_right_left at hdivides
191. 0191specialize nonzero_remainder_not_multiple 11
192. 0192specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
193. 0193specialize nonzero_remainder_not_multiple (2 * (11 * 2 + 0) + 3)
194. 0194specialize nonzero_remainder_not_multiple 4
195. 0195apply nonzero_remainder_not_multiple
196. 0196specialize double_scaled_remainder_lift 11
197. 0197specialize double_scaled_remainder_lift 22
198. 0198specialize double_scaled_remainder_lift 2
199. 0199specialize double_scaled_remainder_lift 0
200. 0200specialize double_scaled_remainder_lift 0
201. 0201specialize double_scaled_remainder_lift 0
202. 0202specialize double_scaled_remainder_lift 3
203. 0203specialize double_scaled_remainder_lift 4
204. 0204apply double_scaled_remainder_lift
205. 0205norm_num
206. 0206norm_num
207. 0207norm_num
208. 0208intro hrem_11_zero
209. 0209apply PA1
210. 0210exact hrem_11_zero
211. 0211exists 6
212. 0212norm_num
213. 0213exact hdivides
214. 0214cases hcases_right_right_right_right_right
215. 0215rewrite hcases_right_right_right_right_right_left at hdivides
216. 0216specialize nonzero_remainder_not_multiple 13
217. 0217specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
218. 0218specialize nonzero_remainder_not_multiple (2 * (11 * 1 + 7) + 4)
219. 0219specialize nonzero_remainder_not_multiple 1
220. 0220apply nonzero_remainder_not_multiple
221. 0221specialize double_scaled_remainder_lift 13
222. 0222specialize double_scaled_remainder_lift 22
223. 0223specialize double_scaled_remainder_lift 1
224. 0224specialize double_scaled_remainder_lift 9
225. 0225specialize double_scaled_remainder_lift 7
226. 0226specialize double_scaled_remainder_lift 8
227. 0227specialize double_scaled_remainder_lift 4
228. 0228specialize double_scaled_remainder_lift 1
229. 0229apply double_scaled_remainder_lift
230. 0230norm_num
231. 0231norm_num
232. 0232norm_num
233. 0233intro hrem_13_zero
234. 0234apply PA1
235. 0235exact hrem_13_zero
236. 0236exists 11
237. 0237norm_num
238. 0238exact hdivides
239. 0239cases hcases_right_right_right_right_right_right
240. 0240rewrite hcases_right_right_right_right_right_right_left at hdivides
241. 0241specialize nonzero_remainder_not_multiple 17
242. 0242specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
243. 0243specialize nonzero_remainder_not_multiple (2 * (11 * 1 + 3) + 2)
244. 0244specialize nonzero_remainder_not_multiple 11
245. 0245apply nonzero_remainder_not_multiple
246. 0246specialize double_scaled_remainder_lift 17
247. 0247specialize double_scaled_remainder_lift 22
248. 0248specialize double_scaled_remainder_lift 1
249. 0249specialize double_scaled_remainder_lift 5
250. 0250specialize double_scaled_remainder_lift 3
251. 0251specialize double_scaled_remainder_lift 4
252. 0252specialize double_scaled_remainder_lift 2
253. 0253specialize double_scaled_remainder_lift 11
254. 0254apply double_scaled_remainder_lift
255. 0255norm_num
256. 0256norm_num
257. 0257norm_num
258. 0258intro hrem_17_zero
259. 0259apply PA1
260. 0260exact hrem_17_zero
261. 0261exists 5
262. 0262norm_num
263. 0263exact hdivides
264. 0264rewrite hcases_right_right_right_right_right_right_right at hdivides
265. 0265specialize nonzero_remainder_not_multiple 19
266. 0266specialize nonzero_remainder_not_multiple (2 * (11 * 22) + 37)
267. 0267specialize nonzero_remainder_not_multiple (2 * (11 * 1 + 1) + 3)
268. 0268specialize nonzero_remainder_not_multiple 8
269. 0269apply nonzero_remainder_not_multiple
270. 0270specialize double_scaled_remainder_lift 19
271. 0271specialize double_scaled_remainder_lift 22
272. 0272specialize double_scaled_remainder_lift 1
273. 0273specialize double_scaled_remainder_lift 3
274. 0274specialize double_scaled_remainder_lift 1
275. 0275specialize double_scaled_remainder_lift 14
276. 0276specialize double_scaled_remainder_lift 3
277. 0277specialize double_scaled_remainder_lift 8
278. 0278apply double_scaled_remainder_lift
279. 0279norm_num
280. 0280norm_num
281. 0281norm_num
282. 0282intro hrem_19_zero
283. 0283apply PA1
284. 0284exact hrem_19_zero
285. 0285exists 10
286. 0286norm_num
287. 0287exact hdivides