prime_one_hundred_sixty_three

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 : ~(13 * (12) + 7 = 0)
2. 0002intro hzero
3. 0003have htail_zero : 7 = 0
4. 0004specialize add_eq_zero_right (13 * (12))
5. 0005specialize add_eq_zero_right 7
6. 0006apply add_eq_zero_right
7. 0007exact hzero
8. 0008apply PA1
9. 0009exact htail_zero
10. 0010have hn1 : ~(13 * (12) + 7 = 1)
11. 0011intro hone
12. 0012have htail_le_one : exists k. k + 7 = 1
13. 0013exists 13 * (12)
14. 0014exact hone
15. 0015have hone_lt_tail : exists k. k + S 1 = 7
16. 0016exists 5
17. 0017norm_num
18. 0018specialize le_not_lt 7
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_one_hundred_sixty_three_square. bpr_gap_bb8cert_prime_one_hundred_sixty_three_square + S (13 * (12) + 7) = S 12 * S 12
24. 0024exists 5
25. 0025trans 13 * 12 + 13
26. 0026rewrite <- PA4
27. 0027trans 13 * 12 + (5 + S 7)
28. 0028trans (5 + 13 * 12) + S 7
29. 0029symm
30. 0030apply add_assoc
31. 0031trans (13 * 12 + 5) + S 7
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 12
42. 0042specialize prime_of_no_small_prime_divisor_below_square (13 * 12 + 7)
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 + 12 = 22
52. 0052exists 10
53. 0053norm_num
54. 0054have hp_22 : exists k. k + p = 22
55. 0055specialize le_trans p
56. 0056specialize le_trans 12
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 : (13 * 12 + 7) = 2 * (13 * 6 + 3) + 1
69. 0069specialize scaled_remainder_lift 2
70. 0070specialize scaled_remainder_lift 12
71. 0071specialize scaled_remainder_lift 6
72. 0072specialize scaled_remainder_lift 0
73. 0073specialize scaled_remainder_lift 13
74. 0074specialize scaled_remainder_lift 7
75. 0075specialize scaled_remainder_lift 3
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 (13 * 12 + 7)
82. 0082specialize nonzero_remainder_not_multiple (13 * 6 + 3)
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 : (13 * 12 + 7) = 3 * (13 * 4 + 2) + 1
95. 0095specialize scaled_remainder_lift 3
96. 0096specialize scaled_remainder_lift 12
97. 0097specialize scaled_remainder_lift 4
98. 0098specialize scaled_remainder_lift 0
99. 0099specialize scaled_remainder_lift 13
100. 0100specialize scaled_remainder_lift 7
101. 0101specialize scaled_remainder_lift 2
102. 0102specialize scaled_remainder_lift 1
103. 0103apply scaled_remainder_lift
104. 0104norm_num
105. 0105norm_num
106. 0106specialize nonzero_remainder_not_multiple 3
107. 0107specialize nonzero_remainder_not_multiple (13 * 12 + 7)
108. 0108specialize nonzero_remainder_not_multiple (13 * 4 + 2)
109. 0109specialize nonzero_remainder_not_multiple 1
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 1
116. 0116norm_num
117. 0117exact hdivides
118. 0118cases hcases_right_right
119. 0119rewrite hcases_right_right_left at hdivides
120. 0120have hdivision_5 : (13 * 12 + 7) = 5 * (13 * 2 + 6) + 3
121. 0121specialize scaled_remainder_lift 5
122. 0122specialize scaled_remainder_lift 12
123. 0123specialize scaled_remainder_lift 2
124. 0124specialize scaled_remainder_lift 2
125. 0125specialize scaled_remainder_lift 13
126. 0126specialize scaled_remainder_lift 7
127. 0127specialize scaled_remainder_lift 6
128. 0128specialize scaled_remainder_lift 3
129. 0129apply scaled_remainder_lift
130. 0130norm_num
131. 0131norm_num
132. 0132specialize nonzero_remainder_not_multiple 5
133. 0133specialize nonzero_remainder_not_multiple (13 * 12 + 7)
134. 0134specialize nonzero_remainder_not_multiple (13 * 2 + 6)
135. 0135specialize nonzero_remainder_not_multiple 3
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 1
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 : (13 * 12 + 7) = 7 * (13 * 1 + 10) + 2
147. 0147specialize scaled_remainder_lift 7
148. 0148specialize scaled_remainder_lift 12
149. 0149specialize scaled_remainder_lift 1
150. 0150specialize scaled_remainder_lift 5
151. 0151specialize scaled_remainder_lift 13
152. 0152specialize scaled_remainder_lift 7
153. 0153specialize scaled_remainder_lift 10
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 (13 * 12 + 7)
160. 0160specialize nonzero_remainder_not_multiple (13 * 1 + 10)
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 : (13 * 12 + 7) = 11 * (13 * 1 + 1) + 9
173. 0173specialize scaled_remainder_lift 11
174. 0174specialize scaled_remainder_lift 12
175. 0175specialize scaled_remainder_lift 1
176. 0176specialize scaled_remainder_lift 1
177. 0177specialize scaled_remainder_lift 13
178. 0178specialize scaled_remainder_lift 7
179. 0179specialize scaled_remainder_lift 1
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 (13 * 12 + 7)
186. 0186specialize nonzero_remainder_not_multiple (13 * 1 + 1)
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. 0197have htoo_large_13 : exists k. k + S 12 = 13
198. 0198exists 0
199. 0199norm_num
200. 0200specialize lt_not_le 12
201. 0201specialize lt_not_le 13
202. 0202apply lt_not_le
203. 0203exact htoo_large_13
204. 0204rewrite hcases_right_right_right_right_right_left at hp_bound
205. 0205exact hp_bound
206. 0206cases hcases_right_right_right_right_right_right
207. 0207have htoo_large_17 : exists k. k + S 12 = 17
208. 0208exists 4
209. 0209norm_num
210. 0210specialize lt_not_le 12
211. 0211specialize lt_not_le 17
212. 0212apply lt_not_le
213. 0213exact htoo_large_17
214. 0214rewrite hcases_right_right_right_right_right_right_left at hp_bound
215. 0215exact hp_bound
216. 0216have htoo_large_19 : exists k. k + S 12 = 19
217. 0217exists 6
218. 0218norm_num
219. 0219specialize lt_not_le 12
220. 0220specialize lt_not_le 19
221. 0221apply lt_not_le
222. 0222exact htoo_large_19
223. 0223rewrite hcases_right_right_right_right_right_right_right at hp_bound
224. 0224exact hp_bound