BT00VC

choose_prime_divides_between

Alpha body-checked · checked-use disabled

A prime between both denominator indices and the row divides Choose.

Exact expanded PA statement

forall n k j p c. k + j = n -> ((~(p = 1) /\ forall bpr_left_bcpdb_prime bpr_right_bcpdb_prime. p = bpr_left_bcpdb_prime * bpr_right_bcpdb_prime -> bpr_left_bcpdb_prime = 1 \/ bpr_right_bcpdb_prime = 1)) -> (exists bpr_gap_bcpdb_left_bound. bpr_gap_bcpdb_left_bound + S (k) = p) -> (exists bpr_gap_bcpdb_right_bound. bpr_gap_bcpdb_right_bound + S (j) = p) -> (exists bpr_le_gap_bcpdb_upper_bound. bpr_le_gap_bcpdb_upper_bound + (p) = (n)) -> (((exists bcf_lt_gap_bcpdb_source_out_of_range. bcf_lt_gap_bcpdb_source_out_of_range + S (n) = k) /\ c = 0) \/ ((exists bcf_le_gap_bcpdb_source_in_range. bcf_le_gap_bcpdb_source_in_range + (k) = n) /\ (exists bcf_row_code_code_bcpdb_source bcf_row_code_scale_bcpdb_source bcf_row_scale_code_bcpdb_source bcf_row_scale_scale_bcpdb_source bcf_row_code_bcpdb_source bcf_row_scale_bcpdb_source. ((forall bcf_row_index_bcpdb_source_table. (exists bcf_lt_gap_bcpdb_source_table_row_bound. bcf_lt_gap_bcpdb_source_table_row_bound + S (bcf_row_index_bcpdb_source_table) = S (n)) -> exists bcf_row_code_bcpdb_source_table bcf_row_scale_bcpdb_source_table. ((((exists bcf_height_bcpdb_source_table_decoded_row_code. bcf_height_bcpdb_source_table_decoded_row_code + S (bcf_row_code_bcpdb_source_table) = S ((S (bcf_row_index_bcpdb_source_table)) * bcf_row_code_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_table_decoded_row_code. bcf_row_code_code_bcpdb_source = bcf_quotient_bcpdb_source_table_decoded_row_code * S ((S (bcf_row_index_bcpdb_source_table)) * bcf_row_code_scale_bcpdb_source) + (bcf_row_code_bcpdb_source_table))) /\ ((((exists bcf_height_bcpdb_source_table_decoded_row_scale. bcf_height_bcpdb_source_table_decoded_row_scale + S (bcf_row_scale_bcpdb_source_table) = S ((S (bcf_row_index_bcpdb_source_table)) * bcf_row_scale_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_table_decoded_row_scale. bcf_row_scale_code_bcpdb_source = bcf_quotient_bcpdb_source_table_decoded_row_scale * S ((S (bcf_row_index_bcpdb_source_table)) * bcf_row_scale_scale_bcpdb_source) + (bcf_row_scale_bcpdb_source_table))) /\ ((bcf_row_index_bcpdb_source_table = 0 /\ (forall bcf_index_bcpdb_source_table_zero_row. (exists bcf_lt_gap_bcpdb_source_table_zero_row_bound. bcf_lt_gap_bcpdb_source_table_zero_row_bound + S (bcf_index_bcpdb_source_table_zero_row) = S (n)) -> exists bcf_value_bcpdb_source_table_zero_row. ((((exists bcf_height_bcpdb_source_table_zero_row_entry. bcf_height_bcpdb_source_table_zero_row_entry + S (bcf_value_bcpdb_source_table_zero_row) = S ((S (bcf_index_bcpdb_source_table_zero_row)) * bcf_row_scale_bcpdb_source_table)) /\ exists bcf_quotient_bcpdb_source_table_zero_row_entry. bcf_row_code_bcpdb_source_table = bcf_quotient_bcpdb_source_table_zero_row_entry * S ((S (bcf_index_bcpdb_source_table_zero_row)) * bcf_row_scale_bcpdb_source_table) + (bcf_value_bcpdb_source_table_zero_row))) /\ ((bcf_index_bcpdb_source_table_zero_row = 0 /\ bcf_value_bcpdb_source_table_zero_row = 1) \/ exists bcf_predecessor_bcpdb_source_table_zero_row. bcf_index_bcpdb_source_table_zero_row = S bcf_predecessor_bcpdb_source_table_zero_row /\ bcf_value_bcpdb_source_table_zero_row = 0)))) \/ exists bcf_predecessor_bcpdb_source_table bcf_previous_code_bcpdb_source_table bcf_previous_scale_bcpdb_source_table. bcf_row_index_bcpdb_source_table = S bcf_predecessor_bcpdb_source_table /\ ((((exists bcf_height_bcpdb_source_table_decoded_previous_code. bcf_height_bcpdb_source_table_decoded_previous_code + S (bcf_previous_code_bcpdb_source_table) = S ((S (bcf_predecessor_bcpdb_source_table)) * bcf_row_code_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_table_decoded_previous_code. bcf_row_code_code_bcpdb_source = bcf_quotient_bcpdb_source_table_decoded_previous_code * S ((S (bcf_predecessor_bcpdb_source_table)) * bcf_row_code_scale_bcpdb_source) + (bcf_previous_code_bcpdb_source_table))) /\ ((((exists bcf_height_bcpdb_source_table_decoded_previous_scale. bcf_height_bcpdb_source_table_decoded_previous_scale + S (bcf_previous_scale_bcpdb_source_table) = S ((S (bcf_predecessor_bcpdb_source_table)) * bcf_row_scale_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_table_decoded_previous_scale. bcf_row_scale_code_bcpdb_source = bcf_quotient_bcpdb_source_table_decoded_previous_scale * S ((S (bcf_predecessor_bcpdb_source_table)) * bcf_row_scale_scale_bcpdb_source) + (bcf_previous_scale_bcpdb_source_table))) /\ (forall bcf_index_bcpdb_source_table_row_step. (exists bcf_lt_gap_bcpdb_source_table_row_step_bound. bcf_lt_gap_bcpdb_source_table_row_step_bound + S (bcf_index_bcpdb_source_table_row_step) = S (n)) -> exists bcf_value_bcpdb_source_table_row_step. ((((exists bcf_height_bcpdb_source_table_row_step_entry. bcf_height_bcpdb_source_table_row_step_entry + S (bcf_value_bcpdb_source_table_row_step) = S ((S (bcf_index_bcpdb_source_table_row_step)) * bcf_row_scale_bcpdb_source_table)) /\ exists bcf_quotient_bcpdb_source_table_row_step_entry. bcf_row_code_bcpdb_source_table = bcf_quotient_bcpdb_source_table_row_step_entry * S ((S (bcf_index_bcpdb_source_table_row_step)) * bcf_row_scale_bcpdb_source_table) + (bcf_value_bcpdb_source_table_row_step))) /\ ((bcf_index_bcpdb_source_table_row_step = 0 /\ bcf_value_bcpdb_source_table_row_step = 1) \/ exists bcf_predecessor_bcpdb_source_table_row_step bcf_left_bcpdb_source_table_row_step bcf_right_bcpdb_source_table_row_step. bcf_index_bcpdb_source_table_row_step = S bcf_predecessor_bcpdb_source_table_row_step /\ ((((exists bcf_height_bcpdb_source_table_row_step_previous_left. bcf_height_bcpdb_source_table_row_step_previous_left + S (bcf_left_bcpdb_source_table_row_step) = S ((S (bcf_predecessor_bcpdb_source_table_row_step)) * bcf_previous_scale_bcpdb_source_table)) /\ exists bcf_quotient_bcpdb_source_table_row_step_previous_left. bcf_previous_code_bcpdb_source_table = bcf_quotient_bcpdb_source_table_row_step_previous_left * S ((S (bcf_predecessor_bcpdb_source_table_row_step)) * bcf_previous_scale_bcpdb_source_table) + (bcf_left_bcpdb_source_table_row_step))) /\ ((((exists bcf_height_bcpdb_source_table_row_step_previous_right. bcf_height_bcpdb_source_table_row_step_previous_right + S (bcf_right_bcpdb_source_table_row_step) = S ((S (S (bcf_predecessor_bcpdb_source_table_row_step))) * bcf_previous_scale_bcpdb_source_table)) /\ exists bcf_quotient_bcpdb_source_table_row_step_previous_right. bcf_previous_code_bcpdb_source_table = bcf_quotient_bcpdb_source_table_row_step_previous_right * S ((S (S (bcf_predecessor_bcpdb_source_table_row_step))) * bcf_previous_scale_bcpdb_source_table) + (bcf_right_bcpdb_source_table_row_step))) /\ bcf_value_bcpdb_source_table_row_step = bcf_left_bcpdb_source_table_row_step + bcf_right_bcpdb_source_table_row_step))))))))))) /\ ((((exists bcf_height_bcpdb_source_decoded_row_code. bcf_height_bcpdb_source_decoded_row_code + S (bcf_row_code_bcpdb_source) = S ((S (n)) * bcf_row_code_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_decoded_row_code. bcf_row_code_code_bcpdb_source = bcf_quotient_bcpdb_source_decoded_row_code * S ((S (n)) * bcf_row_code_scale_bcpdb_source) + (bcf_row_code_bcpdb_source))) /\ ((((exists bcf_height_bcpdb_source_decoded_row_scale. bcf_height_bcpdb_source_decoded_row_scale + S (bcf_row_scale_bcpdb_source) = S ((S (n)) * bcf_row_scale_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_decoded_row_scale. bcf_row_scale_code_bcpdb_source = bcf_quotient_bcpdb_source_decoded_row_scale * S ((S (n)) * bcf_row_scale_scale_bcpdb_source) + (bcf_row_scale_bcpdb_source))) /\ (((exists bcf_height_bcpdb_source_decoded_value. bcf_height_bcpdb_source_decoded_value + S (c) = S ((S (k)) * bcf_row_scale_bcpdb_source)) /\ exists bcf_quotient_bcpdb_source_decoded_value. bcf_row_code_bcpdb_source = bcf_quotient_bcpdb_source_decoded_value * S ((S (k)) * bcf_row_scale_bcpdb_source) + (c))))))))) -> (exists bpr_quotient_bcpdb_result. c = (p) * bpr_quotient_bcpdb_result)

Structural proof guide

A prime between both denominator indices and the row divides Choose.

Direct prerequisites: factorial_exists, choose_factorial_bridge, factorial_prime_divides_of_le, euclid_prime_dvd_product, factorial_prime_le_of_divides, lt_not_le. The authored body proceeds by case analysis (5), intermediate claims (9), equality transport (1).

Proof neighborhood

Direct dependencies

BT008Y factorial_exists BT00TX choose_factorial_bridge BT00VA factorial_prime_divides_of_le BT003N euclid_prime_dvd_product BT00VB factorial_prime_le_of_divides BT001I lt_not_le

Direct dependents

BT00VF primorial_interval_divides_choose_between

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 k
  3. 0003intro j
  4. 0004intro p
  5. 0005intro c
  6. 0006intro hsum
  7. 0007intro hp
  8. 0008intro hk
  9. 0009intro hj
  10. 0010intro hpn
  11. 0011intro hchoose
  12. 0012have hF : exists F. (exists ff_b_bcpdb_total_factorial ff_c_bcpdb_total_factorial. ((forall ff_i_bcpdb_total_factorial_range. (exists ff_lt_bcpdb_total_factorial_range_bound. ff_lt_bcpdb_total_factorial_range_bound + S ff_i_bcpdb_total_factorial_range = n) -> (((exists ff_h_bcpdb_total_factorial_range_decoded. ff_h_bcpdb_total_factorial_range_decoded + S (1 + ff_i_bcpdb_total_factorial_range) = S ((S (ff_i_bcpdb_total_factorial_range)) * ff_c_bcpdb_total_factorial)) /\ exists ff_q_bcpdb_total_factorial_range_decoded. ff_b_bcpdb_total_factorial = ff_q_bcpdb_total_factorial_range_decoded * S ((S (ff_i_bcpdb_total_factorial_range)) * ff_c_bcpdb_total_factorial) + (1 + ff_i_bcpdb_total_factorial_range)))) /\ (exists ff_u_bcpdb_total_factorial_product ff_v_bcpdb_total_factorial_product. ((((exists ff_h_bcpdb_total_factorial_product_start. ff_h_bcpdb_total_factorial_product_start + S (1) = S ((S (0)) * ff_v_bcpdb_total_factorial_product)) /\ exists ff_q_bcpdb_total_factorial_product_start. ff_u_bcpdb_total_factorial_product = ff_q_bcpdb_total_factorial_product_start * S ((S (0)) * ff_v_bcpdb_total_factorial_product) + (1))) /\ ((((exists ff_h_bcpdb_total_factorial_product_terminal. ff_h_bcpdb_total_factorial_product_terminal + S (F) = S ((S (n)) * ff_v_bcpdb_total_factorial_product)) /\ exists ff_q_bcpdb_total_factorial_product_terminal. ff_u_bcpdb_total_factorial_product = ff_q_bcpdb_total_factorial_product_terminal * S ((S (n)) * ff_v_bcpdb_total_factorial_product) + (F))) /\ forall ff_i_bcpdb_total_factorial_product. (exists ff_lt_bcpdb_total_factorial_product_bound. ff_lt_bcpdb_total_factorial_product_bound + S ff_i_bcpdb_total_factorial_product = n) -> exists ff_p_bcpdb_total_factorial_product ff_r_bcpdb_total_factorial_product ff_s_bcpdb_total_factorial_product. ((((exists ff_h_bcpdb_total_factorial_product_factor. ff_h_bcpdb_total_factorial_product_factor + S (ff_p_bcpdb_total_factorial_product) = S ((S (ff_i_bcpdb_total_factorial_product)) * ff_c_bcpdb_total_factorial)) /\ exists ff_q_bcpdb_total_factorial_product_factor. ff_b_bcpdb_total_factorial = ff_q_bcpdb_total_factorial_product_factor * S ((S (ff_i_bcpdb_total_factorial_product)) * ff_c_bcpdb_total_factorial) + (ff_p_bcpdb_total_factorial_product))) /\ ((((exists ff_h_bcpdb_total_factorial_product_partial. ff_h_bcpdb_total_factorial_product_partial + S (ff_r_bcpdb_total_factorial_product) = S ((S (ff_i_bcpdb_total_factorial_product)) * ff_v_bcpdb_total_factorial_product)) /\ exists ff_q_bcpdb_total_factorial_product_partial. ff_u_bcpdb_total_factorial_product = ff_q_bcpdb_total_factorial_product_partial * S ((S (ff_i_bcpdb_total_factorial_product)) * ff_v_bcpdb_total_factorial_product) + (ff_r_bcpdb_total_factorial_product))) /\ ((((exists ff_h_bcpdb_total_factorial_product_successor. ff_h_bcpdb_total_factorial_product_successor + S (ff_s_bcpdb_total_factorial_product) = S ((S (S ff_i_bcpdb_total_factorial_product)) * ff_v_bcpdb_total_factorial_product)) /\ exists ff_q_bcpdb_total_factorial_product_successor. ff_u_bcpdb_total_factorial_product = ff_q_bcpdb_total_factorial_product_successor * S ((S (S ff_i_bcpdb_total_factorial_product)) * ff_v_bcpdb_total_factorial_product) + (ff_s_bcpdb_total_factorial_product))) /\ ff_s_bcpdb_total_factorial_product = ff_r_bcpdb_total_factorial_product * ff_p_bcpdb_total_factorial_product))))))))
  13. 0013apply factorial_exists
  14. 0014cases hF
  15. 0015have hK : exists K. (exists ff_b_bcpdb_left_factorial ff_c_bcpdb_left_factorial. ((forall ff_i_bcpdb_left_factorial_range. (exists ff_lt_bcpdb_left_factorial_range_bound. ff_lt_bcpdb_left_factorial_range_bound + S ff_i_bcpdb_left_factorial_range = k) -> (((exists ff_h_bcpdb_left_factorial_range_decoded. ff_h_bcpdb_left_factorial_range_decoded + S (1 + ff_i_bcpdb_left_factorial_range) = S ((S (ff_i_bcpdb_left_factorial_range)) * ff_c_bcpdb_left_factorial)) /\ exists ff_q_bcpdb_left_factorial_range_decoded. ff_b_bcpdb_left_factorial = ff_q_bcpdb_left_factorial_range_decoded * S ((S (ff_i_bcpdb_left_factorial_range)) * ff_c_bcpdb_left_factorial) + (1 + ff_i_bcpdb_left_factorial_range)))) /\ (exists ff_u_bcpdb_left_factorial_product ff_v_bcpdb_left_factorial_product. ((((exists ff_h_bcpdb_left_factorial_product_start. ff_h_bcpdb_left_factorial_product_start + S (1) = S ((S (0)) * ff_v_bcpdb_left_factorial_product)) /\ exists ff_q_bcpdb_left_factorial_product_start. ff_u_bcpdb_left_factorial_product = ff_q_bcpdb_left_factorial_product_start * S ((S (0)) * ff_v_bcpdb_left_factorial_product) + (1))) /\ ((((exists ff_h_bcpdb_left_factorial_product_terminal. ff_h_bcpdb_left_factorial_product_terminal + S (K) = S ((S (k)) * ff_v_bcpdb_left_factorial_product)) /\ exists ff_q_bcpdb_left_factorial_product_terminal. ff_u_bcpdb_left_factorial_product = ff_q_bcpdb_left_factorial_product_terminal * S ((S (k)) * ff_v_bcpdb_left_factorial_product) + (K))) /\ forall ff_i_bcpdb_left_factorial_product. (exists ff_lt_bcpdb_left_factorial_product_bound. ff_lt_bcpdb_left_factorial_product_bound + S ff_i_bcpdb_left_factorial_product = k) -> exists ff_p_bcpdb_left_factorial_product ff_r_bcpdb_left_factorial_product ff_s_bcpdb_left_factorial_product. ((((exists ff_h_bcpdb_left_factorial_product_factor. ff_h_bcpdb_left_factorial_product_factor + S (ff_p_bcpdb_left_factorial_product) = S ((S (ff_i_bcpdb_left_factorial_product)) * ff_c_bcpdb_left_factorial)) /\ exists ff_q_bcpdb_left_factorial_product_factor. ff_b_bcpdb_left_factorial = ff_q_bcpdb_left_factorial_product_factor * S ((S (ff_i_bcpdb_left_factorial_product)) * ff_c_bcpdb_left_factorial) + (ff_p_bcpdb_left_factorial_product))) /\ ((((exists ff_h_bcpdb_left_factorial_product_partial. ff_h_bcpdb_left_factorial_product_partial + S (ff_r_bcpdb_left_factorial_product) = S ((S (ff_i_bcpdb_left_factorial_product)) * ff_v_bcpdb_left_factorial_product)) /\ exists ff_q_bcpdb_left_factorial_product_partial. ff_u_bcpdb_left_factorial_product = ff_q_bcpdb_left_factorial_product_partial * S ((S (ff_i_bcpdb_left_factorial_product)) * ff_v_bcpdb_left_factorial_product) + (ff_r_bcpdb_left_factorial_product))) /\ ((((exists ff_h_bcpdb_left_factorial_product_successor. ff_h_bcpdb_left_factorial_product_successor + S (ff_s_bcpdb_left_factorial_product) = S ((S (S ff_i_bcpdb_left_factorial_product)) * ff_v_bcpdb_left_factorial_product)) /\ exists ff_q_bcpdb_left_factorial_product_successor. ff_u_bcpdb_left_factorial_product = ff_q_bcpdb_left_factorial_product_successor * S ((S (S ff_i_bcpdb_left_factorial_product)) * ff_v_bcpdb_left_factorial_product) + (ff_s_bcpdb_left_factorial_product))) /\ ff_s_bcpdb_left_factorial_product = ff_r_bcpdb_left_factorial_product * ff_p_bcpdb_left_factorial_product))))))))
  16. 0016apply factorial_exists
  17. 0017cases hK
  18. 0018have hJ : exists J. (exists ff_b_bcpdb_right_factorial ff_c_bcpdb_right_factorial. ((forall ff_i_bcpdb_right_factorial_range. (exists ff_lt_bcpdb_right_factorial_range_bound. ff_lt_bcpdb_right_factorial_range_bound + S ff_i_bcpdb_right_factorial_range = j) -> (((exists ff_h_bcpdb_right_factorial_range_decoded. ff_h_bcpdb_right_factorial_range_decoded + S (1 + ff_i_bcpdb_right_factorial_range) = S ((S (ff_i_bcpdb_right_factorial_range)) * ff_c_bcpdb_right_factorial)) /\ exists ff_q_bcpdb_right_factorial_range_decoded. ff_b_bcpdb_right_factorial = ff_q_bcpdb_right_factorial_range_decoded * S ((S (ff_i_bcpdb_right_factorial_range)) * ff_c_bcpdb_right_factorial) + (1 + ff_i_bcpdb_right_factorial_range)))) /\ (exists ff_u_bcpdb_right_factorial_product ff_v_bcpdb_right_factorial_product. ((((exists ff_h_bcpdb_right_factorial_product_start. ff_h_bcpdb_right_factorial_product_start + S (1) = S ((S (0)) * ff_v_bcpdb_right_factorial_product)) /\ exists ff_q_bcpdb_right_factorial_product_start. ff_u_bcpdb_right_factorial_product = ff_q_bcpdb_right_factorial_product_start * S ((S (0)) * ff_v_bcpdb_right_factorial_product) + (1))) /\ ((((exists ff_h_bcpdb_right_factorial_product_terminal. ff_h_bcpdb_right_factorial_product_terminal + S (J) = S ((S (j)) * ff_v_bcpdb_right_factorial_product)) /\ exists ff_q_bcpdb_right_factorial_product_terminal. ff_u_bcpdb_right_factorial_product = ff_q_bcpdb_right_factorial_product_terminal * S ((S (j)) * ff_v_bcpdb_right_factorial_product) + (J))) /\ forall ff_i_bcpdb_right_factorial_product. (exists ff_lt_bcpdb_right_factorial_product_bound. ff_lt_bcpdb_right_factorial_product_bound + S ff_i_bcpdb_right_factorial_product = j) -> exists ff_p_bcpdb_right_factorial_product ff_r_bcpdb_right_factorial_product ff_s_bcpdb_right_factorial_product. ((((exists ff_h_bcpdb_right_factorial_product_factor. ff_h_bcpdb_right_factorial_product_factor + S (ff_p_bcpdb_right_factorial_product) = S ((S (ff_i_bcpdb_right_factorial_product)) * ff_c_bcpdb_right_factorial)) /\ exists ff_q_bcpdb_right_factorial_product_factor. ff_b_bcpdb_right_factorial = ff_q_bcpdb_right_factorial_product_factor * S ((S (ff_i_bcpdb_right_factorial_product)) * ff_c_bcpdb_right_factorial) + (ff_p_bcpdb_right_factorial_product))) /\ ((((exists ff_h_bcpdb_right_factorial_product_partial. ff_h_bcpdb_right_factorial_product_partial + S (ff_r_bcpdb_right_factorial_product) = S ((S (ff_i_bcpdb_right_factorial_product)) * ff_v_bcpdb_right_factorial_product)) /\ exists ff_q_bcpdb_right_factorial_product_partial. ff_u_bcpdb_right_factorial_product = ff_q_bcpdb_right_factorial_product_partial * S ((S (ff_i_bcpdb_right_factorial_product)) * ff_v_bcpdb_right_factorial_product) + (ff_r_bcpdb_right_factorial_product))) /\ ((((exists ff_h_bcpdb_right_factorial_product_successor. ff_h_bcpdb_right_factorial_product_successor + S (ff_s_bcpdb_right_factorial_product) = S ((S (S ff_i_bcpdb_right_factorial_product)) * ff_v_bcpdb_right_factorial_product)) /\ exists ff_q_bcpdb_right_factorial_product_successor. ff_u_bcpdb_right_factorial_product = ff_q_bcpdb_right_factorial_product_successor * S ((S (S ff_i_bcpdb_right_factorial_product)) * ff_v_bcpdb_right_factorial_product) + (ff_s_bcpdb_right_factorial_product))) /\ ff_s_bcpdb_right_factorial_product = ff_r_bcpdb_right_factorial_product * ff_p_bcpdb_right_factorial_product))))))))
  19. 0019apply factorial_exists
  20. 0020cases hJ
  21. 0021have hbridge : x = (x1 * x2) * c
  22. 0022specialize choose_factorial_bridge n
  23. 0023specialize choose_factorial_bridge k
  24. 0024specialize choose_factorial_bridge j
  25. 0025specialize choose_factorial_bridge c
  26. 0026specialize choose_factorial_bridge x
  27. 0027specialize choose_factorial_bridge x1
  28. 0028specialize choose_factorial_bridge x2
  29. 0029apply choose_factorial_bridge
  30. 0030exact hsum
  31. 0031exact hchoose
  32. 0032exact hF_witness
  33. 0033exact hK_witness
  34. 0034exact hJ_witness
  35. 0035have htotal : exists bpr_quotient_bcpdb_total_divides. x = (p) * bpr_quotient_bcpdb_total_divides
  36. 0036specialize factorial_prime_divides_of_le p
  37. 0037specialize factorial_prime_divides_of_le n
  38. 0038specialize factorial_prime_divides_of_le x
  39. 0039apply factorial_prime_divides_of_le
  40. 0040exact hp
  41. 0041exact hpn
  42. 0042exact hF_witness
  43. 0043rewrite hbridge at htotal
  44. 0044have houter : (exists bpr_quotient_bcpdb_outer_left. x1 * x2 = (p) * bpr_quotient_bcpdb_outer_left) \/ (exists bpr_quotient_bcpdb_outer_right. c = (p) * bpr_quotient_bcpdb_outer_right)
  45. 0045specialize euclid_prime_dvd_product p
  46. 0046specialize euclid_prime_dvd_product (x1 * x2)
  47. 0047specialize euclid_prime_dvd_product c
  48. 0048apply euclid_prime_dvd_product
  49. 0049exact hp
  50. 0050exact htotal
  51. 0051cases houter
  52. 0052have hinner : (exists bpr_quotient_bcpdb_inner_left. x1 = (p) * bpr_quotient_bcpdb_inner_left) \/ (exists bpr_quotient_bcpdb_inner_right. x2 = (p) * bpr_quotient_bcpdb_inner_right)
  53. 0053specialize euclid_prime_dvd_product p
  54. 0054specialize euclid_prime_dvd_product x1
  55. 0055specialize euclid_prime_dvd_product x2
  56. 0056apply euclid_prime_dvd_product
  57. 0057exact hp
  58. 0058exact houter_left
  59. 0059cases hinner
  60. 0060have hpk : exists g. g + p = k
  61. 0061specialize factorial_prime_le_of_divides p
  62. 0062specialize factorial_prime_le_of_divides k
  63. 0063specialize factorial_prime_le_of_divides x1
  64. 0064apply factorial_prime_le_of_divides
  65. 0065exact hp
  66. 0066exact hK_witness
  67. 0067exact hinner_left
  68. 0068exfalso
  69. 0069specialize lt_not_le k
  70. 0070specialize lt_not_le p
  71. 0071apply lt_not_le
  72. 0072exact hk
  73. 0073exact hpk
  74. 0074have hpj : exists g. g + p = j
  75. 0075specialize factorial_prime_le_of_divides p
  76. 0076specialize factorial_prime_le_of_divides j
  77. 0077specialize factorial_prime_le_of_divides x2
  78. 0078apply factorial_prime_le_of_divides
  79. 0079exact hp
  80. 0080exact hJ_witness
  81. 0081exact hinner_right
  82. 0082exfalso
  83. 0083specialize lt_not_le j
  84. 0084specialize lt_not_le p
  85. 0085apply lt_not_le
  86. 0086exact hj
  87. 0087exact hpj
  88. 0088exact houter_right