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. ∀ s. ∀ q. ∀ c. ∀ p. (∀ x. Lt(n,x) ∧ Le(x,n + n) → ¬Prime(x)) → Prime(p) → CentralBinom(n,c) → Dvd(p,c) → Le(p,s) ∨ (Lt(s,p) ∧ Le(p,q) ∨ Lt(q,p) ∧ 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
11 occurrences
In local proof propositions
7 occurrences
Exact expanded native-PA statement
forall n s q c p. (forall bpr_prime_candidate_bnbcpdr_exclusion. ((exists bpr_gap_bnbcpdr_exclusion_lower. bpr_gap_bnbcpdr_exclusion_lower + S (n) = bpr_prime_candidate_bnbcpdr_exclusion) /\ (exists bpr_le_gap_bnbcpdr_exclusion_upper. bpr_le_gap_bnbcpdr_exclusion_upper + (bpr_prime_candidate_bnbcpdr_exclusion) = (n + n))) -> ~((~(bpr_prime_candidate_bnbcpdr_exclusion = 1) /\ forall bpr_left_bnbcpdr_exclusion_prime bpr_right_bnbcpdr_exclusion_prime. bpr_prime_candidate_bnbcpdr_exclusion = bpr_left_bnbcpdr_exclusion_prime * bpr_right_bnbcpdr_exclusion_prime -> bpr_left_bnbcpdr_exclusion_prime = 1 \/ bpr_right_bnbcpdr_exclusion_prime = 1))) -> ((~(p = 1) /\ forall bpr_left_bnbcpdr_prime bpr_right_bnbcpdr_prime. p = bpr_left_bnbcpdr_prime * bpr_right_bnbcpdr_prime -> bpr_left_bnbcpdr_prime = 1 \/ bpr_right_bnbcpdr_prime = 1)) -> (((exists bcf_lt_gap_bnbcpdr_central_out_of_range. bcf_lt_gap_bnbcpdr_central_out_of_range + S (n + n) = n) /\ c = 0) \/ ((exists bcf_le_gap_bnbcpdr_central_in_range. bcf_le_gap_bnbcpdr_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bnbcpdr_central bcf_row_code_scale_bnbcpdr_central bcf_row_scale_code_bnbcpdr_central bcf_row_scale_scale_bnbcpdr_central bcf_row_code_bnbcpdr_central bcf_row_scale_bnbcpdr_central. ((forall bcf_row_index_bnbcpdr_central_table. (exists bcf_lt_gap_bnbcpdr_central_table_row_bound. bcf_lt_gap_bnbcpdr_central_table_row_bound + S (bcf_row_index_bnbcpdr_central_table) = S (n + n)) -> exists bcf_row_code_bnbcpdr_central_table bcf_row_scale_bnbcpdr_central_table. ((((exists bcf_height_bnbcpdr_central_table_decoded_row_code. bcf_height_bnbcpdr_central_table_decoded_row_code + S (bcf_row_code_bnbcpdr_central_table) = S ((S (bcf_row_index_bnbcpdr_central_table)) * bcf_row_code_scale_bnbcpdr_central)) /\ exists bcf_quotient_bnbcpdr_central_table_decoded_row_code. bcf_row_code_code_bnbcpdr_central = bcf_quotient_bnbcpdr_central_table_decoded_row_code * S ((S (bcf_row_index_bnbcpdr_central_table)) * bcf_row_code_scale_bnbcpdr_central) + (bcf_row_code_bnbcpdr_central_table))) /\ ((((exists bcf_height_bnbcpdr_central_table_decoded_row_scale. bcf_height_bnbcpdr_central_table_decoded_row_scale + S (bcf_row_scale_bnbcpdr_central_table) = S ((S (bcf_row_index_bnbcpdr_central_table)) * bcf_row_scale_scale_bnbcpdr_central)) /\ exists bcf_quotient_bnbcpdr_central_table_decoded_row_scale. bcf_row_scale_code_bnbcpdr_central = bcf_quotient_bnbcpdr_central_table_decoded_row_scale * S ((S (bcf_row_index_bnbcpdr_central_table)) * bcf_row_scale_scale_bnbcpdr_central) + (bcf_row_scale_bnbcpdr_central_table))) /\ ((bcf_row_index_bnbcpdr_central_table = 0 /\ (forall bcf_index_bnbcpdr_central_table_zero_row. (exists bcf_lt_gap_bnbcpdr_central_table_zero_row_bound. bcf_lt_gap_bnbcpdr_central_table_zero_row_bound + S (bcf_index_bnbcpdr_central_table_zero_row) = S (n + n)) -> exists bcf_value_bnbcpdr_central_table_zero_row. ((((exists bcf_height_bnbcpdr_central_table_zero_row_entry. bcf_height_bnbcpdr_central_table_zero_row_entry + S (bcf_value_bnbcpdr_central_table_zero_row) = S ((S (bcf_index_bnbcpdr_central_table_zero_row)) * bcf_row_scale_bnbcpdr_central_table)) /\ exists bcf_quotient_bnbcpdr_central_table_zero_row_entry. bcf_row_code_bnbcpdr_central_table = bcf_quotient_bnbcpdr_central_table_zero_row_entry * S ((S (bcf_index_bnbcpdr_central_table_zero_row)) * bcf_row_scale_bnbcpdr_central_table) + (bcf_value_bnbcpdr_central_table_zero_row))) /\ ((bcf_index_bnbcpdr_central_table_zero_row = 0 /\ bcf_value_bnbcpdr_central_table_zero_row = 1) \/ exists bcf_predecessor_bnbcpdr_central_table_zero_row. bcf_index_bnbcpdr_central_table_zero_row = S bcf_predecessor_bnbcpdr_central_table_zero_row /\ bcf_value_bnbcpdr_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bnbcpdr_central_table bcf_previous_code_bnbcpdr_central_table bcf_previous_scale_bnbcpdr_central_table. bcf_row_index_bnbcpdr_central_table = S bcf_predecessor_bnbcpdr_central_table /\ ((((exists bcf_height_bnbcpdr_central_table_decoded_previous_code. bcf_height_bnbcpdr_central_table_decoded_previous_code + S (bcf_previous_code_bnbcpdr_central_table) = S ((S (bcf_predecessor_bnbcpdr_central_table)) * bcf_row_code_scale_bnbcpdr_central)) /\ exists bcf_quotient_bnbcpdr_central_table_decoded_previous_code. bcf_row_code_code_bnbcpdr_central = bcf_quotient_bnbcpdr_central_table_decoded_previous_code * S ((S (bcf_predecessor_bnbcpdr_central_table)) * bcf_row_code_scale_bnbcpdr_central) + (bcf_previous_code_bnbcpdr_central_table))) /\ ((((exists bcf_height_bnbcpdr_central_table_decoded_previous_scale. bcf_height_bnbcpdr_central_table_decoded_previous_scale + S (bcf_previous_scale_bnbcpdr_central_table) = S ((S (bcf_predecessor_bnbcpdr_central_table)) * bcf_row_scale_scale_bnbcpdr_central)) /\ exists bcf_quotient_bnbcpdr_central_table_decoded_previous_scale. bcf_row_scale_code_bnbcpdr_central = bcf_quotient_bnbcpdr_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bnbcpdr_central_table)) * bcf_row_scale_scale_bnbcpdr_central) + (bcf_previous_scale_bnbcpdr_central_table))) /\ (forall bcf_index_bnbcpdr_central_table_row_step. (exists bcf_lt_gap_bnbcpdr_central_table_row_step_bound. bcf_lt_gap_bnbcpdr_central_table_row_step_bound + S (bcf_index_bnbcpdr_central_table_row_step) = S (n + n)) -> exists bcf_value_bnbcpdr_central_table_row_step. ((((exists bcf_height_bnbcpdr_central_table_row_step_entry. bcf_height_bnbcpdr_central_table_row_step_entry + S (bcf_value_bnbcpdr_central_table_row_step) = S ((S (bcf_index_bnbcpdr_central_table_row_step)) * bcf_row_scale_bnbcpdr_central_table)) /\ exists bcf_quotient_bnbcpdr_central_table_row_step_entry. bcf_row_code_bnbcpdr_central_table = bcf_quotient_bnbcpdr_central_table_row_step_entry * S ((S (bcf_index_bnbcpdr_central_table_row_step)) * bcf_row_scale_bnbcpdr_central_table) + (bcf_value_bnbcpdr_central_table_row_step))) /\ ((bcf_index_bnbcpdr_central_table_row_step = 0 /\ bcf_value_bnbcpdr_central_table_row_step = 1) \/ exists bcf_predecessor_bnbcpdr_central_table_row_step bcf_left_bnbcpdr_central_table_row_step bcf_right_bnbcpdr_central_table_row_step. bcf_index_bnbcpdr_central_table_row_step = S bcf_predecessor_bnbcpdr_central_table_row_step /\ ((((exists bcf_height_bnbcpdr_central_table_row_step_previous_left. bcf_height_bnbcpdr_central_table_row_step_previous_left + S (bcf_left_bnbcpdr_central_table_row_step) = S ((S (bcf_predecessor_bnbcpdr_central_table_row_step)) * bcf_previous_scale_bnbcpdr_central_table)) /\ exists bcf_quotient_bnbcpdr_central_table_row_step_previous_left. bcf_previous_code_bnbcpdr_central_table = bcf_quotient_bnbcpdr_central_table_row_step_previous_left * S ((S (bcf_predecessor_bnbcpdr_central_table_row_step)) * bcf_previous_scale_bnbcpdr_central_table) + (bcf_left_bnbcpdr_central_table_row_step))) /\ ((((exists bcf_height_bnbcpdr_central_table_row_step_previous_right. bcf_height_bnbcpdr_central_table_row_step_previous_right + S (bcf_right_bnbcpdr_central_table_row_step) = S ((S (S (bcf_predecessor_bnbcpdr_central_table_row_step))) * bcf_previous_scale_bnbcpdr_central_table)) /\ exists bcf_quotient_bnbcpdr_central_table_row_step_previous_right. bcf_previous_code_bnbcpdr_central_table = bcf_quotient_bnbcpdr_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bnbcpdr_central_table_row_step))) * bcf_previous_scale_bnbcpdr_central_table) + (bcf_right_bnbcpdr_central_table_row_step))) /\ bcf_value_bnbcpdr_central_table_row_step = bcf_left_bnbcpdr_central_table_row_step + bcf_right_bnbcpdr_central_table_row_step))))))))))) /\ ((((exists bcf_height_bnbcpdr_central_decoded_row_code. bcf_height_bnbcpdr_central_decoded_row_code + S (bcf_row_code_bnbcpdr_central) = S ((S (n + n)) * bcf_row_code_scale_bnbcpdr_central)) /\ exists bcf_quotient_bnbcpdr_central_decoded_row_code. bcf_row_code_code_bnbcpdr_central = bcf_quotient_bnbcpdr_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bnbcpdr_central) + (bcf_row_code_bnbcpdr_central))) /\ ((((exists bcf_height_bnbcpdr_central_decoded_row_scale. bcf_height_bnbcpdr_central_decoded_row_scale + S (bcf_row_scale_bnbcpdr_central) = S ((S (n + n)) * bcf_row_scale_scale_bnbcpdr_central)) /\ exists bcf_quotient_bnbcpdr_central_decoded_row_scale. bcf_row_scale_code_bnbcpdr_central = bcf_quotient_bnbcpdr_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bnbcpdr_central) + (bcf_row_scale_bnbcpdr_central))) /\ (((exists bcf_height_bnbcpdr_central_decoded_value. bcf_height_bnbcpdr_central_decoded_value + S (c) = S ((S (n)) * bcf_row_scale_bnbcpdr_central)) /\ exists bcf_quotient_bnbcpdr_central_decoded_value. bcf_row_code_bnbcpdr_central = bcf_quotient_bnbcpdr_central_decoded_value * S ((S (n)) * bcf_row_scale_bnbcpdr_central) + (c))))))))) -> (exists bpr_quotient_bnbcpdr_divides. c = (p) * bpr_quotient_bnbcpdr_divides) -> ((exists bpr_le_gap_bnbcpdr_small. bpr_le_gap_bnbcpdr_small + (p) = (s)) \/ (((exists bpr_gap_bnbcpdr_above_small. bpr_gap_bnbcpdr_above_small + S (s) = p) /\ (exists bpr_le_gap_bnbcpdr_middle_bound. bpr_le_gap_bnbcpdr_middle_bound + (p) = (q))) \/ ((exists bpr_gap_bnbcpdr_above_middle. bpr_gap_bnbcpdr_above_middle + S (q) = p) /\ (exists bpr_le_gap_bnbcpdr_row_bound. bpr_le_gap_bnbcpdr_row_bound + (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–9
02Establish hrowL10–18
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply no bertrand central prime divisor le.
03Establish hpsL19–22
04Separate the logical casesL23–24
05Use earlier factsL25–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
exact hps_left
06Establish hsmall_casesL26–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.
07Separate the logical casesL31–32
08Calculate and transport equalitiesL33–33
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L33
rewrite hsmall_cases_left
09Use earlier factsL34–35
10Establish hpqL36–39
11Separate the logical casesL40–43
12Use earlier factsL44–45
13Establish hmiddle_casesL46–50
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.
14Separate the logical casesL51–54
15Use earlier factsL55–55
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L55
exact hsmall_cases_right
16Calculate and transport equalitiesL56–56
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L56
rewrite hmiddle_cases_left
17Use earlier factsL57–58
18Separate the logical casesL59–61
Original defined command ledger · 63 lines
- 0001
intro n - 0002
intro s - 0003
intro q - 0004
intro c - 0005
intro p - 0006
intro hfree - 0007
intro hp - 0008
intro hcentral - 0009
intro hdivides - 0010
have hrow : Le(p,n)Exact native replay line
have hrow : exists bpr_le_gap_bnbcpdr_row_bound. bpr_le_gap_bnbcpdr_row_bound + (p) = (n) - 0011
specialize no_bertrand_central_prime_divisor_le n - 0012
specialize no_bertrand_central_prime_divisor_le c - 0013
specialize no_bertrand_central_prime_divisor_le p - 0014
apply no_bertrand_central_prime_divisor_le - 0015
exact hfree - 0016
exact hp - 0017
exact hcentral - 0018
exact hdivides - 0019
have hps : Le(p,s) ∨ Le(s,p)Exact native replay line
have hps : (exists a. a + p = s) \/ exists b. b + s = p - 0020
specialize le_total p - 0021
specialize le_total s - 0022
exact le_total - 0023
cases hps - 0024
left - 0025
exact hps_left - 0026
have hsmall_cases : s = p ∨ Lt(s,p)Exact native replay line
have hsmall_cases : s = p \/ exists g. g + S s = p - 0027
specialize le_eq_or_lt s - 0028
specialize le_eq_or_lt p - 0029
apply le_eq_or_lt - 0030
exact hps_right - 0031
cases hsmall_cases - 0032
left - 0033
rewrite hsmall_cases_left - 0034
specialize le_refl p - 0035
exact le_refl - 0036
have hpq : Le(p,q) ∨ Le(q,p)Exact native replay line
have hpq : (exists a. a + p = q) \/ exists b. b + q = p - 0037
specialize le_total p - 0038
specialize le_total q - 0039
exact le_total - 0040
cases hpq - 0041
right - 0042
left - 0043
split - 0044
exact hsmall_cases_right - 0045
exact hpq_left - 0046
have hmiddle_cases : q = p ∨ Lt(q,p)Exact native replay line
have hmiddle_cases : q = p \/ exists g. g + S q = p - 0047
specialize le_eq_or_lt q - 0048
specialize le_eq_or_lt p - 0049
apply le_eq_or_lt - 0050
exact hpq_right - 0051
cases hmiddle_cases - 0052
right - 0053
left - 0054
split - 0055
exact hsmall_cases_right - 0056
rewrite hmiddle_cases_left - 0057
specialize le_refl p - 0058
exact le_refl - 0059
right - 0060
right - 0061
split - 0062
exact hmiddle_cases_right - 0063
exact hrow