PA00AG

prime_bounded_square_one_cases

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

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

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.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

151 script commands · 47 reading checkpoints · 18 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.

Named ingredients (16)
ne zero of one lenonzero is succmul succ leftadd assocadd commadd left cancelfactor differenceeuclid prime dvd productle succ selflt of le of ltzero or succdivisor le nonzerolt not lesucc ne zerole antisymmsucc injective
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro x
  4. L4
    intro hpn
  5. L5
    intro hp
  6. L6
    intro hxpos
  7. L7
    intro hxlt
  8. L8
    intro hsquaremod
02Separate the logical casesL9–9

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

  1. L9
    cases hp
03Establish hprimeL10–10

Establish this local claim before using it. It is not an additional assumption.

  1. L10
    have 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)
04Separate the logical casesL11–11

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

  1. L11
    split
05Use earlier factsL12–13

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

  1. L12
    exact hp_left
  2. L13
    exact hp_right
06Establish hx0L14–19

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

  1. L14
    have hx0 : ~(x = 0)
  2. L15
    specialize ne_zero_of_one_le x
  3. L16
    intro hxzero
  4. L17
    apply ne_zero_of_one_le
  5. L18
    exact hxpos
  6. L19
    exact hxzero
07Establish hxpredL20–23

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

  1. L20
    have hxpred : exists t. x = S t
  2. L21
    specialize nonzero_is_succ x
  3. L22
    apply nonzero_is_succ
  4. L23
    exact hx0
08Separate the logical casesL24–24

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

  1. L24
    cases hxpred
09Establish hsquareL25–34

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

  1. L25
    have hsquare : x * x = 1 + x1 * S (S x1)
  2. L26
    rewrite hxpred_witness
  3. L27
    rewrite hxpred_witness
  4. L28
    specialize mul_succ_left x1
  5. L29
    specialize mul_succ_left (S x1)
  6. L30
    trans x1 * S x1 + S x1
  7. L31
    exact mul_succ_left
  8. L32
    trans S (x1 * S x1 + x1)
  9. L33
    apply PA4
  10. L34
    trans (x1 * S x1 + x1) + 1
10Calculate and transport equalitiesL35–36

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

  1. L35
    symm
  2. L36
    trans S ((x1 * S x1 + x1) + 0)
11Use earlier factsL37–37

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

  1. L37
    apply PA4
12Calculate and transport equalitiesL38–38

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

  1. L38
    congr
13Use earlier factsL39–39

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

  1. L39
    apply PA3
14Calculate and transport equalitiesL40–40

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

  1. L40
    trans 1 + (x1 * S x1 + x1)
15Use earlier factsL41–41

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

  1. L41
    apply add_comm
16Calculate and transport equalitiesL42–44

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

  1. L42
    congr
  2. L43
    refl
  3. L44
    symm
17Use earlier factsL45–45

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

  1. L45
    apply PA6
18Separate the logical casesL46–47

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

  1. L46
    cases hsquaremod
  2. L47
    cases hsquaremod_witness
19Establish hcancelL48–57

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

  1. L48
    have hcancel : x1 * S (S x1) + p * x2 = p * x3
  2. L49
    specialize add_left_cancel 1
  3. L50
    specialize add_left_cancel (x1 * S (S x1) + p * x2)
  4. L51
    specialize add_left_cancel (p * x3)
  5. L52
    apply add_left_cancel
  6. L53
    trans (1 + x1 * S (S x1)) + p * x2
  7. L54
    symm
  8. L55
    apply add_assoc
  9. L56
    trans x * x + p * x2
  10. L57
    congr
20Calculate and transport equalitiesL58–58

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

  1. L58
    symm
21Use earlier factsL59–59

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

  1. L59
    exact hsquare
22Calculate and transport equalitiesL60–61

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

  1. L60
    refl
  2. L61
    trans 1 + p * x3
23Use earlier factsL62–62

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

  1. L62
    exact hsquaremod_witness_witness
24Calculate and transport equalitiesL63–63

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

  1. L63
    refl
25Establish hfactorL64–68

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

  1. L64
    have hfactor : p * x3 = p * x2 + x1 * S (S x1)
  2. L65
    trans x1 * S (S x1) + p * x2
  3. L66
    symm
  4. L67
    exact hcancel
  5. L68
    apply add_comm
26Establish hproductL69–75

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

  1. L69
    have hproduct : exists w. x1 * S (S x1) = p * w
  2. L70
    specialize factor_difference p
  3. L71
    specialize factor_difference x3
  4. L72
    specialize factor_difference x2
  5. L73
    specialize factor_difference (x1 * S (S x1))
  6. L74
    apply factor_difference
  7. L75
    exact hfactor
