PA001S

beta_moduli_pairwise_coprime_bounded

Stable checked-use theorem · independently closed

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.

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

Structural proof guide

Generated structural guide

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

Use the direct prerequisites lt_trichotomy, beta_moduli_coprime_of_lt_bounded_common_multiple as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (2).

Referenced ingredients

PA0011 lt_trichotomy PA001R beta_moduli_coprime_of_lt_bounded_common_multiple

Proof neighborhood

Direct dependencies

PA0011 lt_trichotomy PA001R beta_moduli_coprime_of_lt_bounded_common_multiple

Direct dependents

PA001U beta_exclusive_accumulated_product_step

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

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.

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 : forall e. (exists u. S ((S i) * c) = e * u) -> (exists v. S ((S j) * c) = e * v) -> e = 1
  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 : forall e. (exists u. S ((S j) * c) = e * u) -> (exists v. S ((S i) * c) = e * v) -> e = 1
  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 exact 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 : 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 : 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