PA003Q

coprime_mod_inverse

Stable checked-use theorem · independently closed

A nonzero modulus turns balanced Bezout data into 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 a m. ~(m = 0) -> (forall d. (exists x. a = d * x) -> (exists y. m = d * y) -> d = 1) -> exists z u v. a * z + m * u = 1 + m * v

Structural proof guide

Generated structural guide

A nonzero modulus turns balanced Bezout data into a natural modular inverse.

Use the direct prerequisites nonzero_is_succ, coprime_balanced_mod_inverse, mod_eq_refl, mod_eq_add, mod_eq_predecessor_cancel, mod_eq_trans, mul_add, mul_assoc, mul_comm as previously established PA formulas.

The proof proceeds by case analysis (5), intermediate claims (8), equality transport (3).

Referenced ingredients

PA001V nonzero_is_succ PA003P coprime_balanced_mod_inverse PA0023 mod_eq_refl PA0022 mod_eq_add PA0025 mod_eq_predecessor_cancel PA0024 mod_eq_trans PA000A mul_add PA000B mul_assoc PA000H mul_comm

Proof neighborhood

Direct dependencies

PA001V nonzero_is_succ PA003P coprime_balanced_mod_inverse PA0023 mod_eq_refl PA0022 mod_eq_add PA0025 mod_eq_predecessor_cancel PA0024 mod_eq_trans PA000A mul_add PA000B mul_assoc PA000H mul_comm

Direct dependents

PA003R mod_eq_cancel_coprime PA0062 prime_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

66 script commands · 18 reading checkpoints · 8 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 (9)
nonzero is succcoprime balanced mod inversemod eq reflmod eq addmod eq predecessor cancelmod eq transmul addmul assocmul comm
01Fix variables and assumptionsL1–4

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

  1. L1
    intro a
  2. L2
    intro m
  3. L3
    intro hm
  4. L4
    intro hcop
02Establish hmsL5–8

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

  1. L5
    have hms : exists k. m = S k
  2. L6
    specialize nonzero_is_succ m
  3. L7
    apply nonzero_is_succ
  4. L8
    exact hm
03Establish hbalL9–13

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

  1. L9
    have hbal : exists xp xn u v. a * xp + m * u = (1 + a * xn) + m * v
  2. L10
    specialize coprime_balanced_mod_inverse a
  3. L11
    specialize coprime_balanced_mod_inverse m
  4. L12
    apply coprime_balanced_mod_inverse
  5. L13
    exact hcop
04Separate the logical casesL14–18

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L14
    cases hms
  2. L15
    cases hbal
  3. L16
    cases hbal_witness
  4. L17
    cases hbal_witness_witness
  5. L18
    cases hbal_witness_witness_witness
05Establish hselfL19–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq refl.

  1. L19
    have hself : exists u v. (x * (a * x2)) + m * u = (x * (a * x2)) + m * v
  2. L20
    specialize mod_eq_refl m
  3. L21
    specialize mod_eq_refl (x * (a * x2))
  4. L22
    apply mod_eq_refl
06Establish haddL23–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq add.

  1. L23
    have hadd : exists u v. ((a * x1) + x * (a * x2)) + m * u = ((1 + a * x2) + x * (a * x2)) + m * v
  2. L24
    specialize mod_eq_add m
  3. L25
    specialize mod_eq_add (a * x1)
  4. L26
    specialize mod_eq_add (1 + a * x2)
  5. L27
    specialize mod_eq_add (x * (a * x2))
  6. L28
    specialize mod_eq_add (x * (a * x2))
  7. L29
    apply mod_eq_add
07Construct an explicit witnessL30–31

Supply the displayed value, then prove that it has the required property.

  1. L30
    exists x3
  2. L31
    exists x4
08Use earlier factsL32–33

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

  1. L32
    exact hbal_witness_witness_witness_witness
  2. L33
    exact hself
09Establish hcancelL34–37

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

  1. L34
    have hcancel : exists u v. ((1 + a * x2) + x * (a * x2)) + m * u = 1 + m * v
  2. L35
    specialize mod_eq_predecessor_cancel x
  3. L36
    specialize mod_eq_predecessor_cancel 1
  4. L37
    specialize mod_eq_predecessor_cancel (a * x2)
10Establish hkcancelL38–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq predecessor cancel.

  1. L38
    have hkcancel : exists u v. ((1 + a * x2) + x * (a * x2)) + S x * u = 1 + S x * v
  2. L39
    apply mod_eq_predecessor_cancel
  3. L40
    rewrite <- hms_witness at hkcancel
  4. L41
    rewrite <- hms_witness at hkcancel
  5. L42
    exact hkcancel
