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. ∀ e. ∀ d. ∀ q. ∀ r. Prime(p) → Lt(n,e) → Pow(p,e,d) → DivRem(n,d,q,r) → q = 0Every 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
4 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall p n e d q r. ((~(p = 1) /\ forall frm_prime_left_b5cvqz_prime frm_prime_right_b5cvqz_prime. p = frm_prime_left_b5cvqz_prime * frm_prime_right_b5cvqz_prime -> frm_prime_left_b5cvqz_prime = 1 \/ frm_prime_right_b5cvqz_prime = 1)) -> (exists bcf_lt_gap_b5cvqz_exponent. bcf_lt_gap_b5cvqz_exponent + S (n) = e) -> (exists bpvi_b_b5cvqz_power bpvi_c_b5cvqz_power. ((forall bpvi_i_b5cvqz_power. (exists bpvi_repeat_gap_b5cvqz_power. bpvi_repeat_gap_b5cvqz_power + S bpvi_i_b5cvqz_power = e) -> (((exists bpvi_h_b5cvqz_power_repeat. bpvi_h_b5cvqz_power_repeat + S (p) = S ((S (bpvi_i_b5cvqz_power)) * bpvi_c_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_repeat. bpvi_b_b5cvqz_power = bpvi_q_b5cvqz_power_repeat * S ((S (bpvi_i_b5cvqz_power)) * bpvi_c_b5cvqz_power) + (p)))) /\ (exists bpvi_u_b5cvqz_power bpvi_v_b5cvqz_power. ((((exists bpvi_h_b5cvqz_power_start. bpvi_h_b5cvqz_power_start + S (1) = S ((S (0)) * bpvi_v_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_start. bpvi_u_b5cvqz_power = bpvi_q_b5cvqz_power_start * S ((S (0)) * bpvi_v_b5cvqz_power) + (1))) /\ ((((exists bpvi_h_b5cvqz_power_terminal. bpvi_h_b5cvqz_power_terminal + S (d) = S ((S (e)) * bpvi_v_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_terminal. bpvi_u_b5cvqz_power = bpvi_q_b5cvqz_power_terminal * S ((S (e)) * bpvi_v_b5cvqz_power) + (d))) /\ forall bpvi_j_b5cvqz_power. (exists bpvi_product_gap_b5cvqz_power. bpvi_product_gap_b5cvqz_power + S bpvi_j_b5cvqz_power = e) -> exists bpvi_factor_b5cvqz_power bpvi_partial_b5cvqz_power bpvi_successor_b5cvqz_power. ((((exists bpvi_h_b5cvqz_power_factor. bpvi_h_b5cvqz_power_factor + S (bpvi_factor_b5cvqz_power) = S ((S (bpvi_j_b5cvqz_power)) * bpvi_c_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_factor. bpvi_b_b5cvqz_power = bpvi_q_b5cvqz_power_factor * S ((S (bpvi_j_b5cvqz_power)) * bpvi_c_b5cvqz_power) + (bpvi_factor_b5cvqz_power))) /\ ((((exists bpvi_h_b5cvqz_power_partial. bpvi_h_b5cvqz_power_partial + S (bpvi_partial_b5cvqz_power) = S ((S (bpvi_j_b5cvqz_power)) * bpvi_v_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_partial. bpvi_u_b5cvqz_power = bpvi_q_b5cvqz_power_partial * S ((S (bpvi_j_b5cvqz_power)) * bpvi_v_b5cvqz_power) + (bpvi_partial_b5cvqz_power))) /\ ((((exists bpvi_h_b5cvqz_power_successor. bpvi_h_b5cvqz_power_successor + S (bpvi_successor_b5cvqz_power) = S ((S (S bpvi_j_b5cvqz_power)) * bpvi_v_b5cvqz_power)) /\ exists bpvi_q_b5cvqz_power_successor. bpvi_u_b5cvqz_power = bpvi_q_b5cvqz_power_successor * S ((S (S bpvi_j_b5cvqz_power)) * bpvi_v_b5cvqz_power) + (bpvi_successor_b5cvqz_power))) /\ bpvi_successor_b5cvqz_power = bpvi_partial_b5cvqz_power * bpvi_factor_b5cvqz_power)))))))) -> (((n) = (d) * (q) + (r) /\ (exists bcf_lt_gap_b5cvqz_division_bound. bcf_lt_gap_b5cvqz_division_bound + S (r) = d))) -> q = 0Proof 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 (3)
01Fix variables and assumptionsL1–10
02Establish hpower_boundL11–17
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime power exponent le.
03Establish hvalue_boundL18–27
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt of lt of le.
Original defined command ledger · 31 lines
- 0001
intro p - 0002
intro n - 0003
intro e - 0004
intro d - 0005
intro q - 0006
intro r - 0007
intro hp - 0008
intro hexponent - 0009
intro hpower - 0010
intro hdivision - 0011
have hpower_bound : Le(e,d)Exact native replay line
have hpower_bound : exists g. g + e = d - 0012
specialize prime_power_exponent_le p - 0013
specialize prime_power_exponent_le e - 0014
specialize prime_power_exponent_le d - 0015
apply prime_power_exponent_le - 0016
exact hp - 0017
exact hpower - 0018
have hvalue_bound : Lt(n,d)Exact native replay line
have hvalue_bound : exists g. g + S n = d - 0019
specialize lt_of_lt_of_le n - 0020
specialize lt_of_lt_of_le e - 0021
specialize lt_of_lt_of_le d - 0022
apply lt_of_lt_of_le - 0023
exact hexponent - 0024
exact hpower_bound - 0025
specialize division_zero_quotient_of_lt d - 0026
specialize division_zero_quotient_of_lt n - 0027
specialize division_zero_quotient_of_lt q - 0028
specialize division_zero_quotient_of_lt r - 0029
apply division_zero_quotient_of_lt - 0030
exact hdivision - 0031
exact hvalue_bound