PA00AG

prime_bounded_square_one_cases

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

A bounded square root of one modulo a prime is one or the prime predecessor.

Exact expanded PA statement

forall p n x. p = S n -> ((~(p = 1) /\ forall wsq_prime_left_prime wsq_prime_right_prime. p = wsq_prime_left_prime * wsq_prime_right_prime -> wsq_prime_left_prime = 1 \/ wsq_prime_right_prime = 1)) -> (exists wsq_positive_gap_positive. wsq_positive_gap_positive + 1 = x) -> (exists wsq_strict_gap_bounded. wsq_strict_gap_bounded + S x = p) -> (exists wsq_mod_left_square_one wsq_mod_right_square_one. x * x + p * wsq_mod_left_square_one = 1 + p * wsq_mod_right_square_one) -> x = 1 \/ x = n

Structural proof guide

Generated structural guide

A bounded square root of one modulo a prime is one or the prime predecessor.

Use the direct prerequisites ne_zero_of_one_le, nonzero_is_succ, mul_succ_left, add_assoc, add_comm, add_left_cancel, factor_difference, euclid_prime_dvd_product, le_succ_self, lt_of_le_of_lt, zero_or_succ, divisor_le_nonzero, lt_not_le, succ_ne_zero, le_antisymm, succ_injective as previously established PA formulas.

The proof proceeds by case analysis (7), intermediate claims (18), equality transport (6).

Referenced ingredients

PA003U ne_zero_of_one_le PA001V nonzero_is_succ PA000G mul_succ_left PA0009 add_assoc PA000F add_comm PA002B add_left_cancel PA0013 factor_difference PA0038 euclid_prime_dvd_product PA000Q le_succ_self PA0033 lt_of_le_of_lt PA0008 zero_or_succ PA0039 divisor_le_nonzero PA003A lt_not_le PA0005 succ_ne_zero PA0069 le_antisymm PA003V succ_injective

Proof neighborhood

Direct dependencies

PA003U ne_zero_of_one_le PA001V nonzero_is_succ PA000G mul_succ_left PA0009 add_assoc PA000F add_comm PA002B add_left_cancel PA0013 factor_difference PA0038 euclid_prime_dvd_product PA000Q le_succ_self PA0033 lt_of_le_of_lt PA0008 zero_or_succ PA0039 divisor_le_nonzero PA003A lt_not_le PA0005 succ_ne_zero PA0069 le_antisymm PA003V succ_injective

Direct dependents

