TS0035

distinct_prime_factor_even_valuation_reflects_prefix

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

Removing a distinct prime singleton preserves the even valuation of every other prime in a nonzero product.

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 p q n e f g. ((~(p = 1) /\ forall frm_prime_left_ftsp_p frm_prime_right_ftsp_p. p = frm_prime_left_ftsp_p * frm_prime_right_ftsp_p -> frm_prime_left_ftsp_p = 1 \/ frm_prime_right_ftsp_p = 1)) -> ((~(q = 1) /\ forall frm_prime_left_ftsp_q frm_prime_right_ftsp_q. q = frm_prime_left_ftsp_q * frm_prime_right_ftsp_q -> frm_prime_left_ftsp_q = 1 \/ frm_prime_right_ftsp_q = 1)) -> ~(p = q) -> ~(n = 0) -> (((exists bpv_gap_ftsp_reflected_value_exponent_bound. bpv_gap_ftsp_reflected_value_exponent_bound + e = n) /\ (exists bpv_result_ftsp_reflected_value_selected. ((exists ff_b_ftsp_reflected_value_selected_power ff_c_ftsp_reflected_value_selected_power. ((forall ff_i_ftsp_reflected_value_selected_power_repeat. (exists ff_lt_ftsp_reflected_value_selected_power_repeat_bound. ff_lt_ftsp_reflected_value_selected_power_repeat_bound + S ff_i_ftsp_reflected_value_selected_power_repeat = e) -> (((exists ff_h_ftsp_reflected_value_selected_power_repeat_decoded. ff_h_ftsp_reflected_value_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_reflected_value_selected_power_repeat)) * ff_c_ftsp_reflected_value_selected_power)) /\ exists ff_q_ftsp_reflected_value_selected_power_repeat_decoded. ff_b_ftsp_reflected_value_selected_power = ff_q_ftsp_reflected_value_selected_power_repeat_decoded * S ((S (ff_i_ftsp_reflected_value_selected_power_repeat)) * ff_c_ftsp_reflected_value_selected_power) + (p)))) /\ (exists ff_u_ftsp_reflected_value_selected_power_product ff_v_ftsp_reflected_value_selected_power_product. ((((exists ff_h_ftsp_reflected_value_selected_power_product_start. ff_h_ftsp_reflected_value_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_reflected_value_selected_power_product)) /\ exists ff_q_ftsp_reflected_value_selected_power_product_start. ff_u_ftsp_reflected_value_selected_power_product = ff_q_ftsp_reflected_value_selected_power_product_start * S ((S (0)) * ff_v_ftsp_reflected_value_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_reflected_value_selected_power_product_terminal. ff_h_ftsp_reflected_value_selected_power_product_terminal + S (bpv_result_ftsp_reflected_value_selected) = S ((S (e)) * ff_v_ftsp_reflected_value_selected_power_product)) /\ exists ff_q_ftsp_reflected_value_selected_power_product_terminal. ff_u_ftsp_reflected_value_selected_power_product = ff_q_ftsp_reflected_value_selected_power_product_terminal * S ((S (e)) * ff_v_ftsp_reflected_value_selected_power_product) + (bpv_result_ftsp_reflected_value_selected))) /\ forall ff_i_ftsp_reflected_value_selected_power_product. (exists ff_lt_ftsp_reflected_value_selected_power_product_bound. ff_lt_ftsp_reflected_value_selected_power_product_bound + S ff_i_ftsp_reflected_value_selected_power_product = e) -> exists ff_p_ftsp_reflected_value_selected_power_product ff_r_ftsp_reflected_value_selected_power_product ff_s_ftsp_reflected_value_selected_power_product. ((((exists ff_h_ftsp_reflected_value_selected_power_product_factor. ff_h_ftsp_reflected_value_selected_power_product_factor + S (ff_p_ftsp_reflected_value_selected_power_product) = S ((S (ff_i_ftsp_reflected_value_selected_power_product)) * ff_c_ftsp_reflected_value_selected_power)) /\ exists ff_q_ftsp_reflected_value_selected_power_product_factor. ff_b_ftsp_reflected_value_selected_power = ff_q_ftsp_reflected_value_selected_power_product_factor * S ((S (ff_i_ftsp_reflected_value_selected_power_product)) * ff_c_ftsp_reflected_value_selected_power) + (ff_p_ftsp_reflected_value_selected_power_product))) /\ ((((exists ff_h_ftsp_reflected_value_selected_power_product_partial. ff_h_ftsp_reflected_value_selected_power_product_partial + S (ff_r_ftsp_reflected_value_selected_power_product) = S ((S (ff_i_ftsp_reflected_value_selected_power_product)) * ff_v_ftsp_reflected_value_selected_power_product)) /\ exists ff_q_ftsp_reflected_value_selected_power_product_partial. ff_u_ftsp_reflected_value_selected_power_product = ff_q_ftsp_reflected_value_selected_power_product_partial * S ((S (ff_i_ftsp_reflected_value_selected_power_product)) * ff_v_ftsp_reflected_value_selected_power_product) + (ff_r_ftsp_reflected_value_selected_power_product))) /\ ((((exists ff_h_ftsp_reflected_value_selected_power_product_successor. ff_h_ftsp_reflected_value_selected_power_product_successor + S (ff_s_ftsp_reflected_value_selected_power_product) = S ((S (S ff_i_ftsp_reflected_value_selected_power_product)) * ff_v_ftsp_reflected_value_selected_power_product)) /\ exists ff_q_ftsp_reflected_value_selected_power_product_successor. ff_u_ftsp_reflected_value_selected_power_product = ff_q_ftsp_reflected_value_selected_power_product_successor * S ((S (S ff_i_ftsp_reflected_value_selected_power_product)) * ff_v_ftsp_reflected_value_selected_power_product) + (ff_s_ftsp_reflected_value_selected_power_product))) /\ ff_s_ftsp_reflected_value_selected_power_product = ff_r_ftsp_reflected_value_selected_power_product * ff_p_ftsp_reflected_value_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_reflected_value_selected_divides. n = bpv_result_ftsp_reflected_value_selected * bpv_factor_ftsp_reflected_value_selected_divides)))) /\ forall bpv_candidate_ftsp_reflected_value. (exists bpv_gap_ftsp_reflected_value_candidate_bound. bpv_gap_ftsp_reflected_value_candidate_bound + bpv_candidate_ftsp_reflected_value = n) -> (exists bpv_result_ftsp_reflected_value_candidate. ((exists ff_b_ftsp_reflected_value_candidate_power ff_c_ftsp_reflected_value_candidate_power. ((forall ff_i_ftsp_reflected_value_candidate_power_repeat. (exists ff_lt_ftsp_reflected_value_candidate_power_repeat_bound. ff_lt_ftsp_reflected_value_candidate_power_repeat_bound + S ff_i_ftsp_reflected_value_candidate_power_repeat = bpv_candidate_ftsp_reflected_value) -> (((exists ff_h_ftsp_reflected_value_candidate_power_repeat_decoded. ff_h_ftsp_reflected_value_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_reflected_value_candidate_power_repeat)) * ff_c_ftsp_reflected_value_candidate_power)) /\ exists ff_q_ftsp_reflected_value_candidate_power_repeat_decoded. ff_b_ftsp_reflected_value_candidate_power = ff_q_ftsp_reflected_value_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_reflected_value_candidate_power_repeat)) * ff_c_ftsp_reflected_value_candidate_power) + (p)))) /\ (exists ff_u_ftsp_reflected_value_candidate_power_product ff_v_ftsp_reflected_value_candidate_power_product. ((((exists ff_h_ftsp_reflected_value_candidate_power_product_start. ff_h_ftsp_reflected_value_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_reflected_value_candidate_power_product)) /\ exists ff_q_ftsp_reflected_value_candidate_power_product_start. ff_u_ftsp_reflected_value_candidate_power_product = ff_q_ftsp_reflected_value_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_reflected_value_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_reflected_value_candidate_power_product_terminal. ff_h_ftsp_reflected_value_candidate_power_product_terminal + S (bpv_result_ftsp_reflected_value_candidate) = S ((S (bpv_candidate_ftsp_reflected_value)) * ff_v_ftsp_reflected_value_candidate_power_product)) /\ exists ff_q_ftsp_reflected_value_candidate_power_product_terminal. ff_u_ftsp_reflected_value_candidate_power_product = ff_q_ftsp_reflected_value_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_reflected_value)) * ff_v_ftsp_reflected_value_candidate_power_product) + (bpv_result_ftsp_reflected_value_candidate))) /\ forall ff_i_ftsp_reflected_value_candidate_power_product. (exists ff_lt_ftsp_reflected_value_candidate_power_product_bound. ff_lt_ftsp_reflected_value_candidate_power_product_bound + S ff_i_ftsp_reflected_value_candidate_power_product = bpv_candidate_ftsp_reflected_value) -> exists ff_p_ftsp_reflected_value_candidate_power_product ff_r_ftsp_reflected_value_candidate_power_product ff_s_ftsp_reflected_value_candidate_power_product. ((((exists ff_h_ftsp_reflected_value_candidate_power_product_factor. ff_h_ftsp_reflected_value_candidate_power_product_factor + S (ff_p_ftsp_reflected_value_candidate_power_product) = S ((S (ff_i_ftsp_reflected_value_candidate_power_product)) * ff_c_ftsp_reflected_value_candidate_power)) /\ exists ff_q_ftsp_reflected_value_candidate_power_product_factor. ff_b_ftsp_reflected_value_candidate_power = ff_q_ftsp_reflected_value_candidate_power_product_factor * S ((S (ff_i_ftsp_reflected_value_candidate_power_product)) * ff_c_ftsp_reflected_value_candidate_power) + (ff_p_ftsp_reflected_value_candidate_power_product))) /\ ((((exists ff_h_ftsp_reflected_value_candidate_power_product_partial. ff_h_ftsp_reflected_value_candidate_power_product_partial + S (ff_r_ftsp_reflected_value_candidate_power_product) = S ((S (ff_i_ftsp_reflected_value_candidate_power_product)) * ff_v_ftsp_reflected_value_candidate_power_product)) /\ exists ff_q_ftsp_reflected_value_candidate_power_product_partial. ff_u_ftsp_reflected_value_candidate_power_product = ff_q_ftsp_reflected_value_candidate_power_product_partial * S ((S (ff_i_ftsp_reflected_value_candidate_power_product)) * ff_v_ftsp_reflected_value_candidate_power_product) + (ff_r_ftsp_reflected_value_candidate_power_product))) /\ ((((exists ff_h_ftsp_reflected_value_candidate_power_product_successor. ff_h_ftsp_reflected_value_candidate_power_product_successor + S (ff_s_ftsp_reflected_value_candidate_power_product) = S ((S (S ff_i_ftsp_reflected_value_candidate_power_product)) * ff_v_ftsp_reflected_value_candidate_power_product)) /\ exists ff_q_ftsp_reflected_value_candidate_power_product_successor. ff_u_ftsp_reflected_value_candidate_power_product = ff_q_ftsp_reflected_value_candidate_power_product_successor * S ((S (S ff_i_ftsp_reflected_value_candidate_power_product)) * ff_v_ftsp_reflected_value_candidate_power_product) + (ff_s_ftsp_reflected_value_candidate_power_product))) /\ ff_s_ftsp_reflected_value_candidate_power_product = ff_r_ftsp_reflected_value_candidate_power_product * ff_p_ftsp_reflected_value_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_reflected_value_candidate_divides. n = bpv_result_ftsp_reflected_value_candidate * bpv_factor_ftsp_reflected_value_candidate_divides))) -> (exists bpv_gap_ftsp_reflected_value_maximal. bpv_gap_ftsp_reflected_value_maximal + bpv_candidate_ftsp_reflected_value = e)) -> (((exists bpv_gap_ftsp_reflected_prime_exponent_bound. bpv_gap_ftsp_reflected_prime_exponent_bound + f = q) /\ (exists bpv_result_ftsp_reflected_prime_selected. ((exists ff_b_ftsp_reflected_prime_selected_power ff_c_ftsp_reflected_prime_selected_power. ((forall ff_i_ftsp_reflected_prime_selected_power_repeat. (exists ff_lt_ftsp_reflected_prime_selected_power_repeat_bound. ff_lt_ftsp_reflected_prime_selected_power_repeat_bound + S ff_i_ftsp_reflected_prime_selected_power_repeat = f) -> (((exists ff_h_ftsp_reflected_prime_selected_power_repeat_decoded. ff_h_ftsp_reflected_prime_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_reflected_prime_selected_power_repeat)) * ff_c_ftsp_reflected_prime_selected_power)) /\ exists ff_q_ftsp_reflected_prime_selected_power_repeat_decoded. ff_b_ftsp_reflected_prime_selected_power = ff_q_ftsp_reflected_prime_selected_power_repeat_decoded * S ((S (ff_i_ftsp_reflected_prime_selected_power_repeat)) * ff_c_ftsp_reflected_prime_selected_power) + (p)))) /\ (exists ff_u_ftsp_reflected_prime_selected_power_product ff_v_ftsp_reflected_prime_selected_power_product. ((((exists ff_h_ftsp_reflected_prime_selected_power_product_start. ff_h_ftsp_reflected_prime_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_reflected_prime_selected_power_product)) /\ exists ff_q_ftsp_reflected_prime_selected_power_product_start. ff_u_ftsp_reflected_prime_selected_power_product = ff_q_ftsp_reflected_prime_selected_power_product_start * S ((S (0)) * ff_v_ftsp_reflected_prime_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_reflected_prime_selected_power_product_terminal. ff_h_ftsp_reflected_prime_selected_power_product_terminal + S (bpv_result_ftsp_reflected_prime_selected) = S ((S (f)) * ff_v_ftsp_reflected_prime_selected_power_product)) /\ exists ff_q_ftsp_reflected_prime_selected_power_product_terminal. ff_u_ftsp_reflected_prime_selected_power_product = ff_q_ftsp_reflected_prime_selected_power_product_terminal * S ((S (f)) * ff_v_ftsp_reflected_prime_selected_power_product) + (bpv_result_ftsp_reflected_prime_selected))) /\ forall ff_i_ftsp_reflected_prime_selected_power_product. (exists ff_lt_ftsp_reflected_prime_selected_power_product_bound. ff_lt_ftsp_reflected_prime_selected_power_product_bound + S ff_i_ftsp_reflected_prime_selected_power_product = f) -> exists ff_p_ftsp_reflected_prime_selected_power_product ff_r_ftsp_reflected_prime_selected_power_product ff_s_ftsp_reflected_prime_selected_power_product. ((((exists ff_h_ftsp_reflected_prime_selected_power_product_factor. ff_h_ftsp_reflected_prime_selected_power_product_factor + S (ff_p_ftsp_reflected_prime_selected_power_product) = S ((S (ff_i_ftsp_reflected_prime_selected_power_product)) * ff_c_ftsp_reflected_prime_selected_power)) /\ exists ff_q_ftsp_reflected_prime_selected_power_product_factor. ff_b_ftsp_reflected_prime_selected_power = ff_q_ftsp_reflected_prime_selected_power_product_factor * S ((S (ff_i_ftsp_reflected_prime_selected_power_product)) * ff_c_ftsp_reflected_prime_selected_power) + (ff_p_ftsp_reflected_prime_selected_power_product))) /\ ((((exists ff_h_ftsp_reflected_prime_selected_power_product_partial. ff_h_ftsp_reflected_prime_selected_power_product_partial + S (ff_r_ftsp_reflected_prime_selected_power_product) = S ((S (ff_i_ftsp_reflected_prime_selected_power_product)) * ff_v_ftsp_reflected_prime_selected_power_product)) /\ exists ff_q_ftsp_reflected_prime_selected_power_product_partial. ff_u_ftsp_reflected_prime_selected_power_product = ff_q_ftsp_reflected_prime_selected_power_product_partial * S ((S (ff_i_ftsp_reflected_prime_selected_power_product)) * ff_v_ftsp_reflected_prime_selected_power_product) + (ff_r_ftsp_reflected_prime_selected_power_product))) /\ ((((exists ff_h_ftsp_reflected_prime_selected_power_product_successor. ff_h_ftsp_reflected_prime_selected_power_product_successor + S (ff_s_ftsp_reflected_prime_selected_power_product) = S ((S (S ff_i_ftsp_reflected_prime_selected_power_product)) * ff_v_ftsp_reflected_prime_selected_power_product)) /\ exists ff_q_ftsp_reflected_prime_selected_power_product_successor. ff_u_ftsp_reflected_prime_selected_power_product = ff_q_ftsp_reflected_prime_selected_power_product_successor * S ((S (S ff_i_ftsp_reflected_prime_selected_power_product)) * ff_v_ftsp_reflected_prime_selected_power_product) + (ff_s_ftsp_reflected_prime_selected_power_product))) /\ ff_s_ftsp_reflected_prime_selected_power_product = ff_r_ftsp_reflected_prime_selected_power_product * ff_p_ftsp_reflected_prime_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_reflected_prime_selected_divides. q = bpv_result_ftsp_reflected_prime_selected * bpv_factor_ftsp_reflected_prime_selected_divides)))) /\ forall bpv_candidate_ftsp_reflected_prime. (exists bpv_gap_ftsp_reflected_prime_candidate_bound. bpv_gap_ftsp_reflected_prime_candidate_bound + bpv_candidate_ftsp_reflected_prime = q) -> (exists bpv_result_ftsp_reflected_prime_candidate. ((exists ff_b_ftsp_reflected_prime_candidate_power ff_c_ftsp_reflected_prime_candidate_power. ((forall ff_i_ftsp_reflected_prime_candidate_power_repeat. (exists ff_lt_ftsp_reflected_prime_candidate_power_repeat_bound. ff_lt_ftsp_reflected_prime_candidate_power_repeat_bound + S ff_i_ftsp_reflected_prime_candidate_power_repeat = bpv_candidate_ftsp_reflected_prime) -> (((exists ff_h_ftsp_reflected_prime_candidate_power_repeat_decoded. ff_h_ftsp_reflected_prime_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_reflected_prime_candidate_power_repeat)) * ff_c_ftsp_reflected_prime_candidate_power)) /\ exists ff_q_ftsp_reflected_prime_candidate_power_repeat_decoded. ff_b_ftsp_reflected_prime_candidate_power = ff_q_ftsp_reflected_prime_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_reflected_prime_candidate_power_repeat)) * ff_c_ftsp_reflected_prime_candidate_power) + (p)))) /\ (exists ff_u_ftsp_reflected_prime_candidate_power_product ff_v_ftsp_reflected_prime_candidate_power_product. ((((exists ff_h_ftsp_reflected_prime_candidate_power_product_start. ff_h_ftsp_reflected_prime_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_reflected_prime_candidate_power_product)) /\ exists ff_q_ftsp_reflected_prime_candidate_power_product_start. ff_u_ftsp_reflected_prime_candidate_power_product = ff_q_ftsp_reflected_prime_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_reflected_prime_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_reflected_prime_candidate_power_product_terminal. ff_h_ftsp_reflected_prime_candidate_power_product_terminal + S (bpv_result_ftsp_reflected_prime_candidate) = S ((S (bpv_candidate_ftsp_reflected_prime)) * ff_v_ftsp_reflected_prime_candidate_power_product)) /\ exists ff_q_ftsp_reflected_prime_candidate_power_product_terminal. ff_u_ftsp_reflected_prime_candidate_power_product = ff_q_ftsp_reflected_prime_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_reflected_prime)) * ff_v_ftsp_reflected_prime_candidate_power_product) + (bpv_result_ftsp_reflected_prime_candidate))) /\ forall ff_i_ftsp_reflected_prime_candidate_power_product. (exists ff_lt_ftsp_reflected_prime_candidate_power_product_bound. ff_lt_ftsp_reflected_prime_candidate_power_product_bound + S ff_i_ftsp_reflected_prime_candidate_power_product = bpv_candidate_ftsp_reflected_prime) -> exists ff_p_ftsp_reflected_prime_candidate_power_product ff_r_ftsp_reflected_prime_candidate_power_product ff_s_ftsp_reflected_prime_candidate_power_product. ((((exists ff_h_ftsp_reflected_prime_candidate_power_product_factor. ff_h_ftsp_reflected_prime_candidate_power_product_factor + S (ff_p_ftsp_reflected_prime_candidate_power_product) = S ((S (ff_i_ftsp_reflected_prime_candidate_power_product)) * ff_c_ftsp_reflected_prime_candidate_power)) /\ exists ff_q_ftsp_reflected_prime_candidate_power_product_factor. ff_b_ftsp_reflected_prime_candidate_power = ff_q_ftsp_reflected_prime_candidate_power_product_factor * S ((S (ff_i_ftsp_reflected_prime_candidate_power_product)) * ff_c_ftsp_reflected_prime_candidate_power) + (ff_p_ftsp_reflected_prime_candidate_power_product))) /\ ((((exists ff_h_ftsp_reflected_prime_candidate_power_product_partial. ff_h_ftsp_reflected_prime_candidate_power_product_partial + S (ff_r_ftsp_reflected_prime_candidate_power_product) = S ((S (ff_i_ftsp_reflected_prime_candidate_power_product)) * ff_v_ftsp_reflected_prime_candidate_power_product)) /\ exists ff_q_ftsp_reflected_prime_candidate_power_product_partial. ff_u_ftsp_reflected_prime_candidate_power_product = ff_q_ftsp_reflected_prime_candidate_power_product_partial * S ((S (ff_i_ftsp_reflected_prime_candidate_power_product)) * ff_v_ftsp_reflected_prime_candidate_power_product) + (ff_r_ftsp_reflected_prime_candidate_power_product))) /\ ((((exists ff_h_ftsp_reflected_prime_candidate_power_product_successor. ff_h_ftsp_reflected_prime_candidate_power_product_successor + S (ff_s_ftsp_reflected_prime_candidate_power_product) = S ((S (S ff_i_ftsp_reflected_prime_candidate_power_product)) * ff_v_ftsp_reflected_prime_candidate_power_product)) /\ exists ff_q_ftsp_reflected_prime_candidate_power_product_successor. ff_u_ftsp_reflected_prime_candidate_power_product = ff_q_ftsp_reflected_prime_candidate_power_product_successor * S ((S (S ff_i_ftsp_reflected_prime_candidate_power_product)) * ff_v_ftsp_reflected_prime_candidate_power_product) + (ff_s_ftsp_reflected_prime_candidate_power_product))) /\ ff_s_ftsp_reflected_prime_candidate_power_product = ff_r_ftsp_reflected_prime_candidate_power_product * ff_p_ftsp_reflected_prime_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_reflected_prime_candidate_divides. q = bpv_result_ftsp_reflected_prime_candidate * bpv_factor_ftsp_reflected_prime_candidate_divides))) -> (exists bpv_gap_ftsp_reflected_prime_maximal. bpv_gap_ftsp_reflected_prime_maximal + bpv_candidate_ftsp_reflected_prime = f)) -> (((exists bpv_gap_ftsp_reflected_product_exponent_bound. bpv_gap_ftsp_reflected_product_exponent_bound + g = (n * q)) /\ (exists bpv_result_ftsp_reflected_product_selected. ((exists ff_b_ftsp_reflected_product_selected_power ff_c_ftsp_reflected_product_selected_power. ((forall ff_i_ftsp_reflected_product_selected_power_repeat. (exists ff_lt_ftsp_reflected_product_selected_power_repeat_bound. ff_lt_ftsp_reflected_product_selected_power_repeat_bound + S ff_i_ftsp_reflected_product_selected_power_repeat = g) -> (((exists ff_h_ftsp_reflected_product_selected_power_repeat_decoded. ff_h_ftsp_reflected_product_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_reflected_product_selected_power_repeat)) * ff_c_ftsp_reflected_product_selected_power)) /\ exists ff_q_ftsp_reflected_product_selected_power_repeat_decoded. ff_b_ftsp_reflected_product_selected_power = ff_q_ftsp_reflected_product_selected_power_repeat_decoded * S ((S (ff_i_ftsp_reflected_product_selected_power_repeat)) * ff_c_ftsp_reflected_product_selected_power) + (p)))) /\ (exists ff_u_ftsp_reflected_product_selected_power_product ff_v_ftsp_reflected_product_selected_power_product. ((((exists ff_h_ftsp_reflected_product_selected_power_product_start. ff_h_ftsp_reflected_product_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_reflected_product_selected_power_product)) /\ exists ff_q_ftsp_reflected_product_selected_power_product_start. ff_u_ftsp_reflected_product_selected_power_product = ff_q_ftsp_reflected_product_selected_power_product_start * S ((S (0)) * ff_v_ftsp_reflected_product_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_reflected_product_selected_power_product_terminal. ff_h_ftsp_reflected_product_selected_power_product_terminal + S (bpv_result_ftsp_reflected_product_selected) = S ((S (g)) * ff_v_ftsp_reflected_product_selected_power_product)) /\ exists ff_q_ftsp_reflected_product_selected_power_product_terminal. ff_u_ftsp_reflected_product_selected_power_product = ff_q_ftsp_reflected_product_selected_power_product_terminal * S ((S (g)) * ff_v_ftsp_reflected_product_selected_power_product) + (bpv_result_ftsp_reflected_product_selected))) /\ forall ff_i_ftsp_reflected_product_selected_power_product. (exists ff_lt_ftsp_reflected_product_selected_power_product_bound. ff_lt_ftsp_reflected_product_selected_power_product_bound + S ff_i_ftsp_reflected_product_selected_power_product = g) -> exists ff_p_ftsp_reflected_product_selected_power_product ff_r_ftsp_reflected_product_selected_power_product ff_s_ftsp_reflected_product_selected_power_product. ((((exists ff_h_ftsp_reflected_product_selected_power_product_factor. ff_h_ftsp_reflected_product_selected_power_product_factor + S (ff_p_ftsp_reflected_product_selected_power_product) = S ((S (ff_i_ftsp_reflected_product_selected_power_product)) * ff_c_ftsp_reflected_product_selected_power)) /\ exists ff_q_ftsp_reflected_product_selected_power_product_factor. ff_b_ftsp_reflected_product_selected_power = ff_q_ftsp_reflected_product_selected_power_product_factor * S ((S (ff_i_ftsp_reflected_product_selected_power_product)) * ff_c_ftsp_reflected_product_selected_power) + (ff_p_ftsp_reflected_product_selected_power_product))) /\ ((((exists ff_h_ftsp_reflected_product_selected_power_product_partial. ff_h_ftsp_reflected_product_selected_power_product_partial + S (ff_r_ftsp_reflected_product_selected_power_product) = S ((S (ff_i_ftsp_reflected_product_selected_power_product)) * ff_v_ftsp_reflected_product_selected_power_product)) /\ exists ff_q_ftsp_reflected_product_selected_power_product_partial. ff_u_ftsp_reflected_product_selected_power_product = ff_q_ftsp_reflected_product_selected_power_product_partial * S ((S (ff_i_ftsp_reflected_product_selected_power_product)) * ff_v_ftsp_reflected_product_selected_power_product) + (ff_r_ftsp_reflected_product_selected_power_product))) /\ ((((exists ff_h_ftsp_reflected_product_selected_power_product_successor. ff_h_ftsp_reflected_product_selected_power_product_successor + S (ff_s_ftsp_reflected_product_selected_power_product) = S ((S (S ff_i_ftsp_reflected_product_selected_power_product)) * ff_v_ftsp_reflected_product_selected_power_product)) /\ exists ff_q_ftsp_reflected_product_selected_power_product_successor. ff_u_ftsp_reflected_product_selected_power_product = ff_q_ftsp_reflected_product_selected_power_product_successor * S ((S (S ff_i_ftsp_reflected_product_selected_power_product)) * ff_v_ftsp_reflected_product_selected_power_product) + (ff_s_ftsp_reflected_product_selected_power_product))) /\ ff_s_ftsp_reflected_product_selected_power_product = ff_r_ftsp_reflected_product_selected_power_product * ff_p_ftsp_reflected_product_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_reflected_product_selected_divides. (n * q) = bpv_result_ftsp_reflected_product_selected * bpv_factor_ftsp_reflected_product_selected_divides)))) /\ forall bpv_candidate_ftsp_reflected_product. (exists bpv_gap_ftsp_reflected_product_candidate_bound. bpv_gap_ftsp_reflected_product_candidate_bound + bpv_candidate_ftsp_reflected_product = (n * q)) -> (exists bpv_result_ftsp_reflected_product_candidate. ((exists ff_b_ftsp_reflected_product_candidate_power ff_c_ftsp_reflected_product_candidate_power. ((forall ff_i_ftsp_reflected_product_candidate_power_repeat. (exists ff_lt_ftsp_reflected_product_candidate_power_repeat_bound. ff_lt_ftsp_reflected_product_candidate_power_repeat_bound + S ff_i_ftsp_reflected_product_candidate_power_repeat = bpv_candidate_ftsp_reflected_product) -> (((exists ff_h_ftsp_reflected_product_candidate_power_repeat_decoded. ff_h_ftsp_reflected_product_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsp_reflected_product_candidate_power_repeat)) * ff_c_ftsp_reflected_product_candidate_power)) /\ exists ff_q_ftsp_reflected_product_candidate_power_repeat_decoded. ff_b_ftsp_reflected_product_candidate_power = ff_q_ftsp_reflected_product_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_reflected_product_candidate_power_repeat)) * ff_c_ftsp_reflected_product_candidate_power) + (p)))) /\ (exists ff_u_ftsp_reflected_product_candidate_power_product ff_v_ftsp_reflected_product_candidate_power_product. ((((exists ff_h_ftsp_reflected_product_candidate_power_product_start. ff_h_ftsp_reflected_product_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_reflected_product_candidate_power_product)) /\ exists ff_q_ftsp_reflected_product_candidate_power_product_start. ff_u_ftsp_reflected_product_candidate_power_product = ff_q_ftsp_reflected_product_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_reflected_product_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_reflected_product_candidate_power_product_terminal. ff_h_ftsp_reflected_product_candidate_power_product_terminal + S (bpv_result_ftsp_reflected_product_candidate) = S ((S (bpv_candidate_ftsp_reflected_product)) * ff_v_ftsp_reflected_product_candidate_power_product)) /\ exists ff_q_ftsp_reflected_product_candidate_power_product_terminal. ff_u_ftsp_reflected_product_candidate_power_product = ff_q_ftsp_reflected_product_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_reflected_product)) * ff_v_ftsp_reflected_product_candidate_power_product) + (bpv_result_ftsp_reflected_product_candidate))) /\ forall ff_i_ftsp_reflected_product_candidate_power_product. (exists ff_lt_ftsp_reflected_product_candidate_power_product_bound. ff_lt_ftsp_reflected_product_candidate_power_product_bound + S ff_i_ftsp_reflected_product_candidate_power_product = bpv_candidate_ftsp_reflected_product) -> exists ff_p_ftsp_reflected_product_candidate_power_product ff_r_ftsp_reflected_product_candidate_power_product ff_s_ftsp_reflected_product_candidate_power_product. ((((exists ff_h_ftsp_reflected_product_candidate_power_product_factor. ff_h_ftsp_reflected_product_candidate_power_product_factor + S (ff_p_ftsp_reflected_product_candidate_power_product) = S ((S (ff_i_ftsp_reflected_product_candidate_power_product)) * ff_c_ftsp_reflected_product_candidate_power)) /\ exists ff_q_ftsp_reflected_product_candidate_power_product_factor. ff_b_ftsp_reflected_product_candidate_power = ff_q_ftsp_reflected_product_candidate_power_product_factor * S ((S (ff_i_ftsp_reflected_product_candidate_power_product)) * ff_c_ftsp_reflected_product_candidate_power) + (ff_p_ftsp_reflected_product_candidate_power_product))) /\ ((((exists ff_h_ftsp_reflected_product_candidate_power_product_partial. ff_h_ftsp_reflected_product_candidate_power_product_partial + S (ff_r_ftsp_reflected_product_candidate_power_product) = S ((S (ff_i_ftsp_reflected_product_candidate_power_product)) * ff_v_ftsp_reflected_product_candidate_power_product)) /\ exists ff_q_ftsp_reflected_product_candidate_power_product_partial. ff_u_ftsp_reflected_product_candidate_power_product = ff_q_ftsp_reflected_product_candidate_power_product_partial * S ((S (ff_i_ftsp_reflected_product_candidate_power_product)) * ff_v_ftsp_reflected_product_candidate_power_product) + (ff_r_ftsp_reflected_product_candidate_power_product))) /\ ((((exists ff_h_ftsp_reflected_product_candidate_power_product_successor. ff_h_ftsp_reflected_product_candidate_power_product_successor + S (ff_s_ftsp_reflected_product_candidate_power_product) = S ((S (S ff_i_ftsp_reflected_product_candidate_power_product)) * ff_v_ftsp_reflected_product_candidate_power_product)) /\ exists ff_q_ftsp_reflected_product_candidate_power_product_successor. ff_u_ftsp_reflected_product_candidate_power_product = ff_q_ftsp_reflected_product_candidate_power_product_successor * S ((S (S ff_i_ftsp_reflected_product_candidate_power_product)) * ff_v_ftsp_reflected_product_candidate_power_product) + (ff_s_ftsp_reflected_product_candidate_power_product))) /\ ff_s_ftsp_reflected_product_candidate_power_product = ff_r_ftsp_reflected_product_candidate_power_product * ff_p_ftsp_reflected_product_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_reflected_product_candidate_divides. (n * q) = bpv_result_ftsp_reflected_product_candidate * bpv_factor_ftsp_reflected_product_candidate_divides))) -> (exists bpv_gap_ftsp_reflected_product_maximal. bpv_gap_ftsp_reflected_product_maximal + bpv_candidate_ftsp_reflected_product = g)) -> (exists h. g = h + h) -> exists h. e = h + h

