BT011J

prime_forty_three

Alpha body-checked · checked-use disabled

A native checked trial-division certificate for 43.

Exact expanded PA statement

(~(43 = 1) /\ forall bpr_left_bb8cert_prime_forty_three bpr_right_bb8cert_prime_forty_three. 43 = bpr_left_bb8cert_prime_forty_three * bpr_right_bb8cert_prime_forty_three -> bpr_left_bb8cert_prime_forty_three = 1 \/ bpr_right_bb8cert_prime_forty_three = 1)

Structural proof guide

A native checked trial-division certificate for 43.

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 (11), equality transport (8), closed numeral normalization (13).

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 : ~(43 = 0)
  2. 0002intro hzero
  3. 0003apply PA1
  4. 0004exact hzero
  5. 0005have hn1 : ~(43 = 1)
  6. 0006intro hone
  7. 0007apply PA1
  8. 0008apply PA2
  9. 0009exact hone
  10. 0010have hsquare : exists bpr_gap_bb8cert_prime_forty_three_square. bpr_gap_bb8cert_prime_forty_three_square + S (43) = S 6 * S 6
  11. 0011exists 5
  12. 0012norm_num
  13. 0013specialize prime_of_no_small_prime_divisor_below_square 6
  14. 0014specialize prime_of_no_small_prime_divisor_below_square (43)
  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 + 6 = 22
  24. 0024exists 16
  25. 0025norm_num
  26. 0026have hp_22 : exists k. k + p = 22
  27. 0027specialize le_trans p
  28. 0028specialize le_trans 6
  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 (43)
  42. 0042specialize nonzero_remainder_not_multiple 21
  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 (43)
  56. 0056specialize nonzero_remainder_not_multiple 14
  57. 0057specialize nonzero_remainder_not_multiple 1
  58. 0058apply nonzero_remainder_not_multiple
  59. 0059norm_num
  60. 0060intro hrem_3_zero
  61. 0061apply PA1
  62. 0062exact hrem_3_zero
  63. 0063exists 1
  64. 0064norm_num
  65. 0065exact hdivides
  66. 0066cases hcases_right_right
  67. 0067rewrite hcases_right_right_left at hdivides
  68. 0068specialize nonzero_remainder_not_multiple 5
  69. 0069specialize nonzero_remainder_not_multiple (43)
  70. 0070specialize nonzero_remainder_not_multiple 8
  71. 0071specialize nonzero_remainder_not_multiple 3
  72. 0072apply nonzero_remainder_not_multiple
  73. 0073norm_num
  74. 0074intro hrem_5_zero
  75. 0075apply PA1
  76. 0076exact hrem_5_zero
  77. 0077exists 1
  78. 0078norm_num
  79. 0079exact hdivides
  80. 0080cases hcases_right_right_right
  81. 0081have htoo_large_7 : exists k. k + S 6 = 7
  82. 0082exists 0
  83. 0083norm_num
  84. 0084specialize lt_not_le 6
  85. 0085specialize lt_not_le 7
  86. 0086apply lt_not_le
  87. 0087exact htoo_large_7
  88. 0088rewrite hcases_right_right_right_left at hp_bound
  89. 0089exact hp_bound
  90. 0090cases hcases_right_right_right_right
  91. 0091have htoo_large_11 : exists k. k + S 6 = 11
  92. 0092exists 4
  93. 0093norm_num
  94. 0094specialize lt_not_le 6
  95. 0095specialize lt_not_le 11
  96. 0096apply lt_not_le
  97. 0097exact htoo_large_11
  98. 0098rewrite hcases_right_right_right_right_left at hp_bound
  99. 0099exact hp_bound
  100. 0100cases hcases_right_right_right_right_right
  101. 0101have htoo_large_13 : exists k. k + S 6 = 13
  102. 0102exists 6
  103. 0103norm_num
  104. 0104specialize lt_not_le 6
  105. 0105specialize lt_not_le 13
  106. 0106apply lt_not_le
  107. 0107exact htoo_large_13
  108. 0108rewrite hcases_right_right_right_right_right_left at hp_bound
  109. 0109exact hp_bound
  110. 0110cases hcases_right_right_right_right_right_right
  111. 0111have htoo_large_17 : exists k. k + S 6 = 17
  112. 0112exists 10
  113. 0113norm_num
  114. 0114specialize lt_not_le 6
  115. 0115specialize lt_not_le 17
  116. 0116apply lt_not_le
  117. 0117exact htoo_large_17
  118. 0118rewrite hcases_right_right_right_right_right_right_left at hp_bound
  119. 0119exact hp_bound
  120. 0120have htoo_large_19 : exists k. k + S 6 = 19
  121. 0121exists 12
  122. 0122norm_num
  123. 0123specialize lt_not_le 6
  124. 0124specialize lt_not_le 19
  125. 0125apply lt_not_le
  126. 0126exact htoo_large_19
  127. 0127rewrite hcases_right_right_right_right_right_right_right at hp_bound
  128. 0128exact hp_bound