PA003S · theorem

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.

Statement with defined notation

∀ p. ∀ a. ∀ x. ∀ y. Prime(p) → ¬Dvd(p,a) → ModEq(p,a · x,a · y) → ModEq(p,x,y)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0003 Dvd PD0004 Prime PD0008 ModEq

4 occurrences

In local proof propositions

PD0005 Coprime

2 occurrences

Exact expanded native-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

Proof neighborhood

Direct theorem prerequisites

PA0031 prime_nonzero PA003N prime_not_divides_coprime PA003O coprime_symm PA003R mod_eq_cancel_coprime

Direct theorem 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

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : Coprime(p,a)Definitions: Coprime(p,a)Original native command in the exact edition
  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 : Coprime(a,p)Definitions: Coprime(a,p)Original native command in the exact edition
  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 defined 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 : Coprime(p,a)
    Exact native replay linehave 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 : Coprime(a,p)
    Exact native replay linehave 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