PA009C · theorem

prime_scaled_inverse_unique

Alpha v34 checked-use theorem · independently closed; not Stable

The bounded scaled inverse of a prime unit is unique.

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. ∀ x. ∀ y. ∀ z. Prime(p) → ScaledInverse(p,a,x,y) → ScaledInverse(p,a,x,z) → y = z

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

PD0004 Prime PD0033 ScaledInverse

3 occurrences

In local proof propositions

PD0001 Le PD0003 Dvd PD0008 ModEq

5 occurrences

Exact expanded native-PA statement
forall p a x y z. ((~(p = 1) /\ forall esi_prime_left_unique_prime esi_prime_right_unique_prime. p = esi_prime_left_unique_prime * esi_prime_right_unique_prime -> esi_prime_left_unique_prime = 1 \/ esi_prime_right_unique_prime = 1)) -> ((((~(x = 0) /\ (exists esi_strict_gap_unique_left_left_bound. esi_strict_gap_unique_left_left_bound + S x = p))) /\ (((~(y = 0) /\ (exists esi_strict_gap_unique_left_right_bound. esi_strict_gap_unique_left_right_bound + S y = p))) /\ (exists esi_mod_left_unique_left_mod esi_mod_right_unique_left_mod. (x * y) + p * esi_mod_left_unique_left_mod = (a) + p * esi_mod_right_unique_left_mod)))) -> ((((~(x = 0) /\ (exists esi_strict_gap_unique_right_left_bound. esi_strict_gap_unique_right_left_bound + S x = p))) /\ (((~(z = 0) /\ (exists esi_strict_gap_unique_right_right_bound. esi_strict_gap_unique_right_right_bound + S z = p))) /\ (exists esi_mod_left_unique_right_mod esi_mod_right_unique_right_mod. (x * z) + p * esi_mod_left_unique_right_mod = (a) + p * esi_mod_right_unique_right_mod)))) -> y = z

Proof neighborhood

Direct theorem prerequisites

PA0039 divisor_le_nonzero PA003A lt_not_le PA003L mod_eq_symm PA0024 mod_eq_trans PA003S prime_mod_cancel PA002U mod_eq_bounded_unique

Direct theorem dependents

PA009D scaled_inverse_prefix_extensional

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

59 script commands · 9 reading checkpoints · 5 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 (6)
divisor le nonzerolt not lemod eq symmmod eq transprime mod cancelmod eq bounded unique
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro z
  6. L6
    intro hp
  7. L7
    intro hxy
  8. L8
    intro hxz
02Separate the logical casesL9–16

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

  1. L9
    cases hxy
  2. L10
    cases hxy_left
  3. L11
    cases hxy_right
  4. L12
    cases hxy_right_left
  5. L13
    cases hxz
  6. L14
    cases hxz_left
  7. L15
    cases hxz_right
  8. L16
    cases hxz_right_left
03Establish hnotdivL17–18

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

  1. L17
    have hnotdiv : ¬Dvd(p,x)Definitions: Dvd(p,x)Original native command in the exact edition
  2. L18
    intro hdiv
04Establish hpxL19–28

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

  1. L19
  2. L20
    specialize divisor_le_nonzero p
  3. L21
    specialize divisor_le_nonzero x
  4. L22
    apply divisor_le_nonzero
  5. L23
    exact hxy_left_left
  6. L24
    exact hdiv
  7. L25
    specialize lt_not_le x
  8. L26
    specialize lt_not_le p
  9. L27
    apply lt_not_le
  10. L28
    exact hxy_left_right
05Use earlier factsL29–29

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

  1. L29
    exact hpx
06Establish hreverseL30–35

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

  1. L30
    have hreverse : ModEq(p,a,x · z)Definitions: ModEq(p,a,x · z)Original native command in the exact edition
  2. L31
    specialize mod_eq_symm p
  3. L32
    specialize mod_eq_symm (x * z)
  4. L33
    specialize mod_eq_symm a
  5. L34
    apply mod_eq_symm
  6. L35
    exact hxz_right_right
07Establish hproductsL36–43

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

  1. L36
    have hproducts : ModEq(p,x · y,x · z)Definitions: ModEq(p,x · y,x · z)Original native command in the exact edition
  2. L37
    specialize mod_eq_trans p
  3. L38
    specialize mod_eq_trans (x * y)
  4. L39
    specialize mod_eq_trans a
  5. L40
    specialize mod_eq_trans (x * z)
  6. L41
    apply mod_eq_trans
  7. L42
    exact hxy_right_right
  8. L43
    exact hreverse
