jordan_totient_at_one_unique

Exact expanded first-order arithmetic statement

forall k j. (((~((k)=0)) /\ (((~((1)=0)) /\ (exists jt_codes_unit_arbitrary_count jt_code_scale_unit_arbitrary_count jt_scales_unit_arbitrary_count jt_scale_scale_unit_arbitrary_count. ((forall jt_i_unit_arbitrary_countenum. (exists jt_gap_unit_arbitrary_countenumsoundindex. jt_gap_unit_arbitrary_countenumsoundindex+S (jt_i_unit_arbitrary_countenum)=(j)) -> exists jt_b_unit_arbitrary_countenum jt_c_unit_arbitrary_countenum. ((((((exists fs_h_jt_unit_arbitrary_countenumsoundcode. fs_h_jt_unit_arbitrary_countenumsoundcode + S (jt_b_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumsoundcode. jt_codes_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumsoundcode * S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count) + (jt_b_unit_arbitrary_countenum))) /\ (((exists fs_h_jt_unit_arbitrary_countenumsoundscale. fs_h_jt_unit_arbitrary_countenumsoundscale + S (jt_c_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumsoundscale. jt_scales_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumsoundscale * S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count) + (jt_c_unit_arbitrary_countenum))))) /\ (((forall jt_index_unit_arbitrary_countenumbound. (exists jt_gap_unit_arbitrary_countenumboundindex. jt_gap_unit_arbitrary_countenumboundindex+S (jt_index_unit_arbitrary_countenumbound)=(k)) -> exists jt_value_unit_arbitrary_countenumbound. ((((exists fs_h_jt_unit_arbitrary_countenumboundat. fs_h_jt_unit_arbitrary_countenumboundat + S (jt_value_unit_arbitrary_countenumbound) = S ((S (jt_index_unit_arbitrary_countenumbound)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumboundat. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumboundat * S ((S (jt_index_unit_arbitrary_countenumbound)) * jt_c_unit_arbitrary_countenum) + (jt_value_unit_arbitrary_countenumbound))) /\ (exists jt_gap_unit_arbitrary_countenumboundvalue. jt_gap_unit_arbitrary_countenumboundvalue+S (jt_value_unit_arbitrary_countenumbound)=(1)))) /\ (forall jt_divisor_unit_arbitrary_countenumprimitive. (exists jt_factor_unit_arbitrary_countenumprimitivemodulus. (1)=(jt_divisor_unit_arbitrary_countenumprimitive)*jt_factor_unit_arbitrary_countenumprimitivemodulus) -> (forall jt_index_unit_arbitrary_countenumprimitivecoordinates jt_value_unit_arbitrary_countenumprimitivecoordinates. (exists jt_gap_unit_arbitrary_countenumprimitivecoordinatesindex. jt_gap_unit_arbitrary_countenumprimitivecoordinatesindex+S (jt_index_unit_arbitrary_countenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unit_arbitrary_countenumprimitivecoordinatesat. fs_h_jt_unit_arbitrary_countenumprimitivecoordinatesat + S (jt_value_unit_arbitrary_countenumprimitivecoordinates) = S ((S (jt_index_unit_arbitrary_countenumprimitivecoordinates)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumprimitivecoordinatesat. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumprimitivecoordinatesat * S ((S (jt_index_unit_arbitrary_countenumprimitivecoordinates)) * jt_c_unit_arbitrary_countenum) + (jt_value_unit_arbitrary_countenumprimitivecoordinates))) -> (exists jt_factor_unit_arbitrary_countenumprimitivecoordinatesdivides. (jt_value_unit_arbitrary_countenumprimitivecoordinates)=(jt_divisor_unit_arbitrary_countenumprimitive)*jt_factor_unit_arbitrary_countenumprimitivecoordinatesdivides)) -> jt_divisor_unit_arbitrary_countenumprimitive=1))))) /\ (((forall jt_b_unit_arbitrary_countenum jt_c_unit_arbitrary_countenum. (forall jt_index_unit_arbitrary_countenuminputbound. (exists jt_gap_unit_arbitrary_countenuminputboundindex. jt_gap_unit_arbitrary_countenuminputboundindex+S (jt_index_unit_arbitrary_countenuminputbound)=(k)) -> exists jt_value_unit_arbitrary_countenuminputbound. ((((exists fs_h_jt_unit_arbitrary_countenuminputboundat. fs_h_jt_unit_arbitrary_countenuminputboundat + S (jt_value_unit_arbitrary_countenuminputbound) = S ((S (jt_index_unit_arbitrary_countenuminputbound)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenuminputboundat. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenuminputboundat * S ((S (jt_index_unit_arbitrary_countenuminputbound)) * jt_c_unit_arbitrary_countenum) + (jt_value_unit_arbitrary_countenuminputbound))) /\ (exists jt_gap_unit_arbitrary_countenuminputboundvalue. jt_gap_unit_arbitrary_countenuminputboundvalue+S (jt_value_unit_arbitrary_countenuminputbound)=(1)))) -> (forall jt_divisor_unit_arbitrary_countenuminputprimitive. (exists jt_factor_unit_arbitrary_countenuminputprimitivemodulus. (1)=(jt_divisor_unit_arbitrary_countenuminputprimitive)*jt_factor_unit_arbitrary_countenuminputprimitivemodulus) -> (forall jt_index_unit_arbitrary_countenuminputprimitivecoordinates jt_value_unit_arbitrary_countenuminputprimitivecoordinates. (exists jt_gap_unit_arbitrary_countenuminputprimitivecoordinatesindex. jt_gap_unit_arbitrary_countenuminputprimitivecoordinatesindex+S (jt_index_unit_arbitrary_countenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unit_arbitrary_countenuminputprimitivecoordinatesat. fs_h_jt_unit_arbitrary_countenuminputprimitivecoordinatesat + S (jt_value_unit_arbitrary_countenuminputprimitivecoordinates) = S ((S (jt_index_unit_arbitrary_countenuminputprimitivecoordinates)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenuminputprimitivecoordinatesat. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenuminputprimitivecoordinatesat * S ((S (jt_index_unit_arbitrary_countenuminputprimitivecoordinates)) * jt_c_unit_arbitrary_countenum) + (jt_value_unit_arbitrary_countenuminputprimitivecoordinates))) -> (exists jt_factor_unit_arbitrary_countenuminputprimitivecoordinatesdivides. (jt_value_unit_arbitrary_countenuminputprimitivecoordinates)=(jt_divisor_unit_arbitrary_countenuminputprimitive)*jt_factor_unit_arbitrary_countenuminputprimitivecoordinatesdivides)) -> jt_divisor_unit_arbitrary_countenuminputprimitive=1) -> exists jt_i_unit_arbitrary_countenum jt_d_unit_arbitrary_countenum jt_e_unit_arbitrary_countenum. ((exists jt_gap_unit_arbitrary_countenumcompleteindex. jt_gap_unit_arbitrary_countenumcompleteindex+S (jt_i_unit_arbitrary_countenum)=(j)) /\ (((((((exists fs_h_jt_unit_arbitrary_countenumcompletecode. fs_h_jt_unit_arbitrary_countenumcompletecode + S (jt_d_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumcompletecode. jt_codes_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumcompletecode * S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count) + (jt_d_unit_arbitrary_countenum))) /\ (((exists fs_h_jt_unit_arbitrary_countenumcompletescale. fs_h_jt_unit_arbitrary_countenumcompletescale + S (jt_e_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumcompletescale. jt_scales_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumcompletescale * S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count) + (jt_e_unit_arbitrary_countenum))))) /\ (forall jt_index_unit_arbitrary_countenumrepresented jt_left_unit_arbitrary_countenumrepresented jt_right_unit_arbitrary_countenumrepresented. (exists jt_gap_unit_arbitrary_countenumrepresentedindex. jt_gap_unit_arbitrary_countenumrepresentedindex+S (jt_index_unit_arbitrary_countenumrepresented)=(k)) -> (((exists fs_h_jt_unit_arbitrary_countenumrepresentedleft. fs_h_jt_unit_arbitrary_countenumrepresentedleft + S (jt_left_unit_arbitrary_countenumrepresented) = S ((S (jt_index_unit_arbitrary_countenumrepresented)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumrepresentedleft. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumrepresentedleft * S ((S (jt_index_unit_arbitrary_countenumrepresented)) * jt_c_unit_arbitrary_countenum) + (jt_left_unit_arbitrary_countenumrepresented))) -> (((exists fs_h_jt_unit_arbitrary_countenumrepresentedright. fs_h_jt_unit_arbitrary_countenumrepresentedright + S (jt_right_unit_arbitrary_countenumrepresented) = S ((S (jt_index_unit_arbitrary_countenumrepresented)) * jt_e_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumrepresentedright. jt_d_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumrepresentedright * S ((S (jt_index_unit_arbitrary_countenumrepresented)) * jt_e_unit_arbitrary_countenum) + (jt_right_unit_arbitrary_countenumrepresented))) -> jt_left_unit_arbitrary_countenumrepresented=jt_right_unit_arbitrary_countenumrepresented))))) /\ (forall jt_i_unit_arbitrary_countenum jt_h_unit_arbitrary_countenum jt_b_unit_arbitrary_countenum jt_c_unit_arbitrary_countenum jt_d_unit_arbitrary_countenum jt_e_unit_arbitrary_countenum. (exists jt_gap_unit_arbitrary_countenumfirstindex. jt_gap_unit_arbitrary_countenumfirstindex+S (jt_i_unit_arbitrary_countenum)=(j)) -> (exists jt_gap_unit_arbitrary_countenumsecondindex. jt_gap_unit_arbitrary_countenumsecondindex+S (jt_h_unit_arbitrary_countenum)=(j)) -> (((((exists fs_h_jt_unit_arbitrary_countenumfirstcode. fs_h_jt_unit_arbitrary_countenumfirstcode + S (jt_b_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumfirstcode. jt_codes_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumfirstcode * S ((S (jt_i_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count) + (jt_b_unit_arbitrary_countenum))) /\ (((exists fs_h_jt_unit_arbitrary_countenumfirstscale. fs_h_jt_unit_arbitrary_countenumfirstscale + S (jt_c_unit_arbitrary_countenum) = S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumfirstscale. jt_scales_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumfirstscale * S ((S (jt_i_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count) + (jt_c_unit_arbitrary_countenum))))) -> (((((exists fs_h_jt_unit_arbitrary_countenumsecondcode. fs_h_jt_unit_arbitrary_countenumsecondcode + S (jt_d_unit_arbitrary_countenum) = S ((S (jt_h_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumsecondcode. jt_codes_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumsecondcode * S ((S (jt_h_unit_arbitrary_countenum)) * jt_code_scale_unit_arbitrary_count) + (jt_d_unit_arbitrary_countenum))) /\ (((exists fs_h_jt_unit_arbitrary_countenumsecondscale. fs_h_jt_unit_arbitrary_countenumsecondscale + S (jt_e_unit_arbitrary_countenum) = S ((S (jt_h_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count)) /\ exists fs_q_jt_unit_arbitrary_countenumsecondscale. jt_scales_unit_arbitrary_count = fs_q_jt_unit_arbitrary_countenumsecondscale * S ((S (jt_h_unit_arbitrary_countenum)) * jt_scale_scale_unit_arbitrary_count) + (jt_e_unit_arbitrary_countenum))))) -> (forall jt_index_unit_arbitrary_countenumsame jt_left_unit_arbitrary_countenumsame jt_right_unit_arbitrary_countenumsame. (exists jt_gap_unit_arbitrary_countenumsameindex. jt_gap_unit_arbitrary_countenumsameindex+S (jt_index_unit_arbitrary_countenumsame)=(k)) -> (((exists fs_h_jt_unit_arbitrary_countenumsameleft. fs_h_jt_unit_arbitrary_countenumsameleft + S (jt_left_unit_arbitrary_countenumsame) = S ((S (jt_index_unit_arbitrary_countenumsame)) * jt_c_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumsameleft. jt_b_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumsameleft * S ((S (jt_index_unit_arbitrary_countenumsame)) * jt_c_unit_arbitrary_countenum) + (jt_left_unit_arbitrary_countenumsame))) -> (((exists fs_h_jt_unit_arbitrary_countenumsameright. fs_h_jt_unit_arbitrary_countenumsameright + S (jt_right_unit_arbitrary_countenumsame) = S ((S (jt_index_unit_arbitrary_countenumsame)) * jt_e_unit_arbitrary_countenum)) /\ exists fs_q_jt_unit_arbitrary_countenumsameright. jt_d_unit_arbitrary_countenum = fs_q_jt_unit_arbitrary_countenumsameright * S ((S (jt_index_unit_arbitrary_countenumsame)) * jt_e_unit_arbitrary_countenum) + (jt_right_unit_arbitrary_countenumsame))) -> jt_left_unit_arbitrary_countenumsame=jt_right_unit_arbitrary_countenumsame) -> jt_i_unit_arbitrary_countenum=jt_h_unit_arbitrary_countenum))))))))) -> (j=1)