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. ∀ a. ∀ b. ∀ C. Prime(p) → Lt(a,p) → Lt(b,p) → Le(p,a + b) → Choose(a + b,a,C) → Dvd(p,C)Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
none
Exact expanded first-order statement
forall p a b C. ((~(p = 1) /\ forall frm_prime_left_lucas_digit_prime frm_prime_right_lucas_digit_prime. p = frm_prime_left_lucas_digit_prime * frm_prime_right_lucas_digit_prime -> frm_prime_left_lucas_digit_prime = 1 \/ frm_prime_right_lucas_digit_prime = 1)) -> (exists ldc_lt_left. ldc_lt_left + S (a) = p) -> (exists ldc_lt_right. ldc_lt_right + S (b) = p) -> (exists ldc_le_carry. ldc_le_carry + (p) = a + b) -> (((exists bcf_lt_gap_lucas_digit_choose_out_of_range. bcf_lt_gap_lucas_digit_choose_out_of_range + S (a + b) = a) /\ C = 0) \/ ((exists bcf_le_gap_lucas_digit_choose_in_range. bcf_le_gap_lucas_digit_choose_in_range + (a) = a + b) /\ (exists bcf_row_code_code_lucas_digit_choose bcf_row_code_scale_lucas_digit_choose bcf_row_scale_code_lucas_digit_choose bcf_row_scale_scale_lucas_digit_choose bcf_row_code_lucas_digit_choose bcf_row_scale_lucas_digit_choose. ((forall bcf_row_index_lucas_digit_choose_table. (exists bcf_lt_gap_lucas_digit_choose_table_row_bound. bcf_lt_gap_lucas_digit_choose_table_row_bound + S (bcf_row_index_lucas_digit_choose_table) = S (a + b)) -> exists bcf_row_code_lucas_digit_choose_table bcf_row_scale_lucas_digit_choose_table. ((((exists bcf_height_lucas_digit_choose_table_decoded_row_code. bcf_height_lucas_digit_choose_table_decoded_row_code + S (bcf_row_code_lucas_digit_choose_table) = S ((S (bcf_row_index_lucas_digit_choose_table)) * bcf_row_code_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_table_decoded_row_code. bcf_row_code_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_table_decoded_row_code * S ((S (bcf_row_index_lucas_digit_choose_table)) * bcf_row_code_scale_lucas_digit_choose) + (bcf_row_code_lucas_digit_choose_table))) /\ ((((exists bcf_height_lucas_digit_choose_table_decoded_row_scale. bcf_height_lucas_digit_choose_table_decoded_row_scale + S (bcf_row_scale_lucas_digit_choose_table) = S ((S (bcf_row_index_lucas_digit_choose_table)) * bcf_row_scale_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_table_decoded_row_scale. bcf_row_scale_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_table_decoded_row_scale * S ((S (bcf_row_index_lucas_digit_choose_table)) * bcf_row_scale_scale_lucas_digit_choose) + (bcf_row_scale_lucas_digit_choose_table))) /\ ((bcf_row_index_lucas_digit_choose_table = 0 /\ (forall bcf_index_lucas_digit_choose_table_zero_row. (exists bcf_lt_gap_lucas_digit_choose_table_zero_row_bound. bcf_lt_gap_lucas_digit_choose_table_zero_row_bound + S (bcf_index_lucas_digit_choose_table_zero_row) = S (a + b)) -> exists bcf_value_lucas_digit_choose_table_zero_row. ((((exists bcf_height_lucas_digit_choose_table_zero_row_entry. bcf_height_lucas_digit_choose_table_zero_row_entry + S (bcf_value_lucas_digit_choose_table_zero_row) = S ((S (bcf_index_lucas_digit_choose_table_zero_row)) * bcf_row_scale_lucas_digit_choose_table)) /\ exists bcf_quotient_lucas_digit_choose_table_zero_row_entry. bcf_row_code_lucas_digit_choose_table = bcf_quotient_lucas_digit_choose_table_zero_row_entry * S ((S (bcf_index_lucas_digit_choose_table_zero_row)) * bcf_row_scale_lucas_digit_choose_table) + (bcf_value_lucas_digit_choose_table_zero_row))) /\ ((bcf_index_lucas_digit_choose_table_zero_row = 0 /\ bcf_value_lucas_digit_choose_table_zero_row = 1) \/ exists bcf_predecessor_lucas_digit_choose_table_zero_row. bcf_index_lucas_digit_choose_table_zero_row = S bcf_predecessor_lucas_digit_choose_table_zero_row /\ bcf_value_lucas_digit_choose_table_zero_row = 0)))) \/ exists bcf_predecessor_lucas_digit_choose_table bcf_previous_code_lucas_digit_choose_table bcf_previous_scale_lucas_digit_choose_table. bcf_row_index_lucas_digit_choose_table = S bcf_predecessor_lucas_digit_choose_table /\ ((((exists bcf_height_lucas_digit_choose_table_decoded_previous_code. bcf_height_lucas_digit_choose_table_decoded_previous_code + S (bcf_previous_code_lucas_digit_choose_table) = S ((S (bcf_predecessor_lucas_digit_choose_table)) * bcf_row_code_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_table_decoded_previous_code. bcf_row_code_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_table_decoded_previous_code * S ((S (bcf_predecessor_lucas_digit_choose_table)) * bcf_row_code_scale_lucas_digit_choose) + (bcf_previous_code_lucas_digit_choose_table))) /\ ((((exists bcf_height_lucas_digit_choose_table_decoded_previous_scale. bcf_height_lucas_digit_choose_table_decoded_previous_scale + S (bcf_previous_scale_lucas_digit_choose_table) = S ((S (bcf_predecessor_lucas_digit_choose_table)) * bcf_row_scale_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_table_decoded_previous_scale. bcf_row_scale_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_table_decoded_previous_scale * S ((S (bcf_predecessor_lucas_digit_choose_table)) * bcf_row_scale_scale_lucas_digit_choose) + (bcf_previous_scale_lucas_digit_choose_table))) /\ (forall bcf_index_lucas_digit_choose_table_row_step. (exists bcf_lt_gap_lucas_digit_choose_table_row_step_bound. bcf_lt_gap_lucas_digit_choose_table_row_step_bound + S (bcf_index_lucas_digit_choose_table_row_step) = S (a + b)) -> exists bcf_value_lucas_digit_choose_table_row_step. ((((exists bcf_height_lucas_digit_choose_table_row_step_entry. bcf_height_lucas_digit_choose_table_row_step_entry + S (bcf_value_lucas_digit_choose_table_row_step) = S ((S (bcf_index_lucas_digit_choose_table_row_step)) * bcf_row_scale_lucas_digit_choose_table)) /\ exists bcf_quotient_lucas_digit_choose_table_row_step_entry. bcf_row_code_lucas_digit_choose_table = bcf_quotient_lucas_digit_choose_table_row_step_entry * S ((S (bcf_index_lucas_digit_choose_table_row_step)) * bcf_row_scale_lucas_digit_choose_table) + (bcf_value_lucas_digit_choose_table_row_step))) /\ ((bcf_index_lucas_digit_choose_table_row_step = 0 /\ bcf_value_lucas_digit_choose_table_row_step = 1) \/ exists bcf_predecessor_lucas_digit_choose_table_row_step bcf_left_lucas_digit_choose_table_row_step bcf_right_lucas_digit_choose_table_row_step. bcf_index_lucas_digit_choose_table_row_step = S bcf_predecessor_lucas_digit_choose_table_row_step /\ ((((exists bcf_height_lucas_digit_choose_table_row_step_previous_left. bcf_height_lucas_digit_choose_table_row_step_previous_left + S (bcf_left_lucas_digit_choose_table_row_step) = S ((S (bcf_predecessor_lucas_digit_choose_table_row_step)) * bcf_previous_scale_lucas_digit_choose_table)) /\ exists bcf_quotient_lucas_digit_choose_table_row_step_previous_left. bcf_previous_code_lucas_digit_choose_table = bcf_quotient_lucas_digit_choose_table_row_step_previous_left * S ((S (bcf_predecessor_lucas_digit_choose_table_row_step)) * bcf_previous_scale_lucas_digit_choose_table) + (bcf_left_lucas_digit_choose_table_row_step))) /\ ((((exists bcf_height_lucas_digit_choose_table_row_step_previous_right. bcf_height_lucas_digit_choose_table_row_step_previous_right + S (bcf_right_lucas_digit_choose_table_row_step) = S ((S (S (bcf_predecessor_lucas_digit_choose_table_row_step))) * bcf_previous_scale_lucas_digit_choose_table)) /\ exists bcf_quotient_lucas_digit_choose_table_row_step_previous_right. bcf_previous_code_lucas_digit_choose_table = bcf_quotient_lucas_digit_choose_table_row_step_previous_right * S ((S (S (bcf_predecessor_lucas_digit_choose_table_row_step))) * bcf_previous_scale_lucas_digit_choose_table) + (bcf_right_lucas_digit_choose_table_row_step))) /\ bcf_value_lucas_digit_choose_table_row_step = bcf_left_lucas_digit_choose_table_row_step + bcf_right_lucas_digit_choose_table_row_step))))))))))) /\ ((((exists bcf_height_lucas_digit_choose_decoded_row_code. bcf_height_lucas_digit_choose_decoded_row_code + S (bcf_row_code_lucas_digit_choose) = S ((S (a + b)) * bcf_row_code_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_decoded_row_code. bcf_row_code_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_decoded_row_code * S ((S (a + b)) * bcf_row_code_scale_lucas_digit_choose) + (bcf_row_code_lucas_digit_choose))) /\ ((((exists bcf_height_lucas_digit_choose_decoded_row_scale. bcf_height_lucas_digit_choose_decoded_row_scale + S (bcf_row_scale_lucas_digit_choose) = S ((S (a + b)) * bcf_row_scale_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_decoded_row_scale. bcf_row_scale_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_decoded_row_scale * S ((S (a + b)) * bcf_row_scale_scale_lucas_digit_choose) + (bcf_row_scale_lucas_digit_choose))) /\ (((exists bcf_height_lucas_digit_choose_decoded_value. bcf_height_lucas_digit_choose_decoded_value + S (C) = S ((S (a)) * bcf_row_scale_lucas_digit_choose)) /\ exists bcf_quotient_lucas_digit_choose_decoded_value. bcf_row_code_lucas_digit_choose = bcf_quotient_lucas_digit_choose_decoded_value * S ((S (a)) * bcf_row_scale_lucas_digit_choose) + (C))))))))) -> (exists ldc_quotient_digit. C = p * ldc_quotient_digit)Proof neighborhood
Direct theorem prerequisites
choose_prime_divides_between · Alpha closed
Direct theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.
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.
01Fix variables and assumptionsL1–9
02Use earlier factsL10–15
Instantiate or apply named facts and discharge the corresponding proof obligations.
03Calculate and transport equalitiesL16–16
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L16
refl
Original defined command ledger · 21 lines
- 0001
intro p - 0002
intro a - 0003
intro b - 0004
intro C - 0005
intro hp - 0006
intro ha - 0007
intro hb - 0008
intro hcarry - 0009
intro hchoose - 0010
specialize choose_prime_divides_between (a + b) - 0011
specialize choose_prime_divides_between a - 0012
specialize choose_prime_divides_between b - 0013
specialize choose_prime_divides_between p - 0014
specialize choose_prime_divides_between C - 0015
apply choose_prime_divides_between - 0016
refl - 0017
exact hp - 0018
exact ha - 0019
exact hb - 0020
exact hcarry - 0021
exact hchoose