prime_three_hundred_seventeen

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