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