BT00VX

central_binom_prime_divisor_le_double

Alpha body-checked · checked-use disabled

Every prime divisor of a central coefficient is at most 2*n.

Exact expanded 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))

Structural proof guide

Every prime divisor of a central coefficient is at most 2*n.

Direct prerequisites: factorial_exists, choose_factorial_bridge, mul_comm, multiple_trans, factorial_prime_le_of_divides. The authored body proceeds by case analysis (2), intermediate claims (5).

Proof neighborhood

Direct dependencies

BT008Y factorial_exists BT00TX choose_factorial_bridge BT0006 mul_comm BT002C multiple_trans BT00VB factorial_prime_le_of_divides

Direct dependents

BT00VY no_bertrand_central_prime_divisor_le BT0107 central_binom_prime_contribution_product_exists

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro n
  2. 0002intro c
  3. 0003intro p
  4. 0004intro hp
  5. 0005intro hcentral
  6. 0006intro hdivides
  7. 0007have 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))))))))
  8. 0008specialize factorial_exists (n + n)
  9. 0009exact factorial_exists
  10. 0010cases hF
  11. 0011have 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))))))))
  12. 0012specialize factorial_exists n
  13. 0013exact factorial_exists
  14. 0014cases hK
  15. 0015have hbridge : x = (x1 * x1) * c
  16. 0016specialize choose_factorial_bridge (n + n)
  17. 0017specialize choose_factorial_bridge n
  18. 0018specialize choose_factorial_bridge n
  19. 0019specialize choose_factorial_bridge c
  20. 0020specialize choose_factorial_bridge x
  21. 0021specialize choose_factorial_bridge x1
  22. 0022specialize choose_factorial_bridge x1
  23. 0023apply choose_factorial_bridge
  24. 0024refl
  25. 0025exact hcentral
  26. 0026exact hF_witness
  27. 0027exact hK_witness
  28. 0028exact hK_witness
  29. 0029have hcentral_factor : exists bpr_quotient_bcpdl_central_divides_total. x = (c) * bpr_quotient_bcpdl_central_divides_total
  30. 0030exists (x1 * x1)
  31. 0031trans (x1 * x1) * c
  32. 0032exact hbridge
  33. 0033apply mul_comm
  34. 0034have hprime_factor : exists bpr_quotient_bcpdl_prime_divides_total. x = (p) * bpr_quotient_bcpdl_prime_divides_total
  35. 0035specialize multiple_trans c
  36. 0036specialize multiple_trans p
  37. 0037specialize multiple_trans x
  38. 0038apply multiple_trans
  39. 0039exact hcentral_factor
  40. 0040exact hdivides
  41. 0041specialize factorial_prime_le_of_divides p
  42. 0042specialize factorial_prime_le_of_divides (n + n)
  43. 0043specialize factorial_prime_le_of_divides x
  44. 0044apply factorial_prime_le_of_divides
  45. 0045exact hp
  46. 0046exact hF_witness
  47. 0047exact hprime_factor