Constructive proof overview

Generated structural guide

Removing a distinct prime singleton preserves the even valuation of every other prime in a nonzero product.

The unchanged tactic script uses 3 declared prerequisites and contains 51 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

TS002X distinct_prime_power_valuation_zero prime_nonzero Stable theorem; checked-use authorized prime_power_valuation_mul Alpha theorem; checked-use authorized

Direct dependents

TS0038 all_bad_prime_even_valuations_strip_represented_prime

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

51 script commands · 11 reading checkpoints · 3 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.

Named ingredients (1)
distinct prime power valuation zero
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro n
  4. L4
    intro e
  5. L5
    intro f
  6. L6
    intro g
  7. L7
    intro hp
  8. L8
    intro hq
  9. L9
    intro hdistinct
  10. L10
    intro hnnonzero
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hnvaluation
  2. L12
    intro hqvaluation
  3. L13
    intro hproduct
  4. L14
    intro heven
03Establish hzeroL15–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct prime power valuation zero.

  1. L15
    have hzero : f = 0
  2. L16
    specialize distinct_prime_power_valuation_zero p
  3. L17
    specialize distinct_prime_power_valuation_zero q
  4. L18
    specialize distinct_prime_power_valuation_zero f
  5. L19
    apply distinct_prime_power_valuation_zero
  6. L20
    exact hp
  7. L21
    exact hq
  8. L22
    exact hdistinct
  9. L23
    exact hqvaluation
