PA000L · theorem

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.

Statement with defined notation

∀ N. ∀ C. ∀ B. (∀ x. (∃ y. S x + S y = S N) → Dvd(S x,C)) → ∀ x. (∃ y. S x + S y = S N) → Dvd(S x,C · B)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd

2 occurrences

In local proof propositions

PD0003 Dvd

1 occurrences

Exact expanded native-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

Proof neighborhood

Direct theorem prerequisites

PA000C multiple_mul_right

Direct theorem dependents

PA002X beta_prefix_extend

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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
  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 defined 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 : Dvd(S t,C)
    Exact native replay linehave 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