BT00TW

factorial_weighted_product_combine

Alpha body-checked · checked-use disabled

Weighted factorial products combine by reassociation.

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

Structural proof guide

Weighted factorial products combine by reassociation.

Direct prerequisites: mul_comm, mul_assoc. The authored body proceeds by intermediate claims (4), equality transport (7).

Proof neighborhood

Direct dependencies

BT0006 mul_comm BT0008 mul_assoc

Direct dependents

BT00TX choose_factorial_bridge

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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