04Establish hqnonzeroL24–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime nonzero.

  1. L24
    have hqnonzero : ~(q = 0)
  2. L25
    specialize prime_nonzero q
  3. L26
    intro hqzero
  4. L27
    apply prime_nonzero
  5. L28
    exact hq
  6. L29
    exact hqzero
05Establish hsumL30–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime power valuation mul.

  1. L30
    have hsum : g = e + f
  2. L31
    specialize prime_power_valuation_mul p
  3. L32
    specialize prime_power_valuation_mul n
  4. L33
    specialize prime_power_valuation_mul q
  5. L34
    specialize prime_power_valuation_mul e
  6. L35
    specialize prime_power_valuation_mul f
  7. L36
    specialize prime_power_valuation_mul g
  8. L37
    apply prime_power_valuation_mul
  9. L38
    exact hp
  10. L39
    exact hnnonzero
06Use earlier factsL40–43

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

  1. L40
    exact hqnonzero
  2. L41
    exact hnvaluation
  3. L42
    exact hqvaluation
  4. L43
    exact hproduct
07Calculate and transport equalitiesL44–45

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

  1. L44
    rewrite hzero at hsum
  2. L45
    rewrite PA3 at hsum
08Separate the logical casesL46–46

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

  1. L46
    cases heven
09Construct an explicit witnessL47–47

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

  1. L47
    exists x
10Calculate and transport equalitiesL48–49

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

  1. L48
    trans g
  2. L49
    symm
11Use earlier factsL50–51

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

  1. L50
    exact hsum
  2. L51
    exact heven_witness

Library-wide reading audit

Original exact command ledger · 51 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro n
  4. 0004intro e
  5. 0005intro f
  6. 0006intro g
  7. 0007intro hp
  8. 0008intro hq
  9. 0009intro hdistinct
  10. 0010intro hnnonzero
  11. 0011intro hnvaluation
  12. 0012intro hqvaluation
  13. 0013intro hproduct
  14. 0014intro heven
  15. 0015have hzero : f = 0
  16. 0016specialize distinct_prime_power_valuation_zero p
  17. 0017specialize distinct_prime_power_valuation_zero q
  18. 0018specialize distinct_prime_power_valuation_zero f
  19. 0019apply distinct_prime_power_valuation_zero
  20. 0020exact hp
  21. 0021exact hq
  22. 0022exact hdistinct
  23. 0023exact hqvaluation
  24. 0024have hqnonzero : ~(q = 0)
  25. 0025specialize prime_nonzero q
  26. 0026intro hqzero
  27. 0027apply prime_nonzero
  28. 0028exact hq
  29. 0029exact hqzero
  30. 0030have hsum : g = e + f
  31. 0031specialize prime_power_valuation_mul p
  32. 0032specialize prime_power_valuation_mul n
  33. 0033specialize prime_power_valuation_mul q
  34. 0034specialize prime_power_valuation_mul e
  35. 0035specialize prime_power_valuation_mul f
  36. 0036specialize prime_power_valuation_mul g
  37. 0037apply prime_power_valuation_mul
  38. 0038exact hp
  39. 0039exact hnnonzero
  40. 0040exact hqnonzero
  41. 0041exact hnvaluation
  42. 0042exact hqvaluation
  43. 0043exact hproduct
  44. 0044rewrite hzero at hsum
  45. 0045rewrite PA3 at hsum
  46. 0046cases heven
  47. 0047exists x
  48. 0048trans g
  49. 0049symm
  50. 0050exact hsum
  51. 0051exact heven_witness