PA0062

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.

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

Structural proof guide

Generated structural guide

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

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

The proof proceeds by intermediate claims (3).

Referenced ingredients

PA0031 prime_nonzero PA003N prime_not_divides_coprime PA003Q coprime_mod_inverse

Proof neighborhood

Direct dependencies

PA0031 prime_nonzero PA003N prime_not_divides_coprime PA003Q coprime_mod_inverse

Direct dependents

PA0063 prime_bounded_nonzero_mod_inverse

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

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.

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
    have hcop : forall d. (exists x. a = d * x) -> (exists y. p = d * y) -> d = 1
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 : forall d. (exists x. p = d * x) -> (exists y. a = d * y) -> d = 1
  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 exact 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 : forall d. (exists x. a = d * x) -> (exists y. p = d * y) -> d = 1
  12. 0012have 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