TS003F

two_square_iff_zero_or_even_three_mod_four_prime_valuations

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Full all-natural two-square theorem, with zero explicitly separated from the nonzero even-prime-valuation criterion.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall n. (((exists ftsc_first_ftsp_value_result ftsc_second_ftsp_value_result. (n) = ftsc_first_ftsp_value_result * ftsc_first_ftsp_value_result + ftsc_second_ftsp_value_result * ftsc_second_ftsp_value_result) -> (n = 0 \/ (~(n = 0) /\ (forall ftsp_bad_prime_value ftsp_bad_exponent_value. ((~(ftsp_bad_prime_value = 1) /\ forall frm_prime_left_ftsp_value_prime frm_prime_right_ftsp_value_prime. ftsp_bad_prime_value = frm_prime_left_ftsp_value_prime * frm_prime_right_ftsp_value_prime -> frm_prime_left_ftsp_value_prime = 1 \/ frm_prime_right_ftsp_value_prime = 1)) -> (exists ftsc_four_three_ftsp_value_three. (ftsp_bad_prime_value) = 4 * ftsc_four_three_ftsp_value_three + 3) -> (((exists bpv_gap_ftsp_value_valuation_exponent_bound. bpv_gap_ftsp_value_valuation_exponent_bound + ftsp_bad_exponent_value = (n)) /\ (exists bpv_result_ftsp_value_valuation_selected. ((exists ff_b_ftsp_value_valuation_selected_power ff_c_ftsp_value_valuation_selected_power. ((forall ff_i_ftsp_value_valuation_selected_power_repeat. (exists ff_lt_ftsp_value_valuation_selected_power_repeat_bound. ff_lt_ftsp_value_valuation_selected_power_repeat_bound + S ff_i_ftsp_value_valuation_selected_power_repeat = ftsp_bad_exponent_value) -> (((exists ff_h_ftsp_value_valuation_selected_power_repeat_decoded. ff_h_ftsp_value_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_repeat_decoded. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_selected_power_product ff_v_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_start. ff_h_ftsp_value_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_start. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_terminal. ff_h_ftsp_value_valuation_selected_power_product_terminal + S (bpv_result_ftsp_value_valuation_selected) = S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_terminal. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product) + (bpv_result_ftsp_value_valuation_selected))) /\ forall ff_i_ftsp_value_valuation_selected_power_product. (exists ff_lt_ftsp_value_valuation_selected_power_product_bound. ff_lt_ftsp_value_valuation_selected_power_product_bound + S ff_i_ftsp_value_valuation_selected_power_product = ftsp_bad_exponent_value) -> exists ff_p_ftsp_value_valuation_selected_power_product ff_r_ftsp_value_valuation_selected_power_product ff_s_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_factor. ff_h_ftsp_value_valuation_selected_power_product_factor + S (ff_p_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_factor. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power) + (ff_p_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_partial. ff_h_ftsp_value_valuation_selected_power_product_partial + S (ff_r_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_partial. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_r_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_successor. ff_h_ftsp_value_valuation_selected_power_product_successor + S (ff_s_ftsp_value_valuation_selected_power_product) = S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_successor. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_s_ftsp_value_valuation_selected_power_product))) /\ ff_s_ftsp_value_valuation_selected_power_product = ff_r_ftsp_value_valuation_selected_power_product * ff_p_ftsp_value_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_selected_divides. (n) = bpv_result_ftsp_value_valuation_selected * bpv_factor_ftsp_value_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_value_valuation. (exists bpv_gap_ftsp_value_valuation_candidate_bound. bpv_gap_ftsp_value_valuation_candidate_bound + bpv_candidate_ftsp_value_valuation = (n)) -> (exists bpv_result_ftsp_value_valuation_candidate. ((exists ff_b_ftsp_value_valuation_candidate_power ff_c_ftsp_value_valuation_candidate_power. ((forall ff_i_ftsp_value_valuation_candidate_power_repeat. (exists ff_lt_ftsp_value_valuation_candidate_power_repeat_bound. ff_lt_ftsp_value_valuation_candidate_power_repeat_bound + S ff_i_ftsp_value_valuation_candidate_power_repeat = bpv_candidate_ftsp_value_valuation) -> (((exists ff_h_ftsp_value_valuation_candidate_power_repeat_decoded. ff_h_ftsp_value_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_repeat_decoded. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_candidate_power_product ff_v_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_start. ff_h_ftsp_value_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_start. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_terminal. ff_h_ftsp_value_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_value_valuation_candidate) = S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_terminal. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product) + (bpv_result_ftsp_value_valuation_candidate))) /\ forall ff_i_ftsp_value_valuation_candidate_power_product. (exists ff_lt_ftsp_value_valuation_candidate_power_product_bound. ff_lt_ftsp_value_valuation_candidate_power_product_bound + S ff_i_ftsp_value_valuation_candidate_power_product = bpv_candidate_ftsp_value_valuation) -> exists ff_p_ftsp_value_valuation_candidate_power_product ff_r_ftsp_value_valuation_candidate_power_product ff_s_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_factor. ff_h_ftsp_value_valuation_candidate_power_product_factor + S (ff_p_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_factor. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power) + (ff_p_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_partial. ff_h_ftsp_value_valuation_candidate_power_product_partial + S (ff_r_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_partial. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_r_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_successor. ff_h_ftsp_value_valuation_candidate_power_product_successor + S (ff_s_ftsp_value_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_successor. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_s_ftsp_value_valuation_candidate_power_product))) /\ ff_s_ftsp_value_valuation_candidate_power_product = ff_r_ftsp_value_valuation_candidate_power_product * ff_p_ftsp_value_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_candidate_divides. (n) = bpv_result_ftsp_value_valuation_candidate * bpv_factor_ftsp_value_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_value_valuation_maximal. bpv_gap_ftsp_value_valuation_maximal + bpv_candidate_ftsp_value_valuation = ftsp_bad_exponent_value)) -> exists ftsp_bad_half_value. ftsp_bad_exponent_value = ftsp_bad_half_value + ftsp_bad_half_value)))) /\ ((n = 0 \/ (~(n = 0) /\ (forall ftsp_bad_prime_value ftsp_bad_exponent_value. ((~(ftsp_bad_prime_value = 1) /\ forall frm_prime_left_ftsp_value_prime frm_prime_right_ftsp_value_prime. ftsp_bad_prime_value = frm_prime_left_ftsp_value_prime * frm_prime_right_ftsp_value_prime -> frm_prime_left_ftsp_value_prime = 1 \/ frm_prime_right_ftsp_value_prime = 1)) -> (exists ftsc_four_three_ftsp_value_three. (ftsp_bad_prime_value) = 4 * ftsc_four_three_ftsp_value_three + 3) -> (((exists bpv_gap_ftsp_value_valuation_exponent_bound. bpv_gap_ftsp_value_valuation_exponent_bound + ftsp_bad_exponent_value = (n)) /\ (exists bpv_result_ftsp_value_valuation_selected. ((exists ff_b_ftsp_value_valuation_selected_power ff_c_ftsp_value_valuation_selected_power. ((forall ff_i_ftsp_value_valuation_selected_power_repeat. (exists ff_lt_ftsp_value_valuation_selected_power_repeat_bound. ff_lt_ftsp_value_valuation_selected_power_repeat_bound + S ff_i_ftsp_value_valuation_selected_power_repeat = ftsp_bad_exponent_value) -> (((exists ff_h_ftsp_value_valuation_selected_power_repeat_decoded. ff_h_ftsp_value_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_repeat_decoded. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_selected_power_product ff_v_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_start. ff_h_ftsp_value_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_start. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_terminal. ff_h_ftsp_value_valuation_selected_power_product_terminal + S (bpv_result_ftsp_value_valuation_selected) = S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_terminal. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product) + (bpv_result_ftsp_value_valuation_selected))) /\ forall ff_i_ftsp_value_valuation_selected_power_product. (exists ff_lt_ftsp_value_valuation_selected_power_product_bound. ff_lt_ftsp_value_valuation_selected_power_product_bound + S ff_i_ftsp_value_valuation_selected_power_product = ftsp_bad_exponent_value) -> exists ff_p_ftsp_value_valuation_selected_power_product ff_r_ftsp_value_valuation_selected_power_product ff_s_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_factor. ff_h_ftsp_value_valuation_selected_power_product_factor + S (ff_p_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_factor. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power) + (ff_p_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_partial. ff_h_ftsp_value_valuation_selected_power_product_partial + S (ff_r_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_partial. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_r_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_successor. ff_h_ftsp_value_valuation_selected_power_product_successor + S (ff_s_ftsp_value_valuation_selected_power_product) = S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_successor. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_s_ftsp_value_valuation_selected_power_product))) /\ ff_s_ftsp_value_valuation_selected_power_product = ff_r_ftsp_value_valuation_selected_power_product * ff_p_ftsp_value_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_selected_divides. (n) = bpv_result_ftsp_value_valuation_selected * bpv_factor_ftsp_value_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_value_valuation. (exists bpv_gap_ftsp_value_valuation_candidate_bound. bpv_gap_ftsp_value_valuation_candidate_bound + bpv_candidate_ftsp_value_valuation = (n)) -> (exists bpv_result_ftsp_value_valuation_candidate. ((exists ff_b_ftsp_value_valuation_candidate_power ff_c_ftsp_value_valuation_candidate_power. ((forall ff_i_ftsp_value_valuation_candidate_power_repeat. (exists ff_lt_ftsp_value_valuation_candidate_power_repeat_bound. ff_lt_ftsp_value_valuation_candidate_power_repeat_bound + S ff_i_ftsp_value_valuation_candidate_power_repeat = bpv_candidate_ftsp_value_valuation) -> (((exists ff_h_ftsp_value_valuation_candidate_power_repeat_decoded. ff_h_ftsp_value_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_repeat_decoded. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_candidate_power_product ff_v_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_start. ff_h_ftsp_value_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_start. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_terminal. ff_h_ftsp_value_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_value_valuation_candidate) = S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_terminal. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product) + (bpv_result_ftsp_value_valuation_candidate))) /\ forall ff_i_ftsp_value_valuation_candidate_power_product. (exists ff_lt_ftsp_value_valuation_candidate_power_product_bound. ff_lt_ftsp_value_valuation_candidate_power_product_bound + S ff_i_ftsp_value_valuation_candidate_power_product = bpv_candidate_ftsp_value_valuation) -> exists ff_p_ftsp_value_valuation_candidate_power_product ff_r_ftsp_value_valuation_candidate_power_product ff_s_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_factor. ff_h_ftsp_value_valuation_candidate_power_product_factor + S (ff_p_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_factor. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power) + (ff_p_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_partial. ff_h_ftsp_value_valuation_candidate_power_product_partial + S (ff_r_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_partial. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_r_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_successor. ff_h_ftsp_value_valuation_candidate_power_product_successor + S (ff_s_ftsp_value_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_successor. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_s_ftsp_value_valuation_candidate_power_product))) /\ ff_s_ftsp_value_valuation_candidate_power_product = ff_r_ftsp_value_valuation_candidate_power_product * ff_p_ftsp_value_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_candidate_divides. (n) = bpv_result_ftsp_value_valuation_candidate * bpv_factor_ftsp_value_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_value_valuation_maximal. bpv_gap_ftsp_value_valuation_maximal + bpv_candidate_ftsp_value_valuation = ftsp_bad_exponent_value)) -> exists ftsp_bad_half_value. ftsp_bad_exponent_value = ftsp_bad_half_value + ftsp_bad_half_value))) -> (exists ftsc_first_ftsp_value_result ftsc_second_ftsp_value_result. (n) = ftsc_first_ftsp_value_result * ftsc_first_ftsp_value_result + ftsc_second_ftsp_value_result * ftsc_second_ftsp_value_result)))

Constructive proof overview

Generated structural guide

Full all-natural two-square theorem, with zero explicitly separated from the nonzero even-prime-valuation criterion.

The unchanged tactic script uses 2 declared prerequisites and contains 32 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized TS003E nonzero_two_square_iff_even_three_mod_four_prime_valuations

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

32 script commands · 20 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Separate zero; reuse the nonzero classification

The final theorem adds the zero case to the already proved nonzero two-square criterion. Zero is represented by the explicit pair (0, 0). For a nonzero number, the earlier criterion supplies both directions of the equivalence with even valuations at primes congruent to 3 modulo 4.

The two declarations named hiff are not new conjectures. Each names the equivalence obtained by applying the nonzero criterion to n and the available proof that n is not zero. Their enormous native formulas are expansions of the representation and valuation definitions.

Mathematical commentary bound to this exact script; it grants no proof authority.

Named ingredients (1)
nonzero two square iff even three mod four prime valuations

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–1

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
02Separate the logical casesL2–2

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L2
    split
03Fix variables and assumptionsL3–3

Work with arbitrary variables or the premises of the current implication.

  1. L3
    intro hrepresented
04Use earlier factsL4–5

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L4
    specialize eq_decidable n
  2. L5
    specialize eq_decidable 0
05Separate the logical casesL6–7

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L6
    cases eq_decidable
  2. L7
    left
06Use earlier factsL8–8

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L8
    exact eq_decidable_left
07Separate the logical casesL9–10

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    right
  2. L10
    split
08Use earlier factsL11–12

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L11
    exact eq_decidable_right
  2. L12
    specialize nonzero_two_square_iff_even_three_mod_four_prime_valuations n
09Establish hiffL13–15

Use the nonzero criterion with the nonzero assumption from the current case. The forward implication extracts the valuation condition from the given two-square representation.

  1. L13
    have hiff : (SumTwoSquares(n) → ∀ x. ∀ y. Prime(x) → Mod4Three(x) → BoundedPowerValuation(x,n,n,y) → ∃ z. y = z + z) ∧ ((∀ x. ∀ y. Prime(x) → Mod4Three(x) → BoundedPowerValuation(x,n,n,y) → ∃ z. y = z + z) → SumTwoSquares(n))Definitions: SumTwoSquaresPrimeMod4ThreeBoundedPowerValuation
  2. L14
    apply nonzero_two_square_iff_even_three_mod_four_prime_valuations
  3. L15
    exact eq_decidable_right
10Separate the logical casesL16–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L16
    cases hiff
11Use earlier factsL17–18

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L17
    apply hiff_left
  2. L18
    exact hrepresented
12Fix variables and assumptionsL19–19

Work with arbitrary variables or the premises of the current implication.

  1. L19
    intro hcases
13Separate the logical casesL20–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    cases hcases
14Construct an explicit witnessL21–22

Supply the displayed value, then prove that it has the required property.

  1. L21
    exists 0
  2. L22
    exists 0
15Calculate and transport equalitiesL23–24

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L23
    rewrite hcases_left
  2. L24
    norm_num
16Separate the logical casesL25–25

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L25
    cases hcases_right
17Use earlier factsL26–26

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L26
    specialize nonzero_two_square_iff_even_three_mod_four_prime_valuations n
18Establish hiffL27–29

Use the same nonzero criterion in the reverse direction. The supplied valuation condition gives a representation; zero was handled separately with the pair (0, 0).

  1. L27
    have hiff : (SumTwoSquares(n) → ∀ x. ∀ y. Prime(x) → Mod4Three(x) → BoundedPowerValuation(x,n,n,y) → ∃ z. y = z + z) ∧ ((∀ x. ∀ y. Prime(x) → Mod4Three(x) → BoundedPowerValuation(x,n,n,y) → ∃ z. y = z + z) → SumTwoSquares(n))Definitions: SumTwoSquaresPrimeMod4ThreeBoundedPowerValuation
  2. L28
    apply nonzero_two_square_iff_even_three_mod_four_prime_valuations
  3. L29
    exact hcases_right_left
19Separate the logical casesL30–30

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L30
    cases hiff
20Use earlier factsL31–32

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L31
    apply hiff_right
  2. L32
    exact hcases_right_right

Library-wide reading audit

Original exact command ledger · 32 lines
  1. 0001intro n
  2. 0002split
  3. 0003intro hrepresented
  4. 0004specialize eq_decidable n
  5. 0005specialize eq_decidable 0
  6. 0006cases eq_decidable
  7. 0007left
  8. 0008exact eq_decidable_left
  9. 0009right
  10. 0010split
  11. 0011exact eq_decidable_right
  12. 0012specialize nonzero_two_square_iff_even_three_mod_four_prime_valuations n
  13. 0013have hiff : (((exists ftsc_first_ftsp_value_result ftsc_second_ftsp_value_result. (n) = ftsc_first_ftsp_value_result * ftsc_first_ftsp_value_result + ftsc_second_ftsp_value_result * ftsc_second_ftsp_value_result) -> (forall ftsp_bad_prime_value ftsp_bad_exponent_value. ((~(ftsp_bad_prime_value = 1) /\ forall frm_prime_left_ftsp_value_prime frm_prime_right_ftsp_value_prime. ftsp_bad_prime_value = frm_prime_left_ftsp_value_prime * frm_prime_right_ftsp_value_prime -> frm_prime_left_ftsp_value_prime = 1 \/ frm_prime_right_ftsp_value_prime = 1)) -> (exists ftsc_four_three_ftsp_value_three. (ftsp_bad_prime_value) = 4 * ftsc_four_three_ftsp_value_three + 3) -> (((exists bpv_gap_ftsp_value_valuation_exponent_bound. bpv_gap_ftsp_value_valuation_exponent_bound + ftsp_bad_exponent_value = (n)) /\ (exists bpv_result_ftsp_value_valuation_selected. ((exists ff_b_ftsp_value_valuation_selected_power ff_c_ftsp_value_valuation_selected_power. ((forall ff_i_ftsp_value_valuation_selected_power_repeat. (exists ff_lt_ftsp_value_valuation_selected_power_repeat_bound. ff_lt_ftsp_value_valuation_selected_power_repeat_bound + S ff_i_ftsp_value_valuation_selected_power_repeat = ftsp_bad_exponent_value) -> (((exists ff_h_ftsp_value_valuation_selected_power_repeat_decoded. ff_h_ftsp_value_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_repeat_decoded. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_selected_power_product ff_v_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_start. ff_h_ftsp_value_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_start. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_terminal. ff_h_ftsp_value_valuation_selected_power_product_terminal + S (bpv_result_ftsp_value_valuation_selected) = S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_terminal. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product) + (bpv_result_ftsp_value_valuation_selected))) /\ forall ff_i_ftsp_value_valuation_selected_power_product. (exists ff_lt_ftsp_value_valuation_selected_power_product_bound. ff_lt_ftsp_value_valuation_selected_power_product_bound + S ff_i_ftsp_value_valuation_selected_power_product = ftsp_bad_exponent_value) -> exists ff_p_ftsp_value_valuation_selected_power_product ff_r_ftsp_value_valuation_selected_power_product ff_s_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_factor. ff_h_ftsp_value_valuation_selected_power_product_factor + S (ff_p_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_factor. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power) + (ff_p_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_partial. ff_h_ftsp_value_valuation_selected_power_product_partial + S (ff_r_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_partial. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_r_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_successor. ff_h_ftsp_value_valuation_selected_power_product_successor + S (ff_s_ftsp_value_valuation_selected_power_product) = S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_successor. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_s_ftsp_value_valuation_selected_power_product))) /\ ff_s_ftsp_value_valuation_selected_power_product = ff_r_ftsp_value_valuation_selected_power_product * ff_p_ftsp_value_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_selected_divides. (n) = bpv_result_ftsp_value_valuation_selected * bpv_factor_ftsp_value_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_value_valuation. (exists bpv_gap_ftsp_value_valuation_candidate_bound. bpv_gap_ftsp_value_valuation_candidate_bound + bpv_candidate_ftsp_value_valuation = (n)) -> (exists bpv_result_ftsp_value_valuation_candidate. ((exists ff_b_ftsp_value_valuation_candidate_power ff_c_ftsp_value_valuation_candidate_power. ((forall ff_i_ftsp_value_valuation_candidate_power_repeat. (exists ff_lt_ftsp_value_valuation_candidate_power_repeat_bound. ff_lt_ftsp_value_valuation_candidate_power_repeat_bound + S ff_i_ftsp_value_valuation_candidate_power_repeat = bpv_candidate_ftsp_value_valuation) -> (((exists ff_h_ftsp_value_valuation_candidate_power_repeat_decoded. ff_h_ftsp_value_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_repeat_decoded. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_candidate_power_product ff_v_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_start. ff_h_ftsp_value_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_start. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_terminal. ff_h_ftsp_value_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_value_valuation_candidate) = S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_terminal. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product) + (bpv_result_ftsp_value_valuation_candidate))) /\ forall ff_i_ftsp_value_valuation_candidate_power_product. (exists ff_lt_ftsp_value_valuation_candidate_power_product_bound. ff_lt_ftsp_value_valuation_candidate_power_product_bound + S ff_i_ftsp_value_valuation_candidate_power_product = bpv_candidate_ftsp_value_valuation) -> exists ff_p_ftsp_value_valuation_candidate_power_product ff_r_ftsp_value_valuation_candidate_power_product ff_s_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_factor. ff_h_ftsp_value_valuation_candidate_power_product_factor + S (ff_p_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_factor. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power) + (ff_p_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_partial. ff_h_ftsp_value_valuation_candidate_power_product_partial + S (ff_r_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_partial. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_r_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_successor. ff_h_ftsp_value_valuation_candidate_power_product_successor + S (ff_s_ftsp_value_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_successor. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_s_ftsp_value_valuation_candidate_power_product))) /\ ff_s_ftsp_value_valuation_candidate_power_product = ff_r_ftsp_value_valuation_candidate_power_product * ff_p_ftsp_value_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_candidate_divides. (n) = bpv_result_ftsp_value_valuation_candidate * bpv_factor_ftsp_value_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_value_valuation_maximal. bpv_gap_ftsp_value_valuation_maximal + bpv_candidate_ftsp_value_valuation = ftsp_bad_exponent_value)) -> exists ftsp_bad_half_value. ftsp_bad_exponent_value = ftsp_bad_half_value + ftsp_bad_half_value)) /\ ((forall ftsp_bad_prime_value ftsp_bad_exponent_value. ((~(ftsp_bad_prime_value = 1) /\ forall frm_prime_left_ftsp_value_prime frm_prime_right_ftsp_value_prime. ftsp_bad_prime_value = frm_prime_left_ftsp_value_prime * frm_prime_right_ftsp_value_prime -> frm_prime_left_ftsp_value_prime = 1 \/ frm_prime_right_ftsp_value_prime = 1)) -> (exists ftsc_four_three_ftsp_value_three. (ftsp_bad_prime_value) = 4 * ftsc_four_three_ftsp_value_three + 3) -> (((exists bpv_gap_ftsp_value_valuation_exponent_bound. bpv_gap_ftsp_value_valuation_exponent_bound + ftsp_bad_exponent_value = (n)) /\ (exists bpv_result_ftsp_value_valuation_selected. ((exists ff_b_ftsp_value_valuation_selected_power ff_c_ftsp_value_valuation_selected_power. ((forall ff_i_ftsp_value_valuation_selected_power_repeat. (exists ff_lt_ftsp_value_valuation_selected_power_repeat_bound. ff_lt_ftsp_value_valuation_selected_power_repeat_bound + S ff_i_ftsp_value_valuation_selected_power_repeat = ftsp_bad_exponent_value) -> (((exists ff_h_ftsp_value_valuation_selected_power_repeat_decoded. ff_h_ftsp_value_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_repeat_decoded. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_selected_power_product ff_v_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_start. ff_h_ftsp_value_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_start. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_terminal. ff_h_ftsp_value_valuation_selected_power_product_terminal + S (bpv_result_ftsp_value_valuation_selected) = S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_terminal. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product) + (bpv_result_ftsp_value_valuation_selected))) /\ forall ff_i_ftsp_value_valuation_selected_power_product. (exists ff_lt_ftsp_value_valuation_selected_power_product_bound. ff_lt_ftsp_value_valuation_selected_power_product_bound + S ff_i_ftsp_value_valuation_selected_power_product = ftsp_bad_exponent_value) -> exists ff_p_ftsp_value_valuation_selected_power_product ff_r_ftsp_value_valuation_selected_power_product ff_s_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_factor. ff_h_ftsp_value_valuation_selected_power_product_factor + S (ff_p_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_factor. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power) + (ff_p_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_partial. ff_h_ftsp_value_valuation_selected_power_product_partial + S (ff_r_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_partial. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_r_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_successor. ff_h_ftsp_value_valuation_selected_power_product_successor + S (ff_s_ftsp_value_valuation_selected_power_product) = S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_successor. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_s_ftsp_value_valuation_selected_power_product))) /\ ff_s_ftsp_value_valuation_selected_power_product = ff_r_ftsp_value_valuation_selected_power_product * ff_p_ftsp_value_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_selected_divides. (n) = bpv_result_ftsp_value_valuation_selected * bpv_factor_ftsp_value_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_value_valuation. (exists bpv_gap_ftsp_value_valuation_candidate_bound. bpv_gap_ftsp_value_valuation_candidate_bound + bpv_candidate_ftsp_value_valuation = (n)) -> (exists bpv_result_ftsp_value_valuation_candidate. ((exists ff_b_ftsp_value_valuation_candidate_power ff_c_ftsp_value_valuation_candidate_power. ((forall ff_i_ftsp_value_valuation_candidate_power_repeat. (exists ff_lt_ftsp_value_valuation_candidate_power_repeat_bound. ff_lt_ftsp_value_valuation_candidate_power_repeat_bound + S ff_i_ftsp_value_valuation_candidate_power_repeat = bpv_candidate_ftsp_value_valuation) -> (((exists ff_h_ftsp_value_valuation_candidate_power_repeat_decoded. ff_h_ftsp_value_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_repeat_decoded. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_candidate_power_product ff_v_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_start. ff_h_ftsp_value_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_start. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_terminal. ff_h_ftsp_value_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_value_valuation_candidate) = S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_terminal. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product) + (bpv_result_ftsp_value_valuation_candidate))) /\ forall ff_i_ftsp_value_valuation_candidate_power_product. (exists ff_lt_ftsp_value_valuation_candidate_power_product_bound. ff_lt_ftsp_value_valuation_candidate_power_product_bound + S ff_i_ftsp_value_valuation_candidate_power_product = bpv_candidate_ftsp_value_valuation) -> exists ff_p_ftsp_value_valuation_candidate_power_product ff_r_ftsp_value_valuation_candidate_power_product ff_s_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_factor. ff_h_ftsp_value_valuation_candidate_power_product_factor + S (ff_p_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_factor. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power) + (ff_p_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_partial. ff_h_ftsp_value_valuation_candidate_power_product_partial + S (ff_r_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_partial. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_r_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_successor. ff_h_ftsp_value_valuation_candidate_power_product_successor + S (ff_s_ftsp_value_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_successor. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_s_ftsp_value_valuation_candidate_power_product))) /\ ff_s_ftsp_value_valuation_candidate_power_product = ff_r_ftsp_value_valuation_candidate_power_product * ff_p_ftsp_value_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_candidate_divides. (n) = bpv_result_ftsp_value_valuation_candidate * bpv_factor_ftsp_value_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_value_valuation_maximal. bpv_gap_ftsp_value_valuation_maximal + bpv_candidate_ftsp_value_valuation = ftsp_bad_exponent_value)) -> exists ftsp_bad_half_value. ftsp_bad_exponent_value = ftsp_bad_half_value + ftsp_bad_half_value) -> (exists ftsc_first_ftsp_value_result ftsc_second_ftsp_value_result. (n) = ftsc_first_ftsp_value_result * ftsc_first_ftsp_value_result + ftsc_second_ftsp_value_result * ftsc_second_ftsp_value_result)))
  14. 0014apply nonzero_two_square_iff_even_three_mod_four_prime_valuations
  15. 0015exact eq_decidable_right
  16. 0016cases hiff
  17. 0017apply hiff_left
  18. 0018exact hrepresented
  19. 0019intro hcases
  20. 0020cases hcases
  21. 0021exists 0
  22. 0022exists 0
  23. 0023rewrite hcases_left
  24. 0024norm_num
  25. 0025cases hcases_right
  26. 0026specialize nonzero_two_square_iff_even_three_mod_four_prime_valuations n
  27. 0027have hiff : (((exists ftsc_first_ftsp_value_result ftsc_second_ftsp_value_result. (n) = ftsc_first_ftsp_value_result * ftsc_first_ftsp_value_result + ftsc_second_ftsp_value_result * ftsc_second_ftsp_value_result) -> (forall ftsp_bad_prime_value ftsp_bad_exponent_value. ((~(ftsp_bad_prime_value = 1) /\ forall frm_prime_left_ftsp_value_prime frm_prime_right_ftsp_value_prime. ftsp_bad_prime_value = frm_prime_left_ftsp_value_prime * frm_prime_right_ftsp_value_prime -> frm_prime_left_ftsp_value_prime = 1 \/ frm_prime_right_ftsp_value_prime = 1)) -> (exists ftsc_four_three_ftsp_value_three. (ftsp_bad_prime_value) = 4 * ftsc_four_three_ftsp_value_three + 3) -> (((exists bpv_gap_ftsp_value_valuation_exponent_bound. bpv_gap_ftsp_value_valuation_exponent_bound + ftsp_bad_exponent_value = (n)) /\ (exists bpv_result_ftsp_value_valuation_selected. ((exists ff_b_ftsp_value_valuation_selected_power ff_c_ftsp_value_valuation_selected_power. ((forall ff_i_ftsp_value_valuation_selected_power_repeat. (exists ff_lt_ftsp_value_valuation_selected_power_repeat_bound. ff_lt_ftsp_value_valuation_selected_power_repeat_bound + S ff_i_ftsp_value_valuation_selected_power_repeat = ftsp_bad_exponent_value) -> (((exists ff_h_ftsp_value_valuation_selected_power_repeat_decoded. ff_h_ftsp_value_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_repeat_decoded. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_selected_power_product ff_v_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_start. ff_h_ftsp_value_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_start. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_terminal. ff_h_ftsp_value_valuation_selected_power_product_terminal + S (bpv_result_ftsp_value_valuation_selected) = S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_terminal. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product) + (bpv_result_ftsp_value_valuation_selected))) /\ forall ff_i_ftsp_value_valuation_selected_power_product. (exists ff_lt_ftsp_value_valuation_selected_power_product_bound. ff_lt_ftsp_value_valuation_selected_power_product_bound + S ff_i_ftsp_value_valuation_selected_power_product = ftsp_bad_exponent_value) -> exists ff_p_ftsp_value_valuation_selected_power_product ff_r_ftsp_value_valuation_selected_power_product ff_s_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_factor. ff_h_ftsp_value_valuation_selected_power_product_factor + S (ff_p_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_factor. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power) + (ff_p_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_partial. ff_h_ftsp_value_valuation_selected_power_product_partial + S (ff_r_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_partial. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_r_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_successor. ff_h_ftsp_value_valuation_selected_power_product_successor + S (ff_s_ftsp_value_valuation_selected_power_product) = S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_successor. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_s_ftsp_value_valuation_selected_power_product))) /\ ff_s_ftsp_value_valuation_selected_power_product = ff_r_ftsp_value_valuation_selected_power_product * ff_p_ftsp_value_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_selected_divides. (n) = bpv_result_ftsp_value_valuation_selected * bpv_factor_ftsp_value_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_value_valuation. (exists bpv_gap_ftsp_value_valuation_candidate_bound. bpv_gap_ftsp_value_valuation_candidate_bound + bpv_candidate_ftsp_value_valuation = (n)) -> (exists bpv_result_ftsp_value_valuation_candidate. ((exists ff_b_ftsp_value_valuation_candidate_power ff_c_ftsp_value_valuation_candidate_power. ((forall ff_i_ftsp_value_valuation_candidate_power_repeat. (exists ff_lt_ftsp_value_valuation_candidate_power_repeat_bound. ff_lt_ftsp_value_valuation_candidate_power_repeat_bound + S ff_i_ftsp_value_valuation_candidate_power_repeat = bpv_candidate_ftsp_value_valuation) -> (((exists ff_h_ftsp_value_valuation_candidate_power_repeat_decoded. ff_h_ftsp_value_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_repeat_decoded. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_candidate_power_product ff_v_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_start. ff_h_ftsp_value_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_start. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_terminal. ff_h_ftsp_value_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_value_valuation_candidate) = S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_terminal. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product) + (bpv_result_ftsp_value_valuation_candidate))) /\ forall ff_i_ftsp_value_valuation_candidate_power_product. (exists ff_lt_ftsp_value_valuation_candidate_power_product_bound. ff_lt_ftsp_value_valuation_candidate_power_product_bound + S ff_i_ftsp_value_valuation_candidate_power_product = bpv_candidate_ftsp_value_valuation) -> exists ff_p_ftsp_value_valuation_candidate_power_product ff_r_ftsp_value_valuation_candidate_power_product ff_s_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_factor. ff_h_ftsp_value_valuation_candidate_power_product_factor + S (ff_p_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_factor. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power) + (ff_p_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_partial. ff_h_ftsp_value_valuation_candidate_power_product_partial + S (ff_r_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_partial. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_r_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_successor. ff_h_ftsp_value_valuation_candidate_power_product_successor + S (ff_s_ftsp_value_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_successor. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_s_ftsp_value_valuation_candidate_power_product))) /\ ff_s_ftsp_value_valuation_candidate_power_product = ff_r_ftsp_value_valuation_candidate_power_product * ff_p_ftsp_value_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_candidate_divides. (n) = bpv_result_ftsp_value_valuation_candidate * bpv_factor_ftsp_value_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_value_valuation_maximal. bpv_gap_ftsp_value_valuation_maximal + bpv_candidate_ftsp_value_valuation = ftsp_bad_exponent_value)) -> exists ftsp_bad_half_value. ftsp_bad_exponent_value = ftsp_bad_half_value + ftsp_bad_half_value)) /\ ((forall ftsp_bad_prime_value ftsp_bad_exponent_value. ((~(ftsp_bad_prime_value = 1) /\ forall frm_prime_left_ftsp_value_prime frm_prime_right_ftsp_value_prime. ftsp_bad_prime_value = frm_prime_left_ftsp_value_prime * frm_prime_right_ftsp_value_prime -> frm_prime_left_ftsp_value_prime = 1 \/ frm_prime_right_ftsp_value_prime = 1)) -> (exists ftsc_four_three_ftsp_value_three. (ftsp_bad_prime_value) = 4 * ftsc_four_three_ftsp_value_three + 3) -> (((exists bpv_gap_ftsp_value_valuation_exponent_bound. bpv_gap_ftsp_value_valuation_exponent_bound + ftsp_bad_exponent_value = (n)) /\ (exists bpv_result_ftsp_value_valuation_selected. ((exists ff_b_ftsp_value_valuation_selected_power ff_c_ftsp_value_valuation_selected_power. ((forall ff_i_ftsp_value_valuation_selected_power_repeat. (exists ff_lt_ftsp_value_valuation_selected_power_repeat_bound. ff_lt_ftsp_value_valuation_selected_power_repeat_bound + S ff_i_ftsp_value_valuation_selected_power_repeat = ftsp_bad_exponent_value) -> (((exists ff_h_ftsp_value_valuation_selected_power_repeat_decoded. ff_h_ftsp_value_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_repeat_decoded. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_selected_power_repeat)) * ff_c_ftsp_value_valuation_selected_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_selected_power_product ff_v_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_start. ff_h_ftsp_value_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_start. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_terminal. ff_h_ftsp_value_valuation_selected_power_product_terminal + S (bpv_result_ftsp_value_valuation_selected) = S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_terminal. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_value)) * ff_v_ftsp_value_valuation_selected_power_product) + (bpv_result_ftsp_value_valuation_selected))) /\ forall ff_i_ftsp_value_valuation_selected_power_product. (exists ff_lt_ftsp_value_valuation_selected_power_product_bound. ff_lt_ftsp_value_valuation_selected_power_product_bound + S ff_i_ftsp_value_valuation_selected_power_product = ftsp_bad_exponent_value) -> exists ff_p_ftsp_value_valuation_selected_power_product ff_r_ftsp_value_valuation_selected_power_product ff_s_ftsp_value_valuation_selected_power_product. ((((exists ff_h_ftsp_value_valuation_selected_power_product_factor. ff_h_ftsp_value_valuation_selected_power_product_factor + S (ff_p_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_factor. ff_b_ftsp_value_valuation_selected_power = ff_q_ftsp_value_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_c_ftsp_value_valuation_selected_power) + (ff_p_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_partial. ff_h_ftsp_value_valuation_selected_power_product_partial + S (ff_r_ftsp_value_valuation_selected_power_product) = S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_partial. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_r_ftsp_value_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_selected_power_product_successor. ff_h_ftsp_value_valuation_selected_power_product_successor + S (ff_s_ftsp_value_valuation_selected_power_product) = S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product)) /\ exists ff_q_ftsp_value_valuation_selected_power_product_successor. ff_u_ftsp_value_valuation_selected_power_product = ff_q_ftsp_value_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_selected_power_product)) * ff_v_ftsp_value_valuation_selected_power_product) + (ff_s_ftsp_value_valuation_selected_power_product))) /\ ff_s_ftsp_value_valuation_selected_power_product = ff_r_ftsp_value_valuation_selected_power_product * ff_p_ftsp_value_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_selected_divides. (n) = bpv_result_ftsp_value_valuation_selected * bpv_factor_ftsp_value_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_value_valuation. (exists bpv_gap_ftsp_value_valuation_candidate_bound. bpv_gap_ftsp_value_valuation_candidate_bound + bpv_candidate_ftsp_value_valuation = (n)) -> (exists bpv_result_ftsp_value_valuation_candidate. ((exists ff_b_ftsp_value_valuation_candidate_power ff_c_ftsp_value_valuation_candidate_power. ((forall ff_i_ftsp_value_valuation_candidate_power_repeat. (exists ff_lt_ftsp_value_valuation_candidate_power_repeat_bound. ff_lt_ftsp_value_valuation_candidate_power_repeat_bound + S ff_i_ftsp_value_valuation_candidate_power_repeat = bpv_candidate_ftsp_value_valuation) -> (((exists ff_h_ftsp_value_valuation_candidate_power_repeat_decoded. ff_h_ftsp_value_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_value) = S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_repeat_decoded. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_value_valuation_candidate_power_repeat)) * ff_c_ftsp_value_valuation_candidate_power) + (ftsp_bad_prime_value)))) /\ (exists ff_u_ftsp_value_valuation_candidate_power_product ff_v_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_start. ff_h_ftsp_value_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_start. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_value_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_terminal. ff_h_ftsp_value_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_value_valuation_candidate) = S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_terminal. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_value_valuation)) * ff_v_ftsp_value_valuation_candidate_power_product) + (bpv_result_ftsp_value_valuation_candidate))) /\ forall ff_i_ftsp_value_valuation_candidate_power_product. (exists ff_lt_ftsp_value_valuation_candidate_power_product_bound. ff_lt_ftsp_value_valuation_candidate_power_product_bound + S ff_i_ftsp_value_valuation_candidate_power_product = bpv_candidate_ftsp_value_valuation) -> exists ff_p_ftsp_value_valuation_candidate_power_product ff_r_ftsp_value_valuation_candidate_power_product ff_s_ftsp_value_valuation_candidate_power_product. ((((exists ff_h_ftsp_value_valuation_candidate_power_product_factor. ff_h_ftsp_value_valuation_candidate_power_product_factor + S (ff_p_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_factor. ff_b_ftsp_value_valuation_candidate_power = ff_q_ftsp_value_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_c_ftsp_value_valuation_candidate_power) + (ff_p_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_partial. ff_h_ftsp_value_valuation_candidate_power_product_partial + S (ff_r_ftsp_value_valuation_candidate_power_product) = S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_partial. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_r_ftsp_value_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_value_valuation_candidate_power_product_successor. ff_h_ftsp_value_valuation_candidate_power_product_successor + S (ff_s_ftsp_value_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product)) /\ exists ff_q_ftsp_value_valuation_candidate_power_product_successor. ff_u_ftsp_value_valuation_candidate_power_product = ff_q_ftsp_value_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_value_valuation_candidate_power_product)) * ff_v_ftsp_value_valuation_candidate_power_product) + (ff_s_ftsp_value_valuation_candidate_power_product))) /\ ff_s_ftsp_value_valuation_candidate_power_product = ff_r_ftsp_value_valuation_candidate_power_product * ff_p_ftsp_value_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_value_valuation_candidate_divides. (n) = bpv_result_ftsp_value_valuation_candidate * bpv_factor_ftsp_value_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_value_valuation_maximal. bpv_gap_ftsp_value_valuation_maximal + bpv_candidate_ftsp_value_valuation = ftsp_bad_exponent_value)) -> exists ftsp_bad_half_value. ftsp_bad_exponent_value = ftsp_bad_half_value + ftsp_bad_half_value) -> (exists ftsc_first_ftsp_value_result ftsc_second_ftsp_value_result. (n) = ftsc_first_ftsp_value_result * ftsc_first_ftsp_value_result + ftsc_second_ftsp_value_result * ftsc_second_ftsp_value_result)))
  28. 0028apply nonzero_two_square_iff_even_three_mod_four_prime_valuations
  29. 0029exact hcases_right_left
  30. 0030cases hiff
  31. 0031apply hiff_right
  32. 0032exact hcases_right_right