PA008E · theorem

prime_mul_index_map_injective

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

Multiplication by a nonzero prime residue is injective on 0,...,p-2.

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. ∀ n. ∀ a. ∀ r. ∀ s. p = S n → Prime(p) → ¬Dvd(p,a) → (∀ x. Lt(x,n) → ∃ y. Lt(y,n) ∧ (BetaAt(r,s,x,y) ∧ ModEq(p,a · S x,S y))) → InjectivePrefix(r,s,n)

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

PD0002 Lt PD0003 Dvd PD0004 Prime PD0008 ModEq PD0013 BetaAt PD0025 InjectivePrefix

7 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq PD0013 BetaAt

11 occurrences

Exact expanded native-PA statement
forall p n a r s. p = S n -> ((~(p = 1) /\ forall frm_prime_left_injective_prime frm_prime_right_injective_prime. p = frm_prime_left_injective_prime * frm_prime_right_injective_prime -> frm_prime_left_injective_prime = 1 \/ frm_prime_right_injective_prime = 1)) -> (~(exists frm_factor_injective_multiplier. a = p * frm_factor_injective_multiplier)) -> (forall frm_index_injective_map. (exists frm_gap_injective_map_index_bound. frm_gap_injective_map_index_bound + S frm_index_injective_map = n) -> (exists frm_residue_injective_map_result. (exists frm_gap_injective_map_result_residue_bound. frm_gap_injective_map_result_residue_bound + S frm_residue_injective_map_result = n) /\ ((((exists ff_h_frm_injective_map_result_decoded. ff_h_frm_injective_map_result_decoded + S (frm_residue_injective_map_result) = S ((S (frm_index_injective_map)) * s)) /\ exists ff_q_frm_injective_map_result_decoded. r = ff_q_frm_injective_map_result_decoded * S ((S (frm_index_injective_map)) * s) + (frm_residue_injective_map_result))) /\ (exists frm_mod_left_injective_map_result_congruence frm_mod_right_injective_map_result_congruence. a * S frm_index_injective_map + p * frm_mod_left_injective_map_result_congruence = S frm_residue_injective_map_result + p * frm_mod_right_injective_map_result_congruence)))) -> (forall fp_i_injective_result fp_j_injective_result fp_value_injective_result. (exists fp_gap_injective_result_i. fp_gap_injective_result_i + S fp_i_injective_result = n) -> (exists fp_gap_injective_result_j. fp_gap_injective_result_j + S fp_j_injective_result = n) -> (((exists ff_h_injective_result_left. ff_h_injective_result_left + S (fp_value_injective_result) = S ((S (fp_i_injective_result)) * s)) /\ exists ff_q_injective_result_left. r = ff_q_injective_result_left * S ((S (fp_i_injective_result)) * s) + (fp_value_injective_result))) -> (((exists ff_h_injective_result_right. ff_h_injective_result_right + S (fp_value_injective_result) = S ((S (fp_j_injective_result)) * s)) /\ exists ff_q_injective_result_right. r = ff_q_injective_result_right * S ((S (fp_j_injective_result)) * s) + (fp_value_injective_result))) -> fp_i_injective_result = fp_j_injective_result)

Proof neighborhood

Direct theorem prerequisites

PA002F beta_at_unique PA002K succ_le_succ PA003L mod_eq_symm PA0024 mod_eq_trans PA003S prime_mod_cancel PA002U mod_eq_bounded_unique PA003V succ_injective

Direct theorem dependents

PA008I prime_mul_residue_reindex_exists

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

97 script commands · 16 reading checkpoints · 10 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 (7)
beta at uniquesucc le succmod eq symmmod eq transprime mod cancelmod eq bounded uniquesucc injective
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro a
  4. L4
    intro r
  5. L5
    intro s
  6. L6
    intro hpn
  7. L7
    intro hp
  8. L8
    intro hnotdiv
  9. L9
    intro hmap
  10. L10
    intro i
02Fix variables and assumptionsL11–16

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

  1. L11
    intro k
  2. L12
    intro value
  3. L13
    intro hi
  4. L14
    intro hk
  5. L15
    intro hri
  6. L16
    intro hrk
