BT010E

division_quotient_lower_of_scaled_le

Alpha body-checked · checked-use disabled

A scaled lower bound forces the division quotient above its scale index.

Exact expanded PA statement

forall d N q r s. (((N) = (d) * (q) + (r) /\ (exists bcf_lt_gap_b5rbdqlosl_division_bound. bcf_lt_gap_b5rbdqlosl_division_bound + S (r) = d))) -> (exists bcf_le_gap_b5rbdqlosl_scaled. bcf_le_gap_b5rbdqlosl_scaled + (d * s) = N) -> (exists bcf_le_gap_b5rbdqlosl_result. bcf_le_gap_b5rbdqlosl_result + (s) = q)

Structural proof guide

A scaled lower bound forces the division quotient above its scale index.

Direct prerequisites: division_block_upper, le_or_lt, mul_le_mul_left, lt_of_lt_of_le, lt_not_le. The authored body proceeds by case analysis (2), intermediate claims (5), equality transport (1).

Proof neighborhood

Direct dependencies

BT001R division_block_upper BT001G le_or_lt BT001L mul_le_mul_left BT001D lt_of_lt_of_le BT001I lt_not_le

Direct dependents

BT010F floor_sqrt_le_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 d
  2. 0002intro N
  3. 0003intro q
  4. 0004intro r
  5. 0005intro s
  6. 0006intro hdivision
  7. 0007intro hscaled
  8. 0008cases hdivision
  9. 0009have hcases : (exists bcf_le_gap_b5rbdqlosl_result. bcf_le_gap_b5rbdqlosl_result + (s) = q) \/ (exists bcf_lt_gap_b5rbdqlosl_reverse. bcf_lt_gap_b5rbdqlosl_reverse + S (q) = s)
  10. 0010specialize le_or_lt s
  11. 0011specialize le_or_lt q
  12. 0012exact le_or_lt
  13. 0013cases hcases
  14. 0014exact hcases_left
  15. 0015have hupper : exists bcf_lt_gap_b5rbdqlosl_upper. bcf_lt_gap_b5rbdqlosl_upper + S (N) = d * S q
  16. 0016rewrite hdivision_left
  17. 0017specialize division_block_upper d
  18. 0018specialize division_block_upper q
  19. 0019specialize division_block_upper r
  20. 0020apply division_block_upper
  21. 0021exact hdivision_right
  22. 0022have hreverse : exists bcf_le_gap_b5rbdqlosl_reverse_le. bcf_le_gap_b5rbdqlosl_reverse_le + (S q) = s
  23. 0023exact hcases_right
  24. 0024have hproduct : exists bcf_le_gap_b5rbdqlosl_product_le. bcf_le_gap_b5rbdqlosl_product_le + (d * S q) = d * s
  25. 0025specialize mul_le_mul_left (S q)
  26. 0026specialize mul_le_mul_left s
  27. 0027specialize mul_le_mul_left d
  28. 0028apply mul_le_mul_left
  29. 0029exact hreverse
  30. 0030have hstrict : exists bcf_lt_gap_b5rbdqlosl_contradiction. bcf_lt_gap_b5rbdqlosl_contradiction + S (N) = d * s
  31. 0031specialize lt_of_lt_of_le N
  32. 0032specialize lt_of_lt_of_le (d * S q)
  33. 0033specialize lt_of_lt_of_le (d * s)
  34. 0034apply lt_of_lt_of_le
  35. 0035exact hupper
  36. 0036exact hproduct
  37. 0037exfalso
  38. 0038specialize lt_not_le N
  39. 0039specialize lt_not_le (d * s)
  40. 0040apply lt_not_le
  41. 0041exact hstrict
  42. 0042exact hscaled