PA0018

multiple_trans

Stable checked-use theorem · independently closed

The multiple relation is transitive.

Exact expanded PA statement

forall a b n. (exists q. n = a * q) -> (exists r. a = b * r) -> exists s. n = b * s

Structural proof guide

Generated structural guide

The multiple relation is transitive.

Use the direct prerequisites mul_assoc as previously established PA formulas.

The proof proceeds by case analysis (2), equality transport (2).

Referenced ingredients

PA000B mul_assoc

Proof neighborhood

Direct dependencies

PA000B mul_assoc

Direct dependents

PA001Q beta_moduli_coprime_of_gap_dvd PA001T coprime_mul_left

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. 0002intro b
  3. 0003intro n
  4. 0004intro hn
  5. 0005intro hab
  6. 0006cases hn
  7. 0007cases hab
  8. 0008exists x1 * x
  9. 0009rewrite hn_witness
  10. 0010rewrite hab_witness
  11. 0011apply mul_assoc