BT004I · Bertrand theorem

beta_modulus_coprime_base

Stable checked-use theorem · independently kernel verified

Every beta-shaped successor modulus is coprime to its base c.

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

∀ c. ∀ k. Coprime(S (k · c),c)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0005 Coprime

1 occurrences

In local proof propositions

PD0003 Dvd

1 occurrences

Exact expanded native-PA statement
forall c k d. (exists u. S (k * c) = d * u) -> (exists v. c = d * v) -> d = 1

Proof neighborhood

Direct theorem prerequisites

BT002H divides_remainder BT002E divisor_one BT0006 mul_comm

Direct theorem dependents

BT004K beta_moduli_coprime_of_gap_dvd

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

20 script commands · 4 reading checkpoints · 2 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 (2)
divides remainderdivisor one
01Fix variables and assumptionsL1–5

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

  1. L1
    intro c
  2. L2
    intro k
  3. L3
    intro d
  4. L4
    intro hm
  5. L5
    intro hc
02Establish hstepL6–7

Establish this local claim before using it. It is not an additional assumption.

  1. L6
    have hstep : S (k * c) = c * k + 1
  2. L7
    simp [mul_comm]
03Establish h1L8–17

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

  1. L8
  2. L9
    specialize divides_remainder d
  3. L10
    specialize divides_remainder (S (k * c))
  4. L11
    specialize divides_remainder c
  5. L12
    specialize divides_remainder k
  6. L13
    specialize divides_remainder 1
  7. L14
    apply divides_remainder
  8. L15
    exact hm
  9. L16
    exact hc
  10. L17
    exact hstep
04Use earlier factsL18–20

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L18
    specialize divisor_one d
  2. L19
    apply divisor_one
  3. L20
    exact h1

Library-wide reading audit

Original defined command ledger · 20 lines
  1. 0001intro c
  2. 0002intro k
  3. 0003intro d
  4. 0004intro hm
  5. 0005intro hc
  6. 0006have hstep : S (k * c) = c * k + 1
  7. 0007simp [mul_comm]
  8. 0008have h1 : Dvd(d,1)
    Exact native replay linehave h1 : exists w. 1 = d * w
  9. 0009specialize divides_remainder d
  10. 0010specialize divides_remainder (S (k * c))
  11. 0011specialize divides_remainder c
  12. 0012specialize divides_remainder k
  13. 0013specialize divides_remainder 1
  14. 0014apply divides_remainder
  15. 0015exact hm
  16. 0016exact hc
  17. 0017exact hstep
  18. 0018specialize divisor_one d
  19. 0019apply divisor_one
  20. 0020exact h1