PA006C

mul_double_right

Stable checked-use theorem · independently closed

Doubling commutes through multiplication on the right.

Exact expanded PA statement

forall m b. m * (2 * b) = 2 * (m * b)

Structural proof guide

Generated structural guide

Doubling commutes through multiplication on the right.

Use the direct prerequisites mul_assoc, mul_comm as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA000B mul_assoc PA000H mul_comm

Proof neighborhood

Direct dependencies

PA000B mul_assoc PA000H mul_comm

Direct dependents

PA006D odd_mul_odd PA006E even_mul_right

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro m
  2. 0002intro b
  3. 0003trans (2 * b) * m
  4. 0004apply mul_comm
  5. 0005trans 2 * (b * m)
  6. 0006apply mul_assoc
  7. 0007congr
  8. 0008refl
  9. 0009apply mul_comm