PA0020

mod_eq_mul_left

Stable checked-use theorem · independently closed

Balanced congruence is preserved by multiplication on the left.

Exact expanded PA statement

forall m a b c. (exists u v. a + m * u = b + m * v) -> exists r s. (c * a) + m * r = (c * b) + m * s

Structural proof guide

Generated structural guide

Balanced congruence is preserved by multiplication on the left.

Use the direct prerequisites mod_eq_mul_right, mul_comm as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (1).

Referenced ingredients

PA001Y mod_eq_mul_right PA000H mul_comm

Proof neighborhood

Direct dependencies

PA001Y mod_eq_mul_right PA000H mul_comm

Direct dependents

PA0026 binary_crt PA003R mod_eq_cancel_coprime PA004E mod_eq_mul PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA008N scaled_inverse_from_unit_inverse PA008O scaled_inverse_transport_right

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 a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro h
  6. 0006specialize mod_eq_mul_right m
  7. 0007specialize mod_eq_mul_right a
  8. 0008specialize mod_eq_mul_right b
  9. 0009specialize mod_eq_mul_right c
  10. 0010have hr : exists r s. (a * c) + m * r = (b * c) + m * s
  11. 0011apply mod_eq_mul_right
  12. 0012exact h
  13. 0013cases hr
  14. 0014cases hr_witness
  15. 0015exists x
  16. 0016exists x1
  17. 0017trans a * c + m * x
  18. 0018congr
  19. 0019apply mul_comm
  20. 0020refl
  21. 0021trans b * c + m * x1
  22. 0022exact hr_witness_witness
  23. 0023congr
  24. 0024apply mul_comm
  25. 0025refl