BT004T

mod_eq_of_mod_eq_multiple

Stable · empty-context checked

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

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

Direct prerequisites: mul_assoc. The authored body proceeds by case analysis (3), equality transport (2).

Proof neighborhood

Direct dependencies

BT0008 mul_assoc

Direct dependents

BT004U binary_crt_fold_step

Formal native tactic body

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

  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