PA00AH prime_inverse_prefix_fixed_cases

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 x
  4. 0004intro hpn
  5. 0005intro hp
  6. 0006intro hxpos
  7. 0007intro hxlt
  8. 0008intro hsquaremod
  9. 0009cases hp
  10. 0010have hprime : (~(p = 1) /\ forall wsq_prime_left_prime wsq_prime_right_prime. p = wsq_prime_left_prime * wsq_prime_right_prime -> wsq_prime_left_prime = 1 \/ wsq_prime_right_prime = 1)
  11. 0011split
  12. 0012exact hp_left
  13. 0013exact hp_right
  14. 0014have hx0 : ~(x = 0)
  15. 0015specialize ne_zero_of_one_le x
  16. 0016intro hxzero
  17. 0017apply ne_zero_of_one_le
  18. 0018exact hxpos
  19. 0019exact hxzero
  20. 0020have hxpred : exists t. x = S t
  21. 0021specialize nonzero_is_succ x
  22. 0022apply nonzero_is_succ
  23. 0023exact hx0
  24. 0024cases hxpred
  25. 0025have hsquare : x * x = 1 + x1 * S (S x1)
  26. 0026rewrite hxpred_witness
  27. 0027rewrite hxpred_witness
  28. 0028specialize mul_succ_left x1
  29. 0029specialize mul_succ_left (S x1)
  30. 0030trans x1 * S x1 + S x1
  31. 0031exact mul_succ_left
  32. 0032trans S (x1 * S x1 + x1)
  33. 0033apply PA4
  34. 0034trans (x1 * S x1 + x1) + 1
  35. 0035symm
  36. 0036trans S ((x1 * S x1 + x1) + 0)
  37. 0037apply PA4
  38. 0038congr
  39. 0039apply PA3
  40. 0040trans 1 + (x1 * S x1 + x1)
  41. 0041apply add_comm
  42. 0042congr
  43. 0043refl
  44. 0044symm
  45. 0045apply PA6
  46. 0046cases hsquaremod
  47. 0047cases hsquaremod_witness
  48. 0048have hcancel : x1 * S (S x1) + p * x2 = p * x3
  49. 0049specialize add_left_cancel 1
  50. 0050specialize add_left_cancel (x1 * S (S x1) + p * x2)
  51. 0051specialize add_left_cancel (p * x3)
  52. 0052apply add_left_cancel
  53. 0053trans (1 + x1 * S (S x1)) + p * x2
  54. 0054symm
  55. 0055apply add_assoc
  56. 0056trans x * x + p * x2
  57. 0057congr
  58. 0058symm
  59. 0059exact hsquare
  60. 0060refl
  61. 0061trans 1 + p * x3
  62. 0062exact hsquaremod_witness_witness
  63. 0063refl
  64. 0064have hfactor : p * x3 = p * x2 + x1 * S (S x1)
  65. 0065trans x1 * S (S x1) + p * x2
  66. 0066symm
  67. 0067exact hcancel
  68. 0068apply add_comm
  69. 0069have hproduct : exists w. x1 * S (S x1) = p * w
  70. 0070specialize factor_difference p
  71. 0071specialize factor_difference x3
  72. 0072specialize factor_difference x2
  73. 0073specialize factor_difference (x1 * S (S x1))
  74. 0074apply factor_difference
  75. 0075exact hfactor
  76. 0076have hsplit : (exists u. x1 = p * u) \/ exists v. S (S x1) = p * v
  77. 0077specialize euclid_prime_dvd_product p
  78. 0078specialize euclid_prime_dvd_product x1
  79. 0079specialize euclid_prime_dvd_product (S (S x1))
  80. 0080apply euclid_prime_dvd_product
  81. 0081exact hprime
  82. 0082exact hproduct
  83. 0083cases hsplit
  84. 0084have htx : exists k. k + x1 = x
  85. 0085rewrite hxpred_witness
  86. 0086specialize le_succ_self x1
  87. 0087exact le_succ_self
  88. 0088have htp : exists k. k + S x1 = p
  89. 0089specialize lt_of_le_of_lt x1
  90. 0090specialize lt_of_le_of_lt x
  91. 0091specialize lt_of_le_of_lt p
  92. 0092apply lt_of_le_of_lt
  93. 0093exact htx
  94. 0094exact hxlt
  95. 0095have htcase : x1 = 0 \/ exists t. x1 = S t
  96. 0096specialize zero_or_succ x1
  97. 0097exact zero_or_succ
  98. 0098cases htcase
  99. 0099left
  100. 0100trans S x1
  101. 0101exact hxpred_witness
  102. 0102rewrite htcase_left
  103. 0103refl
  104. 0104cases htcase_right
  105. 0105have ht0 : ~(x1 = 0)
  106. 0106intro htzero
  107. 0107rewrite htcase_right_witness at htzero
  108. 0108apply PA1
  109. 0109exact htzero
  110. 0110have hpt : exists k. k + p = x1
  111. 0111specialize divisor_le_nonzero p
  112. 0112specialize divisor_le_nonzero x1
  113. 0113apply divisor_le_nonzero
  114. 0114exact ht0
  115. 0115exact hsplit_left
  116. 0116exfalso
  117. 0117specialize lt_not_le x1
  118. 0118specialize lt_not_le p
  119. 0119apply lt_not_le
  120. 0120exact htp
  121. 0121exact hpt
  122. 0122right
  123. 0123have hfactor0 : ~(S (S x1) = 0)
  124. 0124specialize succ_ne_zero (S x1)
  125. 0125exact succ_ne_zero
  126. 0126have hpfactor : exists k. k + p = S (S x1)
  127. 0127specialize divisor_le_nonzero p
  128. 0128specialize divisor_le_nonzero (S (S x1))
  129. 0129apply divisor_le_nonzero
  130. 0130exact hfactor0
  131. 0131exact hsplit_right
  132. 0132have hfactorp : exists k. k + S (S x1) = p
  133. 0133rewrite <- hxpred_witness
  134. 0134exact hxlt
  135. 0135have hpeq : p = S (S x1)
  136. 0136specialize le_antisymm p
  137. 0137specialize le_antisymm (S (S x1))
  138. 0138apply le_antisymm
  139. 0139exact hpfactor
  140. 0140exact hfactorp
  141. 0141have hpred_eq : S x1 = n
  142. 0142specialize succ_injective (S x1)
  143. 0143specialize succ_injective n
  144. 0144apply succ_injective
  145. 0145trans p
  146. 0146symm
  147. 0147exact hpeq
  148. 0148exact hpn
  149. 0149trans S x1
  150. 0150exact hxpred_witness
  151. 0151exact hpred_eq