PA00DS

nonzero_remainder_division_positive_multiple_threshold

Alpha v16 checked-use theorem · independently closed; not Stable

A positive multiple lies below a nonintegral division value exactly through the quotient threshold.

Exact expanded PA statement

forall p n q r j. n = p * q + r -> ~(r = 0) -> (exists edt_lt_gap_division_threshold_remainder_bound. edt_lt_gap_division_threshold_remainder_bound + S (r) = p) -> ((((exists edt_lt_gap_division_threshold_result_below. edt_lt_gap_division_threshold_result_below + S (p * S j) = n) -> (exists edt_le_gap_division_threshold_result_bounded. edt_le_gap_division_threshold_result_bounded + (S j) = q)) /\ ((exists edt_le_gap_division_threshold_result_bounded. edt_le_gap_division_threshold_result_bounded + (S j) = q) -> (exists edt_lt_gap_division_threshold_result_below. edt_lt_gap_division_threshold_result_below + S (p * S j) = n))))

Structural proof guide

Generated structural guide

A positive multiple lies below a nonintegral division value exactly through the quotient threshold.

Use the direct prerequisites division_block_upper, lt_trans, le_or_lt, mul_le_mul_left, lt_not_le, nonzero_is_succ, add_comm, lt_of_le_of_lt as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (8), equality transport (3), certified simplification (1).

Referenced ingredients

PA006N division_block_upper PA006O lt_trans PA003B le_or_lt PA006M mul_le_mul_left PA003A lt_not_le PA001V nonzero_is_succ PA000F add_comm PA0033 lt_of_le_of_lt

Proof neighborhood

Direct dependencies

PA006N division_block_upper PA006O lt_trans PA003B le_or_lt PA006M mul_le_mul_left PA003A lt_not_le PA001V nonzero_is_succ PA000F add_comm PA0033 lt_of_le_of_lt

Direct dependents

PA00DT eisenstein_row_indicator_prefix_to_initial_segment

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro p
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro j
  6. 0006intro hdivision
  7. 0007intro hr0
  8. 0008intro hrp
  9. 0009split
  10. 0010intro hbelow
  11. 0011have hupper : exists edt_lt_gap_division_threshold_block_upper. edt_lt_gap_division_threshold_block_upper + S (n) = p * S q
  12. 0012rewrite hdivision
  13. 0013specialize division_block_upper p
  14. 0014specialize division_block_upper q
  15. 0015specialize division_block_upper r
  16. 0016apply division_block_upper
  17. 0017exact hrp
  18. 0018have hstrict : exists edt_lt_gap_division_threshold_strict_products. edt_lt_gap_division_threshold_strict_products + S (p * S j) = p * S q
  19. 0019specialize lt_trans (p * S j)
  20. 0020specialize lt_trans n
  21. 0021specialize lt_trans (p * S q)
  22. 0022apply lt_trans
  23. 0023exact hbelow
  24. 0024exact hupper
  25. 0025specialize le_or_lt (S j)
  26. 0026specialize le_or_lt q
  27. 0027cases le_or_lt
  28. 0028exact le_or_lt_left
  29. 0029have hqreverse : exists edt_lt_gap_division_threshold_quotient_reverse. edt_lt_gap_division_threshold_quotient_reverse + S (q) = S j
  30. 0030exact le_or_lt_right
  31. 0031have hqle : exists edt_le_gap_division_threshold_quotient_reverse_le. edt_le_gap_division_threshold_quotient_reverse_le + (S q) = S j
  32. 0032exact hqreverse
  33. 0033have hproduct_le : exists edt_le_gap_division_threshold_products_reverse_le. edt_le_gap_division_threshold_products_reverse_le + (p * S q) = p * S j
  34. 0034specialize mul_le_mul_left (S q)
  35. 0035specialize mul_le_mul_left (S j)
  36. 0036specialize mul_le_mul_left p
  37. 0037apply mul_le_mul_left
  38. 0038exact hqle
  39. 0039exfalso
  40. 0040specialize lt_not_le (p * S j)
  41. 0041specialize lt_not_le (p * S q)
  42. 0042apply lt_not_le
  43. 0043exact hstrict
  44. 0044exact hproduct_le
  45. 0045intro hbounded
  46. 0046have hproduct_le : exists edt_le_gap_division_threshold_products_forward_le. edt_le_gap_division_threshold_products_forward_le + (p * S j) = p * q
  47. 0047specialize mul_le_mul_left (S j)
  48. 0048specialize mul_le_mul_left q
  49. 0049specialize mul_le_mul_left p
  50. 0050apply mul_le_mul_left
  51. 0051exact hbounded
  52. 0052have hr_succ : exists t. r = S t
  53. 0053specialize nonzero_is_succ r
  54. 0054apply nonzero_is_succ
  55. 0055exact hr0
  56. 0056cases hr_succ
  57. 0057have hpositive : exists edt_lt_gap_division_threshold_positive_remainder_gap. edt_lt_gap_division_threshold_positive_remainder_gap + S (p * q) = n
  58. 0058rewrite hdivision
  59. 0059exists x
  60. 0060rewrite hr_succ_witness
  61. 0061simp [add_comm]
  62. 0062specialize lt_of_le_of_lt (p * S j)
  63. 0063specialize lt_of_le_of_lt (p * q)
  64. 0064specialize lt_of_le_of_lt n
  65. 0065apply lt_of_le_of_lt
  66. 0066exact hproduct_le
  67. 0067exact hpositive