BT00QJ

mul_shuffle_four

Alpha body-checked · checked-use disabled

Four factors may exchange their two middle entries.

Exact expanded PA statement

forall a b c d. (a * b) * (c * d) = (a * c) * (b * d)

Structural proof guide

Four factors may exchange their two middle entries.

Direct prerequisites: mul_assoc, mul_comm. The authored body proceeds by direct introduction and elimination.

Proof neighborhood

Direct dependencies

BT0008 mul_assoc BT0006 mul_comm

Direct dependents

BT00QL power_divides_add_mul BT00QQ power_valuation_mul_successor_not_divides

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005trans a * (b * (c * d))
  6. 0006apply mul_assoc
  7. 0007trans a * ((b * c) * d)
  8. 0008congr
  9. 0009refl
  10. 0010symm
  11. 0011apply mul_assoc
  12. 0012trans a * ((c * b) * d)
  13. 0013congr
  14. 0014refl
  15. 0015congr
  16. 0016apply mul_comm
  17. 0017refl
  18. 0018trans a * (c * (b * d))
  19. 0019congr
  20. 0020refl
  21. 0021apply mul_assoc
  22. 0022symm
  23. 0023apply mul_assoc