PA00DR

odd_half_division_quotient_bounded

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

A division row from the first odd half has quotient at most the second half.

Exact expanded PA statement

forall p q h k i d r. p = 2 * h + 1 -> q = 2 * k + 1 -> (exists edt_lt_gap_odd_half_quotient_index_bound. edt_lt_gap_odd_half_quotient_index_bound + S (i) = h) -> q * S i = p * d + r -> (exists edt_le_gap_odd_half_quotient_bound. edt_le_gap_odd_half_quotient_bound + (d) = k)

Structural proof guide

Generated structural guide

A division row from the first odd half has quotient at most the second half.

Use the direct prerequisites odd_half_cross_product_gap, le_or_lt, mul_le_mul_left, le_add_right, le_trans, lt_not_le as previously established PA formulas.

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

Referenced ingredients

PA00DQ odd_half_cross_product_gap PA003B le_or_lt PA006M mul_le_mul_left PA002S le_add_right PA000R le_trans PA003A lt_not_le

Proof neighborhood

Direct dependencies

PA00DQ odd_half_cross_product_gap PA003B le_or_lt PA006M mul_le_mul_left PA002S le_add_right PA000R le_trans PA003A lt_not_le

Direct dependents

PA00E0 distinct_odd_prime_row_bit_count_equals_division_quotient

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 q
  3. 0003intro h
  4. 0004intro k
  5. 0005intro i
  6. 0006intro d
  7. 0007intro r
  8. 0008intro hp
  9. 0009intro hq
  10. 0010intro hi
  11. 0011intro hdivision
  12. 0012specialize le_or_lt d
  13. 0013specialize le_or_lt k
  14. 0014cases le_or_lt
  15. 0015exact le_or_lt_left
  16. 0016have hreverse : exists edt_lt_gap_odd_half_reverse_quotient. edt_lt_gap_odd_half_reverse_quotient + S (k) = d
  17. 0017exact le_or_lt_right
  18. 0018have hdivisor_le : exists edt_le_gap_odd_half_divisor_product_le. edt_le_gap_odd_half_divisor_product_le + (p * S k) = p * d
  19. 0019specialize mul_le_mul_left (S k)
  20. 0020specialize mul_le_mul_left d
  21. 0021specialize mul_le_mul_left p
  22. 0022apply mul_le_mul_left
  23. 0023exact hreverse
  24. 0024have hdivision_le : exists edt_le_gap_odd_half_division_product_le. edt_le_gap_odd_half_division_product_le + (p * d) = q * S i
  25. 0025rewrite hdivision
  26. 0026specialize le_add_right (p * d)
  27. 0027specialize le_add_right r
  28. 0028exact le_add_right
  29. 0029have hsource_le : exists edt_le_gap_odd_half_source_product_le. edt_le_gap_odd_half_source_product_le + (q * S i) = q * h
  30. 0030specialize mul_le_mul_left (S i)
  31. 0031specialize mul_le_mul_left h
  32. 0032specialize mul_le_mul_left q
  33. 0033apply mul_le_mul_left
  34. 0034exact hi
  35. 0035have hcombined : exists edt_le_gap_odd_half_combined_product_le. edt_le_gap_odd_half_combined_product_le + (p * S k) = q * h
  36. 0036have htrans_all : forall a b c. (exists t. t + a = b) -> (exists t. t + b = c) -> exists t. t + a = c
  37. 0037exact le_trans
  38. 0038specialize le_trans (p * S k)
  39. 0039specialize le_trans (p * d)
  40. 0040specialize le_trans (q * S i)
  41. 0041have hfirst : exists t. t + (p * S k) = q * S i
  42. 0042apply le_trans
  43. 0043exact hdivisor_le
  44. 0044exact hdivision_le
  45. 0045specialize htrans_all (p * S k)
  46. 0046specialize htrans_all (q * S i)
  47. 0047specialize htrans_all (q * h)
  48. 0048apply htrans_all
  49. 0049exact hfirst
  50. 0050exact hsource_le
  51. 0051have hcross : exists edt_lt_gap_odd_half_shaped_cross_gap. edt_lt_gap_odd_half_shaped_cross_gap + S (q * h) = p * S k
  52. 0052rewrite hp
  53. 0053rewrite hq
  54. 0054specialize odd_half_cross_product_gap h
  55. 0055specialize odd_half_cross_product_gap k
  56. 0056exact odd_half_cross_product_gap
  57. 0057exfalso
  58. 0058specialize lt_not_le (q * h)
  59. 0059specialize lt_not_le (p * S k)
  60. 0060apply lt_not_le
  61. 0061exact hcross
  62. 0062exact hcombined