BT00TW · Bertrand theorem

factorial_weighted_product_combine

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Weighted factorial products combine by reassociation.

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 u v x y f K r F J. J = r * u -> F = f * v -> u * y = v * x -> f = (K * r) * x -> F = (K * J) * y

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 u v x y f K r F J. J = r * u -> F = f * v -> u * y = v * x -> f = (K * r) * x -> F = (K * J) * y

Proof neighborhood

Direct theorem prerequisites

BT0006 mul_comm BT0008 mul_assoc

Direct theorem dependents

BT00TX choose_factorial_bridge

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

29 script commands · 7 reading checkpoints · 4 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 (2)
mul commmul assoc
01Fix variables and assumptionsL1–10

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

  1. L1
    intro u
  2. L2
    intro v
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro f
  6. L6
    intro K
  7. L7
    intro r
  8. L8
    intro F
  9. L9
    intro J
  10. L10
    intro hJ
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hF
  2. L12
    intro hweighted
  3. L13
    intro hf
03Calculate and transport equalitiesL14–14

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

  1. L14
    rewrite hf at hF
04Establish hassoc_xvL15–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul assoc.

  1. L15
    have hassoc_xv : ((K * r) * x) * v = (K * r) * (x * v)
  2. L16
    apply mul_assoc
  3. L17
    rewrite hassoc_xv at hF
05Establish hcomm_xvL18–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L18
    have hcomm_xv : x * v = v * x
  2. L19
    apply mul_comm
  3. L20
    rewrite hcomm_xv at hF
  4. L21
    rewrite <- hweighted at hF
06Establish hassoc_uyL22–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul assoc.

  1. L22
    have hassoc_uy : ((K * r) * u) * y = (K * r) * (u * y)
  2. L23
    apply mul_assoc
  3. L24
    rewrite <- hassoc_uy at hF
07Establish hassoc_kruL25–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul assoc.

  1. L25
    have hassoc_kru : (K * r) * u = K * (r * u)
  2. L26
    apply mul_assoc
  3. L27
    rewrite hassoc_kru at hF
  4. L28
    rewrite <- hJ at hF
  5. L29
    exact hF

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro u
  2. 0002intro v
  3. 0003intro x
  4. 0004intro y
  5. 0005intro f
  6. 0006intro K
  7. 0007intro r
  8. 0008intro F
  9. 0009intro J
  10. 0010intro hJ
  11. 0011intro hF
  12. 0012intro hweighted
  13. 0013intro hf
  14. 0014rewrite hf at hF
  15. 0015have hassoc_xv : ((K * r) * x) * v = (K * r) * (x * v)
  16. 0016apply mul_assoc
  17. 0017rewrite hassoc_xv at hF
  18. 0018have hcomm_xv : x * v = v * x
  19. 0019apply mul_comm
  20. 0020rewrite hcomm_xv at hF
  21. 0021rewrite <- hweighted at hF
  22. 0022have hassoc_uy : ((K * r) * u) * y = (K * r) * (u * y)
  23. 0023apply mul_assoc
  24. 0024rewrite <- hassoc_uy at hF
  25. 0025have hassoc_kru : (K * r) * u = K * (r * u)
  26. 0026apply mul_assoc
  27. 0027rewrite hassoc_kru at hF
  28. 0028rewrite <- hJ at hF
  29. 0029exact hF