PA0027

mod_eq_of_mod_eq_multiple

Stable checked-use theorem · independently closed

Balanced congruence descends from a multiple modulus to every divisor modulus.

Exact expanded PA statement

forall m P x a. (exists k. P = m * k) -> (exists u v. x + P * u = a + P * v) -> exists r s. x + m * r = a + m * s

Structural proof guide

Generated structural guide

Balanced congruence descends from a multiple modulus to every divisor modulus.

Use the direct prerequisites mul_assoc as previously established PA formulas.

The proof proceeds by case analysis (3), equality transport (2).

Referenced ingredients

PA000B mul_assoc

Proof neighborhood

Direct dependencies

PA000B mul_assoc

Direct dependents

PA0028 binary_crt_fold_step

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 m
  2. 0002intro P
  3. 0003intro x
  4. 0004intro a
  5. 0005intro hdiv
  6. 0006intro hmod
  7. 0007cases hdiv
  8. 0008cases hmod
  9. 0009cases hmod_witness
  10. 0010rewrite hdiv_witness at hmod_witness_witness
  11. 0011rewrite hdiv_witness at hmod_witness_witness
  12. 0012exists x1 * x2
  13. 0013exists x1 * x3
  14. 0014trans x + (m * x1) * x2
  15. 0015congr
  16. 0016refl
  17. 0017symm
  18. 0018apply mul_assoc
  19. 0019trans a + (m * x1) * x3
  20. 0020exact hmod_witness_witness
  21. 0021congr
  22. 0022refl
  23. 0023apply mul_assoc