PA0013 · theorem

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.

Statement with defined notation

∀ c. ∀ u. ∀ v. ∀ r. c · u = c · v + r → Dvd(c,r)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall c u v r. c * u = c * v + r -> exists w. r = c * w

Proof neighborhood

Direct theorem prerequisites

PA0001 zero_add PA0004 add_eq_zero_right PA0012 add_right_cancel PA0009 add_assoc PA000F add_comm

Direct theorem dependents

PA0014 divides_remainder PA001O common_divisor_divides_balanced_result PA00AG prime_bounded_square_one_cases

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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