27Establish hsplitL76–82

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

  1. L76
    have hsplit : (exists u. x1 = p * u) \/ exists v. S (S x1) = p * v
  2. L77
    specialize euclid_prime_dvd_product p
  3. L78
    specialize euclid_prime_dvd_product x1
  4. L79
    specialize euclid_prime_dvd_product (S (S x1))
  5. L80
    apply euclid_prime_dvd_product
  6. L81
    exact hprime
  7. L82
    exact hproduct
28Separate the logical casesL83–83

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

  1. L83
    cases hsplit
29Establish htxL84–87

Establish this local claim before using it. It is not an additional assumption.

  1. L84
    have htx : exists k. k + x1 = x
  2. L85
    rewrite hxpred_witness
  3. L86
    specialize le_succ_self x1
  4. L87
    exact le_succ_self
30Establish htpL88–94

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

  1. L88
    have htp : exists k. k + S x1 = p
  2. L89
    specialize lt_of_le_of_lt x1
  3. L90
    specialize lt_of_le_of_lt x
  4. L91
    specialize lt_of_le_of_lt p
  5. L92
    apply lt_of_le_of_lt
  6. L93
    exact htx
  7. L94
    exact hxlt
31Establish htcaseL95–97

Establish this local claim before using it. It is not an additional assumption.

  1. L95
    have htcase : x1 = 0 \/ exists t. x1 = S t
  2. L96
    specialize zero_or_succ x1
  3. L97
    exact zero_or_succ
32Separate the logical casesL98–99

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

  1. L98
    cases htcase
  2. L99
    left
33Calculate and transport equalitiesL100–100

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

  1. L100
    trans S x1
34Use earlier factsL101–101

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

  1. L101
    exact hxpred_witness
35Calculate and transport equalitiesL102–103

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

  1. L102
    rewrite htcase_left
  2. L103
    refl
36Separate the logical casesL104–104

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

  1. L104
    cases htcase_right
37Establish ht0L105–109

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

  1. L105
    have ht0 : ~(x1 = 0)
  2. L106
    intro htzero
  3. L107
    rewrite htcase_right_witness at htzero
  4. L108
    apply PA1
  5. L109
    exact htzero
38Establish hptL110–115

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

  1. L110
    have hpt : exists k. k + p = x1
  2. L111
    specialize divisor_le_nonzero p
  3. L112
    specialize divisor_le_nonzero x1
  4. L113
    apply divisor_le_nonzero
  5. L114
    exact ht0
  6. L115
    exact hsplit_left
39Separate the logical casesL116–116

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

  1. L116
    exfalso
40Use earlier factsL117–121

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

  1. L117
    specialize lt_not_le x1
  2. L118
    specialize lt_not_le p
  3. L119
    apply lt_not_le
  4. L120
    exact htp
  5. L121
    exact hpt
41Separate the logical casesL122–122

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

  1. L122
    right
42Establish hfactor0L123–125

Establish this local claim before using it. It is not an additional assumption.

  1. L123
    have hfactor0 : ~(S (S x1) = 0)
  2. L124
    specialize succ_ne_zero (S x1)
  3. L125
    exact succ_ne_zero
43Establish hpfactorL126–131

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

  1. L126
    have hpfactor : exists k. k + p = S (S x1)
  2. L127
    specialize divisor_le_nonzero p
  3. L128
    specialize divisor_le_nonzero (S (S x1))
  4. L129
    apply divisor_le_nonzero
  5. L130
    exact hfactor0
  6. L131
    exact hsplit_right
44Establish hfactorpL132–134

Establish this local claim before using it. It is not an additional assumption.

  1. L132
    have hfactorp : exists k. k + S (S x1) = p
  2. L133
    rewrite <- hxpred_witness
  3. L134
    exact hxlt
45Establish hpeqL135–140

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

  1. L135
    have hpeq : p = S (S x1)
  2. L136
    specialize le_antisymm p
  3. L137
    specialize le_antisymm (S (S x1))
  4. L138
    apply le_antisymm
  5. L139
    exact hpfactor
  6. L140
    exact hfactorp
46Establish hpred_eqL141–150

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

  1. L141
    have hpred_eq : S x1 = n
  2. L142
    specialize succ_injective (S x1)
  3. L143
    specialize succ_injective n
  4. L144
    apply succ_injective
  5. L145
    trans p
  6. L146
    symm
  7. L147
    exact hpeq
  8. L148
    exact hpn
  9. L149
    trans S x1
  10. L150
    exact hxpred_witness
47Use earlier factsL151–151

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

  1. L151
    exact hpred_eq

Library-wide reading audit

Original exact command ledger · 151 lines
  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