PA003Q · theorem

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.

Statement with defined notation

∀ a. ∀ m. ¬m = 0 → Coprime(a,m) → ∃ x. BalancedInverse(m,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

PD0005 Coprime PD0031 BalancedInverse

2 occurrences

In local proof propositions

PD0008 ModEq

6 occurrences

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

Proof neighborhood

Direct theorem prerequisites

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

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

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.

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 (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 : ∃ xp. ∃ xn. ModEq(m,a · xp,1 + a · xn)Definitions: ModEq(m,a · xp,1 + a · xn)Original native command in the exact edition
  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 : ModEq(m,x · (a · x2),x · (a · x2))Definitions: ModEq(m,x · (a · x2),x · (a · x2))Original native command in the exact edition
  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 : ModEq(m,a · x1 + x · (a · x2),1 + a · x2 + x · (a · x2))Definitions: ModEq(m,a · x1 + x · (a · x2),1 + a · x2 + x · (a · x2))Original native command in the exact edition
  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 : ModEq(m,1 + a · x2 + x · (a · x2),1)Definitions: ModEq(m,1 + a · x2 + x · (a · x2),1)Original native command in the exact edition
  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 : ModEq(S x,1 + a · x2 + x · (a · x2),1)Definitions: ModEq(S x,1 + a · x2 + x · (a · x2),1)Original native command in the exact edition
  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 : ModEq(m,a · x1 + x · (a · x2),1)Definitions: ModEq(m,a · x1 + x · (a · x2),1)Original native command in the exact edition
  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 defined 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 : ∃ xp. ∃ xn. ModEq(m,a · xp,1 + a · xn)
    Exact native replay linehave 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 : ModEq(m,x · (a · x2),x · (a · x2))
    Exact native replay linehave 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 : ModEq(m,a · x1 + x · (a · x2),1 + a · x2 + x · (a · x2))
    Exact native replay linehave 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 : ModEq(m,1 + a · x2 + x · (a · x2),1)
    Exact native replay linehave 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 : ModEq(S x,1 + a · x2 + x · (a · x2),1)
    Exact native replay linehave 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 : ModEq(m,a · x1 + x · (a · x2),1)
    Exact native replay linehave 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