BT004I

beta_modulus_coprime_base

Stable · empty-context checked

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

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

Direct prerequisites: divides_remainder, divisor_one, mul_comm. The authored body proceeds by intermediate claims (2).

Proof neighborhood

Direct dependencies

BT002H divides_remainder BT002E divisor_one BT0006 mul_comm

Direct dependents

BT004K beta_moduli_coprime_of_gap_dvd

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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