03Establish hmiL17–20

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

  1. L17
    have hmi : ∃ frm_residue_injective_i. Lt(frm_residue_injective_i,n) ∧ (BetaAt(r,s,i,frm_residue_injective_i) ∧ ModEq(p,a · S i,S frm_residue_injective_i))Definitions: Lt(frm_residue_injective_i,n)BetaAt(r,s,i,frm_residue_injective_i)ModEq(p,a · S i,S frm_residue_injective_i)Original native command in the exact edition
  2. L18
    specialize hmap i
  3. L19
    apply hmap
  4. L20
    exact hi
04Separate the logical casesL21–23

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

  1. L21
    cases hmi
  2. L22
    cases hmi_witness
  3. L23
    cases hmi_witness_right
05Establish hmkL24–27

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

  1. L24
    have hmk : ∃ frm_residue_injective_k. Lt(frm_residue_injective_k,n) ∧ (BetaAt(r,s,k,frm_residue_injective_k) ∧ ModEq(p,a · S k,S frm_residue_injective_k))Definitions: Lt(frm_residue_injective_k,n)BetaAt(r,s,k,frm_residue_injective_k)ModEq(p,a · S k,S frm_residue_injective_k)Original native command in the exact edition
  2. L25
    specialize hmap k
  3. L26
    apply hmap
  4. L27
    exact hk
06Separate the logical casesL28–30

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

  1. L28
    cases hmk
  2. L29
    cases hmk_witness
  3. L30
    cases hmk_witness_right
07Establish hvalue_iL31–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L31
    have hvalue_i : value = x
  2. L32
    specialize beta_at_unique r
  3. L33
    specialize beta_at_unique s
  4. L34
    specialize beta_at_unique i
  5. L35
    specialize beta_at_unique value
  6. L36
    specialize beta_at_unique x
  7. L37
    apply beta_at_unique
  8. L38
    exact hri
  9. L39
    exact hmi_witness_right_left
08Establish hvalue_kL40–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L40
    have hvalue_k : value = x1
  2. L41
    specialize beta_at_unique r
  3. L42
    specialize beta_at_unique s
  4. L43
    specialize beta_at_unique k
  5. L44
    specialize beta_at_unique value
  6. L45
    specialize beta_at_unique x1
  7. L46
    apply beta_at_unique
  8. L47
    exact hrk
  9. L48
    exact hmk_witness_right_left
  10. L49
    rewrite <- hvalue_i at hmi_witness_right_right
09Calculate and transport equalitiesL50–50

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

  1. L50
    rewrite <- hvalue_k at hmk_witness_right_right
10Establish hreverseL51–56

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

  1. L51
    have hreverse : ModEq(p,S value,a · S k)Definitions: ModEq(p,S value,a · S k)Original native command in the exact edition
  2. L52
    specialize mod_eq_symm p
  3. L53
    specialize mod_eq_symm (a * S k)
  4. L54
    specialize mod_eq_symm (S value)
  5. L55
    apply mod_eq_symm
  6. L56
    exact hmk_witness_right_right
11Establish hscaledL57–64

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

  1. L57
    have hscaled : ModEq(p,a · S i,a · S k)Definitions: ModEq(p,a · S i,a · S k)Original native command in the exact edition
  2. L58
    specialize mod_eq_trans p
  3. L59
    specialize mod_eq_trans (a * S i)
  4. L60
    specialize mod_eq_trans (S value)
  5. L61
    specialize mod_eq_trans (a * S k)
  6. L62
    apply mod_eq_trans
  7. L63
    exact hmi_witness_right_right
  8. L64
    exact hreverse
12Establish hcancelL65–73

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

  1. L65
    have hcancel : ModEq(p,S i,S k)Definitions: ModEq(p,S i,S k)Original native command in the exact edition
  2. L66
    specialize prime_mod_cancel p
  3. L67
    specialize prime_mod_cancel a
  4. L68
    specialize prime_mod_cancel (S i)
  5. L69
    specialize prime_mod_cancel (S k)
  6. L70
    apply prime_mod_cancel
  7. L71
    exact hp
  8. L72
    exact hnotdiv
  9. L73
    exact hscaled