11Establish hfinalL43–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L43
    have hfinal : exists u v. ((a * x1) + x * (a * x2)) + m * u = 1 + m * v
  2. L44
    specialize mod_eq_trans m
  3. L45
    specialize mod_eq_trans ((a * x1) + x * (a * x2))
  4. L46
    specialize mod_eq_trans ((1 + a * x2) + x * (a * x2))
  5. L47
    specialize mod_eq_trans 1
  6. L48
    apply mod_eq_trans
  7. L49
    exact hadd
  8. L50
    exact hcancel
12Establish hnormL51–60

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

  1. L51
    have hnorm : a * (x1 + x * x2) = (a * x1) + x * (a * x2)
  2. L52
    trans a * x1 + a * (x * x2)
  3. L53
    apply mul_add
  4. L54
    congr
  5. L55
    refl
  6. L56
    trans (a * x) * x2
  7. L57
    symm
  8. L58
    apply mul_assoc
  9. L59
    trans (x * a) * x2
  10. L60
    congr
13Use earlier factsL61–61

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

  1. L61
    apply mul_comm
14Calculate and transport equalitiesL62–62

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L62
    refl
15Use earlier factsL63–63

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

  1. L63
    apply mul_assoc
16Construct an explicit witnessL64–64

Supply the displayed value, then prove that it has the required property.

  1. L64
    exists x1 + x * x2
17Calculate and transport equalitiesL65–65

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L65
    rewrite hnorm
18Use earlier factsL66–66

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

  1. L66
    exact hfinal

Library-wide reading audit

Original exact command ledger · 66 lines
  1. 0001intro a
  2. 0002intro m
  3. 0003intro hm
  4. 0004intro hcop
  5. 0005have hms : exists k. m = S k
  6. 0006specialize nonzero_is_succ m
  7. 0007apply nonzero_is_succ
  8. 0008exact hm
  9. 0009have hbal : exists xp xn u v. a * xp + m * u = (1 + a * xn) + m * v
  10. 0010specialize coprime_balanced_mod_inverse a
  11. 0011specialize coprime_balanced_mod_inverse m
  12. 0012apply coprime_balanced_mod_inverse
  13. 0013exact hcop
  14. 0014cases hms
  15. 0015cases hbal
  16. 0016cases hbal_witness
  17. 0017cases hbal_witness_witness
  18. 0018cases hbal_witness_witness_witness
  19. 0019have hself : exists u v. (x * (a * x2)) + m * u = (x * (a * x2)) + m * v
  20. 0020specialize mod_eq_refl m
  21. 0021specialize mod_eq_refl (x * (a * x2))
  22. 0022apply mod_eq_refl
  23. 0023have hadd : exists u v. ((a * x1) + x * (a * x2)) + m * u = ((1 + a * x2) + x * (a * x2)) + m * v
  24. 0024specialize mod_eq_add m
  25. 0025specialize mod_eq_add (a * x1)
  26. 0026specialize mod_eq_add (1 + a * x2)
  27. 0027specialize mod_eq_add (x * (a * x2))
  28. 0028specialize mod_eq_add (x * (a * x2))
  29. 0029apply mod_eq_add
  30. 0030exists x3
  31. 0031exists x4
  32. 0032exact hbal_witness_witness_witness_witness
  33. 0033exact hself
  34. 0034have hcancel : exists u v. ((1 + a * x2) + x * (a * x2)) + m * u = 1 + m * v
  35. 0035specialize mod_eq_predecessor_cancel x
  36. 0036specialize mod_eq_predecessor_cancel 1
  37. 0037specialize mod_eq_predecessor_cancel (a * x2)
  38. 0038have hkcancel : exists u v. ((1 + a * x2) + x * (a * x2)) + S x * u = 1 + S x * v
  39. 0039apply mod_eq_predecessor_cancel
  40. 0040rewrite <- hms_witness at hkcancel
  41. 0041rewrite <- hms_witness at hkcancel
  42. 0042exact hkcancel
  43. 0043have hfinal : exists u v. ((a * x1) + x * (a * x2)) + m * u = 1 + m * v
  44. 0044specialize mod_eq_trans m
  45. 0045specialize mod_eq_trans ((a * x1) + x * (a * x2))
  46. 0046specialize mod_eq_trans ((1 + a * x2) + x * (a * x2))
  47. 0047specialize mod_eq_trans 1
  48. 0048apply mod_eq_trans
  49. 0049exact hadd
  50. 0050exact hcancel
  51. 0051have hnorm : a * (x1 + x * x2) = (a * x1) + x * (a * x2)
  52. 0052trans a * x1 + a * (x * x2)
  53. 0053apply mul_add
  54. 0054congr
  55. 0055refl
  56. 0056trans (a * x) * x2
  57. 0057symm
  58. 0058apply mul_assoc
  59. 0059trans (x * a) * x2
  60. 0060congr
  61. 0061apply mul_comm
  62. 0062refl
  63. 0063apply mul_assoc
  64. 0064exists x1 + x * x2
  65. 0065rewrite hnorm
  66. 0066exact hfinal