PA003S

prime_mod_cancel

Stable checked-use theorem · independently closed

A nonzero residue factor cancels from congruence modulo a prime.

Exact expanded PA statement

forall p a x y. (~(p = 1) /\ forall c e. p = c * e -> c = 1 \/ e = 1) -> ~(exists k. a = p * k) -> (exists u v. (a * x) + p * u = (a * y) + p * v) -> exists r s. x + p * r = y + p * s

Structural proof guide

Generated structural guide

A nonzero residue factor cancels from congruence modulo a prime.

Use the direct prerequisites prime_nonzero, prime_not_divides_coprime, coprime_symm, mod_eq_cancel_coprime as previously established PA formulas.

The proof proceeds by intermediate claims (3).

Referenced ingredients

PA0031 prime_nonzero PA003N prime_not_divides_coprime PA003O coprime_symm PA003R mod_eq_cancel_coprime

Proof neighborhood

Direct dependencies

PA0031 prime_nonzero PA003N prime_not_divides_coprime PA003O coprime_symm PA003R mod_eq_cancel_coprime

Direct dependents

PA0079 prime_scaled_same_target_unique PA007B gauss_mixed_sign_scaled_source_impossible PA008E prime_mul_index_map_injective PA009C prime_scaled_inverse_unique

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 p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro y
  5. 0005intro hp
  6. 0006intro hnot
  7. 0007intro hxy
  8. 0008have hp0 : ~(p = 0)
  9. 0009intro hpzero
  10. 0010specialize prime_nonzero p
  11. 0011apply prime_nonzero
  12. 0012exact hp
  13. 0013exact hpzero
  14. 0014have hpacop : forall d. (exists u. p = d * u) -> (exists v. a = d * v) -> d = 1
  15. 0015specialize prime_not_divides_coprime p
  16. 0016specialize prime_not_divides_coprime a
  17. 0017apply prime_not_divides_coprime
  18. 0018exact hp
  19. 0019exact hnot
  20. 0020have hapcop : forall d. (exists u. a = d * u) -> (exists v. p = d * v) -> d = 1
  21. 0021specialize coprime_symm p
  22. 0022specialize coprime_symm a
  23. 0023apply coprime_symm
  24. 0024exact hpacop
  25. 0025specialize mod_eq_cancel_coprime p
  26. 0026specialize mod_eq_cancel_coprime a
  27. 0027specialize mod_eq_cancel_coprime x
  28. 0028specialize mod_eq_cancel_coprime y
  29. 0029apply mod_eq_cancel_coprime
  30. 0030exact hp0
  31. 0031exact hapcop
  32. 0032exact hxy