BT00VX

central_binom_prime_divisor_le_double

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

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

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.

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 the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

47 script commands · 13 reading checkpoints · 5 local claims

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)
factorial existschoose factorial bridgemul commmultiple transfactorial prime le of divides

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro c
  3. L3
    intro p
  4. L4
    intro hp
  5. L5
    intro hcentral
  6. L6
    intro hdivides
02Establish hFL7–9

Establish this local claim before using it. It is not an additional assumption.

  1. L7
    have hF : ∃ F. Factorial(n + n,F)Definitions: Factorial
  2. L8
    specialize factorial_exists (n + n)
  3. L9
    exact factorial_exists
03Separate the logical casesL10–10

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L10
    cases hF
04Establish hKL11–13

Establish this local claim before using it. It is not an additional assumption.

  1. L11
    have hK : ∃ K. Factorial(n,K)Definitions: Factorial
  2. L12
    specialize factorial_exists n
  3. L13
    exact factorial_exists
05Separate the logical casesL14–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. 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.

  1. L15
    have hbridge : x = (x1 * x1) * c
  2. L16
    specialize choose_factorial_bridge (n + n)
  3. L17
    specialize choose_factorial_bridge n
  4. L18
    specialize choose_factorial_bridge n
  5. L19
    specialize choose_factorial_bridge c
  6. L20
    specialize choose_factorial_bridge x
  7. L21
    specialize choose_factorial_bridge x1
  8. L22
    specialize choose_factorial_bridge x1
  9. L23
    apply choose_factorial_bridge
  10. L24
    refl
07Use earlier factsL25–28

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L25
    exact hcentral
  2. L26
    exact hF_witness
  3. L27
    exact hK_witness
  4. L28
    exact hK_witness
08Establish hcentral_factorL29–29

Establish this local claim before using it. It is not an additional assumption.

  1. L29
    have hcentral_factor : exists bpr_quotient_bcpdl_central_divides_total. x = (c) * bpr_quotient_bcpdl_central_divides_total
09Construct an explicit witnessL30–30

Supply the displayed value, then prove that it has the required property.

  1. 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.

  1. L31
    trans (x1 * x1) * c
11Use earlier factsL32–33

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L32
    exact hbridge
  2. L33
    apply mul_comm
12Establish hprime_factorL34–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply multiple trans.

  1. L34
    have hprime_factor : exists bpr_quotient_bcpdl_prime_divides_total. x = (p) * bpr_quotient_bcpdl_prime_divides_total
  2. L35
    specialize multiple_trans c
  3. L36
    specialize multiple_trans p
  4. L37
    specialize multiple_trans x
  5. L38
    apply multiple_trans
  6. L39
    exact hcentral_factor
  7. L40
    exact hdivides
  8. L41
    specialize factorial_prime_le_of_divides p
  9. L42
    specialize factorial_prime_le_of_divides (n + n)
  10. L43
    specialize factorial_prime_le_of_divides x
13Use earlier factsL44–47

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L44
    apply factorial_prime_le_of_divides
  2. L45
    exact hp
  3. L46
    exact hF_witness
  4. L47
    exact hprime_factor

Library-wide reading audit

Original exact command ledger · 47 lines
  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