PA001R · theorem

beta_moduli_coprime_of_lt_bounded_common_multiple

Stable checked-use theorem · independently closed

Ordered bounded indices have coprime beta moduli when c is a common multiple of the bounded positive gaps.

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

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

PD0001 Le PD0002 Lt PD0003 Dvd PD0005 Coprime

4 occurrences

In local proof propositions

PD0002 Lt PD0003 Dvd PD0005 Coprime

3 occurrences

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

PA001Q beta_moduli_coprime_of_gap_dvd PA000F add_comm PA000R le_trans

Direct theorem dependents

PA001S beta_moduli_pairwise_coprime_bounded

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

49 script commands · 15 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 (3)
beta moduli coprime of gap dvdadd commle trans
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 i
  4. L4
    intro j
  5. L5
    intro hcm
  6. L6
    intro hlt
  7. L7
    intro hjB
  8. L8
    intro d
  9. L9
    intro hdi
  10. L10
    intro hdj
02Separate the logical casesL11–11

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

  1. L11
    cases hlt
03Establish hijL12–16

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

  1. L12
    have hij : j = i + S x
  2. L13
    symm
  3. L14
    trans x + S i
  4. L15
    simp [add_comm]
  5. L16
    exact hlt_witness
04Establish hgapleL17–21

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

  1. L17
    have hgaple : Lt(x,B)Definitions: Lt(x,B)Original native command in the exact edition
  2. L18
    specialize le_trans (S x)
  3. L19
    specialize le_trans j
  4. L20
    specialize le_trans B
  5. L21
    apply le_trans
05Construct an explicit witnessL22–22

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

  1. L22
    exists i
06Calculate and transport equalitiesL23–23

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

  1. L23
    symm
07Use earlier factsL24–25

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

  1. L24
    exact hij
  2. L25
    exact hjB
08Separate the logical casesL26–26

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

  1. L26
    cases hgaple
09Establish hgapboundL27–27

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

  1. L27
    have hgapbound : exists h. S x + S h = S B
10Construct an explicit witnessL28–28

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

  1. L28
    exists x1
11Calculate and transport equalitiesL29–31

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

  1. L29
    rewrite PA4
  2. L30
    congr
  3. L31
    trans x1 + S x
12Use earlier factsL32–33

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

  1. L32
    apply add_comm
  2. L33
    exact hgaple_witness
13Establish hgapdvdL34–37

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

  1. L34
    have hgapdvd : Dvd(S x,c)Definitions: Dvd(S x,c)Original native command in the exact edition
  2. L35
    specialize hcm x
  3. L36
    apply hcm
  4. L37
    exact hgapbound
14Establish hcopL38–47

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta moduli coprime of gap dvd.

  1. L38
    have hcop : 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. L39
    specialize beta_moduli_coprime_of_gap_dvd c
  3. L40
    specialize beta_moduli_coprime_of_gap_dvd i
  4. L41
    specialize beta_moduli_coprime_of_gap_dvd j
  5. L42
    specialize beta_moduli_coprime_of_gap_dvd (S x)
  6. L43
    apply beta_moduli_coprime_of_gap_dvd
  7. L44
    exact hij
  8. L45
    exact hgapdvd
  9. L46
    specialize hcop d
  10. L47
    apply hcop
15Use earlier factsL48–49

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

  1. L48
    exact hdi
  2. L49
    exact hdj

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro B
  2. 0002intro c
  3. 0003intro i
  4. 0004intro j
  5. 0005intro hcm
  6. 0006intro hlt
  7. 0007intro hjB
  8. 0008intro d
  9. 0009intro hdi
  10. 0010intro hdj
  11. 0011cases hlt
  12. 0012have hij : j = i + S x
  13. 0013symm
  14. 0014trans x + S i
  15. 0015simp [add_comm]
  16. 0016exact hlt_witness
  17. 0017have hgaple : Lt(x,B)
    Exact native replay linehave hgaple : exists r. r + S x = B
  18. 0018specialize le_trans (S x)
  19. 0019specialize le_trans j
  20. 0020specialize le_trans B
  21. 0021apply le_trans
  22. 0022exists i
  23. 0023symm
  24. 0024exact hij
  25. 0025exact hjB
  26. 0026cases hgaple
  27. 0027have hgapbound : exists h. S x + S h = S B
  28. 0028exists x1
  29. 0029rewrite PA4
  30. 0030congr
  31. 0031trans x1 + S x
  32. 0032apply add_comm
  33. 0033exact hgaple_witness
  34. 0034have hgapdvd : Dvd(S x,c)
    Exact native replay linehave hgapdvd : exists k. c = S x * k
  35. 0035specialize hcm x
  36. 0036apply hcm
  37. 0037exact hgapbound
  38. 0038have hcop : Coprime(S (S i · c),S (S j · c))
    Exact native replay linehave hcop : forall e. (exists u. S ((S i) * c) = e * u) -> (exists v. S ((S j) * c) = e * v) -> e = 1
  39. 0039specialize beta_moduli_coprime_of_gap_dvd c
  40. 0040specialize beta_moduli_coprime_of_gap_dvd i
  41. 0041specialize beta_moduli_coprime_of_gap_dvd j
  42. 0042specialize beta_moduli_coprime_of_gap_dvd (S x)
  43. 0043apply beta_moduli_coprime_of_gap_dvd
  44. 0044exact hij
  45. 0045exact hgapdvd
  46. 0046specialize hcop d
  47. 0047apply hcop
  48. 0048exact hdi
  49. 0049exact hdj