PA000L

scaled_bounded_common_multiple

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites multiple_mul_right as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA000C multiple_mul_right

Proof neighborhood

Direct dependencies

PA000C multiple_mul_right

Direct dependents

PA002X beta_prefix_extend

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