PA0063

prime_bounded_nonzero_mod_inverse

Stable checked-use theorem · independently closed

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

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

Read the argument

Proof checkpoints

125 script commands · 40 reading checkpoints · 16 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 (13)
prime is succ succprime nonzerodivisor le nonzerolt not leprime mod inversedivision remainder existsmul commremainder decomposition to mod eqmod eq mul leftmod eq symmmod eq transmod eq bounded uniquesucc ne zero
01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro hp
  4. L4
    intro ha0
  5. L5
    intro hap
02Establish hp0L6–11

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

  1. L6
    have hp0 : ~(p = 0)
  2. L7
    intro hpzero
  3. L8
    specialize prime_nonzero p
  4. L9
    apply prime_nonzero
  5. L10
    exact hp
  6. L11
    exact hpzero
03Establish hnotdivL12–13

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

  1. L12
    have hnotdiv : ~(exists k. a = p * k)
  2. L13
    intro hdiv
04Establish hpaL14–23

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

  1. L14
    have hpa : exists t. t + p = a
  2. L15
    specialize divisor_le_nonzero p
  3. L16
    specialize divisor_le_nonzero a
  4. L17
    apply divisor_le_nonzero
  5. L18
    exact ha0
  6. L19
    exact hdiv
  7. L20
    specialize lt_not_le a
  8. L21
    specialize lt_not_le p
  9. L22
    apply lt_not_le
  10. L23
    exact hap
05Use earlier factsL24–24

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

  1. L24
    exact hpa
06Establish hinvL25–30

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

  1. L25
    have hinv : exists z u v. a * z + p * u = 1 + p * v
  2. L26
    specialize prime_mod_inverse p
  3. L27
    specialize prime_mod_inverse a
  4. L28
    apply prime_mod_inverse
  5. L29
    exact hp
  6. L30
    exact hnotdiv
07Separate the logical casesL31–33

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

  1. L31
    cases hinv
  2. L32
    cases hinv_witness
  3. L33
    cases hinv_witness_witness
08Establish hdivzL34–38

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

  1. L34
    have hdivz : exists q r. x = p * q + r /\ exists h. h + S r = p
  2. L35
    specialize division_remainder_exists p
  3. L36
    specialize division_remainder_exists x
  4. L37
    apply division_remainder_exists
  5. L38
    exact hp0
09Separate the logical casesL39–41

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

  1. L39
    cases hdivz
  2. L40
    cases hdivz_witness
  3. L41
    cases hdivz_witness_witness
10Establish hzdecompL42–47

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

  1. L42
    have hzdecomp : x = x3 * p + x4
  2. L43
    trans p * x3 + x4
  3. L44
    exact hdivz_witness_witness_left
  4. L45
    congr
  5. L46
    apply mul_comm
  6. L47
    refl
11Establish hzrL48–54

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.

  1. L48
    have hzr : exists u v. x + p * u = x4 + p * v
  2. L49
    specialize remainder_decomposition_to_mod_eq p
  3. L50
    specialize remainder_decomposition_to_mod_eq x
  4. L51
    specialize remainder_decomposition_to_mod_eq x3
  5. L52
    specialize remainder_decomposition_to_mod_eq x4
  6. L53
    apply remainder_decomposition_to_mod_eq
  7. L54
    exact hzdecomp
12Establish hscaledL55–61

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

  1. L55
    have hscaled : exists u v. (a * x) + p * u = (a * x4) + p * v
  2. L56
    specialize mod_eq_mul_left p
  3. L57
    specialize mod_eq_mul_left x
  4. L58
    specialize mod_eq_mul_left x4
  5. L59
    specialize mod_eq_mul_left a
  6. L60
    apply mod_eq_mul_left
  7. L61
    exact hzr
13Establish hrzL62–67

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

  1. L62
    have hrz : exists u v. (a * x4) + p * u = (a * x) + p * v
  2. L63
    specialize mod_eq_symm p
  3. L64
    specialize mod_eq_symm (a * x)
  4. L65
    specialize mod_eq_symm (a * x4)
  5. L66
    apply mod_eq_symm
  6. L67
    exact hscaled
