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.
Statement with defined notation
∀ p. ∀ n. ∀ i. p = S n → Prime(p) → Lt(i,n) → ∃ x. InverseIndex(p,n,i,x)Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.
Definitions used by this theorem
In the theorem statement
3 occurrences
In local proof propositions
3 occurrences
Exact expanded native-PA statement
forall p n i. p = S n -> ((~(p = 1) /\ forall wip_prime_left_exists_prime wip_prime_right_exists_prime. p = wip_prime_left_exists_prime * wip_prime_right_exists_prime -> wip_prime_left_exists_prime = 1 \/ wip_prime_right_exists_prime = 1)) -> (exists wip_strict_gap_exists_index_bound. wip_strict_gap_exists_index_bound + S i = n) -> exists j. (((exists wip_strict_gap_exists_result_left_bound. wip_strict_gap_exists_result_left_bound + S i = n) /\ ((exists wip_strict_gap_exists_result_right_bound. wip_strict_gap_exists_result_right_bound + S j = n) /\ (exists wip_mod_left_exists_result_inverse wip_mod_right_exists_result_inverse. (S i) * S j + p * wip_mod_left_exists_result_inverse = 1 + p * wip_mod_right_exists_result_inverse))))Proof neighborhood
Direct theorem prerequisites
PA0005 succ_ne_zero PA002K succ_le_succ PA0063 prime_bounded_nonzero_mod_inverse PA001V nonzero_is_succ PA000V le_of_succ_le_succDirect theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.
Read the argument
Proof checkpoints
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 (5)
01Fix variables and assumptionsL1–6
02Establish hsi0L7–9
03Establish hsipL10–15
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ le succ.
04Establish hinvL16–22
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime bounded nonzero mod inverse.
- L16
have hinv : BoundedNonzeroInverse(p,S i)Definitions: BoundedNonzeroInverse(p,S i)Original native command in the exact edition - L17
specialize prime_bounded_nonzero_mod_inverse p - L18
specialize prime_bounded_nonzero_mod_inverse (S i) - L19
apply prime_bounded_nonzero_mod_inverse - L20
exact hp - L21
exact hsi0 - L22
exact hsip
05Separate the logical casesL23–25
06Establish hpredL26–29
07Separate the logical casesL30–30
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L30
cases hpred
08Establish hjnL31–37
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.
09Construct an explicit witnessL38–38
Supply the displayed value, then prove that it has the required property.
- L38
exists x1
10Separate the logical casesL39–39
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L39
split
11Use earlier factsL40–40
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L40
exact hi
12Separate the logical casesL41–41
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L41
split
13Use earlier factsL42–42
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L42
exact hjn
14Calculate and transport equalitiesL43–43
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L43
rewrite hpred_witness at hinv_witness_right_right
15Use earlier factsL44–44
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L44
exact hinv_witness_right_right
Original defined command ledger · 44 lines
- 0001
intro p - 0002
intro n - 0003
intro i - 0004
intro hpn - 0005
intro hp - 0006
intro hi - 0007
have hsi0 : ~(S i = 0) - 0008
specialize succ_ne_zero i - 0009
exact succ_ne_zero - 0010
have hsip : Lt(S i,p)Exact native replay line
have hsip : exists wip_successor_gap_exists_residue_bound. wip_successor_gap_exists_residue_bound + S (S i) = p - 0011
rewrite hpn - 0012
specialize succ_le_succ (S i) - 0013
specialize succ_le_succ n - 0014
apply succ_le_succ - 0015
exact hi - 0016
have hinv : BoundedNonzeroInverse(p,S i)Exact native replay line
have hinv : exists wip_inverse_exists_raw. (~(wip_inverse_exists_raw = 0) /\ ((exists wip_strict_gap_exists_raw_bound. wip_strict_gap_exists_raw_bound + S wip_inverse_exists_raw = p) /\ (exists wip_mod_left_exists_raw_congruence wip_mod_right_exists_raw_congruence. (S i) * wip_inverse_exists_raw + p * wip_mod_left_exists_raw_congruence = 1 + p * wip_mod_right_exists_raw_congruence))) - 0017
specialize prime_bounded_nonzero_mod_inverse p - 0018
specialize prime_bounded_nonzero_mod_inverse (S i) - 0019
apply prime_bounded_nonzero_mod_inverse - 0020
exact hp - 0021
exact hsi0 - 0022
exact hsip - 0023
cases hinv - 0024
cases hinv_witness - 0025
cases hinv_witness_right - 0026
have hpred : exists j. x = S j - 0027
specialize nonzero_is_succ x - 0028
apply nonzero_is_succ - 0029
exact hinv_witness_left - 0030
cases hpred - 0031
have hjn : Lt(x1,n)Exact native replay line
have hjn : exists wip_strict_gap_exists_output_bound. wip_strict_gap_exists_output_bound + S x1 = n - 0032
specialize le_of_succ_le_succ (S x1) - 0033
specialize le_of_succ_le_succ n - 0034
apply le_of_succ_le_succ - 0035
rewrite <- hpred_witness - 0036
rewrite <- hpn - 0037
exact hinv_witness_right_left - 0038
exists x1 - 0039
split - 0040
exact hi - 0041
split - 0042
exact hjn - 0043
rewrite hpred_witness at hinv_witness_right_right - 0044
exact hinv_witness_right_right