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
∀ n. ∀ c. ∀ p. (∀ x. Lt(n,x) ∧ Le(x,n + n) → ¬Prime(x)) → Prime(p) → CentralBinom(n,c) → Dvd(p,c) → Le(p,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
7 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall n c p. (forall bpr_prime_candidate_bnbcpdl_exclusion. ((exists bpr_gap_bnbcpdl_exclusion_lower. bpr_gap_bnbcpdl_exclusion_lower + S (n) = bpr_prime_candidate_bnbcpdl_exclusion) /\ (exists bpr_le_gap_bnbcpdl_exclusion_upper. bpr_le_gap_bnbcpdl_exclusion_upper + (bpr_prime_candidate_bnbcpdl_exclusion) = (n + n))) -> ~((~(bpr_prime_candidate_bnbcpdl_exclusion = 1) /\ forall bpr_left_bnbcpdl_exclusion_prime bpr_right_bnbcpdl_exclusion_prime. bpr_prime_candidate_bnbcpdl_exclusion = bpr_left_bnbcpdl_exclusion_prime * bpr_right_bnbcpdl_exclusion_prime -> bpr_left_bnbcpdl_exclusion_prime = 1 \/ bpr_right_bnbcpdl_exclusion_prime = 1))) -> ((~(p = 1) /\ forall bpr_left_bnbcpdl_prime bpr_right_bnbcpdl_prime. p = bpr_left_bnbcpdl_prime * bpr_right_bnbcpdl_prime -> bpr_left_bnbcpdl_prime = 1 \/ bpr_right_bnbcpdl_prime = 1)) -> (((exists bcf_lt_gap_bnbcpdl_central_out_of_range. bcf_lt_gap_bnbcpdl_central_out_of_range + S (n + n) = n) /\ c = 0) \/ ((exists bcf_le_gap_bnbcpdl_central_in_range. bcf_le_gap_bnbcpdl_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bnbcpdl_central bcf_row_code_scale_bnbcpdl_central bcf_row_scale_code_bnbcpdl_central bcf_row_scale_scale_bnbcpdl_central bcf_row_code_bnbcpdl_central bcf_row_scale_bnbcpdl_central. ((forall bcf_row_index_bnbcpdl_central_table. (exists bcf_lt_gap_bnbcpdl_central_table_row_bound. bcf_lt_gap_bnbcpdl_central_table_row_bound + S (bcf_row_index_bnbcpdl_central_table) = S (n + n)) -> exists bcf_row_code_bnbcpdl_central_table bcf_row_scale_bnbcpdl_central_table. ((((exists bcf_height_bnbcpdl_central_table_decoded_row_code. bcf_height_bnbcpdl_central_table_decoded_row_code + S (bcf_row_code_bnbcpdl_central_table) = S ((S (bcf_row_index_bnbcpdl_central_table)) * bcf_row_code_scale_bnbcpdl_central)) /\ exists bcf_quotient_bnbcpdl_central_table_decoded_row_code. bcf_row_code_code_bnbcpdl_central = bcf_quotient_bnbcpdl_central_table_decoded_row_code * S ((S (bcf_row_index_bnbcpdl_central_table)) * bcf_row_code_scale_bnbcpdl_central) + (bcf_row_code_bnbcpdl_central_table))) /\ ((((exists bcf_height_bnbcpdl_central_table_decoded_row_scale. bcf_height_bnbcpdl_central_table_decoded_row_scale + S (bcf_row_scale_bnbcpdl_central_table) = S ((S (bcf_row_index_bnbcpdl_central_table)) * bcf_row_scale_scale_bnbcpdl_central)) /\ exists bcf_quotient_bnbcpdl_central_table_decoded_row_scale. bcf_row_scale_code_bnbcpdl_central = bcf_quotient_bnbcpdl_central_table_decoded_row_scale * S ((S (bcf_row_index_bnbcpdl_central_table)) * bcf_row_scale_scale_bnbcpdl_central) + (bcf_row_scale_bnbcpdl_central_table))) /\ ((bcf_row_index_bnbcpdl_central_table = 0 /\ (forall bcf_index_bnbcpdl_central_table_zero_row. (exists bcf_lt_gap_bnbcpdl_central_table_zero_row_bound. bcf_lt_gap_bnbcpdl_central_table_zero_row_bound + S (bcf_index_bnbcpdl_central_table_zero_row) = S (n + n)) -> exists bcf_value_bnbcpdl_central_table_zero_row. ((((exists bcf_height_bnbcpdl_central_table_zero_row_entry. bcf_height_bnbcpdl_central_table_zero_row_entry + S (bcf_value_bnbcpdl_central_table_zero_row) = S ((S (bcf_index_bnbcpdl_central_table_zero_row)) * bcf_row_scale_bnbcpdl_central_table)) /\ exists bcf_quotient_bnbcpdl_central_table_zero_row_entry. bcf_row_code_bnbcpdl_central_table = bcf_quotient_bnbcpdl_central_table_zero_row_entry * S ((S (bcf_index_bnbcpdl_central_table_zero_row)) * bcf_row_scale_bnbcpdl_central_table) + (bcf_value_bnbcpdl_central_table_zero_row))) /\ ((bcf_index_bnbcpdl_central_table_zero_row = 0 /\ bcf_value_bnbcpdl_central_table_zero_row = 1) \/ exists bcf_predecessor_bnbcpdl_central_table_zero_row. bcf_index_bnbcpdl_central_table_zero_row = S bcf_predecessor_bnbcpdl_central_table_zero_row /\ bcf_value_bnbcpdl_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bnbcpdl_central_table bcf_previous_code_bnbcpdl_central_table bcf_previous_scale_bnbcpdl_central_table. bcf_row_index_bnbcpdl_central_table = S bcf_predecessor_bnbcpdl_central_table /\ ((((exists bcf_height_bnbcpdl_central_table_decoded_previous_code. bcf_height_bnbcpdl_central_table_decoded_previous_code + S (bcf_previous_code_bnbcpdl_central_table) = S ((S (bcf_predecessor_bnbcpdl_central_table)) * bcf_row_code_scale_bnbcpdl_central)) /\ exists bcf_quotient_bnbcpdl_central_table_decoded_previous_code. bcf_row_code_code_bnbcpdl_central = bcf_quotient_bnbcpdl_central_table_decoded_previous_code * S ((S (bcf_predecessor_bnbcpdl_central_table)) * bcf_row_code_scale_bnbcpdl_central) + (bcf_previous_code_bnbcpdl_central_table))) /\ ((((exists bcf_height_bnbcpdl_central_table_decoded_previous_scale. bcf_height_bnbcpdl_central_table_decoded_previous_scale + S (bcf_previous_scale_bnbcpdl_central_table) = S ((S (bcf_predecessor_bnbcpdl_central_table)) * bcf_row_scale_scale_bnbcpdl_central)) /\ exists bcf_quotient_bnbcpdl_central_table_decoded_previous_scale. bcf_row_scale_code_bnbcpdl_central = bcf_quotient_bnbcpdl_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bnbcpdl_central_table)) * bcf_row_scale_scale_bnbcpdl_central) + (bcf_previous_scale_bnbcpdl_central_table))) /\ (forall bcf_index_bnbcpdl_central_table_row_step. (exists bcf_lt_gap_bnbcpdl_central_table_row_step_bound. bcf_lt_gap_bnbcpdl_central_table_row_step_bound + S (bcf_index_bnbcpdl_central_table_row_step) = S (n + n)) -> exists bcf_value_bnbcpdl_central_table_row_step. ((((exists bcf_height_bnbcpdl_central_table_row_step_entry. bcf_height_bnbcpdl_central_table_row_step_entry + S (bcf_value_bnbcpdl_central_table_row_step) = S ((S (bcf_index_bnbcpdl_central_table_row_step)) * bcf_row_scale_bnbcpdl_central_table)) /\ exists bcf_quotient_bnbcpdl_central_table_row_step_entry. bcf_row_code_bnbcpdl_central_table = bcf_quotient_bnbcpdl_central_table_row_step_entry * S ((S (bcf_index_bnbcpdl_central_table_row_step)) * bcf_row_scale_bnbcpdl_central_table) + (bcf_value_bnbcpdl_central_table_row_step))) /\ ((bcf_index_bnbcpdl_central_table_row_step = 0 /\ bcf_value_bnbcpdl_central_table_row_step = 1) \/ exists bcf_predecessor_bnbcpdl_central_table_row_step bcf_left_bnbcpdl_central_table_row_step bcf_right_bnbcpdl_central_table_row_step. bcf_index_bnbcpdl_central_table_row_step = S bcf_predecessor_bnbcpdl_central_table_row_step /\ ((((exists bcf_height_bnbcpdl_central_table_row_step_previous_left. bcf_height_bnbcpdl_central_table_row_step_previous_left + S (bcf_left_bnbcpdl_central_table_row_step) = S ((S (bcf_predecessor_bnbcpdl_central_table_row_step)) * bcf_previous_scale_bnbcpdl_central_table)) /\ exists bcf_quotient_bnbcpdl_central_table_row_step_previous_left. bcf_previous_code_bnbcpdl_central_table = bcf_quotient_bnbcpdl_central_table_row_step_previous_left * S ((S (bcf_predecessor_bnbcpdl_central_table_row_step)) * bcf_previous_scale_bnbcpdl_central_table) + (bcf_left_bnbcpdl_central_table_row_step))) /\ ((((exists bcf_height_bnbcpdl_central_table_row_step_previous_right. bcf_height_bnbcpdl_central_table_row_step_previous_right + S (bcf_right_bnbcpdl_central_table_row_step) = S ((S (S (bcf_predecessor_bnbcpdl_central_table_row_step))) * bcf_previous_scale_bnbcpdl_central_table)) /\ exists bcf_quotient_bnbcpdl_central_table_row_step_previous_right. bcf_previous_code_bnbcpdl_central_table = bcf_quotient_bnbcpdl_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bnbcpdl_central_table_row_step))) * bcf_previous_scale_bnbcpdl_central_table) + (bcf_right_bnbcpdl_central_table_row_step))) /\ bcf_value_bnbcpdl_central_table_row_step = bcf_left_bnbcpdl_central_table_row_step + bcf_right_bnbcpdl_central_table_row_step))))))))))) /\ ((((exists bcf_height_bnbcpdl_central_decoded_row_code. bcf_height_bnbcpdl_central_decoded_row_code + S (bcf_row_code_bnbcpdl_central) = S ((S (n + n)) * bcf_row_code_scale_bnbcpdl_central)) /\ exists bcf_quotient_bnbcpdl_central_decoded_row_code. bcf_row_code_code_bnbcpdl_central = bcf_quotient_bnbcpdl_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bnbcpdl_central) + (bcf_row_code_bnbcpdl_central))) /\ ((((exists bcf_height_bnbcpdl_central_decoded_row_scale. bcf_height_bnbcpdl_central_decoded_row_scale + S (bcf_row_scale_bnbcpdl_central) = S ((S (n + n)) * bcf_row_scale_scale_bnbcpdl_central)) /\ exists bcf_quotient_bnbcpdl_central_decoded_row_scale. bcf_row_scale_code_bnbcpdl_central = bcf_quotient_bnbcpdl_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bnbcpdl_central) + (bcf_row_scale_bnbcpdl_central))) /\ (((exists bcf_height_bnbcpdl_central_decoded_value. bcf_height_bnbcpdl_central_decoded_value + S (c) = S ((S (n)) * bcf_row_scale_bnbcpdl_central)) /\ exists bcf_quotient_bnbcpdl_central_decoded_value. bcf_row_code_bnbcpdl_central = bcf_quotient_bnbcpdl_central_decoded_value * S ((S (n)) * bcf_row_scale_bnbcpdl_central) + (c))))))))) -> (exists bpr_quotient_bnbcpdl_divides. c = (p) * bpr_quotient_bnbcpdl_divides) -> (exists bpr_le_gap_bnbcpdl_result. bpr_le_gap_bnbcpdl_result + (p) = (n))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 (4)
01Fix variables and assumptionsL1–7
02Use earlier factsL8–9
03Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
cases le_total
04Use earlier factsL11–13
05Establish hcasesL14–16
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.
06Separate the logical casesL17–17
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L17
cases hcases
07Calculate and transport equalitiesL18–18
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L18
rewrite hcases_left
08Use earlier factsL19–20
09Establish hdoubleL21–29
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply central binom prime divisor le double.
10Separate the logical casesL30–30
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L30
exfalso
11Use earlier factsL31–31
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L31
apply hfree
12Separate the logical casesL32–32
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L32
split
Original defined command ledger · 35 lines
- 0001
intro n - 0002
intro c - 0003
intro p - 0004
intro hfree - 0005
intro hp - 0006
intro hcentral - 0007
intro hdivides - 0008
specialize le_total p - 0009
specialize le_total n - 0010
cases le_total - 0011
exact le_total_left - 0012
specialize le_eq_or_lt n - 0013
specialize le_eq_or_lt p - 0014
have hcases : n = p ∨ Lt(n,p)Exact native replay line
have hcases : n = p \/ exists gap. gap + S n = p - 0015
apply le_eq_or_lt - 0016
exact le_total_right - 0017
cases hcases - 0018
rewrite hcases_left - 0019
specialize le_refl p - 0020
exact le_refl - 0021
have hdouble : Le(p,n + n)Exact native replay line
have hdouble : exists gap. gap + p = n + n - 0022
specialize central_binom_prime_divisor_le_double n - 0023
specialize central_binom_prime_divisor_le_double c - 0024
specialize central_binom_prime_divisor_le_double p - 0025
apply central_binom_prime_divisor_le_double - 0026
exact hp - 0027
exact hcentral - 0028
exact hdivides - 0029
specialize hfree p - 0030
exfalso - 0031
apply hfree - 0032
split - 0033
exact hcases_right - 0034
exact hdouble - 0035
exact hp