PA008Q

prime_scaled_inverse_exists

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

Every bounded nonzero prime residue has a bounded scaled inverse.

Exact expanded PA statement

forall p a x. ((~(p = 1) /\ forall esi_prime_left_exists_prime esi_prime_right_exists_prime. p = esi_prime_left_exists_prime * esi_prime_right_exists_prime -> esi_prime_left_exists_prime = 1 \/ esi_prime_right_exists_prime = 1)) -> ~(a = 0) -> (exists esi_strict_gap_exists_target_bound. esi_strict_gap_exists_target_bound + S a = p) -> ~(x = 0) -> (exists esi_strict_gap_exists_input_bound. esi_strict_gap_exists_input_bound + S x = p) -> exists y. ((((~(x = 0) /\ (exists esi_strict_gap_exists_result_left_bound. esi_strict_gap_exists_result_left_bound + S x = p))) /\ (((~(y = 0) /\ (exists esi_strict_gap_exists_result_right_bound. esi_strict_gap_exists_result_right_bound + S y = p))) /\ (exists esi_mod_left_exists_result_mod esi_mod_right_exists_result_mod. (x * y) + p * esi_mod_left_exists_result_mod = (a) + p * esi_mod_right_exists_result_mod))))

Structural proof guide

Generated structural guide

Every bounded nonzero prime residue has a bounded scaled inverse.

Use the direct prerequisites prime_bounded_nonzero_mod_inverse, scaled_inverse_from_unit_inverse, prime_nonzero, division_remainder_exists, mul_comm, remainder_decomposition_to_mod_eq, scaled_inverse_transport_right, prime_scaled_inverse_target_nonzero as previously established PA formulas.

The proof proceeds by case analysis (6), intermediate claims (8).

Referenced ingredients

PA0063 prime_bounded_nonzero_mod_inverse PA008N scaled_inverse_from_unit_inverse PA0031 prime_nonzero PA001D division_remainder_exists PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA008O scaled_inverse_transport_right PA008P prime_scaled_inverse_target_nonzero

Proof neighborhood

Direct dependencies

PA0063 prime_bounded_nonzero_mod_inverse PA008N scaled_inverse_from_unit_inverse PA0031 prime_nonzero PA001D division_remainder_exists PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA008O scaled_inverse_transport_right PA008P prime_scaled_inverse_target_nonzero

Direct dependents

PA008R prime_scaled_inverse_prefix_extend

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 a
  3. 0003intro x
  4. 0004intro hp
  5. 0005intro ha0
  6. 0006intro hap
  7. 0007intro hx0
  8. 0008intro hxp
  9. 0009have hinv : exists x1. (~(x1 = 0) /\ ((exists esi_strict_gap_exists_inverse_bound. esi_strict_gap_exists_inverse_bound + S x1 = p) /\ (exists esi_mod_left_exists_inverse_mod esi_mod_right_exists_inverse_mod. (x * x1) + p * esi_mod_left_exists_inverse_mod = (1) + p * esi_mod_right_exists_inverse_mod)))
  10. 0010specialize prime_bounded_nonzero_mod_inverse p
  11. 0011specialize prime_bounded_nonzero_mod_inverse x
  12. 0012apply prime_bounded_nonzero_mod_inverse
  13. 0013exact hp
  14. 0014exact hx0
  15. 0015exact hxp
  16. 0016cases hinv
  17. 0017cases hinv_witness
  18. 0018cases hinv_witness_right
  19. 0019have hraw : exists esi_mod_left_exists_raw esi_mod_right_exists_raw. (x * (a * x1)) + p * esi_mod_left_exists_raw = (a) + p * esi_mod_right_exists_raw
  20. 0020specialize scaled_inverse_from_unit_inverse p
  21. 0021specialize scaled_inverse_from_unit_inverse a
  22. 0022specialize scaled_inverse_from_unit_inverse x
  23. 0023specialize scaled_inverse_from_unit_inverse x1
  24. 0024apply scaled_inverse_from_unit_inverse
  25. 0025exact hinv_witness_right_right
  26. 0026have hp0 : ~(p = 0)
  27. 0027intro hpzero
  28. 0028specialize prime_nonzero p
  29. 0029apply prime_nonzero
  30. 0030exact hp
  31. 0031exact hpzero
  32. 0032have hdiv : exists q r. a * x1 = p * q + r /\ exists h. h + S r = p
  33. 0033specialize division_remainder_exists p
  34. 0034specialize division_remainder_exists (a * x1)
  35. 0035apply division_remainder_exists
  36. 0036exact hp0
  37. 0037cases hdiv
  38. 0038cases hdiv_witness
  39. 0039cases hdiv_witness_witness
  40. 0040have hdecomp : a * x1 = x2 * p + x3
  41. 0041trans p * x2 + x3
  42. 0042exact hdiv_witness_witness_left
  43. 0043congr
  44. 0044apply mul_comm
  45. 0045refl
  46. 0046have hreduced : exists esi_mod_left_exists_reduced esi_mod_right_exists_reduced. (a * x1) + p * esi_mod_left_exists_reduced = (x3) + p * esi_mod_right_exists_reduced
  47. 0047specialize remainder_decomposition_to_mod_eq p
  48. 0048specialize remainder_decomposition_to_mod_eq (a * x1)
  49. 0049specialize remainder_decomposition_to_mod_eq x2
  50. 0050specialize remainder_decomposition_to_mod_eq x3
  51. 0051apply remainder_decomposition_to_mod_eq
  52. 0052exact hdecomp
  53. 0053have hfinal : exists esi_mod_left_exists_final esi_mod_right_exists_final. (x * x3) + p * esi_mod_left_exists_final = (a) + p * esi_mod_right_exists_final
  54. 0054specialize scaled_inverse_transport_right p
  55. 0055specialize scaled_inverse_transport_right a
  56. 0056specialize scaled_inverse_transport_right x
  57. 0057specialize scaled_inverse_transport_right (a * x1)
  58. 0058specialize scaled_inverse_transport_right x3
  59. 0059apply scaled_inverse_transport_right
  60. 0060exact hraw
  61. 0061exact hreduced
  62. 0062have hy0 : ~(x3 = 0)
  63. 0063specialize prime_scaled_inverse_target_nonzero p
  64. 0064specialize prime_scaled_inverse_target_nonzero a
  65. 0065specialize prime_scaled_inverse_target_nonzero x
  66. 0066specialize prime_scaled_inverse_target_nonzero x3
  67. 0067intro hx3zero
  68. 0068apply prime_scaled_inverse_target_nonzero
  69. 0069exact hp
  70. 0070exact ha0
  71. 0071exact hap
  72. 0072exact hfinal
  73. 0073exact hx3zero
  74. 0074exists x3
  75. 0075split
  76. 0076split
  77. 0077exact hx0
  78. 0078exact hxp
  79. 0079split
  80. 0080split
  81. 0081exact hy0
  82. 0082exact hdiv_witness_witness_right
  83. 0083exact hfinal