BT004P · Bertrand theorem

beta_moduli_pairwise_coprime_bounded

Stable checked-use theorem · independently kernel verified

Distinct indices in a bounded prefix have pairwise coprime beta moduli under a bounded common-multiple invariant.

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

∀ B. ∀ c. (∀ x. (∃ y. S x + S y = S B) → Dvd(S x,c)) → ∀ x. ∀ y. ¬x = y → Le(x,B) → Le(y,B) → Coprime(S (S x · c),S (S y · 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

PD0001 Le PD0003 Dvd PD0005 Coprime

4 occurrences

In local proof propositions

PD0005 Coprime

2 occurrences

Exact expanded native-PA statement
forall B c. (forall t. (exists h. S t + S h = S B) -> exists k. c = S t * k) -> forall i j. ~(i = j) -> (exists hi. hi + i = B) -> (exists hj. hj + j = B) -> forall d. (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> d = 1

Proof neighborhood

Direct theorem prerequisites

BT001H lt_trichotomy BT004O beta_moduli_coprime_of_lt_bounded_common_multiple

Direct theorem dependents

BT0059 beta_exclusive_accumulated_product_step

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

44 script commands · 10 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)
lt trichotomybeta moduli coprime of lt bounded common multiple
01Fix variables and assumptionsL1–10

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

  1. L1
    intro B
  2. L2
    intro c
  3. L3
    intro hcm
  4. L4
    intro i
  5. L5
    intro j
  6. L6
    intro hne
  7. L7
    intro hiB
  8. L8
    intro hjB
  9. L9
    intro d
  10. L10
    intro hdi
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hdj
03Use earlier factsL12–13

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

  1. L12
    specialize lt_trichotomy i
  2. L13
    specialize lt_trichotomy j
04Separate the logical casesL14–15

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    cases lt_trichotomy
  2. L15
    exfalso
05Use earlier factsL16–17

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

  1. L16
    apply hne
  2. L17
    exact lt_trichotomy_left
06Separate the logical casesL18–18

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L18
    cases lt_trichotomy_right
07Establish hcopijL19–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta moduli coprime of lt bounded common multiple.

  1. L19
    have hcopij : Coprime(S (S i · c),S (S j · c))Definitions: Coprime(S (S i · c),S (S j · c))Original native command in the exact edition
  2. L20
    specialize beta_moduli_coprime_of_lt_bounded_common_multiple B
  3. L21
    specialize beta_moduli_coprime_of_lt_bounded_common_multiple c
  4. L22
    specialize beta_moduli_coprime_of_lt_bounded_common_multiple i
  5. L23
    specialize beta_moduli_coprime_of_lt_bounded_common_multiple j
  6. L24
    apply beta_moduli_coprime_of_lt_bounded_common_multiple
  7. L25
    exact hcm
  8. L26
    exact lt_trichotomy_right_left
  9. L27
    exact hjB
  10. L28
    specialize hcopij d
08Use earlier factsL29–31

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

  1. L29
    apply hcopij
  2. L30
    exact hdi
  3. L31
    exact hdj
09Establish hcopjiL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta moduli coprime of lt bounded common multiple.

  1. L32
    have hcopji : Coprime(S (S j · c),S (S i · c))Definitions: Coprime(S (S j · c),S (S i · c))Original native command in the exact edition
  2. L33
    specialize beta_moduli_coprime_of_lt_bounded_common_multiple B
  3. L34
    specialize beta_moduli_coprime_of_lt_bounded_common_multiple c
  4. L35
    specialize beta_moduli_coprime_of_lt_bounded_common_multiple j
  5. L36
    specialize beta_moduli_coprime_of_lt_bounded_common_multiple i
  6. L37
    apply beta_moduli_coprime_of_lt_bounded_common_multiple
  7. L38
    exact hcm
  8. L39
    exact lt_trichotomy_right_right
  9. L40
    exact hiB
  10. L41
    specialize hcopji d
10Use earlier factsL42–44

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

  1. L42
    apply hcopji
  2. L43
    exact hdj
  3. L44
    exact hdi

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro B
  2. 0002intro c
  3. 0003intro hcm
  4. 0004intro i
  5. 0005intro j
  6. 0006intro hne
  7. 0007intro hiB
  8. 0008intro hjB
  9. 0009intro d
  10. 0010intro hdi
  11. 0011intro hdj
  12. 0012specialize lt_trichotomy i
  13. 0013specialize lt_trichotomy j
  14. 0014cases lt_trichotomy
  15. 0015exfalso
  16. 0016apply hne
  17. 0017exact lt_trichotomy_left
  18. 0018cases lt_trichotomy_right
  19. 0019have hcopij : Coprime(S (S i · c),S (S j · c))
    Exact native replay linehave hcopij : forall e. (exists u. S ((S i) * c) = e * u) -> (exists v. S ((S j) * c) = e * v) -> e = 1
  20. 0020specialize beta_moduli_coprime_of_lt_bounded_common_multiple B
  21. 0021specialize beta_moduli_coprime_of_lt_bounded_common_multiple c
  22. 0022specialize beta_moduli_coprime_of_lt_bounded_common_multiple i
  23. 0023specialize beta_moduli_coprime_of_lt_bounded_common_multiple j
  24. 0024apply beta_moduli_coprime_of_lt_bounded_common_multiple
  25. 0025exact hcm
  26. 0026exact lt_trichotomy_right_left
  27. 0027exact hjB
  28. 0028specialize hcopij d
  29. 0029apply hcopij
  30. 0030exact hdi
  31. 0031exact hdj
  32. 0032have hcopji : Coprime(S (S j · c),S (S i · c))
    Exact native replay linehave hcopji : forall e. (exists u. S ((S j) * c) = e * u) -> (exists v. S ((S i) * c) = e * v) -> e = 1
  33. 0033specialize beta_moduli_coprime_of_lt_bounded_common_multiple B
  34. 0034specialize beta_moduli_coprime_of_lt_bounded_common_multiple c
  35. 0035specialize beta_moduli_coprime_of_lt_bounded_common_multiple j
  36. 0036specialize beta_moduli_coprime_of_lt_bounded_common_multiple i
  37. 0037apply beta_moduli_coprime_of_lt_bounded_common_multiple
  38. 0038exact hcm
  39. 0039exact lt_trichotomy_right_right
  40. 0040exact hiB
  41. 0041specialize hcopji d
  42. 0042apply hcopji
  43. 0043exact hdj
  44. 0044exact hdi