PA0015

beta_modulus_coprime_base

Stable checked-use theorem · independently closed

Every beta-shaped successor modulus is coprime to its base c.

Exact expanded PA statement

forall c k d. (exists u. S (k * c) = d * u) -> (exists v. c = d * v) -> d = 1

Structural proof guide

Generated structural guide

Every beta-shaped successor modulus is coprime to its base c.

Use the direct prerequisites divides_remainder, divisor_one, mul_comm as previously established PA formulas.

The proof proceeds by intermediate claims (2), certified simplification (1).

Referenced ingredients

PA0014 divides_remainder PA000O divisor_one PA000H mul_comm

Proof neighborhood

Direct dependencies

PA0014 divides_remainder PA000O divisor_one PA000H mul_comm

Direct dependents

PA001Q beta_moduli_coprime_of_gap_dvd

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 k
  3. 0003intro d
  4. 0004intro hm
  5. 0005intro hc
  6. 0006have hstep : S (k * c) = c * k + 1
  7. 0007simp [mul_comm]
  8. 0008have h1 : exists w. 1 = d * w
  9. 0009specialize divides_remainder d
  10. 0010specialize divides_remainder (S (k * c))
  11. 0011specialize divides_remainder c
  12. 0012specialize divides_remainder k
  13. 0013specialize divides_remainder 1
  14. 0014apply divides_remainder
  15. 0015exact hm
  16. 0016exact hc
  17. 0017exact hstep
  18. 0018specialize divisor_one d
  19. 0019apply divisor_one
  20. 0020exact h1