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. ∀ d. Prime(p) → Pow(p,S n,d) → DivRem(n,d,0,n)Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.
Definitions used by this theorem
In the theorem statement
3 occurrences
In local proof propositions
none
0 occurrences
Exact expanded native-PA statement
forall p n d. ((~(p = 1) /\ forall frm_prime_left_blvb_prime frm_prime_right_blvb_prime. p = frm_prime_left_blvb_prime * frm_prime_right_blvb_prime -> frm_prime_left_blvb_prime = 1 \/ frm_prime_right_blvb_prime = 1)) -> (exists bpvi_b_blvb_quotient_tail_power bpvi_c_blvb_quotient_tail_power. ((forall bpvi_i_blvb_quotient_tail_power. (exists bpvi_repeat_gap_blvb_quotient_tail_power. bpvi_repeat_gap_blvb_quotient_tail_power + S bpvi_i_blvb_quotient_tail_power = S n) -> (((exists bpvi_h_blvb_quotient_tail_power_repeat. bpvi_h_blvb_quotient_tail_power_repeat + S (p) = S ((S (bpvi_i_blvb_quotient_tail_power)) * bpvi_c_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_repeat. bpvi_b_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_repeat * S ((S (bpvi_i_blvb_quotient_tail_power)) * bpvi_c_blvb_quotient_tail_power) + (p)))) /\ (exists bpvi_u_blvb_quotient_tail_power bpvi_v_blvb_quotient_tail_power. ((((exists bpvi_h_blvb_quotient_tail_power_start. bpvi_h_blvb_quotient_tail_power_start + S (1) = S ((S (0)) * bpvi_v_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_start. bpvi_u_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_start * S ((S (0)) * bpvi_v_blvb_quotient_tail_power) + (1))) /\ ((((exists bpvi_h_blvb_quotient_tail_power_terminal. bpvi_h_blvb_quotient_tail_power_terminal + S (d) = S ((S (S n)) * bpvi_v_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_terminal. bpvi_u_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_terminal * S ((S (S n)) * bpvi_v_blvb_quotient_tail_power) + (d))) /\ forall bpvi_j_blvb_quotient_tail_power. (exists bpvi_product_gap_blvb_quotient_tail_power. bpvi_product_gap_blvb_quotient_tail_power + S bpvi_j_blvb_quotient_tail_power = S n) -> exists bpvi_factor_blvb_quotient_tail_power bpvi_partial_blvb_quotient_tail_power bpvi_successor_blvb_quotient_tail_power. ((((exists bpvi_h_blvb_quotient_tail_power_factor. bpvi_h_blvb_quotient_tail_power_factor + S (bpvi_factor_blvb_quotient_tail_power) = S ((S (bpvi_j_blvb_quotient_tail_power)) * bpvi_c_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_factor. bpvi_b_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_factor * S ((S (bpvi_j_blvb_quotient_tail_power)) * bpvi_c_blvb_quotient_tail_power) + (bpvi_factor_blvb_quotient_tail_power))) /\ ((((exists bpvi_h_blvb_quotient_tail_power_partial. bpvi_h_blvb_quotient_tail_power_partial + S (bpvi_partial_blvb_quotient_tail_power) = S ((S (bpvi_j_blvb_quotient_tail_power)) * bpvi_v_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_partial. bpvi_u_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_partial * S ((S (bpvi_j_blvb_quotient_tail_power)) * bpvi_v_blvb_quotient_tail_power) + (bpvi_partial_blvb_quotient_tail_power))) /\ ((((exists bpvi_h_blvb_quotient_tail_power_successor. bpvi_h_blvb_quotient_tail_power_successor + S (bpvi_successor_blvb_quotient_tail_power) = S ((S (S bpvi_j_blvb_quotient_tail_power)) * bpvi_v_blvb_quotient_tail_power)) /\ exists bpvi_q_blvb_quotient_tail_power_successor. bpvi_u_blvb_quotient_tail_power = bpvi_q_blvb_quotient_tail_power_successor * S ((S (S bpvi_j_blvb_quotient_tail_power)) * bpvi_v_blvb_quotient_tail_power) + (bpvi_successor_blvb_quotient_tail_power))) /\ bpvi_successor_blvb_quotient_tail_power = bpvi_partial_blvb_quotient_tail_power * bpvi_factor_blvb_quotient_tail_power)))))))) -> ((n = (d) * (0) + (n) /\ exists blvb_remainder_gap_blvb_quotient_tail_zero. blvb_remainder_gap_blvb_quotient_tail_zero + S (n) = (d)))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
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 (2)
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–6
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L6
split
03Calculate and transport equalitiesL7–9
04Use earlier factsL10–10
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L10
apply PA5
05Calculate and transport equalitiesL11–11
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L11
refl
06Use earlier factsL12–18
Original defined command ledger · 18 lines
- 0001
intro p - 0002
intro n - 0003
intro d - 0004
intro hp - 0005
intro hpower - 0006
split - 0007
symm - 0008
trans 0 + n - 0009
congr - 0010
apply PA5 - 0011
refl - 0012
apply zero_add - 0013
specialize prime_power_exponent_le p - 0014
specialize prime_power_exponent_le (S n) - 0015
specialize prime_power_exponent_le d - 0016
apply prime_power_exponent_le - 0017
exact hp - 0018
exact hpower