PA0017

common_divisor_beta_moduli_divides_gap_times_c

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites divides_remainder, add_succ_left, add_mul, zero_add as previously established PA formulas.

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

Referenced ingredients

PA0014 divides_remainder PA000E add_succ_left PA0016 add_mul PA0001 zero_add

Proof neighborhood

Direct dependencies

PA0014 divides_remainder PA000E add_succ_left PA0016 add_mul PA0001 zero_add

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