BT0122

bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one

Alpha body-checked · checked-use disabled

The compact checked cover from 317 to 521.

Exact expanded PA statement

exists bpr_le_gap_bb8c_three_seventeen_five_twenty_one. bpr_le_gap_bb8c_three_seventeen_five_twenty_one + (2 * (11 * 22) + 37) = (18 * 17 + 11 + (18 * 17 + 11))

Structural proof guide

The compact checked cover from 317 to 521.

Direct prerequisites: add_mul, mul_add, mul_assoc, mul_comm, add_assoc, add_comm, one_mul, bertrand_add_six_permute. The authored body proceeds by intermediate claims (17), equality transport (11), closed numeral normalization (8).

Proof neighborhood

Direct dependencies

BT000B add_mul BT0007 mul_add BT0008 mul_assoc BT0006 mul_comm BT0003 add_assoc BT0002 add_comm BT0009 one_mul BT011P bertrand_add_six_permute

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 h22 : 22 = 17 + 5
  2. 0002norm_num
  3. 0003have htwoeleven : 2 * 11 = 22
  4. 0004norm_num
  5. 0005have hsquare : 22 * 22 = (17 + 5) * (17 + 5)
  6. 0006congr
  7. 0007exact h22
  8. 0008exact h22
  9. 0009have hproduct : (17 + 5) * (17 + 5) = (17 * 17 + 17 * 5) + (17 * 5 + 5 * 5)
  10. 0010trans 17 * (17 + 5) + 5 * (17 + 5)
  11. 0011apply add_mul
  12. 0012trans (17 * 17 + 17 * 5) + (5 * 17 + 5 * 5)
  13. 0013congr
  14. 0014apply mul_add
  15. 0015apply mul_add
  16. 0016trans (17 * 17 + 17 * 5) + (17 * 5 + 5 * 5)
  17. 0017congr
  18. 0018refl
  19. 0019congr
  20. 0020apply mul_comm
  21. 0021refl
  22. 0022refl
  23. 0023have hBnorm : 2 * (11 * 22) + 37 = 17 * 17 + (17 * 5 + (17 * 5 + 2 * 31))
  24. 0024trans (2 * 11) * 22 + 37
  25. 0025congr
  26. 0026symm
  27. 0027apply mul_assoc
  28. 0028refl
  29. 0029rewrite htwoeleven
  30. 0030rewrite hsquare
  31. 0031rewrite hproduct
  32. 0032trans (17 * 17 + 17 * 5) + ((17 * 5 + 5 * 5) + 37)
  33. 0033apply add_assoc
  34. 0034trans 17 * 17 + (17 * 5 + ((17 * 5 + 5 * 5) + 37))
  35. 0035apply add_assoc
  36. 0036trans 17 * 17 + (17 * 5 + (17 * 5 + (5 * 5 + 37)))
  37. 0037congr
  38. 0038refl
  39. 0039congr
  40. 0040refl
  41. 0041apply add_assoc
  42. 0042have htail_b : 5 * 5 + 37 = 2 * 31
  43. 0043norm_num
  44. 0044rewrite htail_b
  45. 0045refl
  46. 0046have h18 : 18 = 17 + 1
  47. 0047norm_num
  48. 0048have hAexpand : 18 * 17 + 11 = (17 * 17 + 17) + 11
  49. 0049trans (17 + 1) * 17 + 11
  50. 0050congr
  51. 0051congr
  52. 0052exact h18
  53. 0053refl
  54. 0054refl
  55. 0055trans (17 * 17 + 1 * 17) + 11
  56. 0056congr
  57. 0057apply add_mul
  58. 0058refl
  59. 0059have hone : 1 * 17 = 17
  60. 0060apply one_mul
  61. 0061rewrite hone
  62. 0062refl
  63. 0063have h12 : 12 = 5 + 7
  64. 0064norm_num
  65. 0065have h7 : 7 = 5 + 2
  66. 0066norm_num
  67. 0067have hRexpand : 17 * 12 = 17 * 5 + (17 * 5 + 17 * 2)
  68. 0068trans 17 * (5 + 7)
  69. 0069congr
  70. 0070refl
  71. 0071exact h12
  72. 0072trans 17 * 5 + 17 * 7
  73. 0073apply mul_add
  74. 0074trans 17 * 5 + 17 * (5 + 2)
  75. 0075congr
  76. 0076refl
  77. 0077congr
  78. 0078refl
  79. 0079exact h7
  80. 0080trans 17 * 5 + (17 * 5 + 17 * 2)
  81. 0081congr
  82. 0082refl
  83. 0083apply mul_add
  84. 0084refl
  85. 0085have hRnorm : (18 * 17 + 11) + (17 * 12) = 17 * 17 + (17 * 5 + (17 * 5 + 2 * 31))
  86. 0086rewrite hRexpand
  87. 0087rewrite hAexpand
  88. 0088trans (((17 * 17 + 17) + 11) + 17 * 5) + (17 * 5 + 17 * 2)
  89. 0089symm
  90. 0090apply add_assoc
  91. 0091trans ((17 * 17 + 17) + (11 + 17 * 5)) + (17 * 5 + 17 * 2)
  92. 0092congr
  93. 0093apply add_assoc
  94. 0094refl
  95. 0095trans (17 * 17 + 17 * 5) + ((17 + 11) + (17 * 5 + 17 * 2))
  96. 0096apply bertrand_add_six_permute
  97. 0097trans 17 * 17 + (17 * 5 + ((17 + 11) + (17 * 5 + 17 * 2)))
  98. 0098apply add_assoc
  99. 0099trans 17 * 17 + (17 * 5 + (17 * 5 + ((17 + 11) + 17 * 2)))
  100. 0100congr
  101. 0101refl
  102. 0102congr
  103. 0103refl
  104. 0104trans ((17 + 11) + 17 * 5) + 17 * 2
  105. 0105symm
  106. 0106apply add_assoc
  107. 0107trans (17 * 5 + (17 + 11)) + 17 * 2
  108. 0108congr
  109. 0109apply add_comm
  110. 0110refl
  111. 0111apply add_assoc
  112. 0112have htail_r : (17 + 11) + 17 * 2 = 2 * 31
  113. 0113norm_num
  114. 0114rewrite htail_r
  115. 0115refl
  116. 0116have hcarrier : 2 * (11 * 22) + 37 = (18 * 17 + 11) + (17 * 12)
  117. 0117trans 17 * 17 + (17 * 5 + (17 * 5 + 2 * 31))
  118. 0118exact hBnorm
  119. 0119symm
  120. 0120exact hRnorm
  121. 0121have hgap : (6 * 17 + 11) + (17 * 12) = 18 * 17 + 11
  122. 0122trans 6 * 17 + (11 + (17 * 12))
  123. 0123apply add_assoc
  124. 0124trans 6 * 17 + ((17 * 12) + 11)
  125. 0125congr
  126. 0126refl
  127. 0127apply add_comm
  128. 0128trans (6 * 17 + (17 * 12)) + 11
  129. 0129symm
  130. 0130apply add_assoc
  131. 0131trans (17 * 6 + (17 * 12)) + 11
  132. 0132congr
  133. 0133congr
  134. 0134apply mul_comm
  135. 0135refl
  136. 0136refl
  137. 0137trans 17 * (6 + 12) + 11
  138. 0138congr
  139. 0139symm
  140. 0140apply mul_add
  141. 0141refl
  142. 0142have hsum : 6 + 12 = 18
  143. 0143norm_num
  144. 0144rewrite hsum
  145. 0145trans 18 * 17 + 11
  146. 0146congr
  147. 0147apply mul_comm
  148. 0148refl
  149. 0149refl
  150. 0150exists 6 * 17 + 11
  151. 0151rewrite hcarrier
  152. 0152trans ((6 * 17 + 11) + (18 * 17 + 11)) + (17 * 12)
  153. 0153symm
  154. 0154apply add_assoc
  155. 0155trans ((18 * 17 + 11) + (6 * 17 + 11)) + (17 * 12)
  156. 0156congr
  157. 0157apply add_comm
  158. 0158refl
  159. 0159trans (18 * 17 + 11) + ((6 * 17 + 11) + (17 * 12))
  160. 0160apply add_assoc
  161. 0161rewrite hgap
  162. 0162refl