BT00YB

division_first_two_of_two_three_range

Alpha body-checked · checked-use disabled

The two-thirds range fixes the first quotients at one and two.

Exact expanded PA statement

forall p n. (exists bcf_le_gap_bdftt_lower. bcf_le_gap_bdftt_lower + (p) = n) -> (exists bcf_lt_gap_bdftt_scaled. bcf_lt_gap_bdftt_scaled + S (n + n) = (p + p) + p) -> exists r R. (((n) = (p) * (1) + (r) /\ (exists bcf_lt_gap_bdftt_left_bound. bcf_lt_gap_bdftt_left_bound + S (r) = p))) /\ (((n + n) = (p) * (2) + (R) /\ (exists bcf_lt_gap_bdftt_right_bound. bcf_lt_gap_bdftt_right_bound + S (R) = p)))

Structural proof guide

The two-thirds range fixes the first quotients at one and two.

Direct prerequisites: add_le_add_right, add_le_add_left, le_trans, lt_of_le_of_lt, add_comm, add_lt_cancel_left, division_quotient_one_of_bounds, division_quotient_two_of_bounds. The authored body proceeds by case analysis (2), intermediate claims (10), equality transport (2).

Proof neighborhood

Direct dependencies

BT0014 add_le_add_right BT0015 add_le_add_left BT000F le_trans BT001E lt_of_le_of_lt BT0002 add_comm BT00XC add_lt_cancel_left BT00Y8 division_quotient_one_of_bounds BT00Y9 division_quotient_two_of_bounds

Direct dependents

BT00YE central_binom_prime_valuation_zero_two_thirds_range

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro n
  3. 0003intro hlower
  4. 0004intro hscaled
  5. 0005have hdouble_lower : exists bcf_le_gap_bdftt_double_lower. bcf_le_gap_bdftt_double_lower + (p + p) = n + n
  6. 0006have hdouble_left : exists bcf_le_gap_bdftt_double_left. bcf_le_gap_bdftt_double_left + (p + p) = n + p
  7. 0007specialize add_le_add_right p
  8. 0008specialize add_le_add_right n
  9. 0009specialize add_le_add_right p
  10. 0010apply add_le_add_right
  11. 0011exact hlower
  12. 0012have hshift_lower : exists bcf_le_gap_bdftt_shift_lower. bcf_le_gap_bdftt_shift_lower + (n + p) = n + n
  13. 0013specialize add_le_add_left p
  14. 0014specialize add_le_add_left n
  15. 0015specialize add_le_add_left n
  16. 0016apply add_le_add_left
  17. 0017exact hlower
  18. 0018specialize le_trans (p + p)
  19. 0019specialize le_trans (n + p)
  20. 0020specialize le_trans (n + n)
  21. 0021apply le_trans
  22. 0022exact hdouble_left
  23. 0023exact hshift_lower
  24. 0024have hshift_lower : exists bcf_le_gap_bdftt_shift_lower. bcf_le_gap_bdftt_shift_lower + (n + p) = n + n
  25. 0025specialize add_le_add_left p
  26. 0026specialize add_le_add_left n
  27. 0027specialize add_le_add_left n
  28. 0028apply add_le_add_left
  29. 0029exact hlower
  30. 0030have hshift_strict : exists bcf_lt_gap_bdftt_shift_strict. bcf_lt_gap_bdftt_shift_strict + S (n + p) = (p + p) + p
  31. 0031specialize lt_of_le_of_lt (n + p)
  32. 0032specialize lt_of_le_of_lt (n + n)
  33. 0033specialize lt_of_le_of_lt ((p + p) + p)
  34. 0034apply lt_of_le_of_lt
  35. 0035exact hshift_lower
  36. 0036exact hscaled
  37. 0037have hleft_comm : n + p = p + n
  38. 0038apply add_comm
  39. 0039rewrite hleft_comm at hshift_strict
  40. 0040have hright_comm : (p + p) + p = p + (p + p)
  41. 0041apply add_comm
  42. 0042rewrite hright_comm at hshift_strict
  43. 0043have hfirst_upper : exists bcf_lt_gap_bdftt_upper. bcf_lt_gap_bdftt_upper + S (n) = p + p
  44. 0044specialize add_lt_cancel_left p
  45. 0045specialize add_lt_cancel_left n
  46. 0046specialize add_lt_cancel_left (p + p)
  47. 0047apply add_lt_cancel_left
  48. 0048exact hshift_strict
  49. 0049have hfirst : exists r. ((n) = (p) * (1) + (r) /\ (exists bcf_lt_gap_bdftt_left_bound. bcf_lt_gap_bdftt_left_bound + S (r) = p))
  50. 0050specialize division_quotient_one_of_bounds p
  51. 0051specialize division_quotient_one_of_bounds n
  52. 0052apply division_quotient_one_of_bounds
  53. 0053exact hlower
  54. 0054exact hfirst_upper
  55. 0055have hsecond : exists R. ((n + n) = (p) * (2) + (R) /\ (exists bcf_lt_gap_bdftt_right_bound. bcf_lt_gap_bdftt_right_bound + S (R) = p))
  56. 0056specialize division_quotient_two_of_bounds p
  57. 0057specialize division_quotient_two_of_bounds (n + n)
  58. 0058apply division_quotient_two_of_bounds
  59. 0059exact hdouble_lower
  60. 0060exact hscaled
  61. 0061cases hfirst
  62. 0062cases hsecond
  63. 0063exists x
  64. 0064exists x1
  65. 0065split
  66. 0066exact hfirst_witness
  67. 0067exact hsecond_witness