PA003S

prime_mod_cancel

Stable checked-use theorem · independently closed

A nonzero residue factor cancels from congruence modulo a prime.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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.

Read the argument

Proof checkpoints

32 script commands · 5 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (4)
prime nonzeroprime not divides coprimecoprime symmmod eq cancel coprime
01Fix variables and assumptionsL1–7

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro hp
  6. L6
    intro hnot
  7. L7
    intro hxy
02Establish hp0L8–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime nonzero.

  1. L8
    have hp0 : ~(p = 0)
  2. L9
    intro hpzero
  3. L10
    specialize prime_nonzero p
  4. L11
    apply prime_nonzero
  5. L12
    exact hp
  6. L13
    exact hpzero
03Establish hpacopL14–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime not divides coprime.

  1. L14
    have hpacop : forall d. (exists u. p = d * u) -> (exists v. a = d * v) -> d = 1
  2. L15
    specialize prime_not_divides_coprime p
  3. L16
    specialize prime_not_divides_coprime a
  4. L17
    apply prime_not_divides_coprime
  5. L18
    exact hp
  6. L19
    exact hnot
04Establish hapcopL20–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply coprime symm.

  1. L20
    have hapcop : forall d. (exists u. a = d * u) -> (exists v. p = d * v) -> d = 1
  2. L21
    specialize coprime_symm p
  3. L22
    specialize coprime_symm a
  4. L23
    apply coprime_symm
  5. L24
    exact hpacop
  6. L25
    specialize mod_eq_cancel_coprime p
  7. L26
    specialize mod_eq_cancel_coprime a
  8. L27
    specialize mod_eq_cancel_coprime x
  9. L28
    specialize mod_eq_cancel_coprime y
  10. L29
    apply mod_eq_cancel_coprime
05Use earlier factsL30–32

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L30
    exact hp0
  2. L31
    exact hapcop
  3. L32
    exact hxy

Library-wide reading audit

Original exact command ledger · 32 lines
  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