crt_pairwise_coprime_prefix_product_coprime_last

Exact expanded first-order arithmetic statement

forall b c l x m. (forall bpr_left_index_gcrt_product_last_pairs bpr_right_index_gcrt_product_last_pairs bpr_left_value_gcrt_product_last_pairs bpr_right_value_gcrt_product_last_pairs. (exists bpr_gap_gcrt_product_last_pairs_left_bound. bpr_gap_gcrt_product_last_pairs_left_bound + S (bpr_left_index_gcrt_product_last_pairs) = S l) -> (exists bpr_gap_gcrt_product_last_pairs_right_bound. bpr_gap_gcrt_product_last_pairs_right_bound + S (bpr_right_index_gcrt_product_last_pairs) = S l) -> (((exists bpr_height_gcrt_product_last_pairs_left_at. bpr_height_gcrt_product_last_pairs_left_at + S (bpr_left_value_gcrt_product_last_pairs) = S ((S (bpr_left_index_gcrt_product_last_pairs)) * c)) /\ exists bpr_quotient_gcrt_product_last_pairs_left_at. b = bpr_quotient_gcrt_product_last_pairs_left_at * S ((S (bpr_left_index_gcrt_product_last_pairs)) * c) + (bpr_left_value_gcrt_product_last_pairs))) -> (((exists bpr_height_gcrt_product_last_pairs_right_at. bpr_height_gcrt_product_last_pairs_right_at + S (bpr_right_value_gcrt_product_last_pairs) = S ((S (bpr_right_index_gcrt_product_last_pairs)) * c)) /\ exists bpr_quotient_gcrt_product_last_pairs_right_at. b = bpr_quotient_gcrt_product_last_pairs_right_at * S ((S (bpr_right_index_gcrt_product_last_pairs)) * c) + (bpr_right_value_gcrt_product_last_pairs))) -> ~(bpr_left_index_gcrt_product_last_pairs = bpr_right_index_gcrt_product_last_pairs) -> (forall bpr_coprime_divisor_gcrt_product_last_pairs_coprime. (exists bpr_coprime_left_factor_gcrt_product_last_pairs_coprime. bpr_left_value_gcrt_product_last_pairs = bpr_coprime_divisor_gcrt_product_last_pairs_coprime * bpr_coprime_left_factor_gcrt_product_last_pairs_coprime) -> (exists bpr_coprime_right_factor_gcrt_product_last_pairs_coprime. bpr_right_value_gcrt_product_last_pairs = bpr_coprime_divisor_gcrt_product_last_pairs_coprime * bpr_coprime_right_factor_gcrt_product_last_pairs_coprime) -> bpr_coprime_divisor_gcrt_product_last_pairs_coprime = 1)) -> (exists ff_u_gcrt_product_last_prefix ff_v_gcrt_product_last_prefix. ((((exists ff_h_gcrt_product_last_prefix_start. ff_h_gcrt_product_last_prefix_start + S (1) = S ((S (0)) * ff_v_gcrt_product_last_prefix)) /\ exists ff_q_gcrt_product_last_prefix_start. ff_u_gcrt_product_last_prefix = ff_q_gcrt_product_last_prefix_start * S ((S (0)) * ff_v_gcrt_product_last_prefix) + (1))) /\ ((((exists ff_h_gcrt_product_last_prefix_terminal. ff_h_gcrt_product_last_prefix_terminal + S (x) = S ((S (l)) * ff_v_gcrt_product_last_prefix)) /\ exists ff_q_gcrt_product_last_prefix_terminal. ff_u_gcrt_product_last_prefix = ff_q_gcrt_product_last_prefix_terminal * S ((S (l)) * ff_v_gcrt_product_last_prefix) + (x))) /\ forall ff_i_gcrt_product_last_prefix. (exists ff_lt_gcrt_product_last_prefix_bound. ff_lt_gcrt_product_last_prefix_bound + S ff_i_gcrt_product_last_prefix = l) -> exists ff_p_gcrt_product_last_prefix ff_r_gcrt_product_last_prefix ff_s_gcrt_product_last_prefix. ((((exists ff_h_gcrt_product_last_prefix_factor. ff_h_gcrt_product_last_prefix_factor + S (ff_p_gcrt_product_last_prefix) = S ((S (ff_i_gcrt_product_last_prefix)) * c)) /\ exists ff_q_gcrt_product_last_prefix_factor. b = ff_q_gcrt_product_last_prefix_factor * S ((S (ff_i_gcrt_product_last_prefix)) * c) + (ff_p_gcrt_product_last_prefix))) /\ ((((exists ff_h_gcrt_product_last_prefix_partial. ff_h_gcrt_product_last_prefix_partial + S (ff_r_gcrt_product_last_prefix) = S ((S (ff_i_gcrt_product_last_prefix)) * ff_v_gcrt_product_last_prefix)) /\ exists ff_q_gcrt_product_last_prefix_partial. ff_u_gcrt_product_last_prefix = ff_q_gcrt_product_last_prefix_partial * S ((S (ff_i_gcrt_product_last_prefix)) * ff_v_gcrt_product_last_prefix) + (ff_r_gcrt_product_last_prefix))) /\ ((((exists ff_h_gcrt_product_last_prefix_successor. ff_h_gcrt_product_last_prefix_successor + S (ff_s_gcrt_product_last_prefix) = S ((S (S ff_i_gcrt_product_last_prefix)) * ff_v_gcrt_product_last_prefix)) /\ exists ff_q_gcrt_product_last_prefix_successor. ff_u_gcrt_product_last_prefix = ff_q_gcrt_product_last_prefix_successor * S ((S (S ff_i_gcrt_product_last_prefix)) * ff_v_gcrt_product_last_prefix) + (ff_s_gcrt_product_last_prefix))) /\ ff_s_gcrt_product_last_prefix = ff_r_gcrt_product_last_prefix * ff_p_gcrt_product_last_prefix)))))) -> (((exists ff_h_gcrt_product_last_entry. ff_h_gcrt_product_last_entry + S (m) = S ((S (l)) * c)) /\ exists ff_q_gcrt_product_last_entry. b = ff_q_gcrt_product_last_entry * S ((S (l)) * c) + (m))) -> (forall frp_divisor_gcrt_product_last_coprime. (exists frp_left_factor_gcrt_product_last_coprime. x = frp_divisor_gcrt_product_last_coprime * frp_left_factor_gcrt_product_last_coprime) -> (exists frp_right_factor_gcrt_product_last_coprime. m = frp_divisor_gcrt_product_last_coprime * frp_right_factor_gcrt_product_last_coprime) -> frp_divisor_gcrt_product_last_coprime = 1)