PA004E

mod_eq_mul

Stable checked-use theorem · independently closed

Balanced natural congruence respects multiplication.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Balanced natural congruence respects multiplication.

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

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA001Y mod_eq_mul_right PA0020 mod_eq_mul_left PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA001Y mod_eq_mul_right PA0020 mod_eq_mul_left PA0024 mod_eq_trans

Direct dependents

PA005E pow_predecessor_parity_mod PA005I pow_mod_congruent PA007Q beta_product_pointwise_scale_mod PA00A0 beta_adjacent_target_pairs_product_power PA00B9 beta_adjacent_unit_pairs_product_one

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 d
  6. 0006intro hab
  7. 0007intro hcd
  8. 0008have hacbc : exists r s. (a * c) + m * r = (b * c) + m * s
  9. 0009specialize mod_eq_mul_right m
  10. 0010specialize mod_eq_mul_right a
  11. 0011specialize mod_eq_mul_right b
  12. 0012specialize mod_eq_mul_right c
  13. 0013apply mod_eq_mul_right
  14. 0014exact hab
  15. 0015have hbcbd : exists r s. (b * c) + m * r = (b * d) + m * s
  16. 0016specialize mod_eq_mul_left m
  17. 0017specialize mod_eq_mul_left c
  18. 0018specialize mod_eq_mul_left d
  19. 0019specialize mod_eq_mul_left b
  20. 0020apply mod_eq_mul_left
  21. 0021exact hcd
  22. 0022specialize mod_eq_trans m
  23. 0023specialize mod_eq_trans (a * c)
  24. 0024specialize mod_eq_trans (b * c)
  25. 0025specialize mod_eq_trans (b * d)
  26. 0026apply mod_eq_trans
  27. 0027exact hacbc
  28. 0028exact hbcbd