BT0121

bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen

Alpha body-checked · checked-use disabled

The compact checked cover from 163 to 317.

Exact expanded PA statement

exists bpr_le_gap_bb8c_one_sixty_three_three_seventeen. bpr_le_gap_bb8c_one_sixty_three_three_seventeen + (18 * 17 + 11) = (13 * 12 + 7 + (13 * 12 + 7))

Structural proof guide

The compact checked cover from 163 to 317.

Direct prerequisites: add_mul, mul_add, add_assoc, add_comm, bertrand_add_swap_nested, bertrand_add_six_permute. The authored body proceeds by intermediate claims (11), equality transport (9), closed numeral normalization (5).

Proof neighborhood

Direct dependencies

BT000B add_mul BT0007 mul_add BT0003 add_assoc BT0002 add_comm BT011O bertrand_add_swap_nested 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 h18 : 18 = 13 + 5
  2. 0002norm_num
  3. 0003have h17 : 17 = 12 + 5
  4. 0004norm_num
  5. 0005have h11 : 11 = 7 + 4
  6. 0006norm_num
  7. 0007have hcarrier : 18 * 17 + 11 = (13 * 12 + 7) + ((13 * 5 + 5 * 12) + (5 * 5 + 4))
  8. 0008rewrite h18
  9. 0009rewrite h17
  10. 0010have houter : (13 + 5) * (12 + 5) = 13 * (12 + 5) + 5 * (12 + 5)
  11. 0011apply add_mul
  12. 0012rewrite houter
  13. 0013have hleft_dist : 13 * (12 + 5) = 13 * 12 + 13 * 5
  14. 0014apply mul_add
  15. 0015rewrite hleft_dist
  16. 0016have hright_dist : 5 * (12 + 5) = 5 * 12 + 5 * 5
  17. 0017apply mul_add
  18. 0018rewrite hright_dist
  19. 0019trans ((13 * 12 + 13 * 5) + (5 * 12 + 5 * 5)) + (7 + 4)
  20. 0020congr
  21. 0021refl
  22. 0022exact h11
  23. 0023apply bertrand_add_six_permute
  24. 0024have hgap : 9 + ((13 * 5 + 5 * 12) + (5 * 5 + 4)) = 13 * 12 + 7
  25. 0025have h13 : 13 = 5 + 8
  26. 0026norm_num
  27. 0027have hAexpand : 13 * 12 + 7 = (5 * 12 + 8 * 12) + 7
  28. 0028trans (5 + 8) * 12 + 7
  29. 0029congr
  30. 0030congr
  31. 0031exact h13
  32. 0032refl
  33. 0033refl
  34. 0034trans (5 * 12 + 8 * 12) + 7
  35. 0035congr
  36. 0036apply add_mul
  37. 0037refl
  38. 0038refl
  39. 0039rewrite hAexpand
  40. 0040trans 9 + (13 * 5 + (5 * 12 + (5 * 5 + 4)))
  41. 0041congr
  42. 0042refl
  43. 0043apply add_assoc
  44. 0044trans 9 + (5 * 12 + (13 * 5 + (5 * 5 + 4)))
  45. 0045congr
  46. 0046refl
  47. 0047apply bertrand_add_swap_nested
  48. 0048trans 5 * 12 + (9 + (13 * 5 + (5 * 5 + 4)))
  49. 0049apply bertrand_add_swap_nested
  50. 0050have htail : 9 + (13 * 5 + (5 * 5 + 4)) = 8 * 12 + 7
  51. 0051norm_num
  52. 0052rewrite htail
  53. 0053symm
  54. 0054apply add_assoc
  55. 0055exists 9
  56. 0056rewrite hcarrier
  57. 0057trans (9 + (13 * 12 + 7)) + ((13 * 5 + 5 * 12) + (5 * 5 + 4))
  58. 0058symm
  59. 0059apply add_assoc
  60. 0060trans ((13 * 12 + 7) + 9) + ((13 * 5 + 5 * 12) + (5 * 5 + 4))
  61. 0061congr
  62. 0062apply add_comm
  63. 0063refl
  64. 0064trans (13 * 12 + 7) + (9 + ((13 * 5 + 5 * 12) + (5 * 5 + 4)))
  65. 0065apply add_assoc
  66. 0066rewrite hgap
  67. 0067refl