PA008E

prime_mul_index_map_injective

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

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

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

Structural proof guide

Generated structural guide

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

Use the direct prerequisites beta_at_unique, succ_le_succ, mod_eq_symm, mod_eq_trans, prime_mod_cancel, mod_eq_bounded_unique, succ_injective as previously established PA formulas.

The proof proceeds by case analysis (6), intermediate claims (10), equality transport (4).

Referenced ingredients

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

Proof neighborhood

Direct dependencies

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 dependents

PA008I prime_mul_residue_reindex_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  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 : 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 : 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 : 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 : 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 : 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 : 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 : 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