PA000L

scaled_bounded_common_multiple

Stable checked-use theorem · independently closed

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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.

Read the argument

Proof checkpoints

15 script commands · 2 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (1)
multiple mul right
01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro N
  2. L2
    intro C
  3. L3
    intro B
  4. L4
    intro hcm
  5. L5
    intro t
  6. L6
    intro ht
02Establish htCL7–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hcm.

  1. L7
    have htC : exists q. C = S t * q
  2. L8
    specialize hcm t
  3. L9
    apply hcm
  4. L10
    exact ht
  5. L11
    specialize multiple_mul_right (S t)
  6. L12
    specialize multiple_mul_right C
  7. L13
    specialize multiple_mul_right B
  8. L14
    apply multiple_mul_right
  9. L15
    exact htC

Library-wide reading audit

Original exact command ledger · 15 lines
  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