PA001O

common_divisor_divides_balanced_result

Stable checked-use theorem · independently closed

Every common divisor of two inputs divides the result of a balanced natural combination.

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 a b d xp yp xn yn. (exists u. a = c * u) -> (exists v. b = c * v) -> a * xp + b * yp = d + (a * xn + b * yn) -> exists w. d = c * w

Structural proof guide

Generated structural guide

Every common divisor of two inputs divides the result of a balanced natural combination.

Use the direct prerequisites mul_assoc, mul_add, add_comm, factor_difference as previously established PA formulas.

The proof proceeds by case analysis (2), equality transport (4).

Referenced ingredients

PA000B mul_assoc PA000A mul_add PA000F add_comm PA0013 factor_difference

Proof neighborhood

Direct dependencies

PA000B mul_assoc PA000A mul_add PA000F add_comm PA0013 factor_difference

Direct dependents

PA001P gauss_coprime_cancel

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

48 script commands · 19 reading checkpoints · 0 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 (4)
mul assocmul addadd commfactor difference
01Fix variables and assumptionsL1–10

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

  1. L1
    intro c
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro d
  5. L5
    intro xp
  6. L6
    intro yp
  7. L7
    intro xn
  8. L8
    intro yn
  9. L9
    intro ha
  10. L10
    intro hb
02Fix variables and assumptionsL11–11

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

  1. L11
    intro h
03Separate the logical casesL12–13

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

  1. L12
    cases ha
  2. L13
    cases hb
04Use earlier factsL14–18

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

  1. L14
    specialize factor_difference c
  2. L15
    specialize factor_difference (x * xp + x1 * yp)
  3. L16
    specialize factor_difference (x * xn + x1 * yn)
  4. L17
    specialize factor_difference d
  5. L18
    apply factor_difference
05Calculate and transport equalitiesL19–19

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

  1. L19
    trans c * (x * xp) + c * (x1 * yp)
06Use earlier factsL20–20

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

  1. L20
    apply mul_add
07Calculate and transport equalitiesL21–23

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

  1. L21
    trans (c * x) * xp + (c * x1) * yp
  2. L22
    congr
  3. L23
    symm
08Use earlier factsL24–24

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

  1. L24
    apply mul_assoc
09Calculate and transport equalitiesL25–25

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

  1. L25
    symm
10Use earlier factsL26–26

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

  1. L26
    apply mul_assoc
11Calculate and transport equalitiesL27–31

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

  1. L27
    trans a * xp + b * yp
  2. L28
    rewrite ha_witness
  3. L29
    rewrite hb_witness
  4. L30
    refl
  5. L31
    trans d + (a * xn + b * yn)
12Use earlier factsL32–32

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

  1. L32
    exact h
13Calculate and transport equalitiesL33–33

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

  1. L33
    trans (a * xn + b * yn) + d
14Use earlier factsL34–34

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

  1. L34
    apply add_comm
15Calculate and transport equalitiesL35–41

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

  1. L35
    trans ((c * x) * xn + (c * x1) * yn) + d
  2. L36
    rewrite ha_witness
  3. L37
    rewrite hb_witness
  4. L38
    refl
  5. L39
    trans (c * (x * xn) + c * (x1 * yn)) + d
  6. L40
    congr
  7. L41
    congr
16Use earlier factsL42–43

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

  1. L42
    apply mul_assoc
  2. L43
    apply mul_assoc
17Calculate and transport equalitiesL44–46

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

  1. L44
    refl
  2. L45
    congr
  3. L46
    symm
18Use earlier factsL47–47

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

  1. L47
    apply mul_add
19Calculate and transport equalitiesL48–48

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

  1. L48
    refl

Library-wide reading audit

Original exact command ledger · 48 lines
  1. 0001intro c
  2. 0002intro a
  3. 0003intro b
  4. 0004intro d
  5. 0005intro xp
  6. 0006intro yp
  7. 0007intro xn
  8. 0008intro yn
  9. 0009intro ha
  10. 0010intro hb
  11. 0011intro h
  12. 0012cases ha
  13. 0013cases hb
  14. 0014specialize factor_difference c
  15. 0015specialize factor_difference (x * xp + x1 * yp)
  16. 0016specialize factor_difference (x * xn + x1 * yn)
  17. 0017specialize factor_difference d
  18. 0018apply factor_difference
  19. 0019trans c * (x * xp) + c * (x1 * yp)
  20. 0020apply mul_add
  21. 0021trans (c * x) * xp + (c * x1) * yp
  22. 0022congr
  23. 0023symm
  24. 0024apply mul_assoc
  25. 0025symm
  26. 0026apply mul_assoc
  27. 0027trans a * xp + b * yp
  28. 0028rewrite ha_witness
  29. 0029rewrite hb_witness
  30. 0030refl
  31. 0031trans d + (a * xn + b * yn)
  32. 0032exact h
  33. 0033trans (a * xn + b * yn) + d
  34. 0034apply add_comm
  35. 0035trans ((c * x) * xn + (c * x1) * yn) + d
  36. 0036rewrite ha_witness
  37. 0037rewrite hb_witness
  38. 0038refl
  39. 0039trans (c * (x * xn) + c * (x1 * yn)) + d
  40. 0040congr
  41. 0041congr
  42. 0042apply mul_assoc
  43. 0043apply mul_assoc
  44. 0044refl
  45. 0045congr
  46. 0046symm
  47. 0047apply mul_add
  48. 0048refl