PA00DS

nonzero_remainder_division_positive_multiple_threshold

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

67 script commands · 20 reading checkpoints · 8 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (7)
division block upperlt transle or ltmul le mul leftlt not lenonzero is succlt of le of lt
01Fix variables and assumptionsL1–8

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro j
  6. L6
    intro hdivision
  7. L7
    intro hr0
  8. L8
    intro hrp
02Separate the logical casesL9–9

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    split
03Fix variables and assumptionsL10–10

Work with arbitrary variables or the premises of the current implication.

  1. L10
    intro hbelow
04Establish hupperL11–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division block upper.

  1. L11
    have hupper : exists edt_lt_gap_division_threshold_block_upper. edt_lt_gap_division_threshold_block_upper + S (n) = p * S q
  2. L12
    rewrite hdivision
  3. L13
    specialize division_block_upper p
  4. L14
    specialize division_block_upper q
  5. L15
    specialize division_block_upper r
  6. L16
    apply division_block_upper
  7. L17
    exact hrp
05Establish hstrictL18–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt trans.

  1. L18
    have hstrict : exists edt_lt_gap_division_threshold_strict_products. edt_lt_gap_division_threshold_strict_products + S (p * S j) = p * S q
  2. L19
    specialize lt_trans (p * S j)
  3. L20
    specialize lt_trans n
  4. L21
    specialize lt_trans (p * S q)
  5. L22
    apply lt_trans
  6. L23
    exact hbelow
  7. L24
    exact hupper
  8. L25
    specialize le_or_lt (S j)
  9. L26
    specialize le_or_lt q
06Separate the logical casesL27–27

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L27
    cases le_or_lt
07Use earlier factsL28–28

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L28
    exact le_or_lt_left
08Establish hqreverseL29–30

Establish this local claim before using it. It is not an additional assumption.

  1. L29
    have hqreverse : exists edt_lt_gap_division_threshold_quotient_reverse. edt_lt_gap_division_threshold_quotient_reverse + S (q) = S j
  2. L30
    exact le_or_lt_right
09Establish hqleL31–32

Establish this local claim before using it. It is not an additional assumption.

  1. L31
    have hqle : exists edt_le_gap_division_threshold_quotient_reverse_le. edt_le_gap_division_threshold_quotient_reverse_le + (S q) = S j
  2. L32
    exact hqreverse
10Establish hproduct_leL33–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul left.

  1. L33
    have 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
  2. L34
    specialize mul_le_mul_left (S q)
  3. L35
    specialize mul_le_mul_left (S j)
  4. L36
    specialize mul_le_mul_left p
  5. L37
    apply mul_le_mul_left
  6. L38
    exact hqle
11Separate the logical casesL39–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    exfalso
12Use earlier factsL40–44

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L40
    specialize lt_not_le (p * S j)
  2. L41
    specialize lt_not_le (p * S q)
  3. L42
    apply lt_not_le
  4. L43
    exact hstrict
  5. L44
    exact hproduct_le
13Fix variables and assumptionsL45–45

Work with arbitrary variables or the premises of the current implication.

  1. L45
    intro hbounded
14Establish hproduct_leL46–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul left.

  1. L46
    have hproduct_le : exists edt_le_gap_division_threshold_products_forward_le. edt_le_gap_division_threshold_products_forward_le + (p * S j) = p * q
  2. L47
    specialize mul_le_mul_left (S j)
  3. L48
    specialize mul_le_mul_left q
  4. L49
    specialize mul_le_mul_left p
  5. L50
    apply mul_le_mul_left
  6. L51
    exact hbounded
15Establish hr_succL52–55

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply nonzero is succ.

  1. L52
    have hr_succ : exists t. r = S t
  2. L53
    specialize nonzero_is_succ r
  3. L54
    apply nonzero_is_succ
  4. L55
    exact hr0
16Separate the logical casesL56–56

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L56
    cases hr_succ
17Establish hpositiveL57–58

Establish this local claim before using it. It is not an additional assumption.

  1. L57
    have hpositive : exists edt_lt_gap_division_threshold_positive_remainder_gap. edt_lt_gap_division_threshold_positive_remainder_gap + S (p * q) = n
  2. L58
    rewrite hdivision
18Construct an explicit witnessL59–59

Supply the displayed value, then prove that it has the required property.

  1. L59
    exists x
19Calculate and transport equalitiesL60–61

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L60
    rewrite hr_succ_witness
  2. L61
    simp [add_comm]
20Use earlier factsL62–67

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L62
    specialize lt_of_le_of_lt (p * S j)
  2. L63
    specialize lt_of_le_of_lt (p * q)
  3. L64
    specialize lt_of_le_of_lt n
  4. L65
    apply lt_of_le_of_lt
  5. L66
    exact hproduct_le
  6. L67
    exact hpositive

Library-wide reading audit

Original exact command ledger · 67 lines
  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