BT011I

prime_twenty_three

Alpha body-checked · checked-use disabled

A native checked trial-division certificate for 23.

Exact expanded PA statement

(~(23 = 1) /\ forall bpr_left_bb8cert_prime_twenty_three bpr_right_bb8cert_prime_twenty_three. 23 = bpr_left_bb8cert_prime_twenty_three * bpr_right_bb8cert_prime_twenty_three -> bpr_left_bb8cert_prime_twenty_three = 1 \/ bpr_right_bb8cert_prime_twenty_three = 1)

Structural proof guide

A native checked trial-division certificate for 23.

Direct prerequisites: nonzero_remainder_not_multiple, prime_of_no_small_prime_divisor_below_square, le_trans, prime_le_twenty_two_cases, lt_not_le. The authored body proceeds by case analysis (7), intermediate claims (12), equality transport (8), closed numeral normalization (12).

Proof neighborhood

Direct dependencies

BT011B nonzero_remainder_not_multiple BT0119 prime_of_no_small_prime_divisor_below_square BT000F le_trans BT011A prime_le_twenty_two_cases BT001I lt_not_le

Direct dependents

BT0124 bertrand_small_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. 0001have hn0 : ~(23 = 0)
  2. 0002intro hzero
  3. 0003apply PA1
  4. 0004exact hzero
  5. 0005have hn1 : ~(23 = 1)
  6. 0006intro hone
  7. 0007apply PA1
  8. 0008apply PA2
  9. 0009exact hone
  10. 0010have hsquare : exists bpr_gap_bb8cert_prime_twenty_three_square. bpr_gap_bb8cert_prime_twenty_three_square + S (23) = S 4 * S 4
  11. 0011exists 1
  12. 0012norm_num
  13. 0013specialize prime_of_no_small_prime_divisor_below_square 4
  14. 0014specialize prime_of_no_small_prime_divisor_below_square (23)
  15. 0015apply prime_of_no_small_prime_divisor_below_square
  16. 0016exact hn0
  17. 0017exact hn1
  18. 0018exact hsquare
  19. 0019intro p
  20. 0020intro hp
  21. 0021intro hp_bound
  22. 0022intro hdivides
  23. 0023have hbound_22 : exists k. k + 4 = 22
  24. 0024exists 18
  25. 0025norm_num
  26. 0026have hp_22 : exists k. k + p = 22
  27. 0027specialize le_trans p
  28. 0028specialize le_trans 4
  29. 0029specialize le_trans 22
  30. 0030apply le_trans
  31. 0031exact hp_bound
  32. 0032exact hbound_22
  33. 0033have hcases : p = 2 \/ (p = 3 \/ (p = 5 \/ (p = 7 \/ (p = 11 \/ (p = 13 \/ (p = 17 \/ (p = 19)))))))
  34. 0034specialize prime_le_twenty_two_cases p
  35. 0035apply prime_le_twenty_two_cases
  36. 0036exact hp
  37. 0037exact hp_22
  38. 0038cases hcases
  39. 0039rewrite hcases_left at hdivides
  40. 0040specialize nonzero_remainder_not_multiple 2
  41. 0041specialize nonzero_remainder_not_multiple (23)
  42. 0042specialize nonzero_remainder_not_multiple 11
  43. 0043specialize nonzero_remainder_not_multiple 1
  44. 0044apply nonzero_remainder_not_multiple
  45. 0045norm_num
  46. 0046intro hrem_2_zero
  47. 0047apply PA1
  48. 0048exact hrem_2_zero
  49. 0049exists 0
  50. 0050norm_num
  51. 0051exact hdivides
  52. 0052cases hcases_right
  53. 0053rewrite hcases_right_left at hdivides
  54. 0054specialize nonzero_remainder_not_multiple 3
  55. 0055specialize nonzero_remainder_not_multiple (23)
  56. 0056specialize nonzero_remainder_not_multiple 7
  57. 0057specialize nonzero_remainder_not_multiple 2
  58. 0058apply nonzero_remainder_not_multiple
  59. 0059norm_num
  60. 0060intro hrem_3_zero
  61. 0061apply PA1
  62. 0062exact hrem_3_zero
  63. 0063exists 0
  64. 0064norm_num
  65. 0065exact hdivides
  66. 0066cases hcases_right_right
  67. 0067have htoo_large_5 : exists k. k + S 4 = 5
  68. 0068exists 0
  69. 0069norm_num
  70. 0070specialize lt_not_le 4
  71. 0071specialize lt_not_le 5
  72. 0072apply lt_not_le
  73. 0073exact htoo_large_5
  74. 0074rewrite hcases_right_right_left at hp_bound
  75. 0075exact hp_bound
  76. 0076cases hcases_right_right_right
  77. 0077have htoo_large_7 : exists k. k + S 4 = 7
  78. 0078exists 2
  79. 0079norm_num
  80. 0080specialize lt_not_le 4
  81. 0081specialize lt_not_le 7
  82. 0082apply lt_not_le
  83. 0083exact htoo_large_7
  84. 0084rewrite hcases_right_right_right_left at hp_bound
  85. 0085exact hp_bound
  86. 0086cases hcases_right_right_right_right
  87. 0087have htoo_large_11 : exists k. k + S 4 = 11
  88. 0088exists 6
  89. 0089norm_num
  90. 0090specialize lt_not_le 4
  91. 0091specialize lt_not_le 11
  92. 0092apply lt_not_le
  93. 0093exact htoo_large_11
  94. 0094rewrite hcases_right_right_right_right_left at hp_bound
  95. 0095exact hp_bound
  96. 0096cases hcases_right_right_right_right_right
  97. 0097have htoo_large_13 : exists k. k + S 4 = 13
  98. 0098exists 8
  99. 0099norm_num
  100. 0100specialize lt_not_le 4
  101. 0101specialize lt_not_le 13
  102. 0102apply lt_not_le
  103. 0103exact htoo_large_13
  104. 0104rewrite hcases_right_right_right_right_right_left at hp_bound
  105. 0105exact hp_bound
  106. 0106cases hcases_right_right_right_right_right_right
  107. 0107have htoo_large_17 : exists k. k + S 4 = 17
  108. 0108exists 12
  109. 0109norm_num
  110. 0110specialize lt_not_le 4
  111. 0111specialize lt_not_le 17
  112. 0112apply lt_not_le
  113. 0113exact htoo_large_17
  114. 0114rewrite hcases_right_right_right_right_right_right_left at hp_bound
  115. 0115exact hp_bound
  116. 0116have htoo_large_19 : exists k. k + S 4 = 19
  117. 0117exists 14
  118. 0118norm_num
  119. 0119specialize lt_not_le 4
  120. 0120specialize lt_not_le 19
  121. 0121apply lt_not_le
  122. 0122exact htoo_large_19
  123. 0123rewrite hcases_right_right_right_right_right_right_right at hp_bound
  124. 0124exact hp_bound