PA001Y

mod_eq_mul_right

Stable checked-use theorem · independently closed

Balanced congruence is preserved by multiplication on the right.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Balanced congruence is preserved by multiplication on the right.

Use the direct prerequisites add_mul, mul_assoc as previously established PA formulas.

The proof proceeds by case analysis (2).

Referenced ingredients

PA0016 add_mul PA000B mul_assoc

Proof neighborhood

Direct dependencies

PA0016 add_mul PA000B mul_assoc

Direct dependents

PA0020 mod_eq_mul_left PA003R mod_eq_cancel_coprime PA004E mod_eq_mul PA00AK bounded_mod_inverse_unique PA00BI mod_one_product_restore_predecessor

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. 0006cases h
  7. 0007cases h_witness
  8. 0008exists x * c
  9. 0009exists x1 * c
  10. 0010trans a * c + (m * x) * c
  11. 0011congr
  12. 0012refl
  13. 0013symm
  14. 0014apply mul_assoc
  15. 0015trans (a + m * x) * c
  16. 0016symm
  17. 0017apply add_mul
  18. 0018trans (b + m * x1) * c
  19. 0019congr
  20. 0020exact h_witness_witness
  21. 0021refl
  22. 0022trans b * c + (m * x1) * c
  23. 0023apply add_mul
  24. 0024congr
  25. 0025refl
  26. 0026apply mul_assoc