jordan_modulus_zero_excluded

Exact expanded first-order arithmetic statement

forall k j. ~(((~((k)=0)) /\ (((~((0)=0)) /\ (exists jt_codes_zeromod jt_code_scale_zeromod jt_scales_zeromod jt_scale_scale_zeromod. ((forall jt_i_zeromodenum. (exists jt_gap_zeromodenumsoundindex. jt_gap_zeromodenumsoundindex+S (jt_i_zeromodenum)=(j)) -> exists jt_b_zeromodenum jt_c_zeromodenum. ((((((exists fs_h_jt_zeromodenumsoundcode. fs_h_jt_zeromodenumsoundcode + S (jt_b_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod)) /\ exists fs_q_jt_zeromodenumsoundcode. jt_codes_zeromod = fs_q_jt_zeromodenumsoundcode * S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod) + (jt_b_zeromodenum))) /\ (((exists fs_h_jt_zeromodenumsoundscale. fs_h_jt_zeromodenumsoundscale + S (jt_c_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod)) /\ exists fs_q_jt_zeromodenumsoundscale. jt_scales_zeromod = fs_q_jt_zeromodenumsoundscale * S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod) + (jt_c_zeromodenum))))) /\ (((forall jt_index_zeromodenumbound. (exists jt_gap_zeromodenumboundindex. jt_gap_zeromodenumboundindex+S (jt_index_zeromodenumbound)=(k)) -> exists jt_value_zeromodenumbound. ((((exists fs_h_jt_zeromodenumboundat. fs_h_jt_zeromodenumboundat + S (jt_value_zeromodenumbound) = S ((S (jt_index_zeromodenumbound)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenumboundat. jt_b_zeromodenum = fs_q_jt_zeromodenumboundat * S ((S (jt_index_zeromodenumbound)) * jt_c_zeromodenum) + (jt_value_zeromodenumbound))) /\ (exists jt_gap_zeromodenumboundvalue. jt_gap_zeromodenumboundvalue+S (jt_value_zeromodenumbound)=(0)))) /\ (forall jt_divisor_zeromodenumprimitive. (exists jt_factor_zeromodenumprimitivemodulus. (0)=(jt_divisor_zeromodenumprimitive)*jt_factor_zeromodenumprimitivemodulus) -> (forall jt_index_zeromodenumprimitivecoordinates jt_value_zeromodenumprimitivecoordinates. (exists jt_gap_zeromodenumprimitivecoordinatesindex. jt_gap_zeromodenumprimitivecoordinatesindex+S (jt_index_zeromodenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_zeromodenumprimitivecoordinatesat. fs_h_jt_zeromodenumprimitivecoordinatesat + S (jt_value_zeromodenumprimitivecoordinates) = S ((S (jt_index_zeromodenumprimitivecoordinates)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenumprimitivecoordinatesat. jt_b_zeromodenum = fs_q_jt_zeromodenumprimitivecoordinatesat * S ((S (jt_index_zeromodenumprimitivecoordinates)) * jt_c_zeromodenum) + (jt_value_zeromodenumprimitivecoordinates))) -> (exists jt_factor_zeromodenumprimitivecoordinatesdivides. (jt_value_zeromodenumprimitivecoordinates)=(jt_divisor_zeromodenumprimitive)*jt_factor_zeromodenumprimitivecoordinatesdivides)) -> jt_divisor_zeromodenumprimitive=1))))) /\ (((forall jt_b_zeromodenum jt_c_zeromodenum. (forall jt_index_zeromodenuminputbound. (exists jt_gap_zeromodenuminputboundindex. jt_gap_zeromodenuminputboundindex+S (jt_index_zeromodenuminputbound)=(k)) -> exists jt_value_zeromodenuminputbound. ((((exists fs_h_jt_zeromodenuminputboundat. fs_h_jt_zeromodenuminputboundat + S (jt_value_zeromodenuminputbound) = S ((S (jt_index_zeromodenuminputbound)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenuminputboundat. jt_b_zeromodenum = fs_q_jt_zeromodenuminputboundat * S ((S (jt_index_zeromodenuminputbound)) * jt_c_zeromodenum) + (jt_value_zeromodenuminputbound))) /\ (exists jt_gap_zeromodenuminputboundvalue. jt_gap_zeromodenuminputboundvalue+S (jt_value_zeromodenuminputbound)=(0)))) -> (forall jt_divisor_zeromodenuminputprimitive. (exists jt_factor_zeromodenuminputprimitivemodulus. (0)=(jt_divisor_zeromodenuminputprimitive)*jt_factor_zeromodenuminputprimitivemodulus) -> (forall jt_index_zeromodenuminputprimitivecoordinates jt_value_zeromodenuminputprimitivecoordinates. (exists jt_gap_zeromodenuminputprimitivecoordinatesindex. jt_gap_zeromodenuminputprimitivecoordinatesindex+S (jt_index_zeromodenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_zeromodenuminputprimitivecoordinatesat. fs_h_jt_zeromodenuminputprimitivecoordinatesat + S (jt_value_zeromodenuminputprimitivecoordinates) = S ((S (jt_index_zeromodenuminputprimitivecoordinates)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenuminputprimitivecoordinatesat. jt_b_zeromodenum = fs_q_jt_zeromodenuminputprimitivecoordinatesat * S ((S (jt_index_zeromodenuminputprimitivecoordinates)) * jt_c_zeromodenum) + (jt_value_zeromodenuminputprimitivecoordinates))) -> (exists jt_factor_zeromodenuminputprimitivecoordinatesdivides. (jt_value_zeromodenuminputprimitivecoordinates)=(jt_divisor_zeromodenuminputprimitive)*jt_factor_zeromodenuminputprimitivecoordinatesdivides)) -> jt_divisor_zeromodenuminputprimitive=1) -> exists jt_i_zeromodenum jt_d_zeromodenum jt_e_zeromodenum. ((exists jt_gap_zeromodenumcompleteindex. jt_gap_zeromodenumcompleteindex+S (jt_i_zeromodenum)=(j)) /\ (((((((exists fs_h_jt_zeromodenumcompletecode. fs_h_jt_zeromodenumcompletecode + S (jt_d_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod)) /\ exists fs_q_jt_zeromodenumcompletecode. jt_codes_zeromod = fs_q_jt_zeromodenumcompletecode * S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod) + (jt_d_zeromodenum))) /\ (((exists fs_h_jt_zeromodenumcompletescale. fs_h_jt_zeromodenumcompletescale + S (jt_e_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod)) /\ exists fs_q_jt_zeromodenumcompletescale. jt_scales_zeromod = fs_q_jt_zeromodenumcompletescale * S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod) + (jt_e_zeromodenum))))) /\ (forall jt_index_zeromodenumrepresented jt_left_zeromodenumrepresented jt_right_zeromodenumrepresented. (exists jt_gap_zeromodenumrepresentedindex. jt_gap_zeromodenumrepresentedindex+S (jt_index_zeromodenumrepresented)=(k)) -> (((exists fs_h_jt_zeromodenumrepresentedleft. fs_h_jt_zeromodenumrepresentedleft + S (jt_left_zeromodenumrepresented) = S ((S (jt_index_zeromodenumrepresented)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenumrepresentedleft. jt_b_zeromodenum = fs_q_jt_zeromodenumrepresentedleft * S ((S (jt_index_zeromodenumrepresented)) * jt_c_zeromodenum) + (jt_left_zeromodenumrepresented))) -> (((exists fs_h_jt_zeromodenumrepresentedright. fs_h_jt_zeromodenumrepresentedright + S (jt_right_zeromodenumrepresented) = S ((S (jt_index_zeromodenumrepresented)) * jt_e_zeromodenum)) /\ exists fs_q_jt_zeromodenumrepresentedright. jt_d_zeromodenum = fs_q_jt_zeromodenumrepresentedright * S ((S (jt_index_zeromodenumrepresented)) * jt_e_zeromodenum) + (jt_right_zeromodenumrepresented))) -> jt_left_zeromodenumrepresented=jt_right_zeromodenumrepresented))))) /\ (forall jt_i_zeromodenum jt_h_zeromodenum jt_b_zeromodenum jt_c_zeromodenum jt_d_zeromodenum jt_e_zeromodenum. (exists jt_gap_zeromodenumfirstindex. jt_gap_zeromodenumfirstindex+S (jt_i_zeromodenum)=(j)) -> (exists jt_gap_zeromodenumsecondindex. jt_gap_zeromodenumsecondindex+S (jt_h_zeromodenum)=(j)) -> (((((exists fs_h_jt_zeromodenumfirstcode. fs_h_jt_zeromodenumfirstcode + S (jt_b_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod)) /\ exists fs_q_jt_zeromodenumfirstcode. jt_codes_zeromod = fs_q_jt_zeromodenumfirstcode * S ((S (jt_i_zeromodenum)) * jt_code_scale_zeromod) + (jt_b_zeromodenum))) /\ (((exists fs_h_jt_zeromodenumfirstscale. fs_h_jt_zeromodenumfirstscale + S (jt_c_zeromodenum) = S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod)) /\ exists fs_q_jt_zeromodenumfirstscale. jt_scales_zeromod = fs_q_jt_zeromodenumfirstscale * S ((S (jt_i_zeromodenum)) * jt_scale_scale_zeromod) + (jt_c_zeromodenum))))) -> (((((exists fs_h_jt_zeromodenumsecondcode. fs_h_jt_zeromodenumsecondcode + S (jt_d_zeromodenum) = S ((S (jt_h_zeromodenum)) * jt_code_scale_zeromod)) /\ exists fs_q_jt_zeromodenumsecondcode. jt_codes_zeromod = fs_q_jt_zeromodenumsecondcode * S ((S (jt_h_zeromodenum)) * jt_code_scale_zeromod) + (jt_d_zeromodenum))) /\ (((exists fs_h_jt_zeromodenumsecondscale. fs_h_jt_zeromodenumsecondscale + S (jt_e_zeromodenum) = S ((S (jt_h_zeromodenum)) * jt_scale_scale_zeromod)) /\ exists fs_q_jt_zeromodenumsecondscale. jt_scales_zeromod = fs_q_jt_zeromodenumsecondscale * S ((S (jt_h_zeromodenum)) * jt_scale_scale_zeromod) + (jt_e_zeromodenum))))) -> (forall jt_index_zeromodenumsame jt_left_zeromodenumsame jt_right_zeromodenumsame. (exists jt_gap_zeromodenumsameindex. jt_gap_zeromodenumsameindex+S (jt_index_zeromodenumsame)=(k)) -> (((exists fs_h_jt_zeromodenumsameleft. fs_h_jt_zeromodenumsameleft + S (jt_left_zeromodenumsame) = S ((S (jt_index_zeromodenumsame)) * jt_c_zeromodenum)) /\ exists fs_q_jt_zeromodenumsameleft. jt_b_zeromodenum = fs_q_jt_zeromodenumsameleft * S ((S (jt_index_zeromodenumsame)) * jt_c_zeromodenum) + (jt_left_zeromodenumsame))) -> (((exists fs_h_jt_zeromodenumsameright. fs_h_jt_zeromodenumsameright + S (jt_right_zeromodenumsame) = S ((S (jt_index_zeromodenumsame)) * jt_e_zeromodenum)) /\ exists fs_q_jt_zeromodenumsameright. jt_d_zeromodenum = fs_q_jt_zeromodenumsameright * S ((S (jt_index_zeromodenumsame)) * jt_e_zeromodenum) + (jt_right_zeromodenumsame))) -> jt_left_zeromodenumsame=jt_right_zeromodenumsame) -> jt_i_zeromodenum=jt_h_zeromodenum)))))))))