14Establish hfinalL68–74

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

  1. L68
    have hfinal : exists u v. (a * x4) + p * u = 1 + p * v
  2. L69
    specialize mod_eq_trans p
  3. L70
    specialize mod_eq_trans (a * x4)
  4. L71
    specialize mod_eq_trans (a * x)
  5. L72
    specialize mod_eq_trans 1
  6. L73
    apply mod_eq_trans
  7. L74
    exact hrz
15Construct an explicit witnessL75–76

Supply the displayed value, then prove that it has the required property.

  1. L75
    exists x1
  2. L76
    exists x2
16Use earlier factsL77–77

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

  1. L77
    exact hinv_witness_witness_witness
17Establish hp2L78–81

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

  1. L78
    have hp2 : exists k. p = S (S k)
  2. L79
    specialize prime_is_succ_succ p
  3. L80
    apply prime_is_succ_succ
  4. L81
    exact hp
18Separate the logical casesL82–82

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

  1. L82
    cases hp2
19Establish h0boundL83–83

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

  1. L83
    have h0bound : exists h. h + S 0 = p
20Construct an explicit witnessL84–84

Supply the displayed value, then prove that it has the required property.

  1. L84
    exists S x5
21Calculate and transport equalitiesL85–86

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

  1. L85
    rewrite hp2_witness
  2. L86
    simp
22Establish h1boundL87–87

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

  1. L87
    have h1bound : exists h. h + S 1 = p
23Construct an explicit witnessL88–88

Supply the displayed value, then prove that it has the required property.

  1. L88
    exists x5
24Calculate and transport equalitiesL89–90

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

  1. L89
    rewrite hp2_witness
  2. L90
    simp
25Establish hr0L91–92

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

  1. L91
    have hr0 : ~(x4 = 0)
  2. L92
    intro hrzero
26Establish hzerooneL93–93

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

  1. L93
    have hzeroone : exists u v. 0 + p * u = 1 + p * v
27Separate the logical casesL94–95

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

  1. L94
    cases hfinal
  2. L95
    cases hfinal_witness
28Construct an explicit witnessL96–97

Supply the displayed value, then prove that it has the required property.

  1. L96
    exists x6
  2. L97
    exists x7
29Calculate and transport equalitiesL98–103

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

  1. L98
    trans (a * x4) + p * x6
  2. L99
    congr
  3. L100
    symm
  4. L101
    trans a * 0
  5. L102
    congr
  6. L103
    refl
30Use earlier factsL104–105

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

  1. L104
    exact hrzero
  2. L105
    apply PA5
31Calculate and transport equalitiesL106–106

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

  1. L106
    refl
32Use earlier factsL107–107

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

  1. L107
    exact hfinal_witness_witness
33Establish hzeroeqoneL108–117

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq bounded unique.

  1. L108
    have hzeroeqone : 0 = 1
  2. L109
    specialize mod_eq_bounded_unique p
  3. L110
    specialize mod_eq_bounded_unique 0
  4. L111
    specialize mod_eq_bounded_unique 1
  5. L112
    apply mod_eq_bounded_unique
  6. L113
    exact h0bound
  7. L114
    exact h1bound
  8. L115
    exact hzeroone
  9. L116
    specialize succ_ne_zero 0
  10. L117
    apply succ_ne_zero
34Calculate and transport equalitiesL118–118

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

  1. L118
    symm
35Use earlier factsL119–119

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

  1. L119
    exact hzeroeqone
36Construct an explicit witnessL120–120

Supply the displayed value, then prove that it has the required property.

  1. L120
    exists x4
37Separate the logical casesL121–121

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

  1. L121
    split
38Use earlier factsL122–122

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

  1. L122
    exact hr0
39Separate the logical casesL123–123

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

  1. L123
    split
40Use earlier factsL124–125

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

  1. L124
    exact hdivz_witness_witness_right
  2. L125
    exact hfinal

Library-wide reading audit

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