jordan_rectangle_crt_actual_entry

forall m n k A B C D u E F G H v P Q R T q p f g. (forall jt_index_locrect. (exists jt_gap_locrectindex. jt_gap_locrectindex+S (jt_index_locrect)=(q)) -> exists jt_row_locrect jt_column_locrect jt_b_locrect jt_c_locrect jt_d_locrect jt_e_locrect jt_f_locrect jt_g_locrect. ((exists jt_gap_locrectrow. jt_gap_locrectrow+S (jt_row_locrect)=(u)) /\ (((exists jt_gap_locrectcolumn. jt_gap_locrectcolumn+S (jt_column_locrect)=(v)) /\ (((jt_index_locrect=(v)*jt_row_locrect+jt_column_locrect) /\ (((((((exists fs_h_jt_locrectleftcode. fs_h_jt_locrectleftcode + S (jt_b_locrect) = S ((S (jt_row_locrect)) * B)) /\ exists fs_q_jt_locrectleftcode. A = fs_q_jt_locrectleftcode * S ((S (jt_row_locrect)) * B) + (jt_b_locrect))) /\ (((exists fs_h_jt_locrectleftscale. fs_h_jt_locrectleftscale + S (jt_c_locrect) = S ((S (jt_row_locrect)) * D)) /\ exists fs_q_jt_locrectleftscale. C = fs_q_jt_locrectleftscale * S ((S (jt_row_locrect)) * D) + (jt_c_locrect))))) /\ (((((((exists fs_h_jt_locrectrightcode. fs_h_jt_locrectrightcode + S (jt_d_locrect) = S ((S (jt_column_locrect)) * F)) /\ exists fs_q_jt_locrectrightcode. E = fs_q_jt_locrectrightcode * S ((S (jt_column_locrect)) * F) + (jt_d_locrect))) /\ (((exists fs_h_jt_locrectrightscale. fs_h_jt_locrectrightscale + S (jt_e_locrect) = S ((S (jt_column_locrect)) * H)) /\ exists fs_q_jt_locrectrightscale. G = fs_q_jt_locrectrightscale * S ((S (jt_column_locrect)) * H) + (jt_e_locrect))))) /\ (((((((exists fs_h_jt_locrectoutputcode. fs_h_jt_locrectoutputcode + S (jt_f_locrect) = S ((S (jt_index_locrect)) * Q)) /\ exists fs_q_jt_locrectoutputcode. P = fs_q_jt_locrectoutputcode * S ((S (jt_index_locrect)) * Q) + (jt_f_locrect))) /\ (((exists fs_h_jt_locrectoutputscale. fs_h_jt_locrectoutputscale + S (jt_g_locrect) = S ((S (jt_index_locrect)) * T)) /\ exists fs_q_jt_locrectoutputscale. R = fs_q_jt_locrectoutputscale * S ((S (jt_index_locrect)) * T) + (jt_g_locrect))))) /\ (((((forall jt_index_locrectcrtbound. (exists jt_gap_locrectcrtboundindex. jt_gap_locrectcrtboundindex+S (jt_index_locrectcrtbound)=(k)) -> exists jt_value_locrectcrtbound. ((((exists fs_h_jt_locrectcrtboundat. fs_h_jt_locrectcrtboundat + S (jt_value_locrectcrtbound) = S ((S (jt_index_locrectcrtbound)) * jt_g_locrect)) /\ exists fs_q_jt_locrectcrtboundat. jt_f_locrect = fs_q_jt_locrectcrtboundat * S ((S (jt_index_locrectcrtbound)) * jt_g_locrect) + (jt_value_locrectcrtbound))) /\ (exists jt_gap_locrectcrtboundvalue. jt_gap_locrectcrtboundvalue+S (jt_value_locrectcrtbound)=(m*n)))) /\ (((forall jt_index_locrectcrtleft jt_left_locrectcrtleft jt_right_locrectcrtleft. (exists jt_gap_locrectcrtleftindex. jt_gap_locrectcrtleftindex+S (jt_index_locrectcrtleft)=(k)) -> (((exists fs_h_jt_locrectcrtleftleft. fs_h_jt_locrectcrtleftleft + S (jt_left_locrectcrtleft) = S ((S (jt_index_locrectcrtleft)) * jt_g_locrect)) /\ exists fs_q_jt_locrectcrtleftleft. jt_f_locrect = fs_q_jt_locrectcrtleftleft * S ((S (jt_index_locrectcrtleft)) * jt_g_locrect) + (jt_left_locrectcrtleft))) -> (((exists fs_h_jt_locrectcrtleftright. fs_h_jt_locrectcrtleftright + S (jt_right_locrectcrtleft) = S ((S (jt_index_locrectcrtleft)) * jt_c_locrect)) /\ exists fs_q_jt_locrectcrtleftright. jt_b_locrect = fs_q_jt_locrectcrtleftright * S ((S (jt_index_locrectcrtleft)) * jt_c_locrect) + (jt_right_locrectcrtleft))) -> (exists jt_left_locrectcrtleftmod jt_right_locrectcrtleftmod. (jt_left_locrectcrtleft)+(m)*jt_left_locrectcrtleftmod=(jt_right_locrectcrtleft)+(m)*jt_right_locrectcrtleftmod)) /\ (forall jt_index_locrectcrtright jt_left_locrectcrtright jt_right_locrectcrtright. (exists jt_gap_locrectcrtrightindex. jt_gap_locrectcrtrightindex+S (jt_index_locrectcrtright)=(k)) -> (((exists fs_h_jt_locrectcrtrightleft. fs_h_jt_locrectcrtrightleft + S (jt_left_locrectcrtright) = S ((S (jt_index_locrectcrtright)) * jt_g_locrect)) /\ exists fs_q_jt_locrectcrtrightleft. jt_f_locrect = fs_q_jt_locrectcrtrightleft * S ((S (jt_index_locrectcrtright)) * jt_g_locrect) + (jt_left_locrectcrtright))) -> (((exists fs_h_jt_locrectcrtrightright. fs_h_jt_locrectcrtrightright + S (jt_right_locrectcrtright) = S ((S (jt_index_locrectcrtright)) * jt_e_locrect)) /\ exists fs_q_jt_locrectcrtrightright. jt_d_locrect = fs_q_jt_locrectcrtrightright * S ((S (jt_index_locrectcrtright)) * jt_e_locrect) + (jt_right_locrectcrtright))) -> (exists jt_left_locrectcrtrightmod jt_right_locrectcrtrightmod. (jt_left_locrectcrtright)+(n)*jt_left_locrectcrtrightmod=(jt_right_locrectcrtright)+(n)*jt_right_locrectcrtrightmod)))))) /\ (forall jt_divisor_locrectprimitive. (exists jt_factor_locrectprimitivemodulus. (m*n)=(jt_divisor_locrectprimitive)*jt_factor_locrectprimitivemodulus) -> (forall jt_index_locrectprimitivecoordinates jt_value_locrectprimitivecoordinates. (exists jt_gap_locrectprimitivecoordinatesindex. jt_gap_locrectprimitivecoordinatesindex+S (jt_index_locrectprimitivecoordinates)=(k)) -> (((exists fs_h_jt_locrectprimitivecoordinatesat. fs_h_jt_locrectprimitivecoordinatesat + S (jt_value_locrectprimitivecoordinates) = S ((S (jt_index_locrectprimitivecoordinates)) * jt_g_locrect)) /\ exists fs_q_jt_locrectprimitivecoordinatesat. jt_f_locrect = fs_q_jt_locrectprimitivecoordinatesat * S ((S (jt_index_locrectprimitivecoordinates)) * jt_g_locrect) + (jt_value_locrectprimitivecoordinates))) -> (exists jt_factor_locrectprimitivecoordinatesdivides. (jt_value_locrectprimitivecoordinates)=(jt_divisor_locrectprimitive)*jt_factor_locrectprimitivecoordinatesdivides)) -> jt_divisor_locrectprimitive=1))))))))))))))) -> (exists jt_gap_locbound. jt_gap_locbound+S (p)=(q)) -> (((((exists fs_h_jt_locentrycode. fs_h_jt_locentrycode + S (f) = S ((S (p)) * Q)) /\ exists fs_q_jt_locentrycode. P = fs_q_jt_locentrycode * S ((S (p)) * Q) + (f))) /\ (((exists fs_h_jt_locentryscale. fs_h_jt_locentryscale + S (g) = S ((S (p)) * T)) /\ exists fs_q_jt_locentryscale. R = fs_q_jt_locentryscale * S ((S (p)) * T) + (g))))) -> exists i j b c d e. ((exists jt_gap_locresultrow. jt_gap_locresultrow+S (i)=(u)) /\ (((exists jt_gap_locresultcolumn. jt_gap_locresultcolumn+S (j)=(v)) /\ (((p=(v)*(i)+(j)) /\ (((((((exists fs_h_jt_locresultleftcode. fs_h_jt_locresultleftcode + S (b) = S ((S (i)) * B)) /\ exists fs_q_jt_locresultleftcode. A = fs_q_jt_locresultleftcode * S ((S (i)) * B) + (b))) /\ (((exists fs_h_jt_locresultleftscale. fs_h_jt_locresultleftscale + S (c) = S ((S (i)) * D)) /\ exists fs_q_jt_locresultleftscale. C = fs_q_jt_locresultleftscale * S ((S (i)) * D) + (c))))) /\ (((((((exists fs_h_jt_locresultrightcode. fs_h_jt_locresultrightcode + S (d) = S ((S (j)) * F)) /\ exists fs_q_jt_locresultrightcode. E = fs_q_jt_locresultrightcode * S ((S (j)) * F) + (d))) /\ (((exists fs_h_jt_locresultrightscale. fs_h_jt_locresultrightscale + S (e) = S ((S (j)) * H)) /\ exists fs_q_jt_locresultrightscale. G = fs_q_jt_locresultrightscale * S ((S (j)) * H) + (e))))) /\ (((((((exists fs_h_jt_locresultoutputcode. fs_h_jt_locresultoutputcode + S (f) = S ((S (p)) * Q)) /\ exists fs_q_jt_locresultoutputcode. P = fs_q_jt_locresultoutputcode * S ((S (p)) * Q) + (f))) /\ (((exists fs_h_jt_locresultoutputscale. fs_h_jt_locresultoutputscale + S (g) = S ((S (p)) * T)) /\ exists fs_q_jt_locresultoutputscale. R = fs_q_jt_locresultoutputscale * S ((S (p)) * T) + (g))))) /\ (((((forall jt_index_locresultcrtbound. (exists jt_gap_locresultcrtboundindex. jt_gap_locresultcrtboundindex+S (jt_index_locresultcrtbound)=(k)) -> exists jt_value_locresultcrtbound. ((((exists fs_h_jt_locresultcrtboundat. fs_h_jt_locresultcrtboundat + S (jt_value_locresultcrtbound) = S ((S (jt_index_locresultcrtbound)) * g)) /\ exists fs_q_jt_locresultcrtboundat. f = fs_q_jt_locresultcrtboundat * S ((S (jt_index_locresultcrtbound)) * g) + (jt_value_locresultcrtbound))) /\ (exists jt_gap_locresultcrtboundvalue. jt_gap_locresultcrtboundvalue+S (jt_value_locresultcrtbound)=(m*n)))) /\ (((forall jt_index_locresultcrtleft jt_left_locresultcrtleft jt_right_locresultcrtleft. (exists jt_gap_locresultcrtleftindex. jt_gap_locresultcrtleftindex+S (jt_index_locresultcrtleft)=(k)) -> (((exists fs_h_jt_locresultcrtleftleft. fs_h_jt_locresultcrtleftleft + S (jt_left_locresultcrtleft) = S ((S (jt_index_locresultcrtleft)) * g)) /\ exists fs_q_jt_locresultcrtleftleft. f = fs_q_jt_locresultcrtleftleft * S ((S (jt_index_locresultcrtleft)) * g) + (jt_left_locresultcrtleft))) -> (((exists fs_h_jt_locresultcrtleftright. fs_h_jt_locresultcrtleftright + S (jt_right_locresultcrtleft) = S ((S (jt_index_locresultcrtleft)) * c)) /\ exists fs_q_jt_locresultcrtleftright. b = fs_q_jt_locresultcrtleftright * S ((S (jt_index_locresultcrtleft)) * c) + (jt_right_locresultcrtleft))) -> (exists jt_left_locresultcrtleftmod jt_right_locresultcrtleftmod. (jt_left_locresultcrtleft)+(m)*jt_left_locresultcrtleftmod=(jt_right_locresultcrtleft)+(m)*jt_right_locresultcrtleftmod)) /\ (forall jt_index_locresultcrtright jt_left_locresultcrtright jt_right_locresultcrtright. (exists jt_gap_locresultcrtrightindex. jt_gap_locresultcrtrightindex+S (jt_index_locresultcrtright)=(k)) -> (((exists fs_h_jt_locresultcrtrightleft. fs_h_jt_locresultcrtrightleft + S (jt_left_locresultcrtright) = S ((S (jt_index_locresultcrtright)) * g)) /\ exists fs_q_jt_locresultcrtrightleft. f = fs_q_jt_locresultcrtrightleft * S ((S (jt_index_locresultcrtright)) * g) + (jt_left_locresultcrtright))) -> (((exists fs_h_jt_locresultcrtrightright. fs_h_jt_locresultcrtrightright + S (jt_right_locresultcrtright) = S ((S (jt_index_locresultcrtright)) * e)) /\ exists fs_q_jt_locresultcrtrightright. d = fs_q_jt_locresultcrtrightright * S ((S (jt_index_locresultcrtright)) * e) + (jt_right_locresultcrtright))) -> (exists jt_left_locresultcrtrightmod jt_right_locresultcrtrightmod. (jt_left_locresultcrtright)+(n)*jt_left_locresultcrtrightmod=(jt_right_locresultcrtright)+(n)*jt_right_locresultcrtrightmod)))))) /\ (forall jt_divisor_locresultprimitive. (exists jt_factor_locresultprimitivemodulus. (m*n)=(jt_divisor_locresultprimitive)*jt_factor_locresultprimitivemodulus) -> (forall jt_index_locresultprimitivecoordinates jt_value_locresultprimitivecoordinates. (exists jt_gap_locresultprimitivecoordinatesindex. jt_gap_locresultprimitivecoordinatesindex+S (jt_index_locresultprimitivecoordinates)=(k)) -> (((exists fs_h_jt_locresultprimitivecoordinatesat. fs_h_jt_locresultprimitivecoordinatesat + S (jt_value_locresultprimitivecoordinates) = S ((S (jt_index_locresultprimitivecoordinates)) * g)) /\ exists fs_q_jt_locresultprimitivecoordinatesat. f = fs_q_jt_locresultprimitivecoordinatesat * S ((S (jt_index_locresultprimitivecoordinates)) * g) + (jt_value_locresultprimitivecoordinates))) -> (exists jt_factor_locresultprimitivecoordinatesdivides. (jt_value_locresultprimitivecoordinates)=(jt_divisor_locresultprimitive)*jt_factor_locresultprimitivecoordinatesdivides)) -> jt_divisor_locresultprimitive=1))))))))))))))