jordan_tuple_equal_congruence

Exact expanded first-order arithmetic statement

forall n b c d e k. (forall jt_index_equalcong jt_left_equalcong jt_right_equalcong. (exists jt_gap_equalcongindex. jt_gap_equalcongindex+S (jt_index_equalcong)=(k)) -> (((exists fs_h_jt_equalcongleft. fs_h_jt_equalcongleft + S (jt_left_equalcong) = S ((S (jt_index_equalcong)) * c)) /\ exists fs_q_jt_equalcongleft. b = fs_q_jt_equalcongleft * S ((S (jt_index_equalcong)) * c) + (jt_left_equalcong))) -> (((exists fs_h_jt_equalcongright. fs_h_jt_equalcongright + S (jt_right_equalcong) = S ((S (jt_index_equalcong)) * e)) /\ exists fs_q_jt_equalcongright. d = fs_q_jt_equalcongright * S ((S (jt_index_equalcong)) * e) + (jt_right_equalcong))) -> jt_left_equalcong=jt_right_equalcong) -> (forall jt_index_equalcongresult jt_left_equalcongresult jt_right_equalcongresult. (exists jt_gap_equalcongresultindex. jt_gap_equalcongresultindex+S (jt_index_equalcongresult)=(k)) -> (((exists fs_h_jt_equalcongresultleft. fs_h_jt_equalcongresultleft + S (jt_left_equalcongresult) = S ((S (jt_index_equalcongresult)) * c)) /\ exists fs_q_jt_equalcongresultleft. b = fs_q_jt_equalcongresultleft * S ((S (jt_index_equalcongresult)) * c) + (jt_left_equalcongresult))) -> (((exists fs_h_jt_equalcongresultright. fs_h_jt_equalcongresultright + S (jt_right_equalcongresult) = S ((S (jt_index_equalcongresult)) * e)) /\ exists fs_q_jt_equalcongresultright. d = fs_q_jt_equalcongresultright * S ((S (jt_index_equalcongresult)) * e) + (jt_right_equalcongresult))) -> (exists jt_left_equalcongresultmod jt_right_equalcongresultmod. (jt_left_equalcongresult)+(n)*jt_left_equalcongresultmod=(jt_right_equalcongresult)+(n)*jt_right_equalcongresultmod))