crt_pairwise_coprime_prefix_product_is_lcm

Exact expanded first-order arithmetic statement

forall b c l x. (forall bpr_left_index_gcrt_product_lcm_pairwise bpr_right_index_gcrt_product_lcm_pairwise bpr_left_value_gcrt_product_lcm_pairwise bpr_right_value_gcrt_product_lcm_pairwise. (exists bpr_gap_gcrt_product_lcm_pairwise_left_bound. bpr_gap_gcrt_product_lcm_pairwise_left_bound + S (bpr_left_index_gcrt_product_lcm_pairwise) = l) -> (exists bpr_gap_gcrt_product_lcm_pairwise_right_bound. bpr_gap_gcrt_product_lcm_pairwise_right_bound + S (bpr_right_index_gcrt_product_lcm_pairwise) = l) -> (((exists bpr_height_gcrt_product_lcm_pairwise_left_at. bpr_height_gcrt_product_lcm_pairwise_left_at + S (bpr_left_value_gcrt_product_lcm_pairwise) = S ((S (bpr_left_index_gcrt_product_lcm_pairwise)) * c)) /\ exists bpr_quotient_gcrt_product_lcm_pairwise_left_at. b = bpr_quotient_gcrt_product_lcm_pairwise_left_at * S ((S (bpr_left_index_gcrt_product_lcm_pairwise)) * c) + (bpr_left_value_gcrt_product_lcm_pairwise))) -> (((exists bpr_height_gcrt_product_lcm_pairwise_right_at. bpr_height_gcrt_product_lcm_pairwise_right_at + S (bpr_right_value_gcrt_product_lcm_pairwise) = S ((S (bpr_right_index_gcrt_product_lcm_pairwise)) * c)) /\ exists bpr_quotient_gcrt_product_lcm_pairwise_right_at. b = bpr_quotient_gcrt_product_lcm_pairwise_right_at * S ((S (bpr_right_index_gcrt_product_lcm_pairwise)) * c) + (bpr_right_value_gcrt_product_lcm_pairwise))) -> ~(bpr_left_index_gcrt_product_lcm_pairwise = bpr_right_index_gcrt_product_lcm_pairwise) -> (forall bpr_coprime_divisor_gcrt_product_lcm_pairwise_coprime. (exists bpr_coprime_left_factor_gcrt_product_lcm_pairwise_coprime. bpr_left_value_gcrt_product_lcm_pairwise = bpr_coprime_divisor_gcrt_product_lcm_pairwise_coprime * bpr_coprime_left_factor_gcrt_product_lcm_pairwise_coprime) -> (exists bpr_coprime_right_factor_gcrt_product_lcm_pairwise_coprime. bpr_right_value_gcrt_product_lcm_pairwise = bpr_coprime_divisor_gcrt_product_lcm_pairwise_coprime * bpr_coprime_right_factor_gcrt_product_lcm_pairwise_coprime) -> bpr_coprime_divisor_gcrt_product_lcm_pairwise_coprime = 1)) -> (exists ff_u_gcrt_product_lcm_source ff_v_gcrt_product_lcm_source. ((((exists ff_h_gcrt_product_lcm_source_start. ff_h_gcrt_product_lcm_source_start + S (1) = S ((S (0)) * ff_v_gcrt_product_lcm_source)) /\ exists ff_q_gcrt_product_lcm_source_start. ff_u_gcrt_product_lcm_source = ff_q_gcrt_product_lcm_source_start * S ((S (0)) * ff_v_gcrt_product_lcm_source) + (1))) /\ ((((exists ff_h_gcrt_product_lcm_source_terminal. ff_h_gcrt_product_lcm_source_terminal + S (x) = S ((S (l)) * ff_v_gcrt_product_lcm_source)) /\ exists ff_q_gcrt_product_lcm_source_terminal. ff_u_gcrt_product_lcm_source = ff_q_gcrt_product_lcm_source_terminal * S ((S (l)) * ff_v_gcrt_product_lcm_source) + (x))) /\ forall ff_i_gcrt_product_lcm_source. (exists ff_lt_gcrt_product_lcm_source_bound. ff_lt_gcrt_product_lcm_source_bound + S ff_i_gcrt_product_lcm_source = l) -> exists ff_p_gcrt_product_lcm_source ff_r_gcrt_product_lcm_source ff_s_gcrt_product_lcm_source. ((((exists ff_h_gcrt_product_lcm_source_factor. ff_h_gcrt_product_lcm_source_factor + S (ff_p_gcrt_product_lcm_source) = S ((S (ff_i_gcrt_product_lcm_source)) * c)) /\ exists ff_q_gcrt_product_lcm_source_factor. b = ff_q_gcrt_product_lcm_source_factor * S ((S (ff_i_gcrt_product_lcm_source)) * c) + (ff_p_gcrt_product_lcm_source))) /\ ((((exists ff_h_gcrt_product_lcm_source_partial. ff_h_gcrt_product_lcm_source_partial + S (ff_r_gcrt_product_lcm_source) = S ((S (ff_i_gcrt_product_lcm_source)) * ff_v_gcrt_product_lcm_source)) /\ exists ff_q_gcrt_product_lcm_source_partial. ff_u_gcrt_product_lcm_source = ff_q_gcrt_product_lcm_source_partial * S ((S (ff_i_gcrt_product_lcm_source)) * ff_v_gcrt_product_lcm_source) + (ff_r_gcrt_product_lcm_source))) /\ ((((exists ff_h_gcrt_product_lcm_source_successor. ff_h_gcrt_product_lcm_source_successor + S (ff_s_gcrt_product_lcm_source) = S ((S (S ff_i_gcrt_product_lcm_source)) * ff_v_gcrt_product_lcm_source)) /\ exists ff_q_gcrt_product_lcm_source_successor. ff_u_gcrt_product_lcm_source = ff_q_gcrt_product_lcm_source_successor * S ((S (S ff_i_gcrt_product_lcm_source)) * ff_v_gcrt_product_lcm_source) + (ff_s_gcrt_product_lcm_source))) /\ ff_s_gcrt_product_lcm_source = ff_r_gcrt_product_lcm_source * ff_p_gcrt_product_lcm_source)))))) -> (((forall gcrt_common_index_product_lcm_result_own gcrt_common_modulus_product_lcm_result_own. (exists ff_lt_gcrt_product_lcm_result_own_bound. ff_lt_gcrt_product_lcm_result_own_bound + S gcrt_common_index_product_lcm_result_own = l) -> (((exists ff_h_gcrt_product_lcm_result_own_entry. ff_h_gcrt_product_lcm_result_own_entry + S (gcrt_common_modulus_product_lcm_result_own) = S ((S (gcrt_common_index_product_lcm_result_own)) * c)) /\ exists ff_q_gcrt_product_lcm_result_own_entry. b = ff_q_gcrt_product_lcm_result_own_entry * S ((S (gcrt_common_index_product_lcm_result_own)) * c) + (gcrt_common_modulus_product_lcm_result_own))) -> exists gcrt_common_quotient_product_lcm_result_own. x = gcrt_common_modulus_product_lcm_result_own * gcrt_common_quotient_product_lcm_result_own) /\ forall gcrt_lcm_common_product_lcm_result. (forall gcrt_common_index_product_lcm_result_other gcrt_common_modulus_product_lcm_result_other. (exists ff_lt_gcrt_product_lcm_result_other_bound. ff_lt_gcrt_product_lcm_result_other_bound + S gcrt_common_index_product_lcm_result_other = l) -> (((exists ff_h_gcrt_product_lcm_result_other_entry. ff_h_gcrt_product_lcm_result_other_entry + S (gcrt_common_modulus_product_lcm_result_other) = S ((S (gcrt_common_index_product_lcm_result_other)) * c)) /\ exists ff_q_gcrt_product_lcm_result_other_entry. b = ff_q_gcrt_product_lcm_result_other_entry * S ((S (gcrt_common_index_product_lcm_result_other)) * c) + (gcrt_common_modulus_product_lcm_result_other))) -> exists gcrt_common_quotient_product_lcm_result_other. gcrt_lcm_common_product_lcm_result = gcrt_common_modulus_product_lcm_result_other * gcrt_common_quotient_product_lcm_result_other) -> exists gcrt_lcm_quotient_product_lcm_result. gcrt_lcm_common_product_lcm_result = x * gcrt_lcm_quotient_product_lcm_result))