jordan_rectangle_crt_pair_value

Exact expanded first-order arithmetic statement

forall m n k A B C D u E F G H v P Q R T i j b c d e. (forall jt_index_pairrect. (exists jt_gap_pairrectindex. jt_gap_pairrectindex+S (jt_index_pairrect)=(u*v)) -> exists jt_row_pairrect jt_column_pairrect jt_b_pairrect jt_c_pairrect jt_d_pairrect jt_e_pairrect jt_f_pairrect jt_g_pairrect. ((exists jt_gap_pairrectrow. jt_gap_pairrectrow+S (jt_row_pairrect)=(u)) /\ (((exists jt_gap_pairrectcolumn. jt_gap_pairrectcolumn+S (jt_column_pairrect)=(v)) /\ (((jt_index_pairrect=(v)*jt_row_pairrect+jt_column_pairrect) /\ (((((((exists fs_h_jt_pairrectleftcode. fs_h_jt_pairrectleftcode + S (jt_b_pairrect) = S ((S (jt_row_pairrect)) * B)) /\ exists fs_q_jt_pairrectleftcode. A = fs_q_jt_pairrectleftcode * S ((S (jt_row_pairrect)) * B) + (jt_b_pairrect))) /\ (((exists fs_h_jt_pairrectleftscale. fs_h_jt_pairrectleftscale + S (jt_c_pairrect) = S ((S (jt_row_pairrect)) * D)) /\ exists fs_q_jt_pairrectleftscale. C = fs_q_jt_pairrectleftscale * S ((S (jt_row_pairrect)) * D) + (jt_c_pairrect))))) /\ (((((((exists fs_h_jt_pairrectrightcode. fs_h_jt_pairrectrightcode + S (jt_d_pairrect) = S ((S (jt_column_pairrect)) * F)) /\ exists fs_q_jt_pairrectrightcode. E = fs_q_jt_pairrectrightcode * S ((S (jt_column_pairrect)) * F) + (jt_d_pairrect))) /\ (((exists fs_h_jt_pairrectrightscale. fs_h_jt_pairrectrightscale + S (jt_e_pairrect) = S ((S (jt_column_pairrect)) * H)) /\ exists fs_q_jt_pairrectrightscale. G = fs_q_jt_pairrectrightscale * S ((S (jt_column_pairrect)) * H) + (jt_e_pairrect))))) /\ (((((((exists fs_h_jt_pairrectoutputcode. fs_h_jt_pairrectoutputcode + S (jt_f_pairrect) = S ((S (jt_index_pairrect)) * Q)) /\ exists fs_q_jt_pairrectoutputcode. P = fs_q_jt_pairrectoutputcode * S ((S (jt_index_pairrect)) * Q) + (jt_f_pairrect))) /\ (((exists fs_h_jt_pairrectoutputscale. fs_h_jt_pairrectoutputscale + S (jt_g_pairrect) = S ((S (jt_index_pairrect)) * T)) /\ exists fs_q_jt_pairrectoutputscale. R = fs_q_jt_pairrectoutputscale * S ((S (jt_index_pairrect)) * T) + (jt_g_pairrect))))) /\ (((((forall jt_index_pairrectcrtbound. (exists jt_gap_pairrectcrtboundindex. jt_gap_pairrectcrtboundindex+S (jt_index_pairrectcrtbound)=(k)) -> exists jt_value_pairrectcrtbound. ((((exists fs_h_jt_pairrectcrtboundat. fs_h_jt_pairrectcrtboundat + S (jt_value_pairrectcrtbound) = S ((S (jt_index_pairrectcrtbound)) * jt_g_pairrect)) /\ exists fs_q_jt_pairrectcrtboundat. jt_f_pairrect = fs_q_jt_pairrectcrtboundat * S ((S (jt_index_pairrectcrtbound)) * jt_g_pairrect) + (jt_value_pairrectcrtbound))) /\ (exists jt_gap_pairrectcrtboundvalue. jt_gap_pairrectcrtboundvalue+S (jt_value_pairrectcrtbound)=(m*n)))) /\ (((forall jt_index_pairrectcrtleft jt_left_pairrectcrtleft jt_right_pairrectcrtleft. (exists jt_gap_pairrectcrtleftindex. jt_gap_pairrectcrtleftindex+S (jt_index_pairrectcrtleft)=(k)) -> (((exists fs_h_jt_pairrectcrtleftleft. fs_h_jt_pairrectcrtleftleft + S (jt_left_pairrectcrtleft) = S ((S (jt_index_pairrectcrtleft)) * jt_g_pairrect)) /\ exists fs_q_jt_pairrectcrtleftleft. jt_f_pairrect = fs_q_jt_pairrectcrtleftleft * S ((S (jt_index_pairrectcrtleft)) * jt_g_pairrect) + (jt_left_pairrectcrtleft))) -> (((exists fs_h_jt_pairrectcrtleftright. fs_h_jt_pairrectcrtleftright + S (jt_right_pairrectcrtleft) = S ((S (jt_index_pairrectcrtleft)) * jt_c_pairrect)) /\ exists fs_q_jt_pairrectcrtleftright. jt_b_pairrect = fs_q_jt_pairrectcrtleftright * S ((S (jt_index_pairrectcrtleft)) * jt_c_pairrect) + (jt_right_pairrectcrtleft))) -> (exists jt_left_pairrectcrtleftmod jt_right_pairrectcrtleftmod. (jt_left_pairrectcrtleft)+(m)*jt_left_pairrectcrtleftmod=(jt_right_pairrectcrtleft)+(m)*jt_right_pairrectcrtleftmod)) /\ (forall jt_index_pairrectcrtright jt_left_pairrectcrtright jt_right_pairrectcrtright. (exists jt_gap_pairrectcrtrightindex. jt_gap_pairrectcrtrightindex+S (jt_index_pairrectcrtright)=(k)) -> (((exists fs_h_jt_pairrectcrtrightleft. fs_h_jt_pairrectcrtrightleft + S (jt_left_pairrectcrtright) = S ((S (jt_index_pairrectcrtright)) * jt_g_pairrect)) /\ exists fs_q_jt_pairrectcrtrightleft. jt_f_pairrect = fs_q_jt_pairrectcrtrightleft * S ((S (jt_index_pairrectcrtright)) * jt_g_pairrect) + (jt_left_pairrectcrtright))) -> (((exists fs_h_jt_pairrectcrtrightright. fs_h_jt_pairrectcrtrightright + S (jt_right_pairrectcrtright) = S ((S (jt_index_pairrectcrtright)) * jt_e_pairrect)) /\ exists fs_q_jt_pairrectcrtrightright. jt_d_pairrect = fs_q_jt_pairrectcrtrightright * S ((S (jt_index_pairrectcrtright)) * jt_e_pairrect) + (jt_right_pairrectcrtright))) -> (exists jt_left_pairrectcrtrightmod jt_right_pairrectcrtrightmod. (jt_left_pairrectcrtright)+(n)*jt_left_pairrectcrtrightmod=(jt_right_pairrectcrtright)+(n)*jt_right_pairrectcrtrightmod)))))) /\ (forall jt_divisor_pairrectprimitive. (exists jt_factor_pairrectprimitivemodulus. (m*n)=(jt_divisor_pairrectprimitive)*jt_factor_pairrectprimitivemodulus) -> (forall jt_index_pairrectprimitivecoordinates jt_value_pairrectprimitivecoordinates. (exists jt_gap_pairrectprimitivecoordinatesindex. jt_gap_pairrectprimitivecoordinatesindex+S (jt_index_pairrectprimitivecoordinates)=(k)) -> (((exists fs_h_jt_pairrectprimitivecoordinatesat. fs_h_jt_pairrectprimitivecoordinatesat + S (jt_value_pairrectprimitivecoordinates) = S ((S (jt_index_pairrectprimitivecoordinates)) * jt_g_pairrect)) /\ exists fs_q_jt_pairrectprimitivecoordinatesat. jt_f_pairrect = fs_q_jt_pairrectprimitivecoordinatesat * S ((S (jt_index_pairrectprimitivecoordinates)) * jt_g_pairrect) + (jt_value_pairrectprimitivecoordinates))) -> (exists jt_factor_pairrectprimitivecoordinatesdivides. (jt_value_pairrectprimitivecoordinates)=(jt_divisor_pairrectprimitive)*jt_factor_pairrectprimitivecoordinatesdivides)) -> jt_divisor_pairrectprimitive=1))))))))))))))) -> (exists jt_gap_pairrow. jt_gap_pairrow+S (i)=(u)) -> (exists jt_gap_paircol. jt_gap_paircol+S (j)=(v)) -> (((((exists fs_h_jt_pairleftcode. fs_h_jt_pairleftcode + S (b) = S ((S (i)) * B)) /\ exists fs_q_jt_pairleftcode. A = fs_q_jt_pairleftcode * S ((S (i)) * B) + (b))) /\ (((exists fs_h_jt_pairleftscale. fs_h_jt_pairleftscale + S (c) = S ((S (i)) * D)) /\ exists fs_q_jt_pairleftscale. C = fs_q_jt_pairleftscale * S ((S (i)) * D) + (c))))) -> (((((exists fs_h_jt_pairrightcode. fs_h_jt_pairrightcode + S (d) = S ((S (j)) * F)) /\ exists fs_q_jt_pairrightcode. E = fs_q_jt_pairrightcode * S ((S (j)) * F) + (d))) /\ (((exists fs_h_jt_pairrightscale. fs_h_jt_pairrightscale + S (e) = S ((S (j)) * H)) /\ exists fs_q_jt_pairrightscale. G = fs_q_jt_pairrightscale * S ((S (j)) * H) + (e))))) -> exists f g. ((((((exists fs_h_jt_pairoutputcode. fs_h_jt_pairoutputcode + S (f) = S ((S (v*i+j)) * Q)) /\ exists fs_q_jt_pairoutputcode. P = fs_q_jt_pairoutputcode * S ((S (v*i+j)) * Q) + (f))) /\ (((exists fs_h_jt_pairoutputscale. fs_h_jt_pairoutputscale + S (g) = S ((S (v*i+j)) * T)) /\ exists fs_q_jt_pairoutputscale. R = fs_q_jt_pairoutputscale * S ((S (v*i+j)) * T) + (g))))) /\ (((((forall jt_index_paircrtbound. (exists jt_gap_paircrtboundindex. jt_gap_paircrtboundindex+S (jt_index_paircrtbound)=(k)) -> exists jt_value_paircrtbound. ((((exists fs_h_jt_paircrtboundat. fs_h_jt_paircrtboundat + S (jt_value_paircrtbound) = S ((S (jt_index_paircrtbound)) * g)) /\ exists fs_q_jt_paircrtboundat. f = fs_q_jt_paircrtboundat * S ((S (jt_index_paircrtbound)) * g) + (jt_value_paircrtbound))) /\ (exists jt_gap_paircrtboundvalue. jt_gap_paircrtboundvalue+S (jt_value_paircrtbound)=(m*n)))) /\ (((forall jt_index_paircrtleft jt_left_paircrtleft jt_right_paircrtleft. (exists jt_gap_paircrtleftindex. jt_gap_paircrtleftindex+S (jt_index_paircrtleft)=(k)) -> (((exists fs_h_jt_paircrtleftleft. fs_h_jt_paircrtleftleft + S (jt_left_paircrtleft) = S ((S (jt_index_paircrtleft)) * g)) /\ exists fs_q_jt_paircrtleftleft. f = fs_q_jt_paircrtleftleft * S ((S (jt_index_paircrtleft)) * g) + (jt_left_paircrtleft))) -> (((exists fs_h_jt_paircrtleftright. fs_h_jt_paircrtleftright + S (jt_right_paircrtleft) = S ((S (jt_index_paircrtleft)) * c)) /\ exists fs_q_jt_paircrtleftright. b = fs_q_jt_paircrtleftright * S ((S (jt_index_paircrtleft)) * c) + (jt_right_paircrtleft))) -> (exists jt_left_paircrtleftmod jt_right_paircrtleftmod. (jt_left_paircrtleft)+(m)*jt_left_paircrtleftmod=(jt_right_paircrtleft)+(m)*jt_right_paircrtleftmod)) /\ (forall jt_index_paircrtright jt_left_paircrtright jt_right_paircrtright. (exists jt_gap_paircrtrightindex. jt_gap_paircrtrightindex+S (jt_index_paircrtright)=(k)) -> (((exists fs_h_jt_paircrtrightleft. fs_h_jt_paircrtrightleft + S (jt_left_paircrtright) = S ((S (jt_index_paircrtright)) * g)) /\ exists fs_q_jt_paircrtrightleft. f = fs_q_jt_paircrtrightleft * S ((S (jt_index_paircrtright)) * g) + (jt_left_paircrtright))) -> (((exists fs_h_jt_paircrtrightright. fs_h_jt_paircrtrightright + S (jt_right_paircrtright) = S ((S (jt_index_paircrtright)) * e)) /\ exists fs_q_jt_paircrtrightright. d = fs_q_jt_paircrtrightright * S ((S (jt_index_paircrtright)) * e) + (jt_right_paircrtright))) -> (exists jt_left_paircrtrightmod jt_right_paircrtrightmod. (jt_left_paircrtright)+(n)*jt_left_paircrtrightmod=(jt_right_paircrtright)+(n)*jt_right_paircrtrightmod)))))) /\ (forall jt_divisor_pairprimitive. (exists jt_factor_pairprimitivemodulus. (m*n)=(jt_divisor_pairprimitive)*jt_factor_pairprimitivemodulus) -> (forall jt_index_pairprimitivecoordinates jt_value_pairprimitivecoordinates. (exists jt_gap_pairprimitivecoordinatesindex. jt_gap_pairprimitivecoordinatesindex+S (jt_index_pairprimitivecoordinates)=(k)) -> (((exists fs_h_jt_pairprimitivecoordinatesat. fs_h_jt_pairprimitivecoordinatesat + S (jt_value_pairprimitivecoordinates) = S ((S (jt_index_pairprimitivecoordinates)) * g)) /\ exists fs_q_jt_pairprimitivecoordinatesat. f = fs_q_jt_pairprimitivecoordinatesat * S ((S (jt_index_pairprimitivecoordinates)) * g) + (jt_value_pairprimitivecoordinates))) -> (exists jt_factor_pairprimitivecoordinatesdivides. (jt_value_pairprimitivecoordinates)=(jt_divisor_pairprimitive)*jt_factor_pairprimitivecoordinatesdivides)) -> jt_divisor_pairprimitive=1))))