BT00YF

division_three_scaled_upper_of_quotient_lt

Alpha body-checked · checked-use disabled

A quotient below p places the dividend strictly below 3*p.

Exact expanded PA statement

forall n q r p. (((n + n) = (3) * (q) + (r) /\ (exists bcf_lt_gap_bdtsuql_division_bound. bcf_lt_gap_bdtsuql_division_bound + S (r) = 3))) -> (exists bcf_lt_gap_bdtsuql_quotient. bcf_lt_gap_bdtsuql_quotient + S (q) = p) -> (exists bcf_lt_gap_bdtsuql_result. bcf_lt_gap_bdtsuql_result + S (n + n) = (p + p) + p)

Structural proof guide

A quotient below p places the dividend strictly below 3*p.

Direct prerequisites: division_block_upper, mul_le_mul_left, lt_of_lt_of_le, mul_succ_left, one_mul. The authored body proceeds by case analysis (1), intermediate claims (6), equality transport (4).

Proof neighborhood

Direct dependencies

BT001R division_block_upper BT001L mul_le_mul_left BT001D lt_of_lt_of_le BT0005 mul_succ_left BT0009 one_mul

Direct dependents

BT00YG central_binom_prime_valuation_zero_above_third_quotient

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro q
  3. 0003intro r
  4. 0004intro p
  5. 0005intro hdivision
  6. 0006intro hquotient
  7. 0007cases hdivision
  8. 0008have hblock : exists bcf_lt_gap_bdtsuql_block. bcf_lt_gap_bdtsuql_block + S (3 * q + r) = 3 * S q
  9. 0009specialize division_block_upper 3
  10. 0010specialize division_block_upper q
  11. 0011specialize division_block_upper r
  12. 0012apply division_block_upper
  13. 0013exact hdivision_right
  14. 0014have hblock_aligned : exists bcf_lt_gap_bdtsuql_block_aligned. bcf_lt_gap_bdtsuql_block_aligned + S (n + n) = 3 * S q
  15. 0015rewrite hdivision_left
  16. 0016exact hblock
  17. 0017have hscaled : exists bcf_le_gap_bdtsuql_scaled. bcf_le_gap_bdtsuql_scaled + (3 * S q) = 3 * p
  18. 0018specialize mul_le_mul_left (S q)
  19. 0019specialize mul_le_mul_left p
  20. 0020specialize mul_le_mul_left 3
  21. 0021apply mul_le_mul_left
  22. 0022exact hquotient
  23. 0023have hraw : exists bcf_lt_gap_bdtsuql_raw_result. bcf_lt_gap_bdtsuql_raw_result + S (n + n) = 3 * p
  24. 0024specialize lt_of_lt_of_le (n + n)
  25. 0025specialize lt_of_lt_of_le (3 * S q)
  26. 0026specialize lt_of_lt_of_le (3 * p)
  27. 0027apply lt_of_lt_of_le
  28. 0028exact hblock_aligned
  29. 0029exact hscaled
  30. 0030have hdouble : 2 * p = p + p
  31. 0031trans 1 * p + p
  32. 0032specialize mul_succ_left 1
  33. 0033specialize mul_succ_left p
  34. 0034exact mul_succ_left
  35. 0035specialize one_mul p
  36. 0036rewrite one_mul
  37. 0037refl
  38. 0038have htriple : 3 * p = (p + p) + p
  39. 0039trans 2 * p + p
  40. 0040specialize mul_succ_left 2
  41. 0041specialize mul_succ_left p
  42. 0042exact mul_succ_left
  43. 0043rewrite hdouble
  44. 0044refl
  45. 0045rewrite htriple at hraw
  46. 0046exact hraw