BT0124

bertrand_small_closed_upper

Alpha body-checked · checked-use disabled

Every nonzero input below 16*32 has a closed Bertrand witness.

Exact expanded PA statement

forall n. ~(n = 0) -> (exists bpr_gap_bb8s_cutoff_bound. bpr_gap_bb8s_cutoff_bound + S (n) = 16 * 32) -> (exists p. ((~(p = 1) /\ forall bpr_left_bb8s_result_prime bpr_right_bb8s_result_prime. p = bpr_left_bb8s_result_prime * bpr_right_bb8s_result_prime -> bpr_left_bb8s_result_prime = 1 \/ bpr_right_bb8s_result_prime = 1)) /\ ((exists bpr_gap_bb8s_result_lower. bpr_gap_bb8s_result_lower + S (n) = p) /\ (exists bpr_le_gap_bb8s_result_upper. bpr_le_gap_bb8s_result_upper + (p) = (n + n))))

Structural proof guide

Every nonzero input below 16*32 has a closed Bertrand witness.

Direct prerequisites: nonzero_is_succ, le_or_lt, lt_trans, bertrand_cutoff_lt_final_prime, bertrand_covering_interval, prime_five_hundred_twenty_one, bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one, prime_three_hundred_seventeen, bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen, prime_one_hundred_sixty_three, bertrand_cover_eighty_three_one_hundred_sixty_three, prime_eighty_three, bertrand_cover_forty_three_eighty_three, prime_forty_three, bertrand_cover_twenty_three_forty_three, prime_twenty_three, bertrand_cover_thirteen_twenty_three, prime_thirteen, bertrand_cover_seven_thirteen, prime_seven, bertrand_cover_five_seven, prime_five, bertrand_cover_three_five, prime_three, bertrand_cover_two_three, prime_two, bertrand_cover_one_two. The authored body proceeds by case analysis (11), intermediate claims (23), equality transport (3).

Proof neighborhood

Direct dependencies

BT000R nonzero_is_succ BT001G le_or_lt BT001F lt_trans BT0123 bertrand_cutoff_lt_final_prime BT011Q bertrand_covering_interval BT011N prime_five_hundred_twenty_one BT0122 bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one BT011M prime_three_hundred_seventeen BT0121 bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen BT011L prime_one_hundred_sixty_three BT0120 bertrand_cover_eighty_three_one_hundred_sixty_three BT011K prime_eighty_three BT011Y bertrand_cover_forty_three_eighty_three BT011J prime_forty_three BT011X bertrand_cover_twenty_three_forty_three BT011I prime_twenty_three BT011W bertrand_cover_thirteen_twenty_three BT011H prime_thirteen BT011V bertrand_cover_seven_thirteen BT011G prime_seven BT011U bertrand_cover_five_seven BT011F prime_five BT011T bertrand_cover_three_five BT006N prime_three BT011S bertrand_cover_two_three BT0025 prime_two BT011R bertrand_cover_one_two

Direct dependents