13Establish hiboundL74–79

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

  1. L74
    have hibound : Lt(S i,p)Definitions: Lt(S i,p)Original native command in the exact edition
  2. L75
    rewrite hpn
  3. L76
    specialize succ_le_succ (S i)
  4. L77
    specialize succ_le_succ n
  5. L78
    apply succ_le_succ
  6. L79
    exact hi
14Establish hkboundL80–85

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

  1. L80
    have hkbound : Lt(S k,p)Definitions: Lt(S k,p)Original native command in the exact edition
  2. L81
    rewrite hpn
  3. L82
    specialize succ_le_succ (S k)
  4. L83
    specialize succ_le_succ n
  5. L84
    apply succ_le_succ
  6. L85
    exact hk
15Establish hsuccL86–95

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

  1. L86
    have hsucc : S i = S k
  2. L87
    specialize mod_eq_bounded_unique p
  3. L88
    specialize mod_eq_bounded_unique (S i)
  4. L89
    specialize mod_eq_bounded_unique (S k)
  5. L90
    apply mod_eq_bounded_unique
  6. L91
    exact hibound
  7. L92
    exact hkbound
  8. L93
    exact hcancel
  9. L94
    specialize succ_injective i
  10. L95
    specialize succ_injective k
16Use earlier factsL96–97

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

  1. L96
    apply succ_injective
  2. L97
    exact hsucc

Library-wide reading audit

