BT004K · Bertrand theorem

beta_moduli_coprime_of_gap_dvd

Stable checked-use theorem · independently kernel verified

Beta moduli at an additive index gap dividing c are coprime.

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. ∀ i. ∀ j. ∀ gap. j = i + gap → Dvd(gap,c) → Coprime(S (S i · c),S (S j · 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

PD0003 Dvd PD0005 Coprime

2 occurrences

In local proof propositions

PD0003 Dvd PD0005 Coprime

5 occurrences

Exact expanded native-PA statement
forall c i j gap. j = i + gap -> (exists k. c = gap * k) -> 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

BT004I beta_modulus_coprime_base BT004J common_divisor_beta_moduli_divides_gap_times_c BT002C multiple_trans BT0028 multiple_refl BT0039 gauss_coprime_cancel BT0006 mul_comm

Direct theorem dependents

BT004O beta_moduli_coprime_of_lt_bounded_common_multiple

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

59 script commands · 12 reading checkpoints · 5 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 (6)
beta modulus coprime basecommon divisor beta moduli divides gap times cmultiple transmultiple reflgauss coprime cancelmul comm
01Fix variables and assumptionsL1–9

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

  1. L1
    intro c
  2. L2
    intro i
  3. L3
    intro j
  4. L4
    intro gap
  5. L5
    intro hij
  6. L6
    intro hgapc
  7. L7
    intro d
  8. L8
    intro hmi
  9. L9
    intro hmj
02Establish hcopdcL10–13

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

  1. L10
    have hcopdc : Coprime(d,c)Definitions: Coprime(d,c)Original native command in the exact edition
  2. L11
    intro e
  3. L12
    intro hed
  4. L13
    intro hec
03Establish hmeiL14–23

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

  1. L14
    have hmei : Dvd(e,S (S i · c))Definitions: Dvd(e,S (S i · c))Original native command in the exact edition
  2. L15
    specialize multiple_trans d
  3. L16
    specialize multiple_trans e
  4. L17
    specialize multiple_trans (S ((S i) * c))
  5. L18
    apply multiple_trans
  6. L19
    exact hmi
  7. L20
    exact hed
  8. L21
    specialize beta_modulus_coprime_base c
  9. L22
    specialize beta_modulus_coprime_base (S i)
  10. L23
    specialize beta_modulus_coprime_base e
04Use earlier factsL24–26

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

  1. L24
    apply beta_modulus_coprime_base
  2. L25
    exact hmei
  3. L26
    exact hec
05Establish hgapprodL27–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply common divisor beta moduli divides gap times c.

  1. L27
    have hgapprod : Dvd(d,gap · c)Definitions: Dvd(d,gap · c)Original native command in the exact edition
  2. L28
    specialize common_divisor_beta_moduli_divides_gap_times_c c
  3. L29
    specialize common_divisor_beta_moduli_divides_gap_times_c i
  4. L30
    specialize common_divisor_beta_moduli_divides_gap_times_c j
  5. L31
    specialize common_divisor_beta_moduli_divides_gap_times_c gap
  6. L32
    specialize common_divisor_beta_moduli_divides_gap_times_c d
  7. L33
    apply common_divisor_beta_moduli_divides_gap_times_c
  8. L34
    exact hij
  9. L35
    exact hmi
  10. L36
    exact hmj
06Separate the logical casesL37–37

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

  1. L37
    cases hgapprod
07Establish hdivgapL38–43

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

  1. L38
    have hdivgap : Dvd(d,gap)Definitions: Dvd(d,gap)Original native command in the exact edition
  2. L39
    specialize gauss_coprime_cancel d
  3. L40
    specialize gauss_coprime_cancel c
  4. L41
    specialize gauss_coprime_cancel gap
  5. L42
    apply gauss_coprime_cancel
  6. L43
    exact hcopdc
08Construct an explicit witnessL44–44

Supply the displayed value, then prove that it has the required property.

  1. L44
    exists x
09Calculate and transport equalitiesL45–45

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L45
    trans gap * c
10Use earlier factsL46–47

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

  1. L46
    apply mul_comm
  2. L47
    exact hgapprod_witness
11Establish hdcL48–57

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

  1. L48
  2. L49
    specialize multiple_trans gap
  3. L50
    specialize multiple_trans d
  4. L51
    specialize multiple_trans c
  5. L52
    apply multiple_trans
  6. L53
    exact hgapc
  7. L54
    exact hdivgap
  8. L55
    specialize hcopdc d
  9. L56
    apply hcopdc
  10. L57
    specialize multiple_refl d
12Use earlier factsL58–59

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

  1. L58
    exact multiple_refl
  2. L59
    exact hdc

Library-wide reading audit

Original defined command ledger · 59 lines
  1. 0001intro c
  2. 0002intro i
  3. 0003intro j
  4. 0004intro gap
  5. 0005intro hij
  6. 0006intro hgapc
  7. 0007intro d
  8. 0008intro hmi
  9. 0009intro hmj
  10. 0010have hcopdc : Coprime(d,c)
    Exact native replay linehave hcopdc : forall e. (exists u. d = e * u) -> (exists v. c = e * v) -> e = 1
  11. 0011intro e
  12. 0012intro hed
  13. 0013intro hec
  14. 0014have hmei : Dvd(e,S (S i · c))
    Exact native replay linehave hmei : exists u. S ((S i) * c) = e * u
  15. 0015specialize multiple_trans d
  16. 0016specialize multiple_trans e
  17. 0017specialize multiple_trans (S ((S i) * c))
  18. 0018apply multiple_trans
  19. 0019exact hmi
  20. 0020exact hed
  21. 0021specialize beta_modulus_coprime_base c
  22. 0022specialize beta_modulus_coprime_base (S i)
  23. 0023specialize beta_modulus_coprime_base e
  24. 0024apply beta_modulus_coprime_base
  25. 0025exact hmei
  26. 0026exact hec
  27. 0027have hgapprod : Dvd(d,gap · c)
    Exact native replay linehave hgapprod : exists w. gap * c = d * w
  28. 0028specialize common_divisor_beta_moduli_divides_gap_times_c c
  29. 0029specialize common_divisor_beta_moduli_divides_gap_times_c i
  30. 0030specialize common_divisor_beta_moduli_divides_gap_times_c j
  31. 0031specialize common_divisor_beta_moduli_divides_gap_times_c gap
  32. 0032specialize common_divisor_beta_moduli_divides_gap_times_c d
  33. 0033apply common_divisor_beta_moduli_divides_gap_times_c
  34. 0034exact hij
  35. 0035exact hmi
  36. 0036exact hmj
  37. 0037cases hgapprod
  38. 0038have hdivgap : Dvd(d,gap)
    Exact native replay linehave hdivgap : exists w. gap = d * w
  39. 0039specialize gauss_coprime_cancel d
  40. 0040specialize gauss_coprime_cancel c
  41. 0041specialize gauss_coprime_cancel gap
  42. 0042apply gauss_coprime_cancel
  43. 0043exact hcopdc
  44. 0044exists x
  45. 0045trans gap * c
  46. 0046apply mul_comm
  47. 0047exact hgapprod_witness
  48. 0048have hdc : Dvd(d,c)
    Exact native replay linehave hdc : exists w. c = d * w
  49. 0049specialize multiple_trans gap
  50. 0050specialize multiple_trans d
  51. 0051specialize multiple_trans c
  52. 0052apply multiple_trans
  53. 0053exact hgapc
  54. 0054exact hdivgap
  55. 0055specialize hcopdc d
  56. 0056apply hcopdc
  57. 0057specialize multiple_refl d
  58. 0058exact multiple_refl
  59. 0059exact hdc