BT002C

multiple_trans

Stable · empty-context checked

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

The multiple relation is transitive.

Direct prerequisites: mul_assoc. The authored body proceeds by case analysis (2), equality transport (2).

Proof neighborhood

Direct dependencies

BT0008 mul_assoc

Direct dependents

BT003K prime_divisor_exists_up_to BT004K beta_moduli_coprime_of_gap_dvd BT004R coprime_mul_left BT00VX central_binom_prime_divisor_le_double BT0118 nonprime_has_small_prime_divisor_below_square

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