BT0056

scaled_bounded_common_multiple

Stable · empty-context checked

A right multiple of a bounded common multiple remains such a common multiple.

Exact expanded PA statement

forall N C B. (forall t. (exists h. S t + S h = S N) -> exists q. C = S t * q) -> forall t. (exists h. S t + S h = S N) -> exists q. C * B = S t * q

Structural proof guide

A right multiple of a bounded common multiple remains such a common multiple.

Direct prerequisites: multiple_mul_right. The authored body proceeds by intermediate claims (1).

Proof neighborhood

Direct dependencies

BT002A multiple_mul_right

Direct dependents

BT005D beta_prefix_extend

Formal native tactic body

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

  1. 0001intro N
  2. 0002intro C
  3. 0003intro B
  4. 0004intro hcm
  5. 0005intro t
  6. 0006intro ht
  7. 0007have htC : exists q. C = S t * q
  8. 0008specialize hcm t
  9. 0009apply hcm
  10. 0010exact ht
  11. 0011specialize multiple_mul_right (S t)
  12. 0012specialize multiple_mul_right C
  13. 0013specialize multiple_mul_right B
  14. 0014apply multiple_mul_right
  15. 0015exact htC