BT00R1

ceil_div_six_total

Alpha body-checked · checked-use disabled

Every natural has a constructive ceiling quotient by six.

Exact expanded PA statement

forall x. exists e. (((exists bcs_lower_gap_total_result. bcs_lower_gap_total_result + (x) = 6 * (e)) /\ exists bcs_upper_gap_total_result. bcs_upper_gap_total_result + S (6 * (e)) = (x) + 6))

Structural proof guide

Every natural has a constructive ceiling quotient by six.

Direct prerequisites: division_remainder_exists, succ_ne_zero, zero_or_succ, zero_add, lt_to_le, add_le_add_left, add_comm. The authored body proceeds by case analysis (5), intermediate claims (4), equality transport (7).

Proof neighborhood

Direct dependencies

BT001P division_remainder_exists BT000C succ_ne_zero BT000Q zero_or_succ BT0000 zero_add BT0019 lt_to_le BT0015 add_le_add_left BT0002 add_comm

Direct dependents

BT00X2 bertrand_hj_six_block_iterate_from_total BT00X6 bertrand_main_inequality_factorized_from_total

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro x
  2. 0002have hdiv : exists q r. x = 6 * q + r /\ exists h. h + S r = 6
  3. 0003specialize division_remainder_exists 6
  4. 0004specialize division_remainder_exists x
  5. 0005apply division_remainder_exists
  6. 0006intro h6
  7. 0007specialize succ_ne_zero 5
  8. 0008apply succ_ne_zero
  9. 0009exact h6
  10. 0010cases hdiv
  11. 0011cases hdiv_witness
  12. 0012cases hdiv_witness_witness
  13. 0013specialize zero_or_succ x2
  14. 0014cases zero_or_succ
  15. 0015exists x1
  16. 0016split
  17. 0017exists 0
  18. 0018trans x
  19. 0019apply zero_add
  20. 0020trans 6 * x1 + x2
  21. 0021exact hdiv_witness_witness_left
  22. 0022rewrite zero_or_succ_left
  23. 0023apply PA3
  24. 0024exists 5
  25. 0025rewrite hdiv_witness_witness_left
  26. 0026rewrite zero_or_succ_left
  27. 0027trans S (5 + 6 * x1)
  28. 0028apply PA4
  29. 0029trans S (6 * x1 + 5)
  30. 0030congr
  31. 0031apply add_comm
  32. 0032trans 6 * x1 + 6
  33. 0033symm
  34. 0034apply PA4
  35. 0035congr
  36. 0036symm
  37. 0037apply PA3
  38. 0038refl
  39. 0039cases zero_or_succ_right
  40. 0040exists S x1
  41. 0041split
  42. 0042have hrle : exists k. k + x2 = 6
  43. 0043apply lt_to_le
  44. 0044exact hdiv_witness_witness_right
  45. 0045have hlow : exists k. k + (6 * x1 + x2) = 6 * x1 + 6
  46. 0046apply add_le_add_left
  47. 0047exact hrle
  48. 0048have hsixsucc : 6 * S x1 = 6 * x1 + 6
  49. 0049apply PA6
  50. 0050rewrite hsixsucc
  51. 0051rewrite hdiv_witness_witness_left
  52. 0052exact hlow
  53. 0053exists x3
  54. 0054rewrite hdiv_witness_witness_left
  55. 0055rewrite zero_or_succ_right_witness
  56. 0056simp [add_comm]