BT0125 bertrand_closed_upper

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro hnonzero
  3. 0003intro hcutoff
  4. 0004have hshape : exists k. n = S k
  5. 0005specialize nonzero_is_succ n
  6. 0006apply nonzero_is_succ
  7. 0007exact hnonzero
  8. 0008cases hshape
  9. 0009have hlower_1 : exists k. k + 1 = n
  10. 0010exists x
  11. 0011rewrite hshape_witness
  12. 0012rewrite PA4
  13. 0013rewrite PA3
  14. 0014refl
  15. 0015have hsplit_1 : (exists k. k + (2) = n) \/ (exists k. k + S n = (2))
  16. 0016specialize le_or_lt (2)
  17. 0017specialize le_or_lt n
  18. 0018exact le_or_lt
  19. 0019cases hsplit_1
  20. 0020have hlower_2 : exists k. k + (2) = n
  21. 0021exact hsplit_1_left
  22. 0022have hsplit_2 : (exists k. k + (3) = n) \/ (exists k. k + S n = (3))
  23. 0023specialize le_or_lt (3)
  24. 0024specialize le_or_lt n
  25. 0025exact le_or_lt
  26. 0026cases hsplit_2
  27. 0027have hlower_3 : exists k. k + (3) = n
  28. 0028exact hsplit_2_left
  29. 0029have hsplit_3 : (exists k. k + (5) = n) \/ (exists k. k + S n = (5))
  30. 0030specialize le_or_lt (5)
  31. 0031specialize le_or_lt n
  32. 0032exact le_or_lt
  33. 0033cases hsplit_3
  34. 0034have hlower_4 : exists k. k + (5) = n
  35. 0035exact hsplit_3_left
  36. 0036have hsplit_4 : (exists k. k + (7) = n) \/ (exists k. k + S n = (7))
  37. 0037specialize le_or_lt (7)
  38. 0038specialize le_or_lt n
  39. 0039exact le_or_lt
  40. 0040cases hsplit_4
  41. 0041have hlower_5 : exists k. k + (7) = n
  42. 0042exact hsplit_4_left
  43. 0043have hsplit_5 : (exists k. k + (13) = n) \/ (exists k. k + S n = (13))
  44. 0044specialize le_or_lt (13)
  45. 0045specialize le_or_lt n
  46. 0046exact le_or_lt
  47. 0047cases hsplit_5
  48. 0048have hlower_6 : exists k. k + (13) = n
  49. 0049exact hsplit_5_left
  50. 0050have hsplit_6 : (exists k. k + (23) = n) \/ (exists k. k + S n = (23))
  51. 0051specialize le_or_lt (23)
  52. 0052specialize le_or_lt n
  53. 0053exact le_or_lt
  54. 0054cases hsplit_6
  55. 0055have hlower_7 : exists k. k + (23) = n
  56. 0056exact hsplit_6_left
  57. 0057have hsplit_7 : (exists k. k + (43) = n) \/ (exists k. k + S n = (43))
  58. 0058specialize le_or_lt (43)
  59. 0059specialize le_or_lt n
  60. 0060exact le_or_lt
  61. 0061cases hsplit_7
  62. 0062have hlower_8 : exists k. k + (43) = n
  63. 0063exact hsplit_7_left
  64. 0064have hsplit_8 : (exists k. k + (9 * 9 + 2) = n) \/ (exists k. k + S n = (9 * 9 + 2))
  65. 0065specialize le_or_lt (9 * 9 + 2)
  66. 0066specialize le_or_lt n
  67. 0067exact le_or_lt
  68. 0068cases hsplit_8
  69. 0069have hlower_9 : exists k. k + (9 * 9 + 2) = n
  70. 0070exact hsplit_8_left
  71. 0071have hsplit_9 : (exists k. k + (13 * 12 + 7) = n) \/ (exists k. k + S n = (13 * 12 + 7))
  72. 0072specialize le_or_lt (13 * 12 + 7)
  73. 0073specialize le_or_lt n
  74. 0074exact le_or_lt
  75. 0075cases hsplit_9
  76. 0076have hlower_10 : exists k. k + (13 * 12 + 7) = n
  77. 0077exact hsplit_9_left
  78. 0078have hsplit_10 : (exists k. k + (18 * 17 + 11) = n) \/ (exists k. k + S n = (18 * 17 + 11))
  79. 0079specialize le_or_lt (18 * 17 + 11)
  80. 0080specialize le_or_lt n
  81. 0081exact le_or_lt
  82. 0082cases hsplit_10
  83. 0083have hlower_11 : exists k. k + (18 * 17 + 11) = n
  84. 0084exact hsplit_10_left
  85. 0085have hfinal_strict : exists k. k + S n = (2 * (11 * 22) + 37)
  86. 0086specialize lt_trans n
  87. 0087specialize lt_trans (16 * 32)
  88. 0088specialize lt_trans (2 * (11 * 22) + 37)
  89. 0089apply lt_trans
  90. 0090exact hcutoff
  91. 0091exact bertrand_cutoff_lt_final_prime
  92. 0092specialize bertrand_covering_interval (18 * 17 + 11)
  93. 0093specialize bertrand_covering_interval (2 * (11 * 22) + 37)
  94. 0094specialize bertrand_covering_interval n
  95. 0095apply bertrand_covering_interval
  96. 0096exact prime_five_hundred_twenty_one
  97. 0097exact hlower_11
  98. 0098exact hfinal_strict
  99. 0099exact bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one
  100. 0100specialize bertrand_covering_interval (13 * 12 + 7)
  101. 0101specialize bertrand_covering_interval (18 * 17 + 11)
  102. 0102specialize bertrand_covering_interval n
  103. 0103apply bertrand_covering_interval
  104. 0104exact prime_three_hundred_seventeen
  105. 0105exact hlower_10
  106. 0106exact hsplit_10_right
  107. 0107exact bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen
  108. 0108specialize bertrand_covering_interval (9 * 9 + 2)
  109. 0109specialize bertrand_covering_interval (13 * 12 + 7)
  110. 0110specialize bertrand_covering_interval n
  111. 0111apply bertrand_covering_interval
  112. 0112exact prime_one_hundred_sixty_three
  113. 0113exact hlower_9
  114. 0114exact hsplit_9_right
  115. 0115exact bertrand_cover_eighty_three_one_hundred_sixty_three
  116. 0116specialize bertrand_covering_interval (43)
  117. 0117specialize bertrand_covering_interval (9 * 9 + 2)
  118. 0118specialize bertrand_covering_interval n
  119. 0119apply bertrand_covering_interval
  120. 0120exact prime_eighty_three
  121. 0121exact hlower_8
  122. 0122exact hsplit_8_right
  123. 0123exact bertrand_cover_forty_three_eighty_three
  124. 0124specialize bertrand_covering_interval (23)
  125. 0125specialize bertrand_covering_interval (43)
  126. 0126specialize bertrand_covering_interval n
  127. 0127apply bertrand_covering_interval
  128. 0128exact prime_forty_three
  129. 0129exact hlower_7
  130. 0130exact hsplit_7_right
  131. 0131exact bertrand_cover_twenty_three_forty_three
  132. 0132specialize bertrand_covering_interval (13)
  133. 0133specialize bertrand_covering_interval (23)
  134. 0134specialize bertrand_covering_interval n
  135. 0135apply bertrand_covering_interval
  136. 0136exact prime_twenty_three
  137. 0137exact hlower_6
  138. 0138exact hsplit_6_right
  139. 0139exact bertrand_cover_thirteen_twenty_three
  140. 0140specialize bertrand_covering_interval (7)
  141. 0141specialize bertrand_covering_interval (13)
  142. 0142specialize bertrand_covering_interval n
  143. 0143apply bertrand_covering_interval
  144. 0144exact prime_thirteen
  145. 0145exact hlower_5
  146. 0146exact hsplit_5_right
  147. 0147exact bertrand_cover_seven_thirteen
  148. 0148specialize bertrand_covering_interval (5)
  149. 0149specialize bertrand_covering_interval (7)
  150. 0150specialize bertrand_covering_interval n
  151. 0151apply bertrand_covering_interval
  152. 0152exact prime_seven
  153. 0153exact hlower_4
  154. 0154exact hsplit_4_right
  155. 0155exact bertrand_cover_five_seven
  156. 0156specialize bertrand_covering_interval (3)
  157. 0157specialize bertrand_covering_interval (5)
  158. 0158specialize bertrand_covering_interval n
  159. 0159apply bertrand_covering_interval
  160. 0160exact prime_five
  161. 0161exact hlower_3
  162. 0162exact hsplit_3_right
  163. 0163exact bertrand_cover_three_five
  164. 0164specialize bertrand_covering_interval (2)
  165. 0165specialize bertrand_covering_interval (3)
  166. 0166specialize bertrand_covering_interval n
  167. 0167apply bertrand_covering_interval
  168. 0168exact prime_three
  169. 0169exact hlower_2
  170. 0170exact hsplit_2_right
  171. 0171exact bertrand_cover_two_three
  172. 0172specialize bertrand_covering_interval (1)
  173. 0173specialize bertrand_covering_interval (2)
  174. 0174specialize bertrand_covering_interval n
  175. 0175apply bertrand_covering_interval
  176. 0176exact prime_two
  177. 0177exact hlower_1
  178. 0178exact hsplit_1_right
  179. 0179exact bertrand_cover_one_two