BT004J

common_divisor_beta_moduli_divides_gap_times_c

Stable · empty-context checked

A common divisor of two ordered beta moduli divides the index gap times c.

Exact expanded PA statement

forall c i j gap d. j = i + gap -> (exists u. S ((S i) * c) = d * u) -> (exists v. S ((S j) * c) = d * v) -> exists w. gap * c = d * w

Structural proof guide

A common divisor of two ordered beta moduli divides the index gap times c.

Direct prerequisites: divides_remainder, add_succ_left, add_mul, zero_add. The authored body proceeds by intermediate claims (1), equality transport (2).

Proof neighborhood

Direct dependencies

BT002H divides_remainder BT0001 add_succ_left BT000B add_mul BT0000 zero_add

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 i
  3. 0003intro j
  4. 0004intro gap
  5. 0005intro d
  6. 0006intro hij
  7. 0007intro hmi
  8. 0008intro hmj
  9. 0009have hstep : S ((S j) * c) = S ((S i) * c) * 1 + gap * c
  10. 0010rewrite hij
  11. 0011specialize add_succ_left i
  12. 0012specialize add_succ_left gap
  13. 0013rewrite <- add_succ_left
  14. 0014simp [add_mul, zero_add]
  15. 0015symm
  16. 0016specialize add_succ_left_before (S i * c)
  17. 0017specialize add_succ_left_before (gap * c)
  18. 0018exact add_succ_left_before
  19. 0019specialize divides_remainder d
  20. 0020specialize divides_remainder (S ((S j) * c))
  21. 0021specialize divides_remainder (S ((S i) * c))
  22. 0022specialize divides_remainder 1
  23. 0023specialize divides_remainder (gap * c)
  24. 0024apply divides_remainder
  25. 0025exact hmj
  26. 0026exact hmi
  27. 0027exact hstep