jordan_tuple_congruence_coprime_product

Exact expanded first-order arithmetic statement

forall m n b c d e k. (forall jt_divisor_combinecop. (exists jt_factor_combinecopa. (m)=(jt_divisor_combinecop)*jt_factor_combinecopa) -> (exists jt_factor_combinecopb. (n)=(jt_divisor_combinecop)*jt_factor_combinecopb) -> jt_divisor_combinecop=1) -> (forall jt_index_combinem jt_left_combinem jt_right_combinem. (exists jt_gap_combinemindex. jt_gap_combinemindex+S (jt_index_combinem)=(k)) -> (((exists fs_h_jt_combinemleft. fs_h_jt_combinemleft + S (jt_left_combinem) = S ((S (jt_index_combinem)) * c)) /\ exists fs_q_jt_combinemleft. b = fs_q_jt_combinemleft * S ((S (jt_index_combinem)) * c) + (jt_left_combinem))) -> (((exists fs_h_jt_combinemright. fs_h_jt_combinemright + S (jt_right_combinem) = S ((S (jt_index_combinem)) * e)) /\ exists fs_q_jt_combinemright. d = fs_q_jt_combinemright * S ((S (jt_index_combinem)) * e) + (jt_right_combinem))) -> (exists jt_left_combinemmod jt_right_combinemmod. (jt_left_combinem)+(m)*jt_left_combinemmod=(jt_right_combinem)+(m)*jt_right_combinemmod)) -> (forall jt_index_combinen jt_left_combinen jt_right_combinen. (exists jt_gap_combinenindex. jt_gap_combinenindex+S (jt_index_combinen)=(k)) -> (((exists fs_h_jt_combinenleft. fs_h_jt_combinenleft + S (jt_left_combinen) = S ((S (jt_index_combinen)) * c)) /\ exists fs_q_jt_combinenleft. b = fs_q_jt_combinenleft * S ((S (jt_index_combinen)) * c) + (jt_left_combinen))) -> (((exists fs_h_jt_combinenright. fs_h_jt_combinenright + S (jt_right_combinen) = S ((S (jt_index_combinen)) * e)) /\ exists fs_q_jt_combinenright. d = fs_q_jt_combinenright * S ((S (jt_index_combinen)) * e) + (jt_right_combinen))) -> (exists jt_left_combinenmod jt_right_combinenmod. (jt_left_combinen)+(n)*jt_left_combinenmod=(jt_right_combinen)+(n)*jt_right_combinenmod)) -> (forall jt_index_combineproduct jt_left_combineproduct jt_right_combineproduct. (exists jt_gap_combineproductindex. jt_gap_combineproductindex+S (jt_index_combineproduct)=(k)) -> (((exists fs_h_jt_combineproductleft. fs_h_jt_combineproductleft + S (jt_left_combineproduct) = S ((S (jt_index_combineproduct)) * c)) /\ exists fs_q_jt_combineproductleft. b = fs_q_jt_combineproductleft * S ((S (jt_index_combineproduct)) * c) + (jt_left_combineproduct))) -> (((exists fs_h_jt_combineproductright. fs_h_jt_combineproductright + S (jt_right_combineproduct) = S ((S (jt_index_combineproduct)) * e)) /\ exists fs_q_jt_combineproductright. d = fs_q_jt_combineproductright * S ((S (jt_index_combineproduct)) * e) + (jt_right_combineproduct))) -> (exists jt_left_combineproductmod jt_right_combineproductmod. (jt_left_combineproduct)+(m*n)*jt_left_combineproductmod=(jt_right_combineproduct)+(m*n)*jt_right_combineproductmod))