Original defined command ledger · 97 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro a
  4. 0004intro r
  5. 0005intro s
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro hnotdiv
  9. 0009intro hmap
  10. 0010intro i
  11. 0011intro k
  12. 0012intro value
  13. 0013intro hi
  14. 0014intro hk
  15. 0015intro hri
  16. 0016intro hrk
  17. 0017have hmi : ∃ frm_residue_injective_i. Lt(frm_residue_injective_i,n) ∧ (BetaAt(r,s,i,frm_residue_injective_i) ∧ ModEq(p,a · S i,S frm_residue_injective_i))
    Exact native replay linehave hmi : exists frm_residue_injective_i. (exists frm_gap_injective_i_residue_bound. frm_gap_injective_i_residue_bound + S frm_residue_injective_i = n) /\ ((((exists ff_h_frm_injective_i_decoded. ff_h_frm_injective_i_decoded + S (frm_residue_injective_i) = S ((S (i)) * s)) /\ exists ff_q_frm_injective_i_decoded. r = ff_q_frm_injective_i_decoded * S ((S (i)) * s) + (frm_residue_injective_i))) /\ (exists frm_mod_left_injective_i_congruence frm_mod_right_injective_i_congruence. a * S i + p * frm_mod_left_injective_i_congruence = S frm_residue_injective_i + p * frm_mod_right_injective_i_congruence))
  18. 0018specialize hmap i
  19. 0019apply hmap
  20. 0020exact hi
  21. 0021cases hmi
  22. 0022cases hmi_witness
  23. 0023cases hmi_witness_right
  24. 0024have hmk : ∃ frm_residue_injective_k. Lt(frm_residue_injective_k,n) ∧ (BetaAt(r,s,k,frm_residue_injective_k) ∧ ModEq(p,a · S k,S frm_residue_injective_k))
    Exact native replay linehave hmk : exists frm_residue_injective_k. (exists frm_gap_injective_k_residue_bound. frm_gap_injective_k_residue_bound + S frm_residue_injective_k = n) /\ ((((exists ff_h_frm_injective_k_decoded. ff_h_frm_injective_k_decoded + S (frm_residue_injective_k) = S ((S (k)) * s)) /\ exists ff_q_frm_injective_k_decoded. r = ff_q_frm_injective_k_decoded * S ((S (k)) * s) + (frm_residue_injective_k))) /\ (exists frm_mod_left_injective_k_congruence frm_mod_right_injective_k_congruence. a * S k + p * frm_mod_left_injective_k_congruence = S frm_residue_injective_k + p * frm_mod_right_injective_k_congruence))
  25. 0025specialize hmap k
  26. 0026apply hmap
  27. 0027exact hk
  28. 0028cases hmk
  29. 0029cases hmk_witness
  30. 0030cases hmk_witness_right
  31. 0031have hvalue_i : value = x
  32. 0032specialize beta_at_unique r
  33. 0033specialize beta_at_unique s
  34. 0034specialize beta_at_unique i
  35. 0035specialize beta_at_unique value
  36. 0036specialize beta_at_unique x
  37. 0037apply beta_at_unique
  38. 0038exact hri
  39. 0039exact hmi_witness_right_left
  40. 0040have hvalue_k : value = x1
  41. 0041specialize beta_at_unique r
  42. 0042specialize beta_at_unique s
  43. 0043specialize beta_at_unique k
  44. 0044specialize beta_at_unique value
  45. 0045specialize beta_at_unique x1
  46. 0046apply beta_at_unique
  47. 0047exact hrk
  48. 0048exact hmk_witness_right_left
  49. 0049rewrite <- hvalue_i at hmi_witness_right_right
  50. 0050rewrite <- hvalue_k at hmk_witness_right_right
  51. 0051have hreverse : ModEq(p,S value,a · S k)
    Exact native replay linehave hreverse : exists frr_reverse_left_injective_reverse frr_reverse_right_injective_reverse. S value + p * frr_reverse_left_injective_reverse = a * S k + p * frr_reverse_right_injective_reverse
  52. 0052specialize mod_eq_symm p
  53. 0053specialize mod_eq_symm (a * S k)
  54. 0054specialize mod_eq_symm (S value)
  55. 0055apply mod_eq_symm
  56. 0056exact hmk_witness_right_right
  57. 0057have hscaled : ModEq(p,a · S i,a · S k)
    Exact native replay linehave hscaled : exists frr_scaled_left_injective_scaled frr_scaled_right_injective_scaled. a * S i + p * frr_scaled_left_injective_scaled = a * S k + p * frr_scaled_right_injective_scaled
  58. 0058specialize mod_eq_trans p
  59. 0059specialize mod_eq_trans (a * S i)
  60. 0060specialize mod_eq_trans (S value)
  61. 0061specialize mod_eq_trans (a * S k)
  62. 0062apply mod_eq_trans
  63. 0063exact hmi_witness_right_right
  64. 0064exact hreverse
  65. 0065have hcancel : ModEq(p,S i,S k)
    Exact native replay linehave hcancel : exists frr_cancel_left_injective_canceled frr_cancel_right_injective_canceled. S i + p * frr_cancel_left_injective_canceled = S k + p * frr_cancel_right_injective_canceled
  66. 0066specialize prime_mod_cancel p
  67. 0067specialize prime_mod_cancel a
  68. 0068specialize prime_mod_cancel (S i)
  69. 0069specialize prime_mod_cancel (S k)
  70. 0070apply prime_mod_cancel
  71. 0071exact hp
  72. 0072exact hnotdiv
  73. 0073exact hscaled
  74. 0074have hibound : Lt(S i,p)
    Exact native replay linehave hibound : exists frr_successor_bound_injective_i_bound. frr_successor_bound_injective_i_bound + S (S i) = p
  75. 0075rewrite hpn
  76. 0076specialize succ_le_succ (S i)
  77. 0077specialize succ_le_succ n
  78. 0078apply succ_le_succ
  79. 0079exact hi
  80. 0080have hkbound : Lt(S k,p)
    Exact native replay linehave hkbound : exists frr_successor_bound_injective_k_bound. frr_successor_bound_injective_k_bound + S (S k) = p
  81. 0081rewrite hpn
  82. 0082specialize succ_le_succ (S k)
  83. 0083specialize succ_le_succ n
  84. 0084apply succ_le_succ
  85. 0085exact hk
  86. 0086have hsucc : S i = S k
  87. 0087specialize mod_eq_bounded_unique p
  88. 0088specialize mod_eq_bounded_unique (S i)
  89. 0089specialize mod_eq_bounded_unique (S k)
  90. 0090apply mod_eq_bounded_unique
  91. 0091exact hibound
  92. 0092exact hkbound
  93. 0093exact hcancel
  94. 0094specialize succ_injective i
  95. 0095specialize succ_injective k
  96. 0096apply succ_injective
  97. 0097exact hsucc