PA0022

mod_eq_add

Stable checked-use theorem · independently closed

Balanced natural congruence respects addition.

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 addition.

Use the direct prerequisites mul_add, add_comm, add_permute_outer as previously established PA formulas.

The proof proceeds by case analysis (4).

Referenced ingredients

PA000A mul_add PA000F add_comm PA001I add_permute_outer

Proof neighborhood

Direct dependencies

PA000A mul_add PA000F add_comm PA001I add_permute_outer

Direct dependents

PA0026 binary_crt PA003Q coprime_mod_inverse PA007B gauss_mixed_sign_scaled_source_impossible PA00CM signed_remainder_sum_mod_two PA00CQ beta_sum_pointwise_mod_three_add PA00FH gauss_count_sum_mod_two_from_quotient_sums

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. 0008cases hab
  9. 0009cases hab_witness
  10. 0010cases hcd
  11. 0011cases hcd_witness
  12. 0012exists x2 + x
  13. 0013exists x3 + x1
  14. 0014trans (a + c) + (m * x2 + m * x)
  15. 0015congr
  16. 0016refl
  17. 0017apply mul_add
  18. 0018trans (m * x2 + c) + (a + m * x)
  19. 0019apply add_permute_outer
  20. 0020trans (c + m * x2) + (a + m * x)
  21. 0021congr
  22. 0022apply add_comm
  23. 0023refl
  24. 0024trans (a + m * x) + (c + m * x2)
  25. 0025apply add_comm
  26. 0026trans (b + m * x1) + (d + m * x3)
  27. 0027congr
  28. 0028exact hab_witness_witness
  29. 0029exact hcd_witness_witness
  30. 0030trans (d + m * x3) + (b + m * x1)
  31. 0031apply add_comm
  32. 0032trans (m * x3 + d) + (b + m * x1)
  33. 0033congr
  34. 0034apply add_comm
  35. 0035refl
  36. 0036trans (b + d) + (m * x3 + m * x1)
  37. 0037symm
  38. 0038apply add_permute_outer
  39. 0039congr
  40. 0040refl
  41. 0041symm
  42. 0042apply mul_add