jordan_tuple_congruence_divisor

Exact expanded first-order arithmetic statement

forall m n b c d e k. (exists jt_factor_moddivisor. (n)=(m)*jt_factor_moddivisor) -> (forall jt_index_modlarger jt_left_modlarger jt_right_modlarger. (exists jt_gap_modlargerindex. jt_gap_modlargerindex+S (jt_index_modlarger)=(k)) -> (((exists fs_h_jt_modlargerleft. fs_h_jt_modlargerleft + S (jt_left_modlarger) = S ((S (jt_index_modlarger)) * c)) /\ exists fs_q_jt_modlargerleft. b = fs_q_jt_modlargerleft * S ((S (jt_index_modlarger)) * c) + (jt_left_modlarger))) -> (((exists fs_h_jt_modlargerright. fs_h_jt_modlargerright + S (jt_right_modlarger) = S ((S (jt_index_modlarger)) * e)) /\ exists fs_q_jt_modlargerright. d = fs_q_jt_modlargerright * S ((S (jt_index_modlarger)) * e) + (jt_right_modlarger))) -> (exists jt_left_modlargermod jt_right_modlargermod. (jt_left_modlarger)+(n)*jt_left_modlargermod=(jt_right_modlarger)+(n)*jt_right_modlargermod)) -> (forall jt_index_modsmaller jt_left_modsmaller jt_right_modsmaller. (exists jt_gap_modsmallerindex. jt_gap_modsmallerindex+S (jt_index_modsmaller)=(k)) -> (((exists fs_h_jt_modsmallerleft. fs_h_jt_modsmallerleft + S (jt_left_modsmaller) = S ((S (jt_index_modsmaller)) * c)) /\ exists fs_q_jt_modsmallerleft. b = fs_q_jt_modsmallerleft * S ((S (jt_index_modsmaller)) * c) + (jt_left_modsmaller))) -> (((exists fs_h_jt_modsmallerright. fs_h_jt_modsmallerright + S (jt_right_modsmaller) = S ((S (jt_index_modsmaller)) * e)) /\ exists fs_q_jt_modsmallerright. d = fs_q_jt_modsmallerright * S ((S (jt_index_modsmaller)) * e) + (jt_right_modsmaller))) -> (exists jt_left_modsmallermod jt_right_modsmallermod. (jt_left_modsmaller)+(m)*jt_left_modsmallermod=(jt_right_modsmaller)+(m)*jt_right_modsmallermod))