PA0062 · theorem

prime_mod_inverse

Stable checked-use theorem · independently closed

A nonzero residue modulo a prime has a natural modular inverse.

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. Prime(p) → ¬Dvd(p,a) → ∃ x. BalancedInverse(p,a,x)

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 PD0031 BalancedInverse

3 occurrences

In local proof propositions

PD0005 Coprime

2 occurrences

Exact expanded native-PA statement
forall p a. (~(p = 1) /\ forall c e. p = c * e -> c = 1 \/ e = 1) -> ~(exists k. a = p * k) -> exists z u v. a * z + p * u = 1 + p * v

Proof neighborhood

Direct theorem prerequisites

PA0031 prime_nonzero PA003N prime_not_divides_coprime PA003Q coprime_mod_inverse

Direct theorem dependents

PA0063 prime_bounded_nonzero_mod_inverse

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

29 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 (3)
prime nonzeroprime not divides coprimecoprime mod inverse
01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro hp
  4. L4
    intro hnot
02Establish hp0L5–10

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

  1. L5
    have hp0 : ~(p = 0)
  2. L6
    intro hpzero
  3. L7
    specialize prime_nonzero p
  4. L8
    apply prime_nonzero
  5. L9
    exact hp
  6. L10
    exact hpzero
03Establish hcopL11–11

Establish this local claim before using it. It is not an additional assumption.

  1. L11
04Establish hpacopL12–21

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

  1. L12
    have hpacop : Coprime(p,a)Definitions: Coprime(p,a)Original native command in the exact edition
  2. L13
    specialize prime_not_divides_coprime p
  3. L14
    specialize prime_not_divides_coprime a
  4. L15
    apply prime_not_divides_coprime
  5. L16
    exact hp
  6. L17
    exact hnot
  7. L18
    intro d
  8. L19
    intro hda
  9. L20
    intro hdp
  10. L21
    specialize hpacop d
05Use earlier factsL22–29

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

  1. L22
    apply hpacop
  2. L23
    exact hdp
  3. L24
    exact hda
  4. L25
    specialize coprime_mod_inverse a
  5. L26
    specialize coprime_mod_inverse p
  6. L27
    apply coprime_mod_inverse
  7. L28
    exact hp0
  8. L29
    exact hcop

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro hp
  4. 0004intro hnot
  5. 0005have hp0 : ~(p = 0)
  6. 0006intro hpzero
  7. 0007specialize prime_nonzero p
  8. 0008apply prime_nonzero
  9. 0009exact hp
  10. 0010exact hpzero
  11. 0011have hcop : Coprime(a,p)
    Exact native replay linehave hcop : forall d. (exists x. a = d * x) -> (exists y. p = d * y) -> d = 1
  12. 0012have hpacop : Coprime(p,a)
    Exact native replay linehave hpacop : forall d. (exists x. p = d * x) -> (exists y. a = d * y) -> d = 1
  13. 0013specialize prime_not_divides_coprime p
  14. 0014specialize prime_not_divides_coprime a
  15. 0015apply prime_not_divides_coprime
  16. 0016exact hp
  17. 0017exact hnot
  18. 0018intro d
  19. 0019intro hda
  20. 0020intro hdp
  21. 0021specialize hpacop d
  22. 0022apply hpacop
  23. 0023exact hdp
  24. 0024exact hda
  25. 0025specialize coprime_mod_inverse a
  26. 0026specialize coprime_mod_inverse p
  27. 0027apply coprime_mod_inverse
  28. 0028exact hp0
  29. 0029exact hcop