distinct_odd_prime_half_row_indicator_choices

Exact expanded PA statement

forall p q h k i. p = 2 * h + 1 -> q = 2 * k + 1 -> ((~(p = 1) /\ forall frp_prime_left_row_indicator_prime_p frp_prime_right_row_indicator_prime_p. p = frp_prime_left_row_indicator_prime_p * frp_prime_right_row_indicator_prime_p -> frp_prime_left_row_indicator_prime_p = 1 \/ frp_prime_right_row_indicator_prime_p = 1)) -> ((~(q = 1) /\ forall frp_prime_left_row_indicator_prime_q frp_prime_right_row_indicator_prime_q. q = frp_prime_left_row_indicator_prime_q * frp_prime_right_row_indicator_prime_q -> frp_prime_left_row_indicator_prime_q = 1 \/ frp_prime_right_row_indicator_prime_q = 1)) -> ~(p = q) -> (exists eri_gap_row_indicator_i_bound. eri_gap_row_indicator_i_bound + S (i) = h) -> (forall eri_column_row_indicator_concrete_choices. (exists eri_gap_row_indicator_concrete_choices_bound. eri_gap_row_indicator_concrete_choices_bound + S (eri_column_row_indicator_concrete_choices) = k) -> exists eri_bit_row_indicator_concrete_choices. (((eri_bit_row_indicator_concrete_choices = 0 /\ ((exists eri_gap_row_indicator_concrete_choices_choice_left. eri_gap_row_indicator_concrete_choices_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_choices) /\ ~(exists eri_gap_row_indicator_concrete_choices_choice_right. eri_gap_row_indicator_concrete_choices_choice_right + S (p * S eri_column_row_indicator_concrete_choices) = q * S i))) \/ (eri_bit_row_indicator_concrete_choices = 1 /\ ((exists eri_gap_row_indicator_concrete_choices_choice_right. eri_gap_row_indicator_concrete_choices_choice_right + S (p * S eri_column_row_indicator_concrete_choices) = q * S i) /\ ~(exists eri_gap_row_indicator_concrete_choices_choice_left. eri_gap_row_indicator_concrete_choices_choice_left + S (q * S i) = p * S eri_column_row_indicator_concrete_choices))))))