08Establish hyzL44–53

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

  1. L44
  2. L45
    specialize prime_mod_cancel p
  3. L46
    specialize prime_mod_cancel x
  4. L47
    specialize prime_mod_cancel y
  5. L48
    specialize prime_mod_cancel z
  6. L49
    apply prime_mod_cancel
  7. L50
    exact hp
  8. L51
    exact hnotdiv
  9. L52
    exact hproducts
  10. L53
    specialize mod_eq_bounded_unique p
09Use earlier factsL54–59

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

  1. L54
    specialize mod_eq_bounded_unique y
  2. L55
    specialize mod_eq_bounded_unique z
  3. L56
    apply mod_eq_bounded_unique
  4. L57
    exact hxy_right_left_right
  5. L58
    exact hxz_right_left_right
  6. L59
    exact hyz

Library-wide reading audit

Original defined command ledger · 59 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro y
  5. 0005intro z
  6. 0006intro hp
  7. 0007intro hxy
  8. 0008intro hxz
  9. 0009cases hxy
  10. 0010cases hxy_left
  11. 0011cases hxy_right
  12. 0012cases hxy_right_left
  13. 0013cases hxz
  14. 0014cases hxz_left
  15. 0015cases hxz_right
  16. 0016cases hxz_right_left
  17. 0017have hnotdiv : ¬Dvd(p,x)
    Exact native replay linehave hnotdiv : ~(exists k. x = p * k)
  18. 0018intro hdiv
  19. 0019have hpx : Le(p,x)
    Exact native replay linehave hpx : exists t. t + p = x
  20. 0020specialize divisor_le_nonzero p
  21. 0021specialize divisor_le_nonzero x
  22. 0022apply divisor_le_nonzero
  23. 0023exact hxy_left_left
  24. 0024exact hdiv
  25. 0025specialize lt_not_le x
  26. 0026specialize lt_not_le p
  27. 0027apply lt_not_le
  28. 0028exact hxy_left_right
  29. 0029exact hpx
  30. 0030have hreverse : ModEq(p,a,x · z)
    Exact native replay linehave hreverse : exists esi_mod_left_unique_reverse esi_mod_right_unique_reverse. (a) + p * esi_mod_left_unique_reverse = (x * z) + p * esi_mod_right_unique_reverse
  31. 0031specialize mod_eq_symm p
  32. 0032specialize mod_eq_symm (x * z)
  33. 0033specialize mod_eq_symm a
  34. 0034apply mod_eq_symm
  35. 0035exact hxz_right_right
  36. 0036have hproducts : ModEq(p,x · y,x · z)
    Exact native replay linehave hproducts : exists esi_mod_left_unique_products esi_mod_right_unique_products. (x * y) + p * esi_mod_left_unique_products = (x * z) + p * esi_mod_right_unique_products
  37. 0037specialize mod_eq_trans p
  38. 0038specialize mod_eq_trans (x * y)
  39. 0039specialize mod_eq_trans a
  40. 0040specialize mod_eq_trans (x * z)
  41. 0041apply mod_eq_trans
  42. 0042exact hxy_right_right
  43. 0043exact hreverse
  44. 0044have hyz : ModEq(p,y,z)
    Exact native replay linehave hyz : exists esi_mod_left_unique_residues esi_mod_right_unique_residues. (y) + p * esi_mod_left_unique_residues = (z) + p * esi_mod_right_unique_residues
  45. 0045specialize prime_mod_cancel p
  46. 0046specialize prime_mod_cancel x
  47. 0047specialize prime_mod_cancel y
  48. 0048specialize prime_mod_cancel z
  49. 0049apply prime_mod_cancel
  50. 0050exact hp
  51. 0051exact hnotdiv
  52. 0052exact hproducts
  53. 0053specialize mod_eq_bounded_unique p
  54. 0054specialize mod_eq_bounded_unique y
  55. 0055specialize mod_eq_bounded_unique z
  56. 0056apply mod_eq_bounded_unique
  57. 0057exact hxy_right_left_right
  58. 0058exact hxz_right_left_right
  59. 0059exact hyz