PA0062

prime_mod_inverse

Stable checked-use theorem · independently closed

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

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.

  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