BT0037 · Bertrand theorem

common_divisor_divides_balanced_result

Stable checked-use theorem · independently kernel verified

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.

Statement with defined notation

∀ c. ∀ a. ∀ b. ∀ d. ∀ xp. ∀ yp. ∀ xn. ∀ yn. Dvd(c,a) → Dvd(c,b) → a · xp + b · yp = d + (a · xn + b · yn) → Dvd(c,d)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd

3 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-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

Proof neighborhood

Direct theorem prerequisites

BT0008 mul_assoc BT0007 mul_add BT0002 add_comm BT002G factor_difference

Direct theorem dependents

BT0039 gauss_coprime_cancel

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

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.

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