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. Prime(p) → CentralBinom(n,c) → Dvd(p,c) → Le(p,n + 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
4 occurrences
In local proof propositions
4 occurrences
Exact expanded native-PA statement
forall n c p. ((~(p = 1) /\ forall bpr_left_bcpdl_prime bpr_right_bcpdl_prime. p = bpr_left_bcpdl_prime * bpr_right_bcpdl_prime -> bpr_left_bcpdl_prime = 1 \/ bpr_right_bcpdl_prime = 1)) -> (((exists bcf_lt_gap_bcpdl_central_out_of_range. bcf_lt_gap_bcpdl_central_out_of_range + S (n + n) = n) /\ c = 0) \/ ((exists bcf_le_gap_bcpdl_central_in_range. bcf_le_gap_bcpdl_central_in_range + (n) = n + n) /\ (exists bcf_row_code_code_bcpdl_central bcf_row_code_scale_bcpdl_central bcf_row_scale_code_bcpdl_central bcf_row_scale_scale_bcpdl_central bcf_row_code_bcpdl_central bcf_row_scale_bcpdl_central. ((forall bcf_row_index_bcpdl_central_table. (exists bcf_lt_gap_bcpdl_central_table_row_bound. bcf_lt_gap_bcpdl_central_table_row_bound + S (bcf_row_index_bcpdl_central_table) = S (n + n)) -> exists bcf_row_code_bcpdl_central_table bcf_row_scale_bcpdl_central_table. ((((exists bcf_height_bcpdl_central_table_decoded_row_code. bcf_height_bcpdl_central_table_decoded_row_code + S (bcf_row_code_bcpdl_central_table) = S ((S (bcf_row_index_bcpdl_central_table)) * bcf_row_code_scale_bcpdl_central)) /\ exists bcf_quotient_bcpdl_central_table_decoded_row_code. bcf_row_code_code_bcpdl_central = bcf_quotient_bcpdl_central_table_decoded_row_code * S ((S (bcf_row_index_bcpdl_central_table)) * bcf_row_code_scale_bcpdl_central) + (bcf_row_code_bcpdl_central_table))) /\ ((((exists bcf_height_bcpdl_central_table_decoded_row_scale. bcf_height_bcpdl_central_table_decoded_row_scale + S (bcf_row_scale_bcpdl_central_table) = S ((S (bcf_row_index_bcpdl_central_table)) * bcf_row_scale_scale_bcpdl_central)) /\ exists bcf_quotient_bcpdl_central_table_decoded_row_scale. bcf_row_scale_code_bcpdl_central = bcf_quotient_bcpdl_central_table_decoded_row_scale * S ((S (bcf_row_index_bcpdl_central_table)) * bcf_row_scale_scale_bcpdl_central) + (bcf_row_scale_bcpdl_central_table))) /\ ((bcf_row_index_bcpdl_central_table = 0 /\ (forall bcf_index_bcpdl_central_table_zero_row. (exists bcf_lt_gap_bcpdl_central_table_zero_row_bound. bcf_lt_gap_bcpdl_central_table_zero_row_bound + S (bcf_index_bcpdl_central_table_zero_row) = S (n + n)) -> exists bcf_value_bcpdl_central_table_zero_row. ((((exists bcf_height_bcpdl_central_table_zero_row_entry. bcf_height_bcpdl_central_table_zero_row_entry + S (bcf_value_bcpdl_central_table_zero_row) = S ((S (bcf_index_bcpdl_central_table_zero_row)) * bcf_row_scale_bcpdl_central_table)) /\ exists bcf_quotient_bcpdl_central_table_zero_row_entry. bcf_row_code_bcpdl_central_table = bcf_quotient_bcpdl_central_table_zero_row_entry * S ((S (bcf_index_bcpdl_central_table_zero_row)) * bcf_row_scale_bcpdl_central_table) + (bcf_value_bcpdl_central_table_zero_row))) /\ ((bcf_index_bcpdl_central_table_zero_row = 0 /\ bcf_value_bcpdl_central_table_zero_row = 1) \/ exists bcf_predecessor_bcpdl_central_table_zero_row. bcf_index_bcpdl_central_table_zero_row = S bcf_predecessor_bcpdl_central_table_zero_row /\ bcf_value_bcpdl_central_table_zero_row = 0)))) \/ exists bcf_predecessor_bcpdl_central_table bcf_previous_code_bcpdl_central_table bcf_previous_scale_bcpdl_central_table. bcf_row_index_bcpdl_central_table = S bcf_predecessor_bcpdl_central_table /\ ((((exists bcf_height_bcpdl_central_table_decoded_previous_code. bcf_height_bcpdl_central_table_decoded_previous_code + S (bcf_previous_code_bcpdl_central_table) = S ((S (bcf_predecessor_bcpdl_central_table)) * bcf_row_code_scale_bcpdl_central)) /\ exists bcf_quotient_bcpdl_central_table_decoded_previous_code. bcf_row_code_code_bcpdl_central = bcf_quotient_bcpdl_central_table_decoded_previous_code * S ((S (bcf_predecessor_bcpdl_central_table)) * bcf_row_code_scale_bcpdl_central) + (bcf_previous_code_bcpdl_central_table))) /\ ((((exists bcf_height_bcpdl_central_table_decoded_previous_scale. bcf_height_bcpdl_central_table_decoded_previous_scale + S (bcf_previous_scale_bcpdl_central_table) = S ((S (bcf_predecessor_bcpdl_central_table)) * bcf_row_scale_scale_bcpdl_central)) /\ exists bcf_quotient_bcpdl_central_table_decoded_previous_scale. bcf_row_scale_code_bcpdl_central = bcf_quotient_bcpdl_central_table_decoded_previous_scale * S ((S (bcf_predecessor_bcpdl_central_table)) * bcf_row_scale_scale_bcpdl_central) + (bcf_previous_scale_bcpdl_central_table))) /\ (forall bcf_index_bcpdl_central_table_row_step. (exists bcf_lt_gap_bcpdl_central_table_row_step_bound. bcf_lt_gap_bcpdl_central_table_row_step_bound + S (bcf_index_bcpdl_central_table_row_step) = S (n + n)) -> exists bcf_value_bcpdl_central_table_row_step. ((((exists bcf_height_bcpdl_central_table_row_step_entry. bcf_height_bcpdl_central_table_row_step_entry + S (bcf_value_bcpdl_central_table_row_step) = S ((S (bcf_index_bcpdl_central_table_row_step)) * bcf_row_scale_bcpdl_central_table)) /\ exists bcf_quotient_bcpdl_central_table_row_step_entry. bcf_row_code_bcpdl_central_table = bcf_quotient_bcpdl_central_table_row_step_entry * S ((S (bcf_index_bcpdl_central_table_row_step)) * bcf_row_scale_bcpdl_central_table) + (bcf_value_bcpdl_central_table_row_step))) /\ ((bcf_index_bcpdl_central_table_row_step = 0 /\ bcf_value_bcpdl_central_table_row_step = 1) \/ exists bcf_predecessor_bcpdl_central_table_row_step bcf_left_bcpdl_central_table_row_step bcf_right_bcpdl_central_table_row_step. bcf_index_bcpdl_central_table_row_step = S bcf_predecessor_bcpdl_central_table_row_step /\ ((((exists bcf_height_bcpdl_central_table_row_step_previous_left. bcf_height_bcpdl_central_table_row_step_previous_left + S (bcf_left_bcpdl_central_table_row_step) = S ((S (bcf_predecessor_bcpdl_central_table_row_step)) * bcf_previous_scale_bcpdl_central_table)) /\ exists bcf_quotient_bcpdl_central_table_row_step_previous_left. bcf_previous_code_bcpdl_central_table = bcf_quotient_bcpdl_central_table_row_step_previous_left * S ((S (bcf_predecessor_bcpdl_central_table_row_step)) * bcf_previous_scale_bcpdl_central_table) + (bcf_left_bcpdl_central_table_row_step))) /\ ((((exists bcf_height_bcpdl_central_table_row_step_previous_right. bcf_height_bcpdl_central_table_row_step_previous_right + S (bcf_right_bcpdl_central_table_row_step) = S ((S (S (bcf_predecessor_bcpdl_central_table_row_step))) * bcf_previous_scale_bcpdl_central_table)) /\ exists bcf_quotient_bcpdl_central_table_row_step_previous_right. bcf_previous_code_bcpdl_central_table = bcf_quotient_bcpdl_central_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcpdl_central_table_row_step))) * bcf_previous_scale_bcpdl_central_table) + (bcf_right_bcpdl_central_table_row_step))) /\ bcf_value_bcpdl_central_table_row_step = bcf_left_bcpdl_central_table_row_step + bcf_right_bcpdl_central_table_row_step))))))))))) /\ ((((exists bcf_height_bcpdl_central_decoded_row_code. bcf_height_bcpdl_central_decoded_row_code + S (bcf_row_code_bcpdl_central) = S ((S (n + n)) * bcf_row_code_scale_bcpdl_central)) /\ exists bcf_quotient_bcpdl_central_decoded_row_code. bcf_row_code_code_bcpdl_central = bcf_quotient_bcpdl_central_decoded_row_code * S ((S (n + n)) * bcf_row_code_scale_bcpdl_central) + (bcf_row_code_bcpdl_central))) /\ ((((exists bcf_height_bcpdl_central_decoded_row_scale. bcf_height_bcpdl_central_decoded_row_scale + S (bcf_row_scale_bcpdl_central) = S ((S (n + n)) * bcf_row_scale_scale_bcpdl_central)) /\ exists bcf_quotient_bcpdl_central_decoded_row_scale. bcf_row_scale_code_bcpdl_central = bcf_quotient_bcpdl_central_decoded_row_scale * S ((S (n + n)) * bcf_row_scale_scale_bcpdl_central) + (bcf_row_scale_bcpdl_central))) /\ (((exists bcf_height_bcpdl_central_decoded_value. bcf_height_bcpdl_central_decoded_value + S (c) = S ((S (n)) * bcf_row_scale_bcpdl_central)) /\ exists bcf_quotient_bcpdl_central_decoded_value. bcf_row_code_bcpdl_central = bcf_quotient_bcpdl_central_decoded_value * S ((S (n)) * bcf_row_scale_bcpdl_central) + (c))))))))) -> (exists bpr_quotient_bcpdl_divides. c = (p) * bpr_quotient_bcpdl_divides) -> (exists bpr_le_gap_bcpdl_result. bpr_le_gap_bcpdl_result + (p) = (n + n))Proof neighborhood
Direct theorem prerequisites
BT008Y factorial_exists BT00TX choose_factorial_bridge BT0006 mul_comm BT002C multiple_trans BT00VB factorial_prime_le_of_dividesDirect 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 (5)
01Fix variables and assumptionsL1–6
02Establish hFL7–9
Establish this local claim before using it. It is not an additional assumption.
- L7
have hF : ∃ F. Factorial(n + n,F)Definitions: Factorial(n + n,F)Original native command in the exact edition - L8
specialize factorial_exists (n + n) - L9
exact factorial_exists
03Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
cases hF
04Establish hKL11–13
Establish this local claim before using it. It is not an additional assumption.
- L11
have hK : ∃ K. Factorial(n,K)Definitions: Factorial(n,K)Original native command in the exact edition - L12
specialize factorial_exists n - L13
exact factorial_exists
05Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
cases hK
06Establish hbridgeL15–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply choose factorial bridge.
- L15
have hbridge : x = (x1 * x1) * c - L16
specialize choose_factorial_bridge (n + n) - L17
specialize choose_factorial_bridge n - L18
specialize choose_factorial_bridge n - L19
specialize choose_factorial_bridge c - L20
specialize choose_factorial_bridge x - L21
specialize choose_factorial_bridge x1 - L22
specialize choose_factorial_bridge x1 - L23
apply choose_factorial_bridge - L24
refl
07Use earlier factsL25–28
08Establish hcentral_factorL29–29
Establish this local claim before using it. It is not an additional assumption.
09Construct an explicit witnessL30–30
Supply the displayed value, then prove that it has the required property.
- L30
exists (x1 * x1)
10Calculate and transport equalitiesL31–31
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L31
trans (x1 * x1) * c
11Use earlier factsL32–33
12Establish hprime_factorL34–43
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple trans.
Original defined command ledger · 47 lines
- 0001
intro n - 0002
intro c - 0003
intro p - 0004
intro hp - 0005
intro hcentral - 0006
intro hdivides - 0007
have hF : ∃ F. Factorial(n + n,F)Exact native replay line
have hF : exists F. (exists ff_b_bcpdl_total_factorial ff_c_bcpdl_total_factorial. ((forall ff_i_bcpdl_total_factorial_range. (exists ff_lt_bcpdl_total_factorial_range_bound. ff_lt_bcpdl_total_factorial_range_bound + S ff_i_bcpdl_total_factorial_range = (n + n)) -> (((exists ff_h_bcpdl_total_factorial_range_decoded. ff_h_bcpdl_total_factorial_range_decoded + S (1 + ff_i_bcpdl_total_factorial_range) = S ((S (ff_i_bcpdl_total_factorial_range)) * ff_c_bcpdl_total_factorial)) /\ exists ff_q_bcpdl_total_factorial_range_decoded. ff_b_bcpdl_total_factorial = ff_q_bcpdl_total_factorial_range_decoded * S ((S (ff_i_bcpdl_total_factorial_range)) * ff_c_bcpdl_total_factorial) + (1 + ff_i_bcpdl_total_factorial_range)))) /\ (exists ff_u_bcpdl_total_factorial_product ff_v_bcpdl_total_factorial_product. ((((exists ff_h_bcpdl_total_factorial_product_start. ff_h_bcpdl_total_factorial_product_start + S (1) = S ((S (0)) * ff_v_bcpdl_total_factorial_product)) /\ exists ff_q_bcpdl_total_factorial_product_start. ff_u_bcpdl_total_factorial_product = ff_q_bcpdl_total_factorial_product_start * S ((S (0)) * ff_v_bcpdl_total_factorial_product) + (1))) /\ ((((exists ff_h_bcpdl_total_factorial_product_terminal. ff_h_bcpdl_total_factorial_product_terminal + S (F) = S ((S ((n + n))) * ff_v_bcpdl_total_factorial_product)) /\ exists ff_q_bcpdl_total_factorial_product_terminal. ff_u_bcpdl_total_factorial_product = ff_q_bcpdl_total_factorial_product_terminal * S ((S ((n + n))) * ff_v_bcpdl_total_factorial_product) + (F))) /\ forall ff_i_bcpdl_total_factorial_product. (exists ff_lt_bcpdl_total_factorial_product_bound. ff_lt_bcpdl_total_factorial_product_bound + S ff_i_bcpdl_total_factorial_product = (n + n)) -> exists ff_p_bcpdl_total_factorial_product ff_r_bcpdl_total_factorial_product ff_s_bcpdl_total_factorial_product. ((((exists ff_h_bcpdl_total_factorial_product_factor. ff_h_bcpdl_total_factorial_product_factor + S (ff_p_bcpdl_total_factorial_product) = S ((S (ff_i_bcpdl_total_factorial_product)) * ff_c_bcpdl_total_factorial)) /\ exists ff_q_bcpdl_total_factorial_product_factor. ff_b_bcpdl_total_factorial = ff_q_bcpdl_total_factorial_product_factor * S ((S (ff_i_bcpdl_total_factorial_product)) * ff_c_bcpdl_total_factorial) + (ff_p_bcpdl_total_factorial_product))) /\ ((((exists ff_h_bcpdl_total_factorial_product_partial. ff_h_bcpdl_total_factorial_product_partial + S (ff_r_bcpdl_total_factorial_product) = S ((S (ff_i_bcpdl_total_factorial_product)) * ff_v_bcpdl_total_factorial_product)) /\ exists ff_q_bcpdl_total_factorial_product_partial. ff_u_bcpdl_total_factorial_product = ff_q_bcpdl_total_factorial_product_partial * S ((S (ff_i_bcpdl_total_factorial_product)) * ff_v_bcpdl_total_factorial_product) + (ff_r_bcpdl_total_factorial_product))) /\ ((((exists ff_h_bcpdl_total_factorial_product_successor. ff_h_bcpdl_total_factorial_product_successor + S (ff_s_bcpdl_total_factorial_product) = S ((S (S ff_i_bcpdl_total_factorial_product)) * ff_v_bcpdl_total_factorial_product)) /\ exists ff_q_bcpdl_total_factorial_product_successor. ff_u_bcpdl_total_factorial_product = ff_q_bcpdl_total_factorial_product_successor * S ((S (S ff_i_bcpdl_total_factorial_product)) * ff_v_bcpdl_total_factorial_product) + (ff_s_bcpdl_total_factorial_product))) /\ ff_s_bcpdl_total_factorial_product = ff_r_bcpdl_total_factorial_product * ff_p_bcpdl_total_factorial_product)))))))) - 0008
specialize factorial_exists (n + n) - 0009
exact factorial_exists - 0010
cases hF - 0011
have hK : ∃ K. Factorial(n,K)Exact native replay line
have hK : exists K. (exists ff_b_bcpdl_column_factorial ff_c_bcpdl_column_factorial. ((forall ff_i_bcpdl_column_factorial_range. (exists ff_lt_bcpdl_column_factorial_range_bound. ff_lt_bcpdl_column_factorial_range_bound + S ff_i_bcpdl_column_factorial_range = (n)) -> (((exists ff_h_bcpdl_column_factorial_range_decoded. ff_h_bcpdl_column_factorial_range_decoded + S (1 + ff_i_bcpdl_column_factorial_range) = S ((S (ff_i_bcpdl_column_factorial_range)) * ff_c_bcpdl_column_factorial)) /\ exists ff_q_bcpdl_column_factorial_range_decoded. ff_b_bcpdl_column_factorial = ff_q_bcpdl_column_factorial_range_decoded * S ((S (ff_i_bcpdl_column_factorial_range)) * ff_c_bcpdl_column_factorial) + (1 + ff_i_bcpdl_column_factorial_range)))) /\ (exists ff_u_bcpdl_column_factorial_product ff_v_bcpdl_column_factorial_product. ((((exists ff_h_bcpdl_column_factorial_product_start. ff_h_bcpdl_column_factorial_product_start + S (1) = S ((S (0)) * ff_v_bcpdl_column_factorial_product)) /\ exists ff_q_bcpdl_column_factorial_product_start. ff_u_bcpdl_column_factorial_product = ff_q_bcpdl_column_factorial_product_start * S ((S (0)) * ff_v_bcpdl_column_factorial_product) + (1))) /\ ((((exists ff_h_bcpdl_column_factorial_product_terminal. ff_h_bcpdl_column_factorial_product_terminal + S (K) = S ((S ((n))) * ff_v_bcpdl_column_factorial_product)) /\ exists ff_q_bcpdl_column_factorial_product_terminal. ff_u_bcpdl_column_factorial_product = ff_q_bcpdl_column_factorial_product_terminal * S ((S ((n))) * ff_v_bcpdl_column_factorial_product) + (K))) /\ forall ff_i_bcpdl_column_factorial_product. (exists ff_lt_bcpdl_column_factorial_product_bound. ff_lt_bcpdl_column_factorial_product_bound + S ff_i_bcpdl_column_factorial_product = (n)) -> exists ff_p_bcpdl_column_factorial_product ff_r_bcpdl_column_factorial_product ff_s_bcpdl_column_factorial_product. ((((exists ff_h_bcpdl_column_factorial_product_factor. ff_h_bcpdl_column_factorial_product_factor + S (ff_p_bcpdl_column_factorial_product) = S ((S (ff_i_bcpdl_column_factorial_product)) * ff_c_bcpdl_column_factorial)) /\ exists ff_q_bcpdl_column_factorial_product_factor. ff_b_bcpdl_column_factorial = ff_q_bcpdl_column_factorial_product_factor * S ((S (ff_i_bcpdl_column_factorial_product)) * ff_c_bcpdl_column_factorial) + (ff_p_bcpdl_column_factorial_product))) /\ ((((exists ff_h_bcpdl_column_factorial_product_partial. ff_h_bcpdl_column_factorial_product_partial + S (ff_r_bcpdl_column_factorial_product) = S ((S (ff_i_bcpdl_column_factorial_product)) * ff_v_bcpdl_column_factorial_product)) /\ exists ff_q_bcpdl_column_factorial_product_partial. ff_u_bcpdl_column_factorial_product = ff_q_bcpdl_column_factorial_product_partial * S ((S (ff_i_bcpdl_column_factorial_product)) * ff_v_bcpdl_column_factorial_product) + (ff_r_bcpdl_column_factorial_product))) /\ ((((exists ff_h_bcpdl_column_factorial_product_successor. ff_h_bcpdl_column_factorial_product_successor + S (ff_s_bcpdl_column_factorial_product) = S ((S (S ff_i_bcpdl_column_factorial_product)) * ff_v_bcpdl_column_factorial_product)) /\ exists ff_q_bcpdl_column_factorial_product_successor. ff_u_bcpdl_column_factorial_product = ff_q_bcpdl_column_factorial_product_successor * S ((S (S ff_i_bcpdl_column_factorial_product)) * ff_v_bcpdl_column_factorial_product) + (ff_s_bcpdl_column_factorial_product))) /\ ff_s_bcpdl_column_factorial_product = ff_r_bcpdl_column_factorial_product * ff_p_bcpdl_column_factorial_product)))))))) - 0012
specialize factorial_exists n - 0013
exact factorial_exists - 0014
cases hK - 0015
have hbridge : x = (x1 * x1) * c - 0016
specialize choose_factorial_bridge (n + n) - 0017
specialize choose_factorial_bridge n - 0018
specialize choose_factorial_bridge n - 0019
specialize choose_factorial_bridge c - 0020
specialize choose_factorial_bridge x - 0021
specialize choose_factorial_bridge x1 - 0022
specialize choose_factorial_bridge x1 - 0023
apply choose_factorial_bridge - 0024
refl - 0025
exact hcentral - 0026
exact hF_witness - 0027
exact hK_witness - 0028
exact hK_witness - 0029
have hcentral_factor : Dvd(c,x)Exact native replay line
have hcentral_factor : exists bpr_quotient_bcpdl_central_divides_total. x = (c) * bpr_quotient_bcpdl_central_divides_total - 0030
exists (x1 * x1) - 0031
trans (x1 * x1) * c - 0032
exact hbridge - 0033
apply mul_comm - 0034
have hprime_factor : Dvd(p,x)Exact native replay line
have hprime_factor : exists bpr_quotient_bcpdl_prime_divides_total. x = (p) * bpr_quotient_bcpdl_prime_divides_total - 0035
specialize multiple_trans c - 0036
specialize multiple_trans p - 0037
specialize multiple_trans x - 0038
apply multiple_trans - 0039
exact hcentral_factor - 0040
exact hdivides - 0041
specialize factorial_prime_le_of_divides p - 0042
specialize factorial_prime_le_of_divides (n + n) - 0043
specialize factorial_prime_le_of_divides x - 0044
apply factorial_prime_le_of_divides - 0045
exact hp - 0046
exact hF_witness - 0047
exact hprime_factor