BT0036 · Bertrand theorem

balanced_combination_scale_right

Stable checked-use theorem · independently kernel verified

Scale a balanced natural combination on the right.

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 d xp yp xn yn z. a * xp + b * yp = d + (a * xn + b * yn) -> a * (xp * z) + (b * z) * yp = d * z + (a * (xn * z) + (b * z) * yn)

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 d xp yp xn yn z. a * xp + b * yp = d + (a * xn + b * yn) -> a * (xp * z) + (b * z) * yp = d * z + (a * (xn * z) + (b * z) * yn)

Proof neighborhood

Direct theorem prerequisites

BT0008 mul_assoc BT0006 mul_comm BT000B add_mul

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

56 script commands · 25 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 (3)
mul assocmul commadd mul
01Fix variables and assumptionsL1–9

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro d
  4. L4
    intro xp
  5. L5
    intro yp
  6. L6
    intro xn
  7. L7
    intro yn
  8. L8
    intro z
  9. L9
    intro h
02Calculate and transport equalitiesL10–12

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

  1. L10
    trans (a * xp) * z + (b * z) * yp
  2. L11
    congr
  3. L12
    symm
03Use earlier factsL13–13

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

  1. L13
    apply mul_assoc
04Calculate and transport equalitiesL14–18

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

  1. L14
    refl
  2. L15
    trans (a * xp) * z + (b * yp) * z
  3. L16
    congr
  4. L17
    refl
  5. L18
    trans b * (z * yp)
05Use earlier factsL19–19

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

  1. L19
    apply mul_assoc
06Calculate and transport equalitiesL20–22

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

  1. L20
    trans b * (yp * z)
  2. L21
    congr
  3. L22
    refl
07Use earlier factsL23–23

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

  1. L23
    apply mul_comm
08Calculate and transport equalitiesL24–24

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

  1. L24
    symm
09Use earlier factsL25–25

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

  1. L25
    apply mul_assoc
10Calculate and transport equalitiesL26–27

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

  1. L26
    trans (a * xp + b * yp) * z
  2. L27
    symm
11Use earlier factsL28–28

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

  1. L28
    apply add_mul
12Calculate and transport equalitiesL29–30

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

  1. L29
    trans (d + (a * xn + b * yn)) * z
  2. L30
    congr
13Use earlier factsL31–31

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

  1. L31
    exact h
14Calculate and transport equalitiesL32–33

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

  1. L32
    refl
  2. L33
    trans d * z + (a * xn + b * yn) * z
15Use earlier factsL34–34

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

  1. L34
    apply add_mul
16Calculate and transport equalitiesL35–37

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

  1. L35
    trans d * z + ((a * xn) * z + (b * yn) * z)
  2. L36
    congr
  3. L37
    refl
17Use earlier factsL38–38

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

  1. L38
    apply add_mul
18Calculate and transport equalitiesL39–42

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

  1. L39
    trans d * z + (a * (xn * z) + (b * yn) * z)
  2. L40
    congr
  3. L41
    refl
  4. L42
    congr
19Use earlier factsL43–43

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

  1. L43
    apply mul_assoc
20Calculate and transport equalitiesL44–49

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
    refl
  4. L47
    congr
  5. L48
    refl
  6. L49
    trans b * (yn * z)
21Use earlier factsL50–50

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

  1. L50
    apply mul_assoc
22Calculate and transport equalitiesL51–53

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

  1. L51
    trans b * (z * yn)
  2. L52
    congr
  3. L53
    refl
23Use earlier factsL54–54

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

  1. L54
    apply mul_comm
24Calculate and transport equalitiesL55–55

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

  1. L55
    symm
25Use earlier factsL56–56

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

  1. L56
    apply mul_assoc

Library-wide reading audit

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