PA001Q

beta_moduli_coprime_of_gap_dvd

Stable checked-use theorem · independently closed

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

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

Structural proof guide

Generated structural guide

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

Use the direct prerequisites beta_modulus_coprime_base, common_divisor_beta_moduli_divides_gap_times_c, multiple_trans, multiple_refl, gauss_coprime_cancel, mul_comm as previously established PA formulas.

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

Referenced ingredients

PA0015 beta_modulus_coprime_base PA0017 common_divisor_beta_moduli_divides_gap_times_c PA0018 multiple_trans PA0019 multiple_refl PA001P gauss_coprime_cancel PA000H mul_comm

Proof neighborhood

Direct dependencies

PA0015 beta_modulus_coprime_base PA0017 common_divisor_beta_moduli_divides_gap_times_c PA0018 multiple_trans PA0019 multiple_refl PA001P gauss_coprime_cancel PA000H mul_comm

Direct dependents

PA001R beta_moduli_coprime_of_lt_bounded_common_multiple

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 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 : 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 : 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 : 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 : 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 : 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