BT0033 · Bertrand theorem

balanced_bezout_euclid_step

Stable checked-use theorem · independently kernel verified

Transport balanced natural Bezout coefficients across one Euclidean division step.

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

forall a b q r d xp yp xn yn. a = b * q + r -> b * xp + r * yp = d + (b * xn + r * yn) -> a * yp + b * (xp + q * yn) = d + (a * yn + b * (xn + q * yp))

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

none

0 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall a b q r d xp yp xn yn. a = b * q + r -> b * xp + r * yp = d + (b * xn + r * yn) -> a * yp + b * (xp + q * yn) = d + (a * yn + b * (xn + q * yp))

Proof neighborhood

Direct theorem prerequisites

BT0003 add_assoc BT0002 add_comm BT0007 mul_add BT0008 mul_assoc BT000B add_mul BT0032 add_permute_outer

Direct theorem dependents

BT0034 gcd_balanced_bezout_exists_up_to

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

67 script commands · 26 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 (6)
add assocadd commmul addmul assocadd muladd permute outer
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro hbez
03Calculate and transport equalitiesL12–14

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

  1. L12
    rewrite hab
  2. L13
    trans ((b * q) * yp + r * yp) + b * (xp + q * yn)
  3. L14
    congr
04Use earlier factsL15–15

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

  1. L15
    apply add_mul
05Calculate and transport equalitiesL16–19

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

  1. L16
    refl
  2. L17
    trans ((b * q) * yp + r * yp) + (b * xp + b * (q * yn))
  3. L18
    congr
  4. L19
    refl
06Use earlier factsL20–20

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

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

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

  1. L21
    trans ((b * q) * yp + r * yp) + (b * xp + (b * q) * yn)
  2. L22
    congr
  3. L23
    refl
  4. L24
    congr
  5. L25
    refl
  6. L26
    symm
08Use earlier factsL27–27

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

  1. L27
    apply mul_assoc
09Calculate and transport equalitiesL28–28

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

  1. L28
    trans (b * xp + r * yp) + ((b * q) * yp + (b * q) * yn)
10Use earlier factsL29–29

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

  1. L29
    apply add_permute_outer
11Calculate and transport equalitiesL30–32

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

  1. L30
    trans (b * xp + r * yp) + ((b * q) * yn + (b * q) * yp)
  2. L31
    congr
  3. L32
    refl
12Use earlier factsL33–33

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

  1. L33
    apply add_comm
13Calculate and transport equalitiesL34–35

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

  1. L34
    trans (d + (b * xn + r * yn)) + ((b * q) * yn + (b * q) * yp)
  2. L35
    congr
14Use earlier factsL36–36

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

  1. L36
    exact hbez
15Calculate and transport equalitiesL37–38

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

  1. L37
    refl
  2. L38
    trans d + ((b * xn + r * yn) + ((b * q) * yn + (b * q) * yp))
16Use earlier factsL39–39

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

  1. L39
    apply add_assoc
17Calculate and transport equalitiesL40–42

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

  1. L40
    trans d + (((b * q) * yn + r * yn) + (b * xn + (b * q) * yp))
  2. L41
    congr
  3. L42
    refl
18Use earlier factsL43–43

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

  1. L43
    apply add_permute_outer
19Calculate and transport equalitiesL44–48

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

  1. L44
    trans d + ((b * q + r) * yn + (b * xn + (b * q) * yp))
  2. L45
    congr
  3. L46
    refl
  4. L47
    congr
  5. L48
    symm
20Use earlier factsL49–49

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

  1. L49
    apply add_mul
21Calculate and transport equalitiesL50–57

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

  1. L50
    refl
  2. L51
    trans d + ((b * q + r) * yn + (b * xn + b * (q * yp)))
  3. L52
    congr
  4. L53
    refl
  5. L54
    congr
  6. L55
    refl
  7. L56
    congr
  8. L57
    refl
22Use earlier factsL58–58

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

  1. L58
    apply mul_assoc
23Calculate and transport equalitiesL59–63

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

  1. L59
    congr
  2. L60
    refl
  3. L61
    congr
  4. L62
    congr
  5. L63
    symm
24Use earlier factsL64–64

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

  1. L64
    exact hab
25Calculate and transport equalitiesL65–66

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

  1. L65
    refl
  2. L66
    symm
26Use earlier factsL67–67

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

  1. L67
    apply mul_add

Library-wide reading audit

Original defined command ledger · 67 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro d
  6. 0006intro xp
  7. 0007intro yp
  8. 0008intro xn
  9. 0009intro yn
  10. 0010intro hab
  11. 0011intro hbez
  12. 0012rewrite hab
  13. 0013trans ((b * q) * yp + r * yp) + b * (xp + q * yn)
  14. 0014congr
  15. 0015apply add_mul
  16. 0016refl
  17. 0017trans ((b * q) * yp + r * yp) + (b * xp + b * (q * yn))
  18. 0018congr
  19. 0019refl
  20. 0020apply mul_add
  21. 0021trans ((b * q) * yp + r * yp) + (b * xp + (b * q) * yn)
  22. 0022congr
  23. 0023refl
  24. 0024congr
  25. 0025refl
  26. 0026symm
  27. 0027apply mul_assoc
  28. 0028trans (b * xp + r * yp) + ((b * q) * yp + (b * q) * yn)
  29. 0029apply add_permute_outer
  30. 0030trans (b * xp + r * yp) + ((b * q) * yn + (b * q) * yp)
  31. 0031congr
  32. 0032refl
  33. 0033apply add_comm
  34. 0034trans (d + (b * xn + r * yn)) + ((b * q) * yn + (b * q) * yp)
  35. 0035congr
  36. 0036exact hbez
  37. 0037refl
  38. 0038trans d + ((b * xn + r * yn) + ((b * q) * yn + (b * q) * yp))
  39. 0039apply add_assoc
  40. 0040trans d + (((b * q) * yn + r * yn) + (b * xn + (b * q) * yp))
  41. 0041congr
  42. 0042refl
  43. 0043apply add_permute_outer
  44. 0044trans d + ((b * q + r) * yn + (b * xn + (b * q) * yp))
  45. 0045congr
  46. 0046refl
  47. 0047congr
  48. 0048symm
  49. 0049apply add_mul
  50. 0050refl
  51. 0051trans d + ((b * q + r) * yn + (b * xn + b * (q * yp)))
  52. 0052congr
  53. 0053refl
  54. 0054congr
  55. 0055refl
  56. 0056congr
  57. 0057refl
  58. 0058apply mul_assoc
  59. 0059congr
  60. 0060refl
  61. 0061congr
  62. 0062congr
  63. 0063symm
  64. 0064exact hab
  65. 0065refl
  66. 0066symm
  67. 0067apply mul_add