TS0038 · theorem body

all_bad_prime_even_valuations_strip_represented_prime

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Removing a represented prime singleton preserves the entire universal three-modulo-four even-valuation invariant.

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.

Statement with defined notation

forall q n. ((~(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)) -> (exists ftsc_first_ftsp_good_prime ftsc_second_ftsp_good_prime. (q) = ftsc_first_ftsp_good_prime * ftsc_first_ftsp_good_prime + ftsc_second_ftsp_good_prime * ftsc_second_ftsp_good_prime) -> ~(n = 0) -> (forall ftsp_bad_prime_parity_good_product ftsp_bad_exponent_parity_good_product. ((~(ftsp_bad_prime_parity_good_product = 1) /\ forall frm_prime_left_ftsp_parity_good_product_prime frm_prime_right_ftsp_parity_good_product_prime. ftsp_bad_prime_parity_good_product = frm_prime_left_ftsp_parity_good_product_prime * frm_prime_right_ftsp_parity_good_product_prime -> frm_prime_left_ftsp_parity_good_product_prime = 1 \/ frm_prime_right_ftsp_parity_good_product_prime = 1)) -> (exists ftsc_four_three_ftsp_parity_good_product_three. (ftsp_bad_prime_parity_good_product) = 4 * ftsc_four_three_ftsp_parity_good_product_three + 3) -> (((exists bpv_gap_ftsp_parity_good_product_valuation_exponent_bound. bpv_gap_ftsp_parity_good_product_valuation_exponent_bound + ftsp_bad_exponent_parity_good_product = (n * q)) /\ (exists bpv_result_ftsp_parity_good_product_valuation_selected. ((exists ff_b_ftsp_parity_good_product_valuation_selected_power ff_c_ftsp_parity_good_product_valuation_selected_power. ((forall ff_i_ftsp_parity_good_product_valuation_selected_power_repeat. (exists ff_lt_ftsp_parity_good_product_valuation_selected_power_repeat_bound. ff_lt_ftsp_parity_good_product_valuation_selected_power_repeat_bound + S ff_i_ftsp_parity_good_product_valuation_selected_power_repeat = ftsp_bad_exponent_parity_good_product) -> (((exists ff_h_ftsp_parity_good_product_valuation_selected_power_repeat_decoded. ff_h_ftsp_parity_good_product_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_parity_good_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_repeat)) * ff_c_ftsp_parity_good_product_valuation_selected_power)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_repeat_decoded. ff_b_ftsp_parity_good_product_valuation_selected_power = ff_q_ftsp_parity_good_product_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_repeat)) * ff_c_ftsp_parity_good_product_valuation_selected_power) + (ftsp_bad_prime_parity_good_product)))) /\ (exists ff_u_ftsp_parity_good_product_valuation_selected_power_product ff_v_ftsp_parity_good_product_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_good_product_valuation_selected_power_product_start. ff_h_ftsp_parity_good_product_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_product_start. ff_u_ftsp_parity_good_product_valuation_selected_power_product = ff_q_ftsp_parity_good_product_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_selected_power_product_terminal. ff_h_ftsp_parity_good_product_valuation_selected_power_product_terminal + S (bpv_result_ftsp_parity_good_product_valuation_selected) = S ((S (ftsp_bad_exponent_parity_good_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_product_terminal. ff_u_ftsp_parity_good_product_valuation_selected_power_product = ff_q_ftsp_parity_good_product_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_parity_good_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product) + (bpv_result_ftsp_parity_good_product_valuation_selected))) /\ forall ff_i_ftsp_parity_good_product_valuation_selected_power_product. (exists ff_lt_ftsp_parity_good_product_valuation_selected_power_product_bound. ff_lt_ftsp_parity_good_product_valuation_selected_power_product_bound + S ff_i_ftsp_parity_good_product_valuation_selected_power_product = ftsp_bad_exponent_parity_good_product) -> exists ff_p_ftsp_parity_good_product_valuation_selected_power_product ff_r_ftsp_parity_good_product_valuation_selected_power_product ff_s_ftsp_parity_good_product_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_good_product_valuation_selected_power_product_factor. ff_h_ftsp_parity_good_product_valuation_selected_power_product_factor + S (ff_p_ftsp_parity_good_product_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_c_ftsp_parity_good_product_valuation_selected_power)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_product_factor. ff_b_ftsp_parity_good_product_valuation_selected_power = ff_q_ftsp_parity_good_product_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_c_ftsp_parity_good_product_valuation_selected_power) + (ff_p_ftsp_parity_good_product_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_selected_power_product_partial. ff_h_ftsp_parity_good_product_valuation_selected_power_product_partial + S (ff_r_ftsp_parity_good_product_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_product_partial. ff_u_ftsp_parity_good_product_valuation_selected_power_product = ff_q_ftsp_parity_good_product_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product) + (ff_r_ftsp_parity_good_product_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_selected_power_product_successor. ff_h_ftsp_parity_good_product_valuation_selected_power_product_successor + S (ff_s_ftsp_parity_good_product_valuation_selected_power_product) = S ((S (S ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_product_successor. ff_u_ftsp_parity_good_product_valuation_selected_power_product = ff_q_ftsp_parity_good_product_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product) + (ff_s_ftsp_parity_good_product_valuation_selected_power_product))) /\ ff_s_ftsp_parity_good_product_valuation_selected_power_product = ff_r_ftsp_parity_good_product_valuation_selected_power_product * ff_p_ftsp_parity_good_product_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_good_product_valuation_selected_divides. (n * q) = bpv_result_ftsp_parity_good_product_valuation_selected * bpv_factor_ftsp_parity_good_product_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_parity_good_product_valuation. (exists bpv_gap_ftsp_parity_good_product_valuation_candidate_bound. bpv_gap_ftsp_parity_good_product_valuation_candidate_bound + bpv_candidate_ftsp_parity_good_product_valuation = (n * q)) -> (exists bpv_result_ftsp_parity_good_product_valuation_candidate. ((exists ff_b_ftsp_parity_good_product_valuation_candidate_power ff_c_ftsp_parity_good_product_valuation_candidate_power. ((forall ff_i_ftsp_parity_good_product_valuation_candidate_power_repeat. (exists ff_lt_ftsp_parity_good_product_valuation_candidate_power_repeat_bound. ff_lt_ftsp_parity_good_product_valuation_candidate_power_repeat_bound + S ff_i_ftsp_parity_good_product_valuation_candidate_power_repeat = bpv_candidate_ftsp_parity_good_product_valuation) -> (((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_repeat_decoded. ff_h_ftsp_parity_good_product_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_parity_good_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_good_product_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_repeat_decoded. ff_b_ftsp_parity_good_product_valuation_candidate_power = ff_q_ftsp_parity_good_product_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_good_product_valuation_candidate_power) + (ftsp_bad_prime_parity_good_product)))) /\ (exists ff_u_ftsp_parity_good_product_valuation_candidate_power_product ff_v_ftsp_parity_good_product_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_product_start. ff_h_ftsp_parity_good_product_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_product_start. ff_u_ftsp_parity_good_product_valuation_candidate_power_product = ff_q_ftsp_parity_good_product_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_product_terminal. ff_h_ftsp_parity_good_product_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_parity_good_product_valuation_candidate) = S ((S (bpv_candidate_ftsp_parity_good_product_valuation)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_product_terminal. ff_u_ftsp_parity_good_product_valuation_candidate_power_product = ff_q_ftsp_parity_good_product_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_parity_good_product_valuation)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product) + (bpv_result_ftsp_parity_good_product_valuation_candidate))) /\ forall ff_i_ftsp_parity_good_product_valuation_candidate_power_product. (exists ff_lt_ftsp_parity_good_product_valuation_candidate_power_product_bound. ff_lt_ftsp_parity_good_product_valuation_candidate_power_product_bound + S ff_i_ftsp_parity_good_product_valuation_candidate_power_product = bpv_candidate_ftsp_parity_good_product_valuation) -> exists ff_p_ftsp_parity_good_product_valuation_candidate_power_product ff_r_ftsp_parity_good_product_valuation_candidate_power_product ff_s_ftsp_parity_good_product_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_product_factor. ff_h_ftsp_parity_good_product_valuation_candidate_power_product_factor + S (ff_p_ftsp_parity_good_product_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_c_ftsp_parity_good_product_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_product_factor. ff_b_ftsp_parity_good_product_valuation_candidate_power = ff_q_ftsp_parity_good_product_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_c_ftsp_parity_good_product_valuation_candidate_power) + (ff_p_ftsp_parity_good_product_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_product_partial. ff_h_ftsp_parity_good_product_valuation_candidate_power_product_partial + S (ff_r_ftsp_parity_good_product_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_product_partial. ff_u_ftsp_parity_good_product_valuation_candidate_power_product = ff_q_ftsp_parity_good_product_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product) + (ff_r_ftsp_parity_good_product_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_product_successor. ff_h_ftsp_parity_good_product_valuation_candidate_power_product_successor + S (ff_s_ftsp_parity_good_product_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_product_successor. ff_u_ftsp_parity_good_product_valuation_candidate_power_product = ff_q_ftsp_parity_good_product_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product) + (ff_s_ftsp_parity_good_product_valuation_candidate_power_product))) /\ ff_s_ftsp_parity_good_product_valuation_candidate_power_product = ff_r_ftsp_parity_good_product_valuation_candidate_power_product * ff_p_ftsp_parity_good_product_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_good_product_valuation_candidate_divides. (n * q) = bpv_result_ftsp_parity_good_product_valuation_candidate * bpv_factor_ftsp_parity_good_product_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_parity_good_product_valuation_maximal. bpv_gap_ftsp_parity_good_product_valuation_maximal + bpv_candidate_ftsp_parity_good_product_valuation = ftsp_bad_exponent_parity_good_product)) -> exists ftsp_bad_half_parity_good_product. ftsp_bad_exponent_parity_good_product = ftsp_bad_half_parity_good_product + ftsp_bad_half_parity_good_product) -> (forall ftsp_bad_prime_parity_source ftsp_bad_exponent_parity_source. ((~(ftsp_bad_prime_parity_source = 1) /\ forall frm_prime_left_ftsp_parity_source_prime frm_prime_right_ftsp_parity_source_prime. ftsp_bad_prime_parity_source = frm_prime_left_ftsp_parity_source_prime * frm_prime_right_ftsp_parity_source_prime -> frm_prime_left_ftsp_parity_source_prime = 1 \/ frm_prime_right_ftsp_parity_source_prime = 1)) -> (exists ftsc_four_three_ftsp_parity_source_three. (ftsp_bad_prime_parity_source) = 4 * ftsc_four_three_ftsp_parity_source_three + 3) -> (((exists bpv_gap_ftsp_parity_source_valuation_exponent_bound. bpv_gap_ftsp_parity_source_valuation_exponent_bound + ftsp_bad_exponent_parity_source = (n)) /\ (exists bpv_result_ftsp_parity_source_valuation_selected. ((exists ff_b_ftsp_parity_source_valuation_selected_power ff_c_ftsp_parity_source_valuation_selected_power. ((forall ff_i_ftsp_parity_source_valuation_selected_power_repeat. (exists ff_lt_ftsp_parity_source_valuation_selected_power_repeat_bound. ff_lt_ftsp_parity_source_valuation_selected_power_repeat_bound + S ff_i_ftsp_parity_source_valuation_selected_power_repeat = ftsp_bad_exponent_parity_source) -> (((exists ff_h_ftsp_parity_source_valuation_selected_power_repeat_decoded. ff_h_ftsp_parity_source_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_parity_source) = S ((S (ff_i_ftsp_parity_source_valuation_selected_power_repeat)) * ff_c_ftsp_parity_source_valuation_selected_power)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_repeat_decoded. ff_b_ftsp_parity_source_valuation_selected_power = ff_q_ftsp_parity_source_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_parity_source_valuation_selected_power_repeat)) * ff_c_ftsp_parity_source_valuation_selected_power) + (ftsp_bad_prime_parity_source)))) /\ (exists ff_u_ftsp_parity_source_valuation_selected_power_product ff_v_ftsp_parity_source_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_start. ff_h_ftsp_parity_source_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_start. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_terminal. ff_h_ftsp_parity_source_valuation_selected_power_product_terminal + S (bpv_result_ftsp_parity_source_valuation_selected) = S ((S (ftsp_bad_exponent_parity_source)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_terminal. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_parity_source)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (bpv_result_ftsp_parity_source_valuation_selected))) /\ forall ff_i_ftsp_parity_source_valuation_selected_power_product. (exists ff_lt_ftsp_parity_source_valuation_selected_power_product_bound. ff_lt_ftsp_parity_source_valuation_selected_power_product_bound + S ff_i_ftsp_parity_source_valuation_selected_power_product = ftsp_bad_exponent_parity_source) -> exists ff_p_ftsp_parity_source_valuation_selected_power_product ff_r_ftsp_parity_source_valuation_selected_power_product ff_s_ftsp_parity_source_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_factor. ff_h_ftsp_parity_source_valuation_selected_power_product_factor + S (ff_p_ftsp_parity_source_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_c_ftsp_parity_source_valuation_selected_power)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_factor. ff_b_ftsp_parity_source_valuation_selected_power = ff_q_ftsp_parity_source_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_c_ftsp_parity_source_valuation_selected_power) + (ff_p_ftsp_parity_source_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_partial. ff_h_ftsp_parity_source_valuation_selected_power_product_partial + S (ff_r_ftsp_parity_source_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_partial. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (ff_r_ftsp_parity_source_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_successor. ff_h_ftsp_parity_source_valuation_selected_power_product_successor + S (ff_s_ftsp_parity_source_valuation_selected_power_product) = S ((S (S ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_successor. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (ff_s_ftsp_parity_source_valuation_selected_power_product))) /\ ff_s_ftsp_parity_source_valuation_selected_power_product = ff_r_ftsp_parity_source_valuation_selected_power_product * ff_p_ftsp_parity_source_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_source_valuation_selected_divides. (n) = bpv_result_ftsp_parity_source_valuation_selected * bpv_factor_ftsp_parity_source_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_parity_source_valuation. (exists bpv_gap_ftsp_parity_source_valuation_candidate_bound. bpv_gap_ftsp_parity_source_valuation_candidate_bound + bpv_candidate_ftsp_parity_source_valuation = (n)) -> (exists bpv_result_ftsp_parity_source_valuation_candidate. ((exists ff_b_ftsp_parity_source_valuation_candidate_power ff_c_ftsp_parity_source_valuation_candidate_power. ((forall ff_i_ftsp_parity_source_valuation_candidate_power_repeat. (exists ff_lt_ftsp_parity_source_valuation_candidate_power_repeat_bound. ff_lt_ftsp_parity_source_valuation_candidate_power_repeat_bound + S ff_i_ftsp_parity_source_valuation_candidate_power_repeat = bpv_candidate_ftsp_parity_source_valuation) -> (((exists ff_h_ftsp_parity_source_valuation_candidate_power_repeat_decoded. ff_h_ftsp_parity_source_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_parity_source) = S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_source_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_repeat_decoded. ff_b_ftsp_parity_source_valuation_candidate_power = ff_q_ftsp_parity_source_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_source_valuation_candidate_power) + (ftsp_bad_prime_parity_source)))) /\ (exists ff_u_ftsp_parity_source_valuation_candidate_power_product ff_v_ftsp_parity_source_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_start. ff_h_ftsp_parity_source_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_start. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_terminal. ff_h_ftsp_parity_source_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_parity_source_valuation_candidate) = S ((S (bpv_candidate_ftsp_parity_source_valuation)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_terminal. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_parity_source_valuation)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (bpv_result_ftsp_parity_source_valuation_candidate))) /\ forall ff_i_ftsp_parity_source_valuation_candidate_power_product. (exists ff_lt_ftsp_parity_source_valuation_candidate_power_product_bound. ff_lt_ftsp_parity_source_valuation_candidate_power_product_bound + S ff_i_ftsp_parity_source_valuation_candidate_power_product = bpv_candidate_ftsp_parity_source_valuation) -> exists ff_p_ftsp_parity_source_valuation_candidate_power_product ff_r_ftsp_parity_source_valuation_candidate_power_product ff_s_ftsp_parity_source_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_factor. ff_h_ftsp_parity_source_valuation_candidate_power_product_factor + S (ff_p_ftsp_parity_source_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_c_ftsp_parity_source_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_factor. ff_b_ftsp_parity_source_valuation_candidate_power = ff_q_ftsp_parity_source_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_c_ftsp_parity_source_valuation_candidate_power) + (ff_p_ftsp_parity_source_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_partial. ff_h_ftsp_parity_source_valuation_candidate_power_product_partial + S (ff_r_ftsp_parity_source_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_partial. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (ff_r_ftsp_parity_source_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_successor. ff_h_ftsp_parity_source_valuation_candidate_power_product_successor + S (ff_s_ftsp_parity_source_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_successor. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (ff_s_ftsp_parity_source_valuation_candidate_power_product))) /\ ff_s_ftsp_parity_source_valuation_candidate_power_product = ff_r_ftsp_parity_source_valuation_candidate_power_product * ff_p_ftsp_parity_source_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_source_valuation_candidate_divides. (n) = bpv_result_ftsp_parity_source_valuation_candidate * bpv_factor_ftsp_parity_source_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_parity_source_valuation_maximal. bpv_gap_ftsp_parity_source_valuation_maximal + bpv_candidate_ftsp_parity_source_valuation = ftsp_bad_exponent_parity_source)) -> exists ftsp_bad_half_parity_source. ftsp_bad_exponent_parity_source = ftsp_bad_half_parity_source + ftsp_bad_half_parity_source)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

none

In local proof propositions

PD0046 PowerValuation
Exact expanded first-order statement
forall q n. ((~(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)) -> (exists ftsc_first_ftsp_good_prime ftsc_second_ftsp_good_prime. (q) = ftsc_first_ftsp_good_prime * ftsc_first_ftsp_good_prime + ftsc_second_ftsp_good_prime * ftsc_second_ftsp_good_prime) -> ~(n = 0) -> (forall ftsp_bad_prime_parity_good_product ftsp_bad_exponent_parity_good_product. ((~(ftsp_bad_prime_parity_good_product = 1) /\ forall frm_prime_left_ftsp_parity_good_product_prime frm_prime_right_ftsp_parity_good_product_prime. ftsp_bad_prime_parity_good_product = frm_prime_left_ftsp_parity_good_product_prime * frm_prime_right_ftsp_parity_good_product_prime -> frm_prime_left_ftsp_parity_good_product_prime = 1 \/ frm_prime_right_ftsp_parity_good_product_prime = 1)) -> (exists ftsc_four_three_ftsp_parity_good_product_three. (ftsp_bad_prime_parity_good_product) = 4 * ftsc_four_three_ftsp_parity_good_product_three + 3) -> (((exists bpv_gap_ftsp_parity_good_product_valuation_exponent_bound. bpv_gap_ftsp_parity_good_product_valuation_exponent_bound + ftsp_bad_exponent_parity_good_product = (n * q)) /\ (exists bpv_result_ftsp_parity_good_product_valuation_selected. ((exists ff_b_ftsp_parity_good_product_valuation_selected_power ff_c_ftsp_parity_good_product_valuation_selected_power. ((forall ff_i_ftsp_parity_good_product_valuation_selected_power_repeat. (exists ff_lt_ftsp_parity_good_product_valuation_selected_power_repeat_bound. ff_lt_ftsp_parity_good_product_valuation_selected_power_repeat_bound + S ff_i_ftsp_parity_good_product_valuation_selected_power_repeat = ftsp_bad_exponent_parity_good_product) -> (((exists ff_h_ftsp_parity_good_product_valuation_selected_power_repeat_decoded. ff_h_ftsp_parity_good_product_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_parity_good_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_repeat)) * ff_c_ftsp_parity_good_product_valuation_selected_power)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_repeat_decoded. ff_b_ftsp_parity_good_product_valuation_selected_power = ff_q_ftsp_parity_good_product_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_repeat)) * ff_c_ftsp_parity_good_product_valuation_selected_power) + (ftsp_bad_prime_parity_good_product)))) /\ (exists ff_u_ftsp_parity_good_product_valuation_selected_power_product ff_v_ftsp_parity_good_product_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_good_product_valuation_selected_power_product_start. ff_h_ftsp_parity_good_product_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_product_start. ff_u_ftsp_parity_good_product_valuation_selected_power_product = ff_q_ftsp_parity_good_product_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_selected_power_product_terminal. ff_h_ftsp_parity_good_product_valuation_selected_power_product_terminal + S (bpv_result_ftsp_parity_good_product_valuation_selected) = S ((S (ftsp_bad_exponent_parity_good_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_product_terminal. ff_u_ftsp_parity_good_product_valuation_selected_power_product = ff_q_ftsp_parity_good_product_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_parity_good_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product) + (bpv_result_ftsp_parity_good_product_valuation_selected))) /\ forall ff_i_ftsp_parity_good_product_valuation_selected_power_product. (exists ff_lt_ftsp_parity_good_product_valuation_selected_power_product_bound. ff_lt_ftsp_parity_good_product_valuation_selected_power_product_bound + S ff_i_ftsp_parity_good_product_valuation_selected_power_product = ftsp_bad_exponent_parity_good_product) -> exists ff_p_ftsp_parity_good_product_valuation_selected_power_product ff_r_ftsp_parity_good_product_valuation_selected_power_product ff_s_ftsp_parity_good_product_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_good_product_valuation_selected_power_product_factor. ff_h_ftsp_parity_good_product_valuation_selected_power_product_factor + S (ff_p_ftsp_parity_good_product_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_c_ftsp_parity_good_product_valuation_selected_power)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_product_factor. ff_b_ftsp_parity_good_product_valuation_selected_power = ff_q_ftsp_parity_good_product_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_c_ftsp_parity_good_product_valuation_selected_power) + (ff_p_ftsp_parity_good_product_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_selected_power_product_partial. ff_h_ftsp_parity_good_product_valuation_selected_power_product_partial + S (ff_r_ftsp_parity_good_product_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_product_partial. ff_u_ftsp_parity_good_product_valuation_selected_power_product = ff_q_ftsp_parity_good_product_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product) + (ff_r_ftsp_parity_good_product_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_selected_power_product_successor. ff_h_ftsp_parity_good_product_valuation_selected_power_product_successor + S (ff_s_ftsp_parity_good_product_valuation_selected_power_product) = S ((S (S ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_selected_power_product_successor. ff_u_ftsp_parity_good_product_valuation_selected_power_product = ff_q_ftsp_parity_good_product_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_parity_good_product_valuation_selected_power_product)) * ff_v_ftsp_parity_good_product_valuation_selected_power_product) + (ff_s_ftsp_parity_good_product_valuation_selected_power_product))) /\ ff_s_ftsp_parity_good_product_valuation_selected_power_product = ff_r_ftsp_parity_good_product_valuation_selected_power_product * ff_p_ftsp_parity_good_product_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_good_product_valuation_selected_divides. (n * q) = bpv_result_ftsp_parity_good_product_valuation_selected * bpv_factor_ftsp_parity_good_product_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_parity_good_product_valuation. (exists bpv_gap_ftsp_parity_good_product_valuation_candidate_bound. bpv_gap_ftsp_parity_good_product_valuation_candidate_bound + bpv_candidate_ftsp_parity_good_product_valuation = (n * q)) -> (exists bpv_result_ftsp_parity_good_product_valuation_candidate. ((exists ff_b_ftsp_parity_good_product_valuation_candidate_power ff_c_ftsp_parity_good_product_valuation_candidate_power. ((forall ff_i_ftsp_parity_good_product_valuation_candidate_power_repeat. (exists ff_lt_ftsp_parity_good_product_valuation_candidate_power_repeat_bound. ff_lt_ftsp_parity_good_product_valuation_candidate_power_repeat_bound + S ff_i_ftsp_parity_good_product_valuation_candidate_power_repeat = bpv_candidate_ftsp_parity_good_product_valuation) -> (((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_repeat_decoded. ff_h_ftsp_parity_good_product_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_parity_good_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_good_product_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_repeat_decoded. ff_b_ftsp_parity_good_product_valuation_candidate_power = ff_q_ftsp_parity_good_product_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_good_product_valuation_candidate_power) + (ftsp_bad_prime_parity_good_product)))) /\ (exists ff_u_ftsp_parity_good_product_valuation_candidate_power_product ff_v_ftsp_parity_good_product_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_product_start. ff_h_ftsp_parity_good_product_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_product_start. ff_u_ftsp_parity_good_product_valuation_candidate_power_product = ff_q_ftsp_parity_good_product_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_product_terminal. ff_h_ftsp_parity_good_product_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_parity_good_product_valuation_candidate) = S ((S (bpv_candidate_ftsp_parity_good_product_valuation)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_product_terminal. ff_u_ftsp_parity_good_product_valuation_candidate_power_product = ff_q_ftsp_parity_good_product_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_parity_good_product_valuation)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product) + (bpv_result_ftsp_parity_good_product_valuation_candidate))) /\ forall ff_i_ftsp_parity_good_product_valuation_candidate_power_product. (exists ff_lt_ftsp_parity_good_product_valuation_candidate_power_product_bound. ff_lt_ftsp_parity_good_product_valuation_candidate_power_product_bound + S ff_i_ftsp_parity_good_product_valuation_candidate_power_product = bpv_candidate_ftsp_parity_good_product_valuation) -> exists ff_p_ftsp_parity_good_product_valuation_candidate_power_product ff_r_ftsp_parity_good_product_valuation_candidate_power_product ff_s_ftsp_parity_good_product_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_product_factor. ff_h_ftsp_parity_good_product_valuation_candidate_power_product_factor + S (ff_p_ftsp_parity_good_product_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_c_ftsp_parity_good_product_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_product_factor. ff_b_ftsp_parity_good_product_valuation_candidate_power = ff_q_ftsp_parity_good_product_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_c_ftsp_parity_good_product_valuation_candidate_power) + (ff_p_ftsp_parity_good_product_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_product_partial. ff_h_ftsp_parity_good_product_valuation_candidate_power_product_partial + S (ff_r_ftsp_parity_good_product_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_product_partial. ff_u_ftsp_parity_good_product_valuation_candidate_power_product = ff_q_ftsp_parity_good_product_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product) + (ff_r_ftsp_parity_good_product_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_good_product_valuation_candidate_power_product_successor. ff_h_ftsp_parity_good_product_valuation_candidate_power_product_successor + S (ff_s_ftsp_parity_good_product_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_good_product_valuation_candidate_power_product_successor. ff_u_ftsp_parity_good_product_valuation_candidate_power_product = ff_q_ftsp_parity_good_product_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_parity_good_product_valuation_candidate_power_product)) * ff_v_ftsp_parity_good_product_valuation_candidate_power_product) + (ff_s_ftsp_parity_good_product_valuation_candidate_power_product))) /\ ff_s_ftsp_parity_good_product_valuation_candidate_power_product = ff_r_ftsp_parity_good_product_valuation_candidate_power_product * ff_p_ftsp_parity_good_product_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_good_product_valuation_candidate_divides. (n * q) = bpv_result_ftsp_parity_good_product_valuation_candidate * bpv_factor_ftsp_parity_good_product_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_parity_good_product_valuation_maximal. bpv_gap_ftsp_parity_good_product_valuation_maximal + bpv_candidate_ftsp_parity_good_product_valuation = ftsp_bad_exponent_parity_good_product)) -> exists ftsp_bad_half_parity_good_product. ftsp_bad_exponent_parity_good_product = ftsp_bad_half_parity_good_product + ftsp_bad_half_parity_good_product) -> (forall ftsp_bad_prime_parity_source ftsp_bad_exponent_parity_source. ((~(ftsp_bad_prime_parity_source = 1) /\ forall frm_prime_left_ftsp_parity_source_prime frm_prime_right_ftsp_parity_source_prime. ftsp_bad_prime_parity_source = frm_prime_left_ftsp_parity_source_prime * frm_prime_right_ftsp_parity_source_prime -> frm_prime_left_ftsp_parity_source_prime = 1 \/ frm_prime_right_ftsp_parity_source_prime = 1)) -> (exists ftsc_four_three_ftsp_parity_source_three. (ftsp_bad_prime_parity_source) = 4 * ftsc_four_three_ftsp_parity_source_three + 3) -> (((exists bpv_gap_ftsp_parity_source_valuation_exponent_bound. bpv_gap_ftsp_parity_source_valuation_exponent_bound + ftsp_bad_exponent_parity_source = (n)) /\ (exists bpv_result_ftsp_parity_source_valuation_selected. ((exists ff_b_ftsp_parity_source_valuation_selected_power ff_c_ftsp_parity_source_valuation_selected_power. ((forall ff_i_ftsp_parity_source_valuation_selected_power_repeat. (exists ff_lt_ftsp_parity_source_valuation_selected_power_repeat_bound. ff_lt_ftsp_parity_source_valuation_selected_power_repeat_bound + S ff_i_ftsp_parity_source_valuation_selected_power_repeat = ftsp_bad_exponent_parity_source) -> (((exists ff_h_ftsp_parity_source_valuation_selected_power_repeat_decoded. ff_h_ftsp_parity_source_valuation_selected_power_repeat_decoded + S (ftsp_bad_prime_parity_source) = S ((S (ff_i_ftsp_parity_source_valuation_selected_power_repeat)) * ff_c_ftsp_parity_source_valuation_selected_power)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_repeat_decoded. ff_b_ftsp_parity_source_valuation_selected_power = ff_q_ftsp_parity_source_valuation_selected_power_repeat_decoded * S ((S (ff_i_ftsp_parity_source_valuation_selected_power_repeat)) * ff_c_ftsp_parity_source_valuation_selected_power) + (ftsp_bad_prime_parity_source)))) /\ (exists ff_u_ftsp_parity_source_valuation_selected_power_product ff_v_ftsp_parity_source_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_start. ff_h_ftsp_parity_source_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_start. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_start * S ((S (0)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_terminal. ff_h_ftsp_parity_source_valuation_selected_power_product_terminal + S (bpv_result_ftsp_parity_source_valuation_selected) = S ((S (ftsp_bad_exponent_parity_source)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_terminal. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_terminal * S ((S (ftsp_bad_exponent_parity_source)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (bpv_result_ftsp_parity_source_valuation_selected))) /\ forall ff_i_ftsp_parity_source_valuation_selected_power_product. (exists ff_lt_ftsp_parity_source_valuation_selected_power_product_bound. ff_lt_ftsp_parity_source_valuation_selected_power_product_bound + S ff_i_ftsp_parity_source_valuation_selected_power_product = ftsp_bad_exponent_parity_source) -> exists ff_p_ftsp_parity_source_valuation_selected_power_product ff_r_ftsp_parity_source_valuation_selected_power_product ff_s_ftsp_parity_source_valuation_selected_power_product. ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_factor. ff_h_ftsp_parity_source_valuation_selected_power_product_factor + S (ff_p_ftsp_parity_source_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_c_ftsp_parity_source_valuation_selected_power)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_factor. ff_b_ftsp_parity_source_valuation_selected_power = ff_q_ftsp_parity_source_valuation_selected_power_product_factor * S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_c_ftsp_parity_source_valuation_selected_power) + (ff_p_ftsp_parity_source_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_partial. ff_h_ftsp_parity_source_valuation_selected_power_product_partial + S (ff_r_ftsp_parity_source_valuation_selected_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_partial. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_partial * S ((S (ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (ff_r_ftsp_parity_source_valuation_selected_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_selected_power_product_successor. ff_h_ftsp_parity_source_valuation_selected_power_product_successor + S (ff_s_ftsp_parity_source_valuation_selected_power_product) = S ((S (S ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_selected_power_product_successor. ff_u_ftsp_parity_source_valuation_selected_power_product = ff_q_ftsp_parity_source_valuation_selected_power_product_successor * S ((S (S ff_i_ftsp_parity_source_valuation_selected_power_product)) * ff_v_ftsp_parity_source_valuation_selected_power_product) + (ff_s_ftsp_parity_source_valuation_selected_power_product))) /\ ff_s_ftsp_parity_source_valuation_selected_power_product = ff_r_ftsp_parity_source_valuation_selected_power_product * ff_p_ftsp_parity_source_valuation_selected_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_source_valuation_selected_divides. (n) = bpv_result_ftsp_parity_source_valuation_selected * bpv_factor_ftsp_parity_source_valuation_selected_divides)))) /\ forall bpv_candidate_ftsp_parity_source_valuation. (exists bpv_gap_ftsp_parity_source_valuation_candidate_bound. bpv_gap_ftsp_parity_source_valuation_candidate_bound + bpv_candidate_ftsp_parity_source_valuation = (n)) -> (exists bpv_result_ftsp_parity_source_valuation_candidate. ((exists ff_b_ftsp_parity_source_valuation_candidate_power ff_c_ftsp_parity_source_valuation_candidate_power. ((forall ff_i_ftsp_parity_source_valuation_candidate_power_repeat. (exists ff_lt_ftsp_parity_source_valuation_candidate_power_repeat_bound. ff_lt_ftsp_parity_source_valuation_candidate_power_repeat_bound + S ff_i_ftsp_parity_source_valuation_candidate_power_repeat = bpv_candidate_ftsp_parity_source_valuation) -> (((exists ff_h_ftsp_parity_source_valuation_candidate_power_repeat_decoded. ff_h_ftsp_parity_source_valuation_candidate_power_repeat_decoded + S (ftsp_bad_prime_parity_source) = S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_source_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_repeat_decoded. ff_b_ftsp_parity_source_valuation_candidate_power = ff_q_ftsp_parity_source_valuation_candidate_power_repeat_decoded * S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_repeat)) * ff_c_ftsp_parity_source_valuation_candidate_power) + (ftsp_bad_prime_parity_source)))) /\ (exists ff_u_ftsp_parity_source_valuation_candidate_power_product ff_v_ftsp_parity_source_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_start. ff_h_ftsp_parity_source_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_start. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_start * S ((S (0)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_terminal. ff_h_ftsp_parity_source_valuation_candidate_power_product_terminal + S (bpv_result_ftsp_parity_source_valuation_candidate) = S ((S (bpv_candidate_ftsp_parity_source_valuation)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_terminal. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_ftsp_parity_source_valuation)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (bpv_result_ftsp_parity_source_valuation_candidate))) /\ forall ff_i_ftsp_parity_source_valuation_candidate_power_product. (exists ff_lt_ftsp_parity_source_valuation_candidate_power_product_bound. ff_lt_ftsp_parity_source_valuation_candidate_power_product_bound + S ff_i_ftsp_parity_source_valuation_candidate_power_product = bpv_candidate_ftsp_parity_source_valuation) -> exists ff_p_ftsp_parity_source_valuation_candidate_power_product ff_r_ftsp_parity_source_valuation_candidate_power_product ff_s_ftsp_parity_source_valuation_candidate_power_product. ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_factor. ff_h_ftsp_parity_source_valuation_candidate_power_product_factor + S (ff_p_ftsp_parity_source_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_c_ftsp_parity_source_valuation_candidate_power)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_factor. ff_b_ftsp_parity_source_valuation_candidate_power = ff_q_ftsp_parity_source_valuation_candidate_power_product_factor * S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_c_ftsp_parity_source_valuation_candidate_power) + (ff_p_ftsp_parity_source_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_partial. ff_h_ftsp_parity_source_valuation_candidate_power_product_partial + S (ff_r_ftsp_parity_source_valuation_candidate_power_product) = S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_partial. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_partial * S ((S (ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (ff_r_ftsp_parity_source_valuation_candidate_power_product))) /\ ((((exists ff_h_ftsp_parity_source_valuation_candidate_power_product_successor. ff_h_ftsp_parity_source_valuation_candidate_power_product_successor + S (ff_s_ftsp_parity_source_valuation_candidate_power_product) = S ((S (S ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product)) /\ exists ff_q_ftsp_parity_source_valuation_candidate_power_product_successor. ff_u_ftsp_parity_source_valuation_candidate_power_product = ff_q_ftsp_parity_source_valuation_candidate_power_product_successor * S ((S (S ff_i_ftsp_parity_source_valuation_candidate_power_product)) * ff_v_ftsp_parity_source_valuation_candidate_power_product) + (ff_s_ftsp_parity_source_valuation_candidate_power_product))) /\ ff_s_ftsp_parity_source_valuation_candidate_power_product = ff_r_ftsp_parity_source_valuation_candidate_power_product * ff_p_ftsp_parity_source_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_ftsp_parity_source_valuation_candidate_divides. (n) = bpv_result_ftsp_parity_source_valuation_candidate * bpv_factor_ftsp_parity_source_valuation_candidate_divides))) -> (exists bpv_gap_ftsp_parity_source_valuation_maximal. bpv_gap_ftsp_parity_source_valuation_maximal + bpv_candidate_ftsp_parity_source_valuation = ftsp_bad_exponent_parity_source)) -> exists ftsp_bad_half_parity_source. ftsp_bad_exponent_parity_source = ftsp_bad_half_parity_source + ftsp_bad_half_parity_source)

Proof neighborhood

Direct theorem prerequisites

TS0037 three_mod_four_number_not_equal_represented power_valuation_exists · Alpha closed TS0035 distinct_prime_factor_even_valuation_reflects_prefix

Direct theorem dependents

TS003C all_bad_prime_even_two_square_sufficiency_bounded

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

47 script commands · 10 reading checkpoints · 4 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
three mod four number not equal representeddistinct prime factor even valuation reflects prefix
01Fix variables and assumptionsL1–10

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

  1. L1
    intro q
  2. L2
    intro n
  3. L3
    intro hqprime
  4. L4
    intro hrepresented
  5. L5
    intro hnonzero
  6. L6
    intro htotal
  7. L7
    intro p
  8. L8
    intro e
  9. L9
    intro hpprime
  10. L10
    intro hpbad
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hnvaluation
03Establish hdistinctL12–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply three mod four number not equal represented.

  1. L12
    have hdistinct : ~(p = q)
  2. L13
    specialize three_mod_four_number_not_equal_represented p
  3. L14
    specialize three_mod_four_number_not_equal_represented q
  4. L15
    intro hequal
  5. L16
    apply three_mod_four_number_not_equal_represented
  6. L17
    exact hpbad
  7. L18
    exact hrepresented
  8. L19
    exact hequal
04Establish hqvaluationL20–21

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

  1. L20
    have hqvaluation : ∃ f. PowerValuation(p,q,f)Definitions: PowerValuation(p,q,f)Original native command in the exact edition
  2. L21
    apply power_valuation_exists
05Separate the logical casesL22–22

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

  1. L22
    cases hqvaluation
06Establish hproductL23–24

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

  1. L23
    have hproduct : ∃ g. PowerValuation(p,n · q,g)Definitions: PowerValuation(p,n · q,g)Original native command in the exact edition
  2. L24
    apply power_valuation_exists
07Separate the logical casesL25–25

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

  1. L25
    cases hproduct
08Establish hevenL26–35

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

  1. L26
    have heven : exists h. x1 = h + h
  2. L27
    specialize htotal p
  3. L28
    specialize htotal x1
  4. L29
    apply htotal
  5. L30
    exact hpprime
  6. L31
    exact hpbad
  7. L32
    exact hproduct_witness
  8. L33
    specialize distinct_prime_factor_even_valuation_reflects_prefix p
  9. L34
    specialize distinct_prime_factor_even_valuation_reflects_prefix q
  10. L35
    specialize distinct_prime_factor_even_valuation_reflects_prefix n
09Use earlier factsL36–45

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

  1. L36
    specialize distinct_prime_factor_even_valuation_reflects_prefix e
  2. L37
    specialize distinct_prime_factor_even_valuation_reflects_prefix x
  3. L38
    specialize distinct_prime_factor_even_valuation_reflects_prefix x1
  4. L39
    apply distinct_prime_factor_even_valuation_reflects_prefix
  5. L40
    exact hpprime
  6. L41
    exact hqprime
  7. L42
    exact hdistinct
  8. L43
    exact hnonzero
  9. L44
    exact hnvaluation
  10. L45
    exact hqvaluation_witness
10Use earlier factsL46–47

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

  1. L46
    exact hproduct_witness
  2. L47
    exact heven

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro q
  2. 0002intro n
  3. 0003intro hqprime
  4. 0004intro hrepresented
  5. 0005intro hnonzero
  6. 0006intro htotal
  7. 0007intro p
  8. 0008intro e
  9. 0009intro hpprime
  10. 0010intro hpbad
  11. 0011intro hnvaluation
  12. 0012have hdistinct : ~(p = q)
  13. 0013specialize three_mod_four_number_not_equal_represented p
  14. 0014specialize three_mod_four_number_not_equal_represented q
  15. 0015intro hequal
  16. 0016apply three_mod_four_number_not_equal_represented
  17. 0017exact hpbad
  18. 0018exact hrepresented
  19. 0019exact hequal
  20. 0020have hqvaluation : ∃ f. PowerValuation(p,q,f)
    Exact native replay linehave hqvaluation : exists f. (((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))
  21. 0021apply power_valuation_exists
  22. 0022cases hqvaluation
  23. 0023have hproduct : ∃ g. PowerValuation(p,n · q,g)
    Exact native replay linehave hproduct : exists g. (((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))
  24. 0024apply power_valuation_exists
  25. 0025cases hproduct
  26. 0026have heven : exists h. x1 = h + h
  27. 0027specialize htotal p
  28. 0028specialize htotal x1
  29. 0029apply htotal
  30. 0030exact hpprime
  31. 0031exact hpbad
  32. 0032exact hproduct_witness
  33. 0033specialize distinct_prime_factor_even_valuation_reflects_prefix p
  34. 0034specialize distinct_prime_factor_even_valuation_reflects_prefix q
  35. 0035specialize distinct_prime_factor_even_valuation_reflects_prefix n
  36. 0036specialize distinct_prime_factor_even_valuation_reflects_prefix e
  37. 0037specialize distinct_prime_factor_even_valuation_reflects_prefix x
  38. 0038specialize distinct_prime_factor_even_valuation_reflects_prefix x1
  39. 0039apply distinct_prime_factor_even_valuation_reflects_prefix
  40. 0040exact hpprime
  41. 0041exact hqprime
  42. 0042exact hdistinct
  43. 0043exact hnonzero
  44. 0044exact hnvaluation
  45. 0045exact hqvaluation_witness
  46. 0046exact hproduct_witness
  47. 0047exact heven