PA001R

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.

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

Structural proof guide

Generated structural guide

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

Use the direct prerequisites beta_moduli_coprime_of_gap_dvd, add_comm, le_trans as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (5), equality transport (1), certified simplification (1).

Referenced ingredients

PA001Q beta_moduli_coprime_of_gap_dvd PA000F add_comm PA000R le_trans

Proof neighborhood

Direct dependencies

PA001Q beta_moduli_coprime_of_gap_dvd PA000F add_comm PA000R le_trans

Direct dependents

PA001S beta_moduli_pairwise_coprime_bounded

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 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 : 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 : exists k. c = S x * k
  35. 0035specialize hcm x
  36. 0036apply hcm
  37. 0037exact hgapbound
  38. 0038have 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