PA0063

prime_bounded_nonzero_mod_inverse

Stable checked-use theorem · independently closed

A nonzero residue below a prime has a nonzero bounded inverse.

Exact expanded PA statement

forall p a. ((~(p = 1) /\ forall qrbu_factor_left_prime_p qrbu_factor_right_prime_p. p = qrbu_factor_left_prime_p * qrbu_factor_right_prime_p -> qrbu_factor_left_prime_p = 1 \/ qrbu_factor_right_prime_p = 1)) -> ~(a = 0) -> (exists qrbu_gap_a_lt_p. qrbu_gap_a_lt_p + S a = p) -> (exists qrbu_inverse_bounded_inverse. (~(qrbu_inverse_bounded_inverse = 0) /\ ((exists qrbu_gap_bounded_inverse_bound. qrbu_gap_bounded_inverse_bound + S qrbu_inverse_bounded_inverse = p) /\ (exists qrbu_mod_left_bounded_inverse_mod qrbu_mod_right_bounded_inverse_mod. a * qrbu_inverse_bounded_inverse + p * qrbu_mod_left_bounded_inverse_mod = 1 + p * qrbu_mod_right_bounded_inverse_mod))))

Structural proof guide

Generated structural guide

A nonzero residue below a prime has a nonzero bounded inverse.

Use the direct prerequisites prime_is_succ_succ, prime_nonzero, divisor_le_nonzero, lt_not_le, prime_mod_inverse, division_remainder_exists, mul_comm, remainder_decomposition_to_mod_eq, mod_eq_mul_left, mod_eq_symm, mod_eq_trans, mod_eq_bounded_unique, succ_ne_zero as previously established PA formulas.

The proof proceeds by case analysis (9), intermediate claims (16), equality transport (2), certified simplification (2).

Referenced ingredients

PA0061 prime_is_succ_succ PA0031 prime_nonzero PA0039 divisor_le_nonzero PA003A lt_not_le PA0062 prime_mod_inverse PA001D division_remainder_exists PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA0020 mod_eq_mul_left PA003L mod_eq_symm PA0024 mod_eq_trans PA002U mod_eq_bounded_unique PA0005 succ_ne_zero

Proof neighborhood

Direct dependencies

PA0061 prime_is_succ_succ PA0031 prime_nonzero PA0039 divisor_le_nonzero PA003A lt_not_le PA0062 prime_mod_inverse PA001D division_remainder_exists PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA0020 mod_eq_mul_left PA003L mod_eq_symm PA0024 mod_eq_trans PA002U mod_eq_bounded_unique PA0005 succ_ne_zero

Direct dependents

PA008Q prime_scaled_inverse_exists PA00A4 prime_inverse_index_exists

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro a
  3. 0003intro hp
  4. 0004intro ha0
  5. 0005intro hap
  6. 0006have hp0 : ~(p = 0)
  7. 0007intro hpzero
  8. 0008specialize prime_nonzero p
  9. 0009apply prime_nonzero
  10. 0010exact hp
  11. 0011exact hpzero
  12. 0012have hnotdiv : ~(exists k. a = p * k)
  13. 0013intro hdiv
  14. 0014have hpa : exists t. t + p = a
  15. 0015specialize divisor_le_nonzero p
  16. 0016specialize divisor_le_nonzero a
  17. 0017apply divisor_le_nonzero
  18. 0018exact ha0
  19. 0019exact hdiv
  20. 0020specialize lt_not_le a
  21. 0021specialize lt_not_le p
  22. 0022apply lt_not_le
  23. 0023exact hap
  24. 0024exact hpa
  25. 0025have hinv : exists z u v. a * z + p * u = 1 + p * v
  26. 0026specialize prime_mod_inverse p
  27. 0027specialize prime_mod_inverse a
  28. 0028apply prime_mod_inverse
  29. 0029exact hp
  30. 0030exact hnotdiv
  31. 0031cases hinv
  32. 0032cases hinv_witness
  33. 0033cases hinv_witness_witness
  34. 0034have hdivz : exists q r. x = p * q + r /\ exists h. h + S r = p
  35. 0035specialize division_remainder_exists p
  36. 0036specialize division_remainder_exists x
  37. 0037apply division_remainder_exists
  38. 0038exact hp0
  39. 0039cases hdivz
  40. 0040cases hdivz_witness
  41. 0041cases hdivz_witness_witness
  42. 0042have hzdecomp : x = x3 * p + x4
  43. 0043trans p * x3 + x4
  44. 0044exact hdivz_witness_witness_left
  45. 0045congr
  46. 0046apply mul_comm
  47. 0047refl
  48. 0048have hzr : exists u v. x + p * u = x4 + p * v
  49. 0049specialize remainder_decomposition_to_mod_eq p
  50. 0050specialize remainder_decomposition_to_mod_eq x
  51. 0051specialize remainder_decomposition_to_mod_eq x3
  52. 0052specialize remainder_decomposition_to_mod_eq x4
  53. 0053apply remainder_decomposition_to_mod_eq
  54. 0054exact hzdecomp
  55. 0055have hscaled : exists u v. (a * x) + p * u = (a * x4) + p * v
  56. 0056specialize mod_eq_mul_left p
  57. 0057specialize mod_eq_mul_left x
  58. 0058specialize mod_eq_mul_left x4
  59. 0059specialize mod_eq_mul_left a
  60. 0060apply mod_eq_mul_left
  61. 0061exact hzr
  62. 0062have hrz : exists u v. (a * x4) + p * u = (a * x) + p * v
  63. 0063specialize mod_eq_symm p
  64. 0064specialize mod_eq_symm (a * x)
  65. 0065specialize mod_eq_symm (a * x4)
  66. 0066apply mod_eq_symm
  67. 0067exact hscaled
  68. 0068have hfinal : exists u v. (a * x4) + p * u = 1 + p * v
  69. 0069specialize mod_eq_trans p
  70. 0070specialize mod_eq_trans (a * x4)
  71. 0071specialize mod_eq_trans (a * x)
  72. 0072specialize mod_eq_trans 1
  73. 0073apply mod_eq_trans
  74. 0074exact hrz
  75. 0075exists x1
  76. 0076exists x2
  77. 0077exact hinv_witness_witness_witness
  78. 0078have hp2 : exists k. p = S (S k)
  79. 0079specialize prime_is_succ_succ p
  80. 0080apply prime_is_succ_succ
  81. 0081exact hp
  82. 0082cases hp2
  83. 0083have h0bound : exists h. h + S 0 = p
  84. 0084exists S x5
  85. 0085rewrite hp2_witness
  86. 0086simp
  87. 0087have h1bound : exists h. h + S 1 = p
  88. 0088exists x5
  89. 0089rewrite hp2_witness
  90. 0090simp
  91. 0091have hr0 : ~(x4 = 0)
  92. 0092intro hrzero
  93. 0093have hzeroone : exists u v. 0 + p * u = 1 + p * v
  94. 0094cases hfinal
  95. 0095cases hfinal_witness
  96. 0096exists x6
  97. 0097exists x7
  98. 0098trans (a * x4) + p * x6
  99. 0099congr
  100. 0100symm
  101. 0101trans a * 0
  102. 0102congr
  103. 0103refl
  104. 0104exact hrzero
  105. 0105apply PA5
  106. 0106refl
  107. 0107exact hfinal_witness_witness
  108. 0108have hzeroeqone : 0 = 1
  109. 0109specialize mod_eq_bounded_unique p
  110. 0110specialize mod_eq_bounded_unique 0
  111. 0111specialize mod_eq_bounded_unique 1
  112. 0112apply mod_eq_bounded_unique
  113. 0113exact h0bound
  114. 0114exact h1bound
  115. 0115exact hzeroone
  116. 0116specialize succ_ne_zero 0
  117. 0117apply succ_ne_zero
  118. 0118symm
  119. 0119exact hzeroeqone
  120. 0120exists x4
  121. 0121split
  122. 0122exact hr0
  123. 0123split
  124. 0124exact hdivz_witness_witness_right
  125. 0125exact hfinal