PA0013

factor_difference

Stable checked-use theorem · independently closed

A common-factor difference is itself a multiple of that factor.

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 c u v r. c * u = c * v + r -> exists w. r = c * w

Structural proof guide

Generated structural guide

A common-factor difference is itself a multiple of that factor.

Use the direct prerequisites zero_add, add_eq_zero_right, add_right_cancel, add_assoc, add_comm as previously established PA formulas.

The proof proceeds by structural induction (2), intermediate claims (2), equality transport (7).

Referenced ingredients

PA0001 zero_add PA0004 add_eq_zero_right PA0012 add_right_cancel PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA0001 zero_add PA0004 add_eq_zero_right PA0012 add_right_cancel PA0009 add_assoc PA000F add_comm

Direct dependents

PA0014 divides_remainder PA001O common_divisor_divides_balanced_result PA00AG prime_bounded_square_one_cases

Formal native tactic body

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

Read the argument

Proof checkpoints

47 script commands · 19 reading checkpoints · 2 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 (5)
zero addadd eq zero rightadd right canceladd assocadd comm
01Fix variables and assumptionsL1–1

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

  1. L1
    intro c
02Induction on uL2–6

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction u
  2. L3
    intro v
  3. L4
    intro r
  4. L5
    intro h
  5. L6
    rewrite PA5 at h
03Establish hrL7–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L7
    have hr : r = 0
  2. L8
    apply add_eq_zero_right
  3. L9
    symm
  4. L10
    exact h
04Construct an explicit witnessL11–11

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

  1. L11
    exists 0
05Calculate and transport equalitiesL12–14

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

  1. L12
    rewrite hr
  2. L13
    rewrite PA5
  3. L14
    refl
06Fix variables and assumptionsL15–15

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

  1. L15
    intro v
07Induction on vL16–18

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L16
    induction v
  2. L17
    intro r
  3. L18
    intro h
08Construct an explicit witnessL19–19

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

  1. L19
    exists S u
09Calculate and transport equalitiesL20–20

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

  1. L20
    rewrite PA5 at h
10Use earlier factsL21–21

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

  1. L21
    specialize zero_add r
11Calculate and transport equalitiesL22–23

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

  1. L22
    rewrite zero_add at h
  2. L23
    symm
12Use earlier factsL24–24

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

  1. L24
    exact h
13Fix variables and assumptionsL25–26

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

  1. L25
    intro r
  2. L26
    intro h
14Establish hredL27–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add right cancel.

  1. L27
    have hred : c * u = c * v + r
  2. L28
    specialize add_right_cancel (c * u)
  3. L29
    specialize add_right_cancel (c * v + r)
  4. L30
    specialize add_right_cancel c
  5. L31
    apply add_right_cancel
  6. L32
    rewrite PA6 at h
  7. L33
    rewrite PA6 at h
  8. L34
    trans (c * v + c) + r
  9. L35
    exact h
  10. L36
    trans c * v + (c + r)
15Use earlier factsL37–37

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

  1. L37
    apply add_assoc
16Calculate and transport equalitiesL38–40

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

  1. L38
    trans c * v + (r + c)
  2. L39
    congr
  3. L40
    refl
17Use earlier factsL41–41

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

  1. L41
    apply add_comm
18Calculate and transport equalitiesL42–42

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

  1. L42
    symm
19Use earlier factsL43–47

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

  1. L43
    apply add_assoc
  2. L44
    specialize IH v
  3. L45
    specialize IH r
  4. L46
    apply IH
  5. L47
    exact hred

Library-wide reading audit

Original exact command ledger · 47 lines
  1. 0001intro c
  2. 0002induction u
  3. 0003intro v
  4. 0004intro r
  5. 0005intro h
  6. 0006rewrite PA5 at h
  7. 0007have hr : r = 0
  8. 0008apply add_eq_zero_right
  9. 0009symm
  10. 0010exact h
  11. 0011exists 0
  12. 0012rewrite hr
  13. 0013rewrite PA5
  14. 0014refl
  15. 0015intro v
  16. 0016induction v
  17. 0017intro r
  18. 0018intro h
  19. 0019exists S u
  20. 0020rewrite PA5 at h
  21. 0021specialize zero_add r
  22. 0022rewrite zero_add at h
  23. 0023symm
  24. 0024exact h
  25. 0025intro r
  26. 0026intro h
  27. 0027have hred : c * u = c * v + r
  28. 0028specialize add_right_cancel (c * u)
  29. 0029specialize add_right_cancel (c * v + r)
  30. 0030specialize add_right_cancel c
  31. 0031apply add_right_cancel
  32. 0032rewrite PA6 at h
  33. 0033rewrite PA6 at h
  34. 0034trans (c * v + c) + r
  35. 0035exact h
  36. 0036trans c * v + (c + r)
  37. 0037apply add_assoc
  38. 0038trans c * v + (r + c)
  39. 0039congr
  40. 0040refl
  41. 0041apply add_comm
  42. 0042symm
  43. 0043apply add_assoc
  44. 0044specialize IH v
  45. 0045specialize IH r
  46. 0046apply IH
  47. 0047exact hred