euler_theorem_for_units

Exact expanded first-order arithmetic statement

forall a m t. ((exists eut_gap_eu_G014_domain. eut_gap_eu_G014_domain + S (1) = (m)) /\ (((exists eut_gap_eu_G014_unit_domain. eut_gap_eu_G014_unit_domain + S (1) = (m)) /\ exists eu_inverse_G014_unit. (exists eut_gap_eu_G014_unit_bound. eut_gap_eu_G014_unit_bound + S (eu_inverse_G014_unit) = (m)) /\ (exists eu_mod_left_G014_unit_inverse eu_mod_right_G014_unit_inverse. ((a)*eu_inverse_G014_unit) + (m) * eu_mod_left_G014_unit_inverse = (1) + (m) * eu_mod_right_G014_unit_inverse)) /\ ((~((m)=0) /\ (exists eut_code_eu_G014_phi_count eut_scale_eu_G014_phi_count. (forall eut_index_eu_G014_phi_count_mask. (exists eut_gap_eu_G014_phi_count_mask_bound. eut_gap_eu_G014_phi_count_mask_bound + S (eut_index_eu_G014_phi_count_mask) = (m)) -> exists eut_bit_eu_G014_phi_count_mask. (((exists fs_h_eut_eu_G014_phi_count_mask_entry. fs_h_eut_eu_G014_phi_count_mask_entry + S (eut_bit_eu_G014_phi_count_mask) = S ((S (eut_index_eu_G014_phi_count_mask)) * eut_scale_eu_G014_phi_count)) /\ exists fs_q_eut_eu_G014_phi_count_mask_entry. eut_code_eu_G014_phi_count = fs_q_eut_eu_G014_phi_count_mask_entry * S ((S (eut_index_eu_G014_phi_count_mask)) * eut_scale_eu_G014_phi_count) + (eut_bit_eu_G014_phi_count_mask))) /\ ((((forall eut_divisor_eu_G014_phi_count_mask_choice_coprime. (exists eut_left_eu_G014_phi_count_mask_choice_coprime. (eut_index_eu_G014_phi_count_mask) = eut_divisor_eu_G014_phi_count_mask_choice_coprime * eut_left_eu_G014_phi_count_mask_choice_coprime) -> (exists eut_right_eu_G014_phi_count_mask_choice_coprime. (m) = eut_divisor_eu_G014_phi_count_mask_choice_coprime * eut_right_eu_G014_phi_count_mask_choice_coprime) -> eut_divisor_eu_G014_phi_count_mask_choice_coprime = 1) /\ (eut_bit_eu_G014_phi_count_mask) = 1) \/ (~(forall eut_divisor_eu_G014_phi_count_mask_choice_coprime. (exists eut_left_eu_G014_phi_count_mask_choice_coprime. (eut_index_eu_G014_phi_count_mask) = eut_divisor_eu_G014_phi_count_mask_choice_coprime * eut_left_eu_G014_phi_count_mask_choice_coprime) -> (exists eut_right_eu_G014_phi_count_mask_choice_coprime. (m) = eut_divisor_eu_G014_phi_count_mask_choice_coprime * eut_right_eu_G014_phi_count_mask_choice_coprime) -> eut_divisor_eu_G014_phi_count_mask_choice_coprime = 1) /\ (eut_bit_eu_G014_phi_count_mask) = 0)))) /\ (exists fs_u_eut_eu_G014_phi_count_sum fs_v_eut_eu_G014_phi_count_sum. ((((exists fs_h_eut_eu_G014_phi_count_sum_body_start. fs_h_eut_eu_G014_phi_count_sum_body_start + S (0) = S ((S (0)) * fs_v_eut_eu_G014_phi_count_sum)) /\ exists fs_q_eut_eu_G014_phi_count_sum_body_start. fs_u_eut_eu_G014_phi_count_sum = fs_q_eut_eu_G014_phi_count_sum_body_start * S ((S (0)) * fs_v_eut_eu_G014_phi_count_sum) + (0))) /\ ((((exists fs_h_eut_eu_G014_phi_count_sum_body_terminal. fs_h_eut_eu_G014_phi_count_sum_body_terminal + S (t) = S ((S (m)) * fs_v_eut_eu_G014_phi_count_sum)) /\ exists fs_q_eut_eu_G014_phi_count_sum_body_terminal. fs_u_eut_eu_G014_phi_count_sum = fs_q_eut_eu_G014_phi_count_sum_body_terminal * S ((S (m)) * fs_v_eut_eu_G014_phi_count_sum) + (t))) /\ forall fs_i_eut_eu_G014_phi_count_sum_body_steps. (exists fs_lt_eut_eu_G014_phi_count_sum_body_steps_bound. fs_lt_eut_eu_G014_phi_count_sum_body_steps_bound + S fs_i_eut_eu_G014_phi_count_sum_body_steps = m) -> exists fs_a_eut_eu_G014_phi_count_sum_body_steps fs_r_eut_eu_G014_phi_count_sum_body_steps fs_s_eut_eu_G014_phi_count_sum_body_steps. ((((exists fs_h_eut_eu_G014_phi_count_sum_body_steps_summand. fs_h_eut_eu_G014_phi_count_sum_body_steps_summand + S (fs_a_eut_eu_G014_phi_count_sum_body_steps) = S ((S (fs_i_eut_eu_G014_phi_count_sum_body_steps)) * eut_scale_eu_G014_phi_count)) /\ exists fs_q_eut_eu_G014_phi_count_sum_body_steps_summand. eut_code_eu_G014_phi_count = fs_q_eut_eu_G014_phi_count_sum_body_steps_summand * S ((S (fs_i_eut_eu_G014_phi_count_sum_body_steps)) * eut_scale_eu_G014_phi_count) + (fs_a_eut_eu_G014_phi_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_G014_phi_count_sum_body_steps_partial. fs_h_eut_eu_G014_phi_count_sum_body_steps_partial + S (fs_r_eut_eu_G014_phi_count_sum_body_steps) = S ((S (fs_i_eut_eu_G014_phi_count_sum_body_steps)) * fs_v_eut_eu_G014_phi_count_sum)) /\ exists fs_q_eut_eu_G014_phi_count_sum_body_steps_partial. fs_u_eut_eu_G014_phi_count_sum = fs_q_eut_eu_G014_phi_count_sum_body_steps_partial * S ((S (fs_i_eut_eu_G014_phi_count_sum_body_steps)) * fs_v_eut_eu_G014_phi_count_sum) + (fs_r_eut_eu_G014_phi_count_sum_body_steps))) /\ ((((exists fs_h_eut_eu_G014_phi_count_sum_body_steps_successor. fs_h_eut_eu_G014_phi_count_sum_body_steps_successor + S (fs_s_eut_eu_G014_phi_count_sum_body_steps) = S ((S (S fs_i_eut_eu_G014_phi_count_sum_body_steps)) * fs_v_eut_eu_G014_phi_count_sum)) /\ exists fs_q_eut_eu_G014_phi_count_sum_body_steps_successor. fs_u_eut_eu_G014_phi_count_sum = fs_q_eut_eu_G014_phi_count_sum_body_steps_successor * S ((S (S fs_i_eut_eu_G014_phi_count_sum_body_steps)) * fs_v_eut_eu_G014_phi_count_sum) + (fs_s_eut_eu_G014_phi_count_sum_body_steps))) /\ fs_s_eut_eu_G014_phi_count_sum_body_steps = fs_r_eut_eu_G014_phi_count_sum_body_steps + fs_a_eut_eu_G014_phi_count_sum_body_steps))))))))))) -> exists w. (exists pa_b_euta_eu_G014_power pa_c_euta_eu_G014_power. ((forall pa_i_euta_eu_G014_power_repeat. (exists pa_lt_euta_eu_G014_power_repeat_bound. pa_lt_euta_eu_G014_power_repeat_bound + S pa_i_euta_eu_G014_power_repeat = t) -> (((exists pa_h_euta_eu_G014_power_repeat_decoded. pa_h_euta_eu_G014_power_repeat_decoded + S (a) = S ((S (pa_i_euta_eu_G014_power_repeat)) * pa_c_euta_eu_G014_power)) /\ exists pa_q_euta_eu_G014_power_repeat_decoded. pa_b_euta_eu_G014_power = pa_q_euta_eu_G014_power_repeat_decoded * S ((S (pa_i_euta_eu_G014_power_repeat)) * pa_c_euta_eu_G014_power) + (a)))) /\ (exists pa_u_euta_eu_G014_power_product pa_v_euta_eu_G014_power_product. ((((exists pa_h_euta_eu_G014_power_product_start. pa_h_euta_eu_G014_power_product_start + S (1) = S ((S (0)) * pa_v_euta_eu_G014_power_product)) /\ exists pa_q_euta_eu_G014_power_product_start. pa_u_euta_eu_G014_power_product = pa_q_euta_eu_G014_power_product_start * S ((S (0)) * pa_v_euta_eu_G014_power_product) + (1))) /\ ((((exists pa_h_euta_eu_G014_power_product_terminal. pa_h_euta_eu_G014_power_product_terminal + S (w) = S ((S (t)) * pa_v_euta_eu_G014_power_product)) /\ exists pa_q_euta_eu_G014_power_product_terminal. pa_u_euta_eu_G014_power_product = pa_q_euta_eu_G014_power_product_terminal * S ((S (t)) * pa_v_euta_eu_G014_power_product) + (w))) /\ forall pa_i_euta_eu_G014_power_product. (exists pa_lt_euta_eu_G014_power_product_bound. pa_lt_euta_eu_G014_power_product_bound + S pa_i_euta_eu_G014_power_product = t) -> exists pa_p_euta_eu_G014_power_product pa_r_euta_eu_G014_power_product pa_s_euta_eu_G014_power_product. ((((exists pa_h_euta_eu_G014_power_product_factor. pa_h_euta_eu_G014_power_product_factor + S (pa_p_euta_eu_G014_power_product) = S ((S (pa_i_euta_eu_G014_power_product)) * pa_c_euta_eu_G014_power)) /\ exists pa_q_euta_eu_G014_power_product_factor. pa_b_euta_eu_G014_power = pa_q_euta_eu_G014_power_product_factor * S ((S (pa_i_euta_eu_G014_power_product)) * pa_c_euta_eu_G014_power) + (pa_p_euta_eu_G014_power_product))) /\ ((((exists pa_h_euta_eu_G014_power_product_partial. pa_h_euta_eu_G014_power_product_partial + S (pa_r_euta_eu_G014_power_product) = S ((S (pa_i_euta_eu_G014_power_product)) * pa_v_euta_eu_G014_power_product)) /\ exists pa_q_euta_eu_G014_power_product_partial. pa_u_euta_eu_G014_power_product = pa_q_euta_eu_G014_power_product_partial * S ((S (pa_i_euta_eu_G014_power_product)) * pa_v_euta_eu_G014_power_product) + (pa_r_euta_eu_G014_power_product))) /\ ((((exists pa_h_euta_eu_G014_power_product_successor. pa_h_euta_eu_G014_power_product_successor + S (pa_s_euta_eu_G014_power_product) = S ((S (S pa_i_euta_eu_G014_power_product)) * pa_v_euta_eu_G014_power_product)) /\ exists pa_q_euta_eu_G014_power_product_successor. pa_u_euta_eu_G014_power_product = pa_q_euta_eu_G014_power_product_successor * S ((S (S pa_i_euta_eu_G014_power_product)) * pa_v_euta_eu_G014_power_product) + (pa_s_euta_eu_G014_power_product))) /\ pa_s_euta_eu_G014_power_product = pa_r_euta_eu_G014_power_product * pa_p_euta_eu_G014_power_product)))))))) /\ (exists eu_mod_left_G014_result eu_mod_right_G014_result. (w) + (m) * eu_mod_left_G014_result = (1) + (m) * eu_mod_right_G014_result)