BT0120

bertrand_cover_eighty_three_one_hundred_sixty_three

Alpha body-checked · checked-use disabled

The compact checked cover from 83 to 163.

Exact expanded PA statement

exists bpr_le_gap_bb8c_eighty_three_one_sixty_three. bpr_le_gap_bb8c_eighty_three_one_sixty_three + (13 * 12 + 7) = (9 * 9 + 2 + (9 * 9 + 2))

Structural proof guide

The compact checked cover from 83 to 163.

Direct prerequisites: add_mul, add_assoc, add_comm. The authored body proceeds by intermediate claims (6), equality transport (7), closed numeral normalization (5).

Proof neighborhood

Direct dependencies

BT000B add_mul BT0003 add_assoc BT0002 add_comm

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 h13 : 13 = 9 + 4
  2. 0002norm_num
  3. 0003have h9twelve : 9 * 12 = 9 * 9 + 27
  4. 0004norm_num
  5. 0005have h4twelve : 4 * 12 = 48
  6. 0006norm_num
  7. 0007have hcarrier : 13 * 12 + 7 = (9 * 9 + 2) + (8 * 10)
  8. 0008rewrite h13
  9. 0009specialize add_mul 9
  10. 0010specialize add_mul 4
  11. 0011specialize add_mul 12
  12. 0012rewrite add_mul
  13. 0013rewrite h9twelve
  14. 0014rewrite h4twelve
  15. 0015trans (9 * 9 + (27 + 48)) + 7
  16. 0016congr
  17. 0017apply add_assoc
  18. 0018refl
  19. 0019trans 9 * 9 + ((27 + 48) + 7)
  20. 0020apply add_assoc
  21. 0021have htail : (27 + 48) + 7 = 2 + (8 * 10)
  22. 0022norm_num
  23. 0023rewrite htail
  24. 0024symm
  25. 0025apply add_assoc
  26. 0026exists 3
  27. 0027rewrite hcarrier
  28. 0028trans (3 + (9 * 9 + 2)) + (8 * 10)
  29. 0029symm
  30. 0030apply add_assoc
  31. 0031trans ((9 * 9 + 2) + 3) + (8 * 10)
  32. 0032congr
  33. 0033apply add_comm
  34. 0034refl
  35. 0035trans (9 * 9 + 2) + (3 + (8 * 10))
  36. 0036apply add_assoc
  37. 0037have hgap : 3 + (8 * 10) = 9 * 9 + 2
  38. 0038norm_num
  39. 0039rewrite hgap
  40. 0040refl