BT011A

prime_le_twenty_two_cases

Alpha body-checked · checked-use disabled

The only primes at most twenty-two are the eight displayed values.

Exact expanded PA statement

forall p. ((~(p = 1) /\ forall bpr_left_bb8p22_prime bpr_right_bb8p22_prime. p = bpr_left_bb8p22_prime * bpr_right_bb8p22_prime -> bpr_left_bb8p22_prime = 1 \/ bpr_right_bb8p22_prime = 1)) -> (exists bpr_le_gap_bb8p22_bound. bpr_le_gap_bb8p22_bound + (p) = (22)) -> (p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19))))))))

Structural proof guide

The only primes at most twenty-two are the eight displayed values.

Direct prerequisites: le_eq_or_lt, le_of_succ_le_succ, prime_is_succ_succ, lt_not_le, fixed_nontrivial_factor_not_prime. The authored body proceeds by case analysis (22), intermediate claims (43), equality transport (3), closed numeral normalization (13).

Proof neighborhood

Direct dependencies

BT001C le_eq_or_lt BT0017 le_of_succ_le_succ BT00AW prime_is_succ_succ BT001I lt_not_le BT0116 fixed_nontrivial_factor_not_prime

Direct dependents

BT011F prime_five BT011G prime_seven BT011H prime_thirteen BT011I prime_twenty_three BT011J prime_forty_three BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro hp
  3. 0003intro hbound
  4. 0004have hsplit_22 : p = 22 \/ (exists k. k + S p = 22)
  5. 0005specialize le_eq_or_lt p
  6. 0006specialize le_eq_or_lt 22
  7. 0007apply le_eq_or_lt
  8. 0008exact hbound
  9. 0009cases hsplit_22
  10. 0010exfalso
  11. 0011specialize fixed_nontrivial_factor_not_prime p
  12. 0012specialize fixed_nontrivial_factor_not_prime 2
  13. 0013specialize fixed_nontrivial_factor_not_prime 11
  14. 0014apply fixed_nontrivial_factor_not_prime
  15. 0015trans 22
  16. 0016exact hsplit_22_left
  17. 0017norm_num
  18. 0018intro hleft_one
  19. 0019apply PA1
  20. 0020apply PA2
  21. 0021exact hleft_one
  22. 0022intro hright_one
  23. 0023apply PA1
  24. 0024apply PA2
  25. 0025exact hright_one
  26. 0026exact hp
  27. 0027have hbound_21 : exists k. k + p = 21
  28. 0028apply le_of_succ_le_succ
  29. 0029exact hsplit_22_right
  30. 0030have hsplit_21 : p = 21 \/ (exists k. k + S p = 21)
  31. 0031specialize le_eq_or_lt p
  32. 0032specialize le_eq_or_lt 21
  33. 0033apply le_eq_or_lt
  34. 0034exact hbound_21
  35. 0035cases hsplit_21
  36. 0036exfalso
  37. 0037specialize fixed_nontrivial_factor_not_prime p
  38. 0038specialize fixed_nontrivial_factor_not_prime 3
  39. 0039specialize fixed_nontrivial_factor_not_prime 7
  40. 0040apply fixed_nontrivial_factor_not_prime
  41. 0041trans 21
  42. 0042exact hsplit_21_left
  43. 0043norm_num
  44. 0044intro hleft_one
  45. 0045apply PA1
  46. 0046apply PA2
  47. 0047exact hleft_one
  48. 0048intro hright_one
  49. 0049apply PA1
  50. 0050apply PA2
  51. 0051exact hright_one
  52. 0052exact hp
  53. 0053have hbound_20 : exists k. k + p = 20
  54. 0054apply le_of_succ_le_succ
  55. 0055exact hsplit_21_right
  56. 0056have hsplit_20 : p = 20 \/ (exists k. k + S p = 20)
  57. 0057specialize le_eq_or_lt p
  58. 0058specialize le_eq_or_lt 20
  59. 0059apply le_eq_or_lt
  60. 0060exact hbound_20
  61. 0061cases hsplit_20
  62. 0062exfalso
  63. 0063specialize fixed_nontrivial_factor_not_prime p
  64. 0064specialize fixed_nontrivial_factor_not_prime 4
  65. 0065specialize fixed_nontrivial_factor_not_prime 5
  66. 0066apply fixed_nontrivial_factor_not_prime
  67. 0067trans 20
  68. 0068exact hsplit_20_left
  69. 0069norm_num
  70. 0070intro hleft_one
  71. 0071apply PA1
  72. 0072apply PA2
  73. 0073exact hleft_one
  74. 0074intro hright_one
  75. 0075apply PA1
  76. 0076apply PA2
  77. 0077exact hright_one
  78. 0078exact hp
  79. 0079have hbound_19 : exists k. k + p = 19
  80. 0080apply le_of_succ_le_succ
  81. 0081exact hsplit_20_right
  82. 0082have hsplit_19 : p = 19 \/ (exists k. k + S p = 19)
  83. 0083specialize le_eq_or_lt p
  84. 0084specialize le_eq_or_lt 19
  85. 0085apply le_eq_or_lt
  86. 0086exact hbound_19
  87. 0087cases hsplit_19
  88. 0088right
  89. 0089right
  90. 0090right
  91. 0091right
  92. 0092right
  93. 0093right
  94. 0094right
  95. 0095exact hsplit_19_left
  96. 0096have hbound_18 : exists k. k + p = 18
  97. 0097apply le_of_succ_le_succ
  98. 0098exact hsplit_19_right
  99. 0099have hsplit_18 : p = 18 \/ (exists k. k + S p = 18)
  100. 0100specialize le_eq_or_lt p
  101. 0101specialize le_eq_or_lt 18
  102. 0102apply le_eq_or_lt
  103. 0103exact hbound_18
  104. 0104cases hsplit_18
  105. 0105exfalso
  106. 0106specialize fixed_nontrivial_factor_not_prime p
  107. 0107specialize fixed_nontrivial_factor_not_prime 3
  108. 0108specialize fixed_nontrivial_factor_not_prime 6
  109. 0109apply fixed_nontrivial_factor_not_prime
  110. 0110trans 18
  111. 0111exact hsplit_18_left
  112. 0112norm_num
  113. 0113intro hleft_one
  114. 0114apply PA1
  115. 0115apply PA2
  116. 0116exact hleft_one
  117. 0117intro hright_one
  118. 0118apply PA1
  119. 0119apply PA2
  120. 0120exact hright_one
  121. 0121exact hp
  122. 0122have hbound_17 : exists k. k + p = 17
  123. 0123apply le_of_succ_le_succ
  124. 0124exact hsplit_18_right
  125. 0125have hsplit_17 : p = 17 \/ (exists k. k + S p = 17)
  126. 0126specialize le_eq_or_lt p
  127. 0127specialize le_eq_or_lt 17
  128. 0128apply le_eq_or_lt
  129. 0129exact hbound_17
  130. 0130cases hsplit_17
  131. 0131right
  132. 0132right
  133. 0133right
  134. 0134right
  135. 0135right
  136. 0136right
  137. 0137left
  138. 0138exact hsplit_17_left
  139. 0139have hbound_16 : exists k. k + p = 16
  140. 0140apply le_of_succ_le_succ
  141. 0141exact hsplit_17_right
  142. 0142have hsplit_16 : p = 16 \/ (exists k. k + S p = 16)
  143. 0143specialize le_eq_or_lt p
  144. 0144specialize le_eq_or_lt 16
  145. 0145apply le_eq_or_lt
  146. 0146exact hbound_16
  147. 0147cases hsplit_16
  148. 0148exfalso
  149. 0149specialize fixed_nontrivial_factor_not_prime p
  150. 0150specialize fixed_nontrivial_factor_not_prime 4
  151. 0151specialize fixed_nontrivial_factor_not_prime 4
  152. 0152apply fixed_nontrivial_factor_not_prime
  153. 0153trans 16
  154. 0154exact hsplit_16_left
  155. 0155norm_num
  156. 0156intro hleft_one
  157. 0157apply PA1
  158. 0158apply PA2
  159. 0159exact hleft_one
  160. 0160intro hright_one
  161. 0161apply PA1
  162. 0162apply PA2
  163. 0163exact hright_one
  164. 0164exact hp
  165. 0165have hbound_15 : exists k. k + p = 15
  166. 0166apply le_of_succ_le_succ
  167. 0167exact hsplit_16_right
  168. 0168have hsplit_15 : p = 15 \/ (exists k. k + S p = 15)
  169. 0169specialize le_eq_or_lt p
  170. 0170specialize le_eq_or_lt 15
  171. 0171apply le_eq_or_lt
  172. 0172exact hbound_15
  173. 0173cases hsplit_15
  174. 0174exfalso
  175. 0175specialize fixed_nontrivial_factor_not_prime p
  176. 0176specialize fixed_nontrivial_factor_not_prime 3
  177. 0177specialize fixed_nontrivial_factor_not_prime 5
  178. 0178apply fixed_nontrivial_factor_not_prime
  179. 0179trans 15
  180. 0180exact hsplit_15_left
  181. 0181norm_num
  182. 0182intro hleft_one
  183. 0183apply PA1
  184. 0184apply PA2
  185. 0185exact hleft_one
  186. 0186intro hright_one
  187. 0187apply PA1
  188. 0188apply PA2
  189. 0189exact hright_one
  190. 0190exact hp
  191. 0191have hbound_14 : exists k. k + p = 14
  192. 0192apply le_of_succ_le_succ
  193. 0193exact hsplit_15_right
  194. 0194have hsplit_14 : p = 14 \/ (exists k. k + S p = 14)
  195. 0195specialize le_eq_or_lt p
  196. 0196specialize le_eq_or_lt 14
  197. 0197apply le_eq_or_lt
  198. 0198exact hbound_14
  199. 0199cases hsplit_14
  200. 0200exfalso
  201. 0201specialize fixed_nontrivial_factor_not_prime p
  202. 0202specialize fixed_nontrivial_factor_not_prime 2
  203. 0203specialize fixed_nontrivial_factor_not_prime 7
  204. 0204apply fixed_nontrivial_factor_not_prime
  205. 0205trans 14
  206. 0206exact hsplit_14_left
  207. 0207norm_num
  208. 0208intro hleft_one
  209. 0209apply PA1
  210. 0210apply PA2
  211. 0211exact hleft_one
  212. 0212intro hright_one
  213. 0213apply PA1
  214. 0214apply PA2
  215. 0215exact hright_one
  216. 0216exact hp
  217. 0217have hbound_13 : exists k. k + p = 13
  218. 0218apply le_of_succ_le_succ
  219. 0219exact hsplit_14_right
  220. 0220have hsplit_13 : p = 13 \/ (exists k. k + S p = 13)
  221. 0221specialize le_eq_or_lt p
  222. 0222specialize le_eq_or_lt 13
  223. 0223apply le_eq_or_lt
  224. 0224exact hbound_13
  225. 0225cases hsplit_13
  226. 0226right
  227. 0227right
  228. 0228right
  229. 0229right
  230. 0230right
  231. 0231left
  232. 0232exact hsplit_13_left
  233. 0233have hbound_12 : exists k. k + p = 12
  234. 0234apply le_of_succ_le_succ
  235. 0235exact hsplit_13_right
  236. 0236have hsplit_12 : p = 12 \/ (exists k. k + S p = 12)
  237. 0237specialize le_eq_or_lt p
  238. 0238specialize le_eq_or_lt 12
  239. 0239apply le_eq_or_lt
  240. 0240exact hbound_12
  241. 0241cases hsplit_12
  242. 0242exfalso
  243. 0243specialize fixed_nontrivial_factor_not_prime p
  244. 0244specialize fixed_nontrivial_factor_not_prime 3
  245. 0245specialize fixed_nontrivial_factor_not_prime 4
  246. 0246apply fixed_nontrivial_factor_not_prime
  247. 0247trans 12
  248. 0248exact hsplit_12_left
  249. 0249norm_num
  250. 0250intro hleft_one
  251. 0251apply PA1
  252. 0252apply PA2
  253. 0253exact hleft_one
  254. 0254intro hright_one
  255. 0255apply PA1
  256. 0256apply PA2
  257. 0257exact hright_one
  258. 0258exact hp
  259. 0259have hbound_11 : exists k. k + p = 11
  260. 0260apply le_of_succ_le_succ
  261. 0261exact hsplit_12_right
  262. 0262have hsplit_11 : p = 11 \/ (exists k. k + S p = 11)
  263. 0263specialize le_eq_or_lt p
  264. 0264specialize le_eq_or_lt 11
  265. 0265apply le_eq_or_lt
  266. 0266exact hbound_11
  267. 0267cases hsplit_11
  268. 0268right
  269. 0269right
  270. 0270right
  271. 0271right
  272. 0272left
  273. 0273exact hsplit_11_left
  274. 0274have hbound_10 : exists k. k + p = 10
  275. 0275apply le_of_succ_le_succ
  276. 0276exact hsplit_11_right
  277. 0277have hsplit_10 : p = 10 \/ (exists k. k + S p = 10)
  278. 0278specialize le_eq_or_lt p
  279. 0279specialize le_eq_or_lt 10
  280. 0280apply le_eq_or_lt
  281. 0281exact hbound_10
  282. 0282cases hsplit_10
  283. 0283exfalso
  284. 0284specialize fixed_nontrivial_factor_not_prime p
  285. 0285specialize fixed_nontrivial_factor_not_prime 2
  286. 0286specialize fixed_nontrivial_factor_not_prime 5
  287. 0287apply fixed_nontrivial_factor_not_prime
  288. 0288trans 10
  289. 0289exact hsplit_10_left
  290. 0290norm_num
  291. 0291intro hleft_one
  292. 0292apply PA1
  293. 0293apply PA2
  294. 0294exact hleft_one
  295. 0295intro hright_one
  296. 0296apply PA1
  297. 0297apply PA2
  298. 0298exact hright_one
  299. 0299exact hp
  300. 0300have hbound_9 : exists k. k + p = 9
  301. 0301apply le_of_succ_le_succ
  302. 0302exact hsplit_10_right
  303. 0303have hsplit_9 : p = 9 \/ (exists k. k + S p = 9)
  304. 0304specialize le_eq_or_lt p
  305. 0305specialize le_eq_or_lt 9
  306. 0306apply le_eq_or_lt
  307. 0307exact hbound_9
  308. 0308cases hsplit_9
  309. 0309exfalso
  310. 0310specialize fixed_nontrivial_factor_not_prime p
  311. 0311specialize fixed_nontrivial_factor_not_prime 3
  312. 0312specialize fixed_nontrivial_factor_not_prime 3
  313. 0313apply fixed_nontrivial_factor_not_prime
  314. 0314trans 9
  315. 0315exact hsplit_9_left
  316. 0316norm_num
  317. 0317intro hleft_one
  318. 0318apply PA1
  319. 0319apply PA2
  320. 0320exact hleft_one
  321. 0321intro hright_one
  322. 0322apply PA1
  323. 0323apply PA2
  324. 0324exact hright_one
  325. 0325exact hp
  326. 0326have hbound_8 : exists k. k + p = 8
  327. 0327apply le_of_succ_le_succ
  328. 0328exact hsplit_9_right
  329. 0329have hsplit_8 : p = 8 \/ (exists k. k + S p = 8)
  330. 0330specialize le_eq_or_lt p
  331. 0331specialize le_eq_or_lt 8
  332. 0332apply le_eq_or_lt
  333. 0333exact hbound_8
  334. 0334cases hsplit_8
  335. 0335exfalso
  336. 0336specialize fixed_nontrivial_factor_not_prime p
  337. 0337specialize fixed_nontrivial_factor_not_prime 2
  338. 0338specialize fixed_nontrivial_factor_not_prime 4
  339. 0339apply fixed_nontrivial_factor_not_prime
  340. 0340trans 8
  341. 0341exact hsplit_8_left
  342. 0342norm_num
  343. 0343intro hleft_one
  344. 0344apply PA1
  345. 0345apply PA2
  346. 0346exact hleft_one
  347. 0347intro hright_one
  348. 0348apply PA1
  349. 0349apply PA2
  350. 0350exact hright_one
  351. 0351exact hp
  352. 0352have hbound_7 : exists k. k + p = 7
  353. 0353apply le_of_succ_le_succ
  354. 0354exact hsplit_8_right
  355. 0355have hsplit_7 : p = 7 \/ (exists k. k + S p = 7)
  356. 0356specialize le_eq_or_lt p
  357. 0357specialize le_eq_or_lt 7
  358. 0358apply le_eq_or_lt
  359. 0359exact hbound_7
  360. 0360cases hsplit_7
  361. 0361right
  362. 0362right
  363. 0363right
  364. 0364left
  365. 0365exact hsplit_7_left
  366. 0366have hbound_6 : exists k. k + p = 6
  367. 0367apply le_of_succ_le_succ
  368. 0368exact hsplit_7_right
  369. 0369have hsplit_6 : p = 6 \/ (exists k. k + S p = 6)
  370. 0370specialize le_eq_or_lt p
  371. 0371specialize le_eq_or_lt 6
  372. 0372apply le_eq_or_lt
  373. 0373exact hbound_6
  374. 0374cases hsplit_6
  375. 0375exfalso
  376. 0376specialize fixed_nontrivial_factor_not_prime p
  377. 0377specialize fixed_nontrivial_factor_not_prime 2
  378. 0378specialize fixed_nontrivial_factor_not_prime 3
  379. 0379apply fixed_nontrivial_factor_not_prime
  380. 0380trans 6
  381. 0381exact hsplit_6_left
  382. 0382norm_num
  383. 0383intro hleft_one
  384. 0384apply PA1
  385. 0385apply PA2
  386. 0386exact hleft_one
  387. 0387intro hright_one
  388. 0388apply PA1
  389. 0389apply PA2
  390. 0390exact hright_one
  391. 0391exact hp
  392. 0392have hbound_5 : exists k. k + p = 5
  393. 0393apply le_of_succ_le_succ
  394. 0394exact hsplit_6_right
  395. 0395have hsplit_5 : p = 5 \/ (exists k. k + S p = 5)
  396. 0396specialize le_eq_or_lt p
  397. 0397specialize le_eq_or_lt 5
  398. 0398apply le_eq_or_lt
  399. 0399exact hbound_5
  400. 0400cases hsplit_5
  401. 0401right
  402. 0402right
  403. 0403left
  404. 0404exact hsplit_5_left
  405. 0405have hbound_4 : exists k. k + p = 4
  406. 0406apply le_of_succ_le_succ
  407. 0407exact hsplit_5_right
  408. 0408have hsplit_4 : p = 4 \/ (exists k. k + S p = 4)
  409. 0409specialize le_eq_or_lt p
  410. 0410specialize le_eq_or_lt 4
  411. 0411apply le_eq_or_lt
  412. 0412exact hbound_4
  413. 0413cases hsplit_4
  414. 0414exfalso
  415. 0415specialize fixed_nontrivial_factor_not_prime p
  416. 0416specialize fixed_nontrivial_factor_not_prime 2
  417. 0417specialize fixed_nontrivial_factor_not_prime 2
  418. 0418apply fixed_nontrivial_factor_not_prime
  419. 0419trans 4
  420. 0420exact hsplit_4_left
  421. 0421norm_num
  422. 0422intro hleft_one
  423. 0423apply PA1
  424. 0424apply PA2
  425. 0425exact hleft_one
  426. 0426intro hright_one
  427. 0427apply PA1
  428. 0428apply PA2
  429. 0429exact hright_one
  430. 0430exact hp
  431. 0431have hbound_3 : exists k. k + p = 3
  432. 0432apply le_of_succ_le_succ
  433. 0433exact hsplit_4_right
  434. 0434have hsplit_3 : p = 3 \/ (exists k. k + S p = 3)
  435. 0435specialize le_eq_or_lt p
  436. 0436specialize le_eq_or_lt 3
  437. 0437apply le_eq_or_lt
  438. 0438exact hbound_3
  439. 0439cases hsplit_3
  440. 0440right
  441. 0441left
  442. 0442exact hsplit_3_left
  443. 0443have hbound_2 : exists k. k + p = 2
  444. 0444apply le_of_succ_le_succ
  445. 0445exact hsplit_3_right
  446. 0446have hsplit_2 : p = 2 \/ (exists k. k + S p = 2)
  447. 0447specialize le_eq_or_lt p
  448. 0448specialize le_eq_or_lt 2
  449. 0449apply le_eq_or_lt
  450. 0450exact hbound_2
  451. 0451cases hsplit_2
  452. 0452left
  453. 0453exact hsplit_2_left
  454. 0454have hshape : exists k. p = S (S k)
  455. 0455specialize prime_is_succ_succ p
  456. 0456apply prime_is_succ_succ
  457. 0457exact hp
  458. 0458cases hshape
  459. 0459have htwo : exists k. k + 2 = p
  460. 0460exists x
  461. 0461trans S (S x)
  462. 0462rewrite PA4
  463. 0463rewrite PA4
  464. 0464rewrite PA3
  465. 0465refl
  466. 0466symm
  467. 0467exact hshape_witness
  468. 0468exfalso
  469. 0469specialize lt_not_le p
  470. 0470specialize lt_not_le 2
  471. 0471apply lt_not_le
  472. 0472exact hsplit_2_right
  473. 0473exact htwo