PA0024

mod_eq_trans

Stable checked-use theorem · independently closed

Balanced natural congruence is transitive.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Balanced natural congruence is transitive.

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

The proof proceeds by case analysis (4).

Referenced ingredients

PA0009 add_assoc PA000F add_comm PA000A mul_add

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000F add_comm PA000A mul_add

Direct dependents

PA0026 binary_crt PA0028 binary_crt_fold_step PA002V mod_eq_to_remainder_decomposition PA003Q coprime_mod_inverse PA003R mod_eq_cancel_coprime PA004E mod_eq_mul PA005E pow_predecessor_parity_mod PA005J mod_eq_decidable_from_remainders PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA0070 gauss_pointwise_signed_half_representative PA0079 prime_scaled_same_target_unique PA007B gauss_mixed_sign_scaled_source_impossible PA0087 quadratic_residue_mod_equiv PA008E prime_mul_index_map_injective PA008M quadratic_residue_half_power_mod_one PA008O scaled_inverse_transport_right PA009C prime_scaled_inverse_unique PA00BK scaled_pair_order_terminal_power_mod_predecessor PA00BQ bounded_euler_criterion_residue_iff PA00BR arbitrary_euler_criterion_residue_iff PA00BS bounded_euler_criterion_nonresidue_iff PA00BT arbitrary_euler_criterion_nonresidue_iff PA00BV arbitrary_gauss_lemma_complete PA00C5 canonical_remainder_from_mod PA00C6 odd_signed_division_branch_exact PA00CJ matching_parity_mod_two PA00CN odd_scaled_division_signed_mod_two PA00FL mod_two_preserves_parity

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