BT0123

bertrand_cutoff_lt_final_prime

Alpha body-checked · checked-use disabled

The factorized production cutoff lies below the final prime.

Exact expanded PA statement

exists bpr_gap_bb8s_cutoff_final. bpr_gap_bb8s_cutoff_final + S (16 * 32) = 2 * (11 * 22) + 37

Structural proof guide

The factorized production cutoff lies below the final prime.

Direct prerequisites: add_succ_left, mul_add, bertrand_add_swap_nested, mul_comm, add_mul, add_assoc, add_comm, mul_assoc. The authored body proceeds by intermediate claims (12), equality transport (5), closed numeral normalization (6).

Proof neighborhood

Direct dependencies

BT0001 add_succ_left BT0007 mul_add BT011O bertrand_add_swap_nested BT0006 mul_comm BT000B add_mul BT0003 add_assoc BT0002 add_comm BT0008 mul_assoc

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. 0001exists 8
  2. 0002have hsucc : 8 + S (16 * 32) = 9 + (16 * 32)
  3. 0003trans S (8 + (16 * 32))
  4. 0004apply PA4
  5. 0005symm
  6. 0006apply add_succ_left
  7. 0007have h32 : 32 = 22 + 10
  8. 0008norm_num
  9. 0009have hleft : 9 + (16 * 32) = 22 * 16 + (10 * 6 + (9 + 10 * 10))
  10. 0010rewrite h32
  11. 0011trans 9 + (16 * 22 + 16 * 10)
  12. 0012congr
  13. 0013refl
  14. 0014apply mul_add
  15. 0015trans 16 * 22 + (9 + 16 * 10)
  16. 0016apply bertrand_add_swap_nested
  17. 0017trans 22 * 16 + (9 + 16 * 10)
  18. 0018congr
  19. 0019apply mul_comm
  20. 0020refl
  21. 0021have h16 : 16 = 10 + 6
  22. 0022norm_num
  23. 0023have htail16 : 16 * 10 = (10 + 6) * 10
  24. 0024congr
  25. 0025exact h16
  26. 0026refl
  27. 0027rewrite htail16
  28. 0028trans 22 * 16 + (9 + (10 * 10 + 6 * 10))
  29. 0029congr
  30. 0030refl
  31. 0031congr
  32. 0032refl
  33. 0033apply add_mul
  34. 0034trans 22 * 16 + (9 + (10 * 10 + 10 * 6))
  35. 0035congr
  36. 0036refl
  37. 0037congr
  38. 0038refl
  39. 0039congr
  40. 0040refl
  41. 0041apply mul_comm
  42. 0042trans 22 * 16 + ((9 + 10 * 10) + 10 * 6)
  43. 0043congr
  44. 0044refl
  45. 0045symm
  46. 0046apply add_assoc
  47. 0047trans 22 * 16 + (10 * 6 + (9 + 10 * 10))
  48. 0048congr
  49. 0049refl
  50. 0050apply add_comm
  51. 0051refl
  52. 0052have htwoeleven : 2 * 11 = 22
  53. 0053norm_num
  54. 0054have h22sixteen : 22 = 16 + 6
  55. 0055norm_num
  56. 0056have h22twelve : 22 = 10 + 12
  57. 0057norm_num
  58. 0058have hright : (2 * (11 * 22) + 37) = 22 * 16 + (10 * 6 + (12 * 6 + 37))
  59. 0059trans (2 * 11) * 22 + 37
  60. 0060congr
  61. 0061symm
  62. 0062apply mul_assoc
  63. 0063refl
  64. 0064rewrite htwoeleven
  65. 0065trans 22 * (16 + 6) + 37
  66. 0066congr
  67. 0067congr
  68. 0068refl
  69. 0069exact h22sixteen
  70. 0070refl
  71. 0071trans (22 * 16 + 22 * 6) + 37
  72. 0072congr
  73. 0073apply mul_add
  74. 0074refl
  75. 0075trans 22 * 16 + (22 * 6 + 37)
  76. 0076apply add_assoc
  77. 0077have htail22 : 22 * 6 = (10 + 12) * 6
  78. 0078congr
  79. 0079exact h22twelve
  80. 0080refl
  81. 0081rewrite htail22
  82. 0082trans 22 * 16 + ((10 * 6 + 12 * 6) + 37)
  83. 0083congr
  84. 0084refl
  85. 0085congr
  86. 0086apply add_mul
  87. 0087refl
  88. 0088trans 22 * 16 + (10 * 6 + (12 * 6 + 37))
  89. 0089congr
  90. 0090refl
  91. 0091apply add_assoc
  92. 0092refl
  93. 0093have htail : 9 + 10 * 10 = 12 * 6 + 37
  94. 0094norm_num
  95. 0095rewrite htail at hleft
  96. 0096have hcarrier : 9 + (16 * 32) = (2 * (11 * 22) + 37)
  97. 0097trans 22 * 16 + (10 * 6 + (12 * 6 + 37))
  98. 0098exact hleft
  99. 0099symm
  100. 0100exact hright
  101. 0101trans 9 + (16 * 32)
  102. 0102exact hsucc
  103. 0103exact hcarrier