PA006R

four_mul_eq_double_double

Stable checked-use theorem · independently closed

Multiplication by four is iterated doubling.

Exact expanded PA statement

forall a. 4 * a = 2 * (2 * a)

Structural proof guide

Generated structural guide

Multiplication by four is iterated doubling.

Use the direct prerequisites mul_assoc as previously established PA formulas.

The proof proceeds by closed numeral normalization (1).

Referenced ingredients

PA000B mul_assoc

Proof neighborhood

Direct dependencies

PA000B mul_assoc

Direct dependents

PA00FI odd_half_of_mod4_one_exact PA00FJ odd_half_even_iff_mod4_one PA00FQ odd_half_of_mod4_three_exact PA00FR odd_half_odd_iff_mod4_three

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 a
  2. 0002trans (2 * 2) * a
  3. 0003congr
  4. 0004norm_num
  5. 0005refl
  6. 0006apply mul_assoc