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.

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.

  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