TS003P

prime_power_valuation_square_factor_shift

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

Multiplying a nonzero value by a nonzero square increases its prime valuation by exactly twice the factor valuation.

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 z n e f g. ((~(p = 1) /\ forall frm_prime_left_ftsv_prime frm_prime_right_ftsv_prime. p = frm_prime_left_ftsv_prime * frm_prime_right_ftsv_prime -> frm_prime_left_ftsv_prime = 1 \/ frm_prime_right_ftsv_prime = 1)) -> ~(z = 0) -> ~(n = 0) -> (((exists bpv_gap_ftsv_shift_factor_exponent_bound. bpv_gap_ftsv_shift_factor_exponent_bound + e = z) /\ (exists bpv_result_ftsv_shift_factor_selected. ((exists ff_b_ftsv_shift_factor_selected_power ff_c_ftsv_shift_factor_selected_power. ((forall ff_i_ftsv_shift_factor_selected_power_repeat. (exists ff_lt_ftsv_shift_factor_selected_power_repeat_bound. ff_lt_ftsv_shift_factor_selected_power_repeat_bound + S ff_i_ftsv_shift_factor_selected_power_repeat = e) -> (((exists ff_h_ftsv_shift_factor_selected_power_repeat_decoded. ff_h_ftsv_shift_factor_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_shift_factor_selected_power_repeat)) * ff_c_ftsv_shift_factor_selected_power)) /\ exists ff_q_ftsv_shift_factor_selected_power_repeat_decoded. ff_b_ftsv_shift_factor_selected_power = ff_q_ftsv_shift_factor_selected_power_repeat_decoded * S ((S (ff_i_ftsv_shift_factor_selected_power_repeat)) * ff_c_ftsv_shift_factor_selected_power) + (p)))) /\ (exists ff_u_ftsv_shift_factor_selected_power_product ff_v_ftsv_shift_factor_selected_power_product. ((((exists ff_h_ftsv_shift_factor_selected_power_product_start. ff_h_ftsv_shift_factor_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_shift_factor_selected_power_product)) /\ exists ff_q_ftsv_shift_factor_selected_power_product_start. ff_u_ftsv_shift_factor_selected_power_product = ff_q_ftsv_shift_factor_selected_power_product_start * S ((S (0)) * ff_v_ftsv_shift_factor_selected_power_product) + (1))) /\ ((((exists ff_h_ftsv_shift_factor_selected_power_product_terminal. ff_h_ftsv_shift_factor_selected_power_product_terminal + S (bpv_result_ftsv_shift_factor_selected) = S ((S (e)) * ff_v_ftsv_shift_factor_selected_power_product)) /\ exists ff_q_ftsv_shift_factor_selected_power_product_terminal. ff_u_ftsv_shift_factor_selected_power_product = ff_q_ftsv_shift_factor_selected_power_product_terminal * S ((S (e)) * ff_v_ftsv_shift_factor_selected_power_product) + (bpv_result_ftsv_shift_factor_selected))) /\ forall ff_i_ftsv_shift_factor_selected_power_product. (exists ff_lt_ftsv_shift_factor_selected_power_product_bound. ff_lt_ftsv_shift_factor_selected_power_product_bound + S ff_i_ftsv_shift_factor_selected_power_product = e) -> exists ff_p_ftsv_shift_factor_selected_power_product ff_r_ftsv_shift_factor_selected_power_product ff_s_ftsv_shift_factor_selected_power_product. ((((exists ff_h_ftsv_shift_factor_selected_power_product_factor. ff_h_ftsv_shift_factor_selected_power_product_factor + S (ff_p_ftsv_shift_factor_selected_power_product) = S ((S (ff_i_ftsv_shift_factor_selected_power_product)) * ff_c_ftsv_shift_factor_selected_power)) /\ exists ff_q_ftsv_shift_factor_selected_power_product_factor. ff_b_ftsv_shift_factor_selected_power = ff_q_ftsv_shift_factor_selected_power_product_factor * S ((S (ff_i_ftsv_shift_factor_selected_power_product)) * ff_c_ftsv_shift_factor_selected_power) + (ff_p_ftsv_shift_factor_selected_power_product))) /\ ((((exists ff_h_ftsv_shift_factor_selected_power_product_partial. ff_h_ftsv_shift_factor_selected_power_product_partial + S (ff_r_ftsv_shift_factor_selected_power_product) = S ((S (ff_i_ftsv_shift_factor_selected_power_product)) * ff_v_ftsv_shift_factor_selected_power_product)) /\ exists ff_q_ftsv_shift_factor_selected_power_product_partial. ff_u_ftsv_shift_factor_selected_power_product = ff_q_ftsv_shift_factor_selected_power_product_partial * S ((S (ff_i_ftsv_shift_factor_selected_power_product)) * ff_v_ftsv_shift_factor_selected_power_product) + (ff_r_ftsv_shift_factor_selected_power_product))) /\ ((((exists ff_h_ftsv_shift_factor_selected_power_product_successor. ff_h_ftsv_shift_factor_selected_power_product_successor + S (ff_s_ftsv_shift_factor_selected_power_product) = S ((S (S ff_i_ftsv_shift_factor_selected_power_product)) * ff_v_ftsv_shift_factor_selected_power_product)) /\ exists ff_q_ftsv_shift_factor_selected_power_product_successor. ff_u_ftsv_shift_factor_selected_power_product = ff_q_ftsv_shift_factor_selected_power_product_successor * S ((S (S ff_i_ftsv_shift_factor_selected_power_product)) * ff_v_ftsv_shift_factor_selected_power_product) + (ff_s_ftsv_shift_factor_selected_power_product))) /\ ff_s_ftsv_shift_factor_selected_power_product = ff_r_ftsv_shift_factor_selected_power_product * ff_p_ftsv_shift_factor_selected_power_product)))))))) /\ (exists bpv_factor_ftsv_shift_factor_selected_divides. z = bpv_result_ftsv_shift_factor_selected * bpv_factor_ftsv_shift_factor_selected_divides)))) /\ forall bpv_candidate_ftsv_shift_factor. (exists bpv_gap_ftsv_shift_factor_candidate_bound. bpv_gap_ftsv_shift_factor_candidate_bound + bpv_candidate_ftsv_shift_factor = z) -> (exists bpv_result_ftsv_shift_factor_candidate. ((exists ff_b_ftsv_shift_factor_candidate_power ff_c_ftsv_shift_factor_candidate_power. ((forall ff_i_ftsv_shift_factor_candidate_power_repeat. (exists ff_lt_ftsv_shift_factor_candidate_power_repeat_bound. ff_lt_ftsv_shift_factor_candidate_power_repeat_bound + S ff_i_ftsv_shift_factor_candidate_power_repeat = bpv_candidate_ftsv_shift_factor) -> (((exists ff_h_ftsv_shift_factor_candidate_power_repeat_decoded. ff_h_ftsv_shift_factor_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_shift_factor_candidate_power_repeat)) * ff_c_ftsv_shift_factor_candidate_power)) /\ exists ff_q_ftsv_shift_factor_candidate_power_repeat_decoded. ff_b_ftsv_shift_factor_candidate_power = ff_q_ftsv_shift_factor_candidate_power_repeat_decoded * S ((S (ff_i_ftsv_shift_factor_candidate_power_repeat)) * ff_c_ftsv_shift_factor_candidate_power) + (p)))) /\ (exists ff_u_ftsv_shift_factor_candidate_power_product ff_v_ftsv_shift_factor_candidate_power_product. ((((exists ff_h_ftsv_shift_factor_candidate_power_product_start. ff_h_ftsv_shift_factor_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_shift_factor_candidate_power_product)) /\ exists ff_q_ftsv_shift_factor_candidate_power_product_start. ff_u_ftsv_shift_factor_candidate_power_product = ff_q_ftsv_shift_factor_candidate_power_product_start * S ((S (0)) * ff_v_ftsv_shift_factor_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsv_shift_factor_candidate_power_product_terminal. ff_h_ftsv_shift_factor_candidate_power_product_terminal + S (bpv_result_ftsv_shift_factor_candidate) = S ((S (bpv_candidate_ftsv_shift_factor)) * ff_v_ftsv_shift_factor_candidate_power_product)) /\ exists ff_q_ftsv_shift_factor_candidate_power_product_terminal. ff_u_ftsv_shift_factor_candidate_power_product = ff_q_ftsv_shift_factor_candidate_power_product_terminal * S ((S (bpv_candidate_ftsv_shift_factor)) * ff_v_ftsv_shift_factor_candidate_power_product) + (bpv_result_ftsv_shift_factor_candidate))) /\ forall ff_i_ftsv_shift_factor_candidate_power_product. (exists ff_lt_ftsv_shift_factor_candidate_power_product_bound. ff_lt_ftsv_shift_factor_candidate_power_product_bound + S ff_i_ftsv_shift_factor_candidate_power_product = bpv_candidate_ftsv_shift_factor) -> exists ff_p_ftsv_shift_factor_candidate_power_product ff_r_ftsv_shift_factor_candidate_power_product ff_s_ftsv_shift_factor_candidate_power_product. ((((exists ff_h_ftsv_shift_factor_candidate_power_product_factor. ff_h_ftsv_shift_factor_candidate_power_product_factor + S (ff_p_ftsv_shift_factor_candidate_power_product) = S ((S (ff_i_ftsv_shift_factor_candidate_power_product)) * ff_c_ftsv_shift_factor_candidate_power)) /\ exists ff_q_ftsv_shift_factor_candidate_power_product_factor. ff_b_ftsv_shift_factor_candidate_power = ff_q_ftsv_shift_factor_candidate_power_product_factor * S ((S (ff_i_ftsv_shift_factor_candidate_power_product)) * ff_c_ftsv_shift_factor_candidate_power) + (ff_p_ftsv_shift_factor_candidate_power_product))) /\ ((((exists ff_h_ftsv_shift_factor_candidate_power_product_partial. ff_h_ftsv_shift_factor_candidate_power_product_partial + S (ff_r_ftsv_shift_factor_candidate_power_product) = S ((S (ff_i_ftsv_shift_factor_candidate_power_product)) * ff_v_ftsv_shift_factor_candidate_power_product)) /\ exists ff_q_ftsv_shift_factor_candidate_power_product_partial. ff_u_ftsv_shift_factor_candidate_power_product = ff_q_ftsv_shift_factor_candidate_power_product_partial * S ((S (ff_i_ftsv_shift_factor_candidate_power_product)) * ff_v_ftsv_shift_factor_candidate_power_product) + (ff_r_ftsv_shift_factor_candidate_power_product))) /\ ((((exists ff_h_ftsv_shift_factor_candidate_power_product_successor. ff_h_ftsv_shift_factor_candidate_power_product_successor + S (ff_s_ftsv_shift_factor_candidate_power_product) = S ((S (S ff_i_ftsv_shift_factor_candidate_power_product)) * ff_v_ftsv_shift_factor_candidate_power_product)) /\ exists ff_q_ftsv_shift_factor_candidate_power_product_successor. ff_u_ftsv_shift_factor_candidate_power_product = ff_q_ftsv_shift_factor_candidate_power_product_successor * S ((S (S ff_i_ftsv_shift_factor_candidate_power_product)) * ff_v_ftsv_shift_factor_candidate_power_product) + (ff_s_ftsv_shift_factor_candidate_power_product))) /\ ff_s_ftsv_shift_factor_candidate_power_product = ff_r_ftsv_shift_factor_candidate_power_product * ff_p_ftsv_shift_factor_candidate_power_product)))))))) /\ (exists bpv_factor_ftsv_shift_factor_candidate_divides. z = bpv_result_ftsv_shift_factor_candidate * bpv_factor_ftsv_shift_factor_candidate_divides))) -> (exists bpv_gap_ftsv_shift_factor_maximal. bpv_gap_ftsv_shift_factor_maximal + bpv_candidate_ftsv_shift_factor = e)) -> (((exists bpv_gap_ftsv_shift_value_exponent_bound. bpv_gap_ftsv_shift_value_exponent_bound + f = n) /\ (exists bpv_result_ftsv_shift_value_selected. ((exists ff_b_ftsv_shift_value_selected_power ff_c_ftsv_shift_value_selected_power. ((forall ff_i_ftsv_shift_value_selected_power_repeat. (exists ff_lt_ftsv_shift_value_selected_power_repeat_bound. ff_lt_ftsv_shift_value_selected_power_repeat_bound + S ff_i_ftsv_shift_value_selected_power_repeat = f) -> (((exists ff_h_ftsv_shift_value_selected_power_repeat_decoded. ff_h_ftsv_shift_value_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_shift_value_selected_power_repeat)) * ff_c_ftsv_shift_value_selected_power)) /\ exists ff_q_ftsv_shift_value_selected_power_repeat_decoded. ff_b_ftsv_shift_value_selected_power = ff_q_ftsv_shift_value_selected_power_repeat_decoded * S ((S (ff_i_ftsv_shift_value_selected_power_repeat)) * ff_c_ftsv_shift_value_selected_power) + (p)))) /\ (exists ff_u_ftsv_shift_value_selected_power_product ff_v_ftsv_shift_value_selected_power_product. ((((exists ff_h_ftsv_shift_value_selected_power_product_start. ff_h_ftsv_shift_value_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_shift_value_selected_power_product)) /\ exists ff_q_ftsv_shift_value_selected_power_product_start. ff_u_ftsv_shift_value_selected_power_product = ff_q_ftsv_shift_value_selected_power_product_start * S ((S (0)) * ff_v_ftsv_shift_value_selected_power_product) + (1))) /\ ((((exists ff_h_ftsv_shift_value_selected_power_product_terminal. ff_h_ftsv_shift_value_selected_power_product_terminal + S (bpv_result_ftsv_shift_value_selected) = S ((S (f)) * ff_v_ftsv_shift_value_selected_power_product)) /\ exists ff_q_ftsv_shift_value_selected_power_product_terminal. ff_u_ftsv_shift_value_selected_power_product = ff_q_ftsv_shift_value_selected_power_product_terminal * S ((S (f)) * ff_v_ftsv_shift_value_selected_power_product) + (bpv_result_ftsv_shift_value_selected))) /\ forall ff_i_ftsv_shift_value_selected_power_product. (exists ff_lt_ftsv_shift_value_selected_power_product_bound. ff_lt_ftsv_shift_value_selected_power_product_bound + S ff_i_ftsv_shift_value_selected_power_product = f) -> exists ff_p_ftsv_shift_value_selected_power_product ff_r_ftsv_shift_value_selected_power_product ff_s_ftsv_shift_value_selected_power_product. ((((exists ff_h_ftsv_shift_value_selected_power_product_factor. ff_h_ftsv_shift_value_selected_power_product_factor + S (ff_p_ftsv_shift_value_selected_power_product) = S ((S (ff_i_ftsv_shift_value_selected_power_product)) * ff_c_ftsv_shift_value_selected_power)) /\ exists ff_q_ftsv_shift_value_selected_power_product_factor. ff_b_ftsv_shift_value_selected_power = ff_q_ftsv_shift_value_selected_power_product_factor * S ((S (ff_i_ftsv_shift_value_selected_power_product)) * ff_c_ftsv_shift_value_selected_power) + (ff_p_ftsv_shift_value_selected_power_product))) /\ ((((exists ff_h_ftsv_shift_value_selected_power_product_partial. ff_h_ftsv_shift_value_selected_power_product_partial + S (ff_r_ftsv_shift_value_selected_power_product) = S ((S (ff_i_ftsv_shift_value_selected_power_product)) * ff_v_ftsv_shift_value_selected_power_product)) /\ exists ff_q_ftsv_shift_value_selected_power_product_partial. ff_u_ftsv_shift_value_selected_power_product = ff_q_ftsv_shift_value_selected_power_product_partial * S ((S (ff_i_ftsv_shift_value_selected_power_product)) * ff_v_ftsv_shift_value_selected_power_product) + (ff_r_ftsv_shift_value_selected_power_product))) /\ ((((exists ff_h_ftsv_shift_value_selected_power_product_successor. ff_h_ftsv_shift_value_selected_power_product_successor + S (ff_s_ftsv_shift_value_selected_power_product) = S ((S (S ff_i_ftsv_shift_value_selected_power_product)) * ff_v_ftsv_shift_value_selected_power_product)) /\ exists ff_q_ftsv_shift_value_selected_power_product_successor. ff_u_ftsv_shift_value_selected_power_product = ff_q_ftsv_shift_value_selected_power_product_successor * S ((S (S ff_i_ftsv_shift_value_selected_power_product)) * ff_v_ftsv_shift_value_selected_power_product) + (ff_s_ftsv_shift_value_selected_power_product))) /\ ff_s_ftsv_shift_value_selected_power_product = ff_r_ftsv_shift_value_selected_power_product * ff_p_ftsv_shift_value_selected_power_product)))))))) /\ (exists bpv_factor_ftsv_shift_value_selected_divides. n = bpv_result_ftsv_shift_value_selected * bpv_factor_ftsv_shift_value_selected_divides)))) /\ forall bpv_candidate_ftsv_shift_value. (exists bpv_gap_ftsv_shift_value_candidate_bound. bpv_gap_ftsv_shift_value_candidate_bound + bpv_candidate_ftsv_shift_value = n) -> (exists bpv_result_ftsv_shift_value_candidate. ((exists ff_b_ftsv_shift_value_candidate_power ff_c_ftsv_shift_value_candidate_power. ((forall ff_i_ftsv_shift_value_candidate_power_repeat. (exists ff_lt_ftsv_shift_value_candidate_power_repeat_bound. ff_lt_ftsv_shift_value_candidate_power_repeat_bound + S ff_i_ftsv_shift_value_candidate_power_repeat = bpv_candidate_ftsv_shift_value) -> (((exists ff_h_ftsv_shift_value_candidate_power_repeat_decoded. ff_h_ftsv_shift_value_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_shift_value_candidate_power_repeat)) * ff_c_ftsv_shift_value_candidate_power)) /\ exists ff_q_ftsv_shift_value_candidate_power_repeat_decoded. ff_b_ftsv_shift_value_candidate_power = ff_q_ftsv_shift_value_candidate_power_repeat_decoded * S ((S (ff_i_ftsv_shift_value_candidate_power_repeat)) * ff_c_ftsv_shift_value_candidate_power) + (p)))) /\ (exists ff_u_ftsv_shift_value_candidate_power_product ff_v_ftsv_shift_value_candidate_power_product. ((((exists ff_h_ftsv_shift_value_candidate_power_product_start. ff_h_ftsv_shift_value_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_shift_value_candidate_power_product)) /\ exists ff_q_ftsv_shift_value_candidate_power_product_start. ff_u_ftsv_shift_value_candidate_power_product = ff_q_ftsv_shift_value_candidate_power_product_start * S ((S (0)) * ff_v_ftsv_shift_value_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsv_shift_value_candidate_power_product_terminal. ff_h_ftsv_shift_value_candidate_power_product_terminal + S (bpv_result_ftsv_shift_value_candidate) = S ((S (bpv_candidate_ftsv_shift_value)) * ff_v_ftsv_shift_value_candidate_power_product)) /\ exists ff_q_ftsv_shift_value_candidate_power_product_terminal. ff_u_ftsv_shift_value_candidate_power_product = ff_q_ftsv_shift_value_candidate_power_product_terminal * S ((S (bpv_candidate_ftsv_shift_value)) * ff_v_ftsv_shift_value_candidate_power_product) + (bpv_result_ftsv_shift_value_candidate))) /\ forall ff_i_ftsv_shift_value_candidate_power_product. (exists ff_lt_ftsv_shift_value_candidate_power_product_bound. ff_lt_ftsv_shift_value_candidate_power_product_bound + S ff_i_ftsv_shift_value_candidate_power_product = bpv_candidate_ftsv_shift_value) -> exists ff_p_ftsv_shift_value_candidate_power_product ff_r_ftsv_shift_value_candidate_power_product ff_s_ftsv_shift_value_candidate_power_product. ((((exists ff_h_ftsv_shift_value_candidate_power_product_factor. ff_h_ftsv_shift_value_candidate_power_product_factor + S (ff_p_ftsv_shift_value_candidate_power_product) = S ((S (ff_i_ftsv_shift_value_candidate_power_product)) * ff_c_ftsv_shift_value_candidate_power)) /\ exists ff_q_ftsv_shift_value_candidate_power_product_factor. ff_b_ftsv_shift_value_candidate_power = ff_q_ftsv_shift_value_candidate_power_product_factor * S ((S (ff_i_ftsv_shift_value_candidate_power_product)) * ff_c_ftsv_shift_value_candidate_power) + (ff_p_ftsv_shift_value_candidate_power_product))) /\ ((((exists ff_h_ftsv_shift_value_candidate_power_product_partial. ff_h_ftsv_shift_value_candidate_power_product_partial + S (ff_r_ftsv_shift_value_candidate_power_product) = S ((S (ff_i_ftsv_shift_value_candidate_power_product)) * ff_v_ftsv_shift_value_candidate_power_product)) /\ exists ff_q_ftsv_shift_value_candidate_power_product_partial. ff_u_ftsv_shift_value_candidate_power_product = ff_q_ftsv_shift_value_candidate_power_product_partial * S ((S (ff_i_ftsv_shift_value_candidate_power_product)) * ff_v_ftsv_shift_value_candidate_power_product) + (ff_r_ftsv_shift_value_candidate_power_product))) /\ ((((exists ff_h_ftsv_shift_value_candidate_power_product_successor. ff_h_ftsv_shift_value_candidate_power_product_successor + S (ff_s_ftsv_shift_value_candidate_power_product) = S ((S (S ff_i_ftsv_shift_value_candidate_power_product)) * ff_v_ftsv_shift_value_candidate_power_product)) /\ exists ff_q_ftsv_shift_value_candidate_power_product_successor. ff_u_ftsv_shift_value_candidate_power_product = ff_q_ftsv_shift_value_candidate_power_product_successor * S ((S (S ff_i_ftsv_shift_value_candidate_power_product)) * ff_v_ftsv_shift_value_candidate_power_product) + (ff_s_ftsv_shift_value_candidate_power_product))) /\ ff_s_ftsv_shift_value_candidate_power_product = ff_r_ftsv_shift_value_candidate_power_product * ff_p_ftsv_shift_value_candidate_power_product)))))))) /\ (exists bpv_factor_ftsv_shift_value_candidate_divides. n = bpv_result_ftsv_shift_value_candidate * bpv_factor_ftsv_shift_value_candidate_divides))) -> (exists bpv_gap_ftsv_shift_value_maximal. bpv_gap_ftsv_shift_value_maximal + bpv_candidate_ftsv_shift_value = f)) -> (((exists bpv_gap_ftsv_shift_product_exponent_bound. bpv_gap_ftsv_shift_product_exponent_bound + g = ((z * z) * n)) /\ (exists bpv_result_ftsv_shift_product_selected. ((exists ff_b_ftsv_shift_product_selected_power ff_c_ftsv_shift_product_selected_power. ((forall ff_i_ftsv_shift_product_selected_power_repeat. (exists ff_lt_ftsv_shift_product_selected_power_repeat_bound. ff_lt_ftsv_shift_product_selected_power_repeat_bound + S ff_i_ftsv_shift_product_selected_power_repeat = g) -> (((exists ff_h_ftsv_shift_product_selected_power_repeat_decoded. ff_h_ftsv_shift_product_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_shift_product_selected_power_repeat)) * ff_c_ftsv_shift_product_selected_power)) /\ exists ff_q_ftsv_shift_product_selected_power_repeat_decoded. ff_b_ftsv_shift_product_selected_power = ff_q_ftsv_shift_product_selected_power_repeat_decoded * S ((S (ff_i_ftsv_shift_product_selected_power_repeat)) * ff_c_ftsv_shift_product_selected_power) + (p)))) /\ (exists ff_u_ftsv_shift_product_selected_power_product ff_v_ftsv_shift_product_selected_power_product. ((((exists ff_h_ftsv_shift_product_selected_power_product_start. ff_h_ftsv_shift_product_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_shift_product_selected_power_product)) /\ exists ff_q_ftsv_shift_product_selected_power_product_start. ff_u_ftsv_shift_product_selected_power_product = ff_q_ftsv_shift_product_selected_power_product_start * S ((S (0)) * ff_v_ftsv_shift_product_selected_power_product) + (1))) /\ ((((exists ff_h_ftsv_shift_product_selected_power_product_terminal. ff_h_ftsv_shift_product_selected_power_product_terminal + S (bpv_result_ftsv_shift_product_selected) = S ((S (g)) * ff_v_ftsv_shift_product_selected_power_product)) /\ exists ff_q_ftsv_shift_product_selected_power_product_terminal. ff_u_ftsv_shift_product_selected_power_product = ff_q_ftsv_shift_product_selected_power_product_terminal * S ((S (g)) * ff_v_ftsv_shift_product_selected_power_product) + (bpv_result_ftsv_shift_product_selected))) /\ forall ff_i_ftsv_shift_product_selected_power_product. (exists ff_lt_ftsv_shift_product_selected_power_product_bound. ff_lt_ftsv_shift_product_selected_power_product_bound + S ff_i_ftsv_shift_product_selected_power_product = g) -> exists ff_p_ftsv_shift_product_selected_power_product ff_r_ftsv_shift_product_selected_power_product ff_s_ftsv_shift_product_selected_power_product. ((((exists ff_h_ftsv_shift_product_selected_power_product_factor. ff_h_ftsv_shift_product_selected_power_product_factor + S (ff_p_ftsv_shift_product_selected_power_product) = S ((S (ff_i_ftsv_shift_product_selected_power_product)) * ff_c_ftsv_shift_product_selected_power)) /\ exists ff_q_ftsv_shift_product_selected_power_product_factor. ff_b_ftsv_shift_product_selected_power = ff_q_ftsv_shift_product_selected_power_product_factor * S ((S (ff_i_ftsv_shift_product_selected_power_product)) * ff_c_ftsv_shift_product_selected_power) + (ff_p_ftsv_shift_product_selected_power_product))) /\ ((((exists ff_h_ftsv_shift_product_selected_power_product_partial. ff_h_ftsv_shift_product_selected_power_product_partial + S (ff_r_ftsv_shift_product_selected_power_product) = S ((S (ff_i_ftsv_shift_product_selected_power_product)) * ff_v_ftsv_shift_product_selected_power_product)) /\ exists ff_q_ftsv_shift_product_selected_power_product_partial. ff_u_ftsv_shift_product_selected_power_product = ff_q_ftsv_shift_product_selected_power_product_partial * S ((S (ff_i_ftsv_shift_product_selected_power_product)) * ff_v_ftsv_shift_product_selected_power_product) + (ff_r_ftsv_shift_product_selected_power_product))) /\ ((((exists ff_h_ftsv_shift_product_selected_power_product_successor. ff_h_ftsv_shift_product_selected_power_product_successor + S (ff_s_ftsv_shift_product_selected_power_product) = S ((S (S ff_i_ftsv_shift_product_selected_power_product)) * ff_v_ftsv_shift_product_selected_power_product)) /\ exists ff_q_ftsv_shift_product_selected_power_product_successor. ff_u_ftsv_shift_product_selected_power_product = ff_q_ftsv_shift_product_selected_power_product_successor * S ((S (S ff_i_ftsv_shift_product_selected_power_product)) * ff_v_ftsv_shift_product_selected_power_product) + (ff_s_ftsv_shift_product_selected_power_product))) /\ ff_s_ftsv_shift_product_selected_power_product = ff_r_ftsv_shift_product_selected_power_product * ff_p_ftsv_shift_product_selected_power_product)))))))) /\ (exists bpv_factor_ftsv_shift_product_selected_divides. ((z * z) * n) = bpv_result_ftsv_shift_product_selected * bpv_factor_ftsv_shift_product_selected_divides)))) /\ forall bpv_candidate_ftsv_shift_product. (exists bpv_gap_ftsv_shift_product_candidate_bound. bpv_gap_ftsv_shift_product_candidate_bound + bpv_candidate_ftsv_shift_product = ((z * z) * n)) -> (exists bpv_result_ftsv_shift_product_candidate. ((exists ff_b_ftsv_shift_product_candidate_power ff_c_ftsv_shift_product_candidate_power. ((forall ff_i_ftsv_shift_product_candidate_power_repeat. (exists ff_lt_ftsv_shift_product_candidate_power_repeat_bound. ff_lt_ftsv_shift_product_candidate_power_repeat_bound + S ff_i_ftsv_shift_product_candidate_power_repeat = bpv_candidate_ftsv_shift_product) -> (((exists ff_h_ftsv_shift_product_candidate_power_repeat_decoded. ff_h_ftsv_shift_product_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_shift_product_candidate_power_repeat)) * ff_c_ftsv_shift_product_candidate_power)) /\ exists ff_q_ftsv_shift_product_candidate_power_repeat_decoded. ff_b_ftsv_shift_product_candidate_power = ff_q_ftsv_shift_product_candidate_power_repeat_decoded * S ((S (ff_i_ftsv_shift_product_candidate_power_repeat)) * ff_c_ftsv_shift_product_candidate_power) + (p)))) /\ (exists ff_u_ftsv_shift_product_candidate_power_product ff_v_ftsv_shift_product_candidate_power_product. ((((exists ff_h_ftsv_shift_product_candidate_power_product_start. ff_h_ftsv_shift_product_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_shift_product_candidate_power_product)) /\ exists ff_q_ftsv_shift_product_candidate_power_product_start. ff_u_ftsv_shift_product_candidate_power_product = ff_q_ftsv_shift_product_candidate_power_product_start * S ((S (0)) * ff_v_ftsv_shift_product_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsv_shift_product_candidate_power_product_terminal. ff_h_ftsv_shift_product_candidate_power_product_terminal + S (bpv_result_ftsv_shift_product_candidate) = S ((S (bpv_candidate_ftsv_shift_product)) * ff_v_ftsv_shift_product_candidate_power_product)) /\ exists ff_q_ftsv_shift_product_candidate_power_product_terminal. ff_u_ftsv_shift_product_candidate_power_product = ff_q_ftsv_shift_product_candidate_power_product_terminal * S ((S (bpv_candidate_ftsv_shift_product)) * ff_v_ftsv_shift_product_candidate_power_product) + (bpv_result_ftsv_shift_product_candidate))) /\ forall ff_i_ftsv_shift_product_candidate_power_product. (exists ff_lt_ftsv_shift_product_candidate_power_product_bound. ff_lt_ftsv_shift_product_candidate_power_product_bound + S ff_i_ftsv_shift_product_candidate_power_product = bpv_candidate_ftsv_shift_product) -> exists ff_p_ftsv_shift_product_candidate_power_product ff_r_ftsv_shift_product_candidate_power_product ff_s_ftsv_shift_product_candidate_power_product. ((((exists ff_h_ftsv_shift_product_candidate_power_product_factor. ff_h_ftsv_shift_product_candidate_power_product_factor + S (ff_p_ftsv_shift_product_candidate_power_product) = S ((S (ff_i_ftsv_shift_product_candidate_power_product)) * ff_c_ftsv_shift_product_candidate_power)) /\ exists ff_q_ftsv_shift_product_candidate_power_product_factor. ff_b_ftsv_shift_product_candidate_power = ff_q_ftsv_shift_product_candidate_power_product_factor * S ((S (ff_i_ftsv_shift_product_candidate_power_product)) * ff_c_ftsv_shift_product_candidate_power) + (ff_p_ftsv_shift_product_candidate_power_product))) /\ ((((exists ff_h_ftsv_shift_product_candidate_power_product_partial. ff_h_ftsv_shift_product_candidate_power_product_partial + S (ff_r_ftsv_shift_product_candidate_power_product) = S ((S (ff_i_ftsv_shift_product_candidate_power_product)) * ff_v_ftsv_shift_product_candidate_power_product)) /\ exists ff_q_ftsv_shift_product_candidate_power_product_partial. ff_u_ftsv_shift_product_candidate_power_product = ff_q_ftsv_shift_product_candidate_power_product_partial * S ((S (ff_i_ftsv_shift_product_candidate_power_product)) * ff_v_ftsv_shift_product_candidate_power_product) + (ff_r_ftsv_shift_product_candidate_power_product))) /\ ((((exists ff_h_ftsv_shift_product_candidate_power_product_successor. ff_h_ftsv_shift_product_candidate_power_product_successor + S (ff_s_ftsv_shift_product_candidate_power_product) = S ((S (S ff_i_ftsv_shift_product_candidate_power_product)) * ff_v_ftsv_shift_product_candidate_power_product)) /\ exists ff_q_ftsv_shift_product_candidate_power_product_successor. ff_u_ftsv_shift_product_candidate_power_product = ff_q_ftsv_shift_product_candidate_power_product_successor * S ((S (S ff_i_ftsv_shift_product_candidate_power_product)) * ff_v_ftsv_shift_product_candidate_power_product) + (ff_s_ftsv_shift_product_candidate_power_product))) /\ ff_s_ftsv_shift_product_candidate_power_product = ff_r_ftsv_shift_product_candidate_power_product * ff_p_ftsv_shift_product_candidate_power_product)))))))) /\ (exists bpv_factor_ftsv_shift_product_candidate_divides. ((z * z) * n) = bpv_result_ftsv_shift_product_candidate * bpv_factor_ftsv_shift_product_candidate_divides))) -> (exists bpv_gap_ftsv_shift_product_maximal. bpv_gap_ftsv_shift_product_maximal + bpv_candidate_ftsv_shift_product = g)) -> g = (e + e) + f

Constructive proof overview

Generated structural guide

Multiplying a nonzero value by a nonzero square increases its prime valuation by exactly twice the factor valuation.

The unchanged tactic script uses 4 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

power_valuation_exists Alpha theorem; checked-use authorized TS003I prime_power_valuation_square_even mul_ne_zero Stable theorem; checked-use authorized prime_power_valuation_mul Alpha theorem; checked-use authorized

Direct dependents

TS0036 square_factor_even_valuation_reflects_cofactor TS003Q prime_power_valuation_square_factor_preserves_evenness

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 · 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.

Named ingredients (1)
prime power valuation square even

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

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro z
  3. L3
    intro n
  4. L4
    intro e
  5. L5
    intro f
  6. L6
    intro g
  7. L7
    intro hprime
  8. L8
    intro hfactor_nonzero
  9. L9
    intro hvalue_nonzero
  10. L10
    intro hfactor
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hvalue
  2. L12
    intro hproduct
03Establish hsquareL13–16

Establish this local claim before using it. It is not an additional assumption.

  1. L13
    have hsquare : ∃ E. BoundedPowerValuation(p,z · z,z · z,E)Definitions: BoundedPowerValuation
  2. L14
    specialize power_valuation_exists p
  3. L15
    specialize power_valuation_exists (z * z)
  4. L16
    exact power_valuation_exists
04Separate the logical casesL17–17

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

  1. L17
    cases hsquare
05Establish hdoubledL18–27

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

  1. L18
    have hdoubled : x = e + e
  2. L19
    specialize prime_power_valuation_square_even p
  3. L20
    specialize prime_power_valuation_square_even z
  4. L21
    specialize prime_power_valuation_square_even e
  5. L22
    specialize prime_power_valuation_square_even x
  6. L23
    apply prime_power_valuation_square_even
  7. L24
    exact hprime
  8. L25
    exact hfactor_nonzero
  9. L26
    exact hfactor
  10. L27
    exact hsquare_witness
06Establish hsquare_nonzeroL28–35

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

  1. L28
    have hsquare_nonzero : ~(z * z = 0)
  2. L29
    specialize mul_ne_zero z
  3. L30
    specialize mul_ne_zero z
  4. L31
    intro hsquare_zero
  5. L32
    apply mul_ne_zero
  6. L33
    exact hfactor_nonzero
  7. L34
    exact hfactor_nonzero
  8. L35
    exact hsquare_zero
07Establish hshiftL36–45

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

  1. L36
    have hshift : g = x + f
  2. L37
    specialize prime_power_valuation_mul p
  3. L38
    specialize prime_power_valuation_mul (z * z)
  4. L39
    specialize prime_power_valuation_mul n
  5. L40
    specialize prime_power_valuation_mul x
  6. L41
    specialize prime_power_valuation_mul f
  7. L42
    specialize prime_power_valuation_mul g
  8. L43
    apply prime_power_valuation_mul
  9. L44
    exact hprime
  10. L45
    exact hsquare_nonzero
08Use earlier factsL46–49

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

  1. L46
    exact hvalue_nonzero
  2. L47
    exact hsquare_witness
  3. L48
    exact hvalue
  4. L49
    exact hproduct
09Calculate and transport equalitiesL50–50

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

  1. L50
    rewrite hdoubled at hshift
10Use earlier factsL51–51

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

  1. L51
    exact hshift

Library-wide reading audit

Original exact command ledger · 51 lines
  1. 0001intro p
  2. 0002intro z
  3. 0003intro n
  4. 0004intro e
  5. 0005intro f
  6. 0006intro g
  7. 0007intro hprime
  8. 0008intro hfactor_nonzero
  9. 0009intro hvalue_nonzero
  10. 0010intro hfactor
  11. 0011intro hvalue
  12. 0012intro hproduct
  13. 0013have hsquare : exists E. (((exists bpv_gap_ftsv_shift_square_witness_exponent_bound. bpv_gap_ftsv_shift_square_witness_exponent_bound + E = (z * z)) /\ (exists bpv_result_ftsv_shift_square_witness_selected. ((exists ff_b_ftsv_shift_square_witness_selected_power ff_c_ftsv_shift_square_witness_selected_power. ((forall ff_i_ftsv_shift_square_witness_selected_power_repeat. (exists ff_lt_ftsv_shift_square_witness_selected_power_repeat_bound. ff_lt_ftsv_shift_square_witness_selected_power_repeat_bound + S ff_i_ftsv_shift_square_witness_selected_power_repeat = E) -> (((exists ff_h_ftsv_shift_square_witness_selected_power_repeat_decoded. ff_h_ftsv_shift_square_witness_selected_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_shift_square_witness_selected_power_repeat)) * ff_c_ftsv_shift_square_witness_selected_power)) /\ exists ff_q_ftsv_shift_square_witness_selected_power_repeat_decoded. ff_b_ftsv_shift_square_witness_selected_power = ff_q_ftsv_shift_square_witness_selected_power_repeat_decoded * S ((S (ff_i_ftsv_shift_square_witness_selected_power_repeat)) * ff_c_ftsv_shift_square_witness_selected_power) + (p)))) /\ (exists ff_u_ftsv_shift_square_witness_selected_power_product ff_v_ftsv_shift_square_witness_selected_power_product. ((((exists ff_h_ftsv_shift_square_witness_selected_power_product_start. ff_h_ftsv_shift_square_witness_selected_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_shift_square_witness_selected_power_product)) /\ exists ff_q_ftsv_shift_square_witness_selected_power_product_start. ff_u_ftsv_shift_square_witness_selected_power_product = ff_q_ftsv_shift_square_witness_selected_power_product_start * S ((S (0)) * ff_v_ftsv_shift_square_witness_selected_power_product) + (1))) /\ ((((exists ff_h_ftsv_shift_square_witness_selected_power_product_terminal. ff_h_ftsv_shift_square_witness_selected_power_product_terminal + S (bpv_result_ftsv_shift_square_witness_selected) = S ((S (E)) * ff_v_ftsv_shift_square_witness_selected_power_product)) /\ exists ff_q_ftsv_shift_square_witness_selected_power_product_terminal. ff_u_ftsv_shift_square_witness_selected_power_product = ff_q_ftsv_shift_square_witness_selected_power_product_terminal * S ((S (E)) * ff_v_ftsv_shift_square_witness_selected_power_product) + (bpv_result_ftsv_shift_square_witness_selected))) /\ forall ff_i_ftsv_shift_square_witness_selected_power_product. (exists ff_lt_ftsv_shift_square_witness_selected_power_product_bound. ff_lt_ftsv_shift_square_witness_selected_power_product_bound + S ff_i_ftsv_shift_square_witness_selected_power_product = E) -> exists ff_p_ftsv_shift_square_witness_selected_power_product ff_r_ftsv_shift_square_witness_selected_power_product ff_s_ftsv_shift_square_witness_selected_power_product. ((((exists ff_h_ftsv_shift_square_witness_selected_power_product_factor. ff_h_ftsv_shift_square_witness_selected_power_product_factor + S (ff_p_ftsv_shift_square_witness_selected_power_product) = S ((S (ff_i_ftsv_shift_square_witness_selected_power_product)) * ff_c_ftsv_shift_square_witness_selected_power)) /\ exists ff_q_ftsv_shift_square_witness_selected_power_product_factor. ff_b_ftsv_shift_square_witness_selected_power = ff_q_ftsv_shift_square_witness_selected_power_product_factor * S ((S (ff_i_ftsv_shift_square_witness_selected_power_product)) * ff_c_ftsv_shift_square_witness_selected_power) + (ff_p_ftsv_shift_square_witness_selected_power_product))) /\ ((((exists ff_h_ftsv_shift_square_witness_selected_power_product_partial. ff_h_ftsv_shift_square_witness_selected_power_product_partial + S (ff_r_ftsv_shift_square_witness_selected_power_product) = S ((S (ff_i_ftsv_shift_square_witness_selected_power_product)) * ff_v_ftsv_shift_square_witness_selected_power_product)) /\ exists ff_q_ftsv_shift_square_witness_selected_power_product_partial. ff_u_ftsv_shift_square_witness_selected_power_product = ff_q_ftsv_shift_square_witness_selected_power_product_partial * S ((S (ff_i_ftsv_shift_square_witness_selected_power_product)) * ff_v_ftsv_shift_square_witness_selected_power_product) + (ff_r_ftsv_shift_square_witness_selected_power_product))) /\ ((((exists ff_h_ftsv_shift_square_witness_selected_power_product_successor. ff_h_ftsv_shift_square_witness_selected_power_product_successor + S (ff_s_ftsv_shift_square_witness_selected_power_product) = S ((S (S ff_i_ftsv_shift_square_witness_selected_power_product)) * ff_v_ftsv_shift_square_witness_selected_power_product)) /\ exists ff_q_ftsv_shift_square_witness_selected_power_product_successor. ff_u_ftsv_shift_square_witness_selected_power_product = ff_q_ftsv_shift_square_witness_selected_power_product_successor * S ((S (S ff_i_ftsv_shift_square_witness_selected_power_product)) * ff_v_ftsv_shift_square_witness_selected_power_product) + (ff_s_ftsv_shift_square_witness_selected_power_product))) /\ ff_s_ftsv_shift_square_witness_selected_power_product = ff_r_ftsv_shift_square_witness_selected_power_product * ff_p_ftsv_shift_square_witness_selected_power_product)))))))) /\ (exists bpv_factor_ftsv_shift_square_witness_selected_divides. (z * z) = bpv_result_ftsv_shift_square_witness_selected * bpv_factor_ftsv_shift_square_witness_selected_divides)))) /\ forall bpv_candidate_ftsv_shift_square_witness. (exists bpv_gap_ftsv_shift_square_witness_candidate_bound. bpv_gap_ftsv_shift_square_witness_candidate_bound + bpv_candidate_ftsv_shift_square_witness = (z * z)) -> (exists bpv_result_ftsv_shift_square_witness_candidate. ((exists ff_b_ftsv_shift_square_witness_candidate_power ff_c_ftsv_shift_square_witness_candidate_power. ((forall ff_i_ftsv_shift_square_witness_candidate_power_repeat. (exists ff_lt_ftsv_shift_square_witness_candidate_power_repeat_bound. ff_lt_ftsv_shift_square_witness_candidate_power_repeat_bound + S ff_i_ftsv_shift_square_witness_candidate_power_repeat = bpv_candidate_ftsv_shift_square_witness) -> (((exists ff_h_ftsv_shift_square_witness_candidate_power_repeat_decoded. ff_h_ftsv_shift_square_witness_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_ftsv_shift_square_witness_candidate_power_repeat)) * ff_c_ftsv_shift_square_witness_candidate_power)) /\ exists ff_q_ftsv_shift_square_witness_candidate_power_repeat_decoded. ff_b_ftsv_shift_square_witness_candidate_power = ff_q_ftsv_shift_square_witness_candidate_power_repeat_decoded * S ((S (ff_i_ftsv_shift_square_witness_candidate_power_repeat)) * ff_c_ftsv_shift_square_witness_candidate_power) + (p)))) /\ (exists ff_u_ftsv_shift_square_witness_candidate_power_product ff_v_ftsv_shift_square_witness_candidate_power_product. ((((exists ff_h_ftsv_shift_square_witness_candidate_power_product_start. ff_h_ftsv_shift_square_witness_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_ftsv_shift_square_witness_candidate_power_product)) /\ exists ff_q_ftsv_shift_square_witness_candidate_power_product_start. ff_u_ftsv_shift_square_witness_candidate_power_product = ff_q_ftsv_shift_square_witness_candidate_power_product_start * S ((S (0)) * ff_v_ftsv_shift_square_witness_candidate_power_product) + (1))) /\ ((((exists ff_h_ftsv_shift_square_witness_candidate_power_product_terminal. ff_h_ftsv_shift_square_witness_candidate_power_product_terminal + S (bpv_result_ftsv_shift_square_witness_candidate) = S ((S (bpv_candidate_ftsv_shift_square_witness)) * ff_v_ftsv_shift_square_witness_candidate_power_product)) /\ exists ff_q_ftsv_shift_square_witness_candidate_power_product_terminal. ff_u_ftsv_shift_square_witness_candidate_power_product = ff_q_ftsv_shift_square_witness_candidate_power_product_terminal * S ((S (bpv_candidate_ftsv_shift_square_witness)) * ff_v_ftsv_shift_square_witness_candidate_power_product) + (bpv_result_ftsv_shift_square_witness_candidate))) /\ forall ff_i_ftsv_shift_square_witness_candidate_power_product. (exists ff_lt_ftsv_shift_square_witness_candidate_power_product_bound. ff_lt_ftsv_shift_square_witness_candidate_power_product_bound + S ff_i_ftsv_shift_square_witness_candidate_power_product = bpv_candidate_ftsv_shift_square_witness) -> exists ff_p_ftsv_shift_square_witness_candidate_power_product ff_r_ftsv_shift_square_witness_candidate_power_product ff_s_ftsv_shift_square_witness_candidate_power_product. ((((exists ff_h_ftsv_shift_square_witness_candidate_power_product_factor. ff_h_ftsv_shift_square_witness_candidate_power_product_factor + S (ff_p_ftsv_shift_square_witness_candidate_power_product) = S ((S (ff_i_ftsv_shift_square_witness_candidate_power_product)) * ff_c_ftsv_shift_square_witness_candidate_power)) /\ exists ff_q_ftsv_shift_square_witness_candidate_power_product_factor. ff_b_ftsv_shift_square_witness_candidate_power = ff_q_ftsv_shift_square_witness_candidate_power_product_factor * S ((S (ff_i_ftsv_shift_square_witness_candidate_power_product)) * ff_c_ftsv_shift_square_witness_candidate_power) + (ff_p_ftsv_shift_square_witness_candidate_power_product))) /\ ((((exists ff_h_ftsv_shift_square_witness_candidate_power_product_partial. ff_h_ftsv_shift_square_witness_candidate_power_product_partial + S (ff_r_ftsv_shift_square_witness_candidate_power_product) = S ((S (ff_i_ftsv_shift_square_witness_candidate_power_product)) * ff_v_ftsv_shift_square_witness_candidate_power_product)) /\ exists ff_q_ftsv_shift_square_witness_candidate_power_product_partial. ff_u_ftsv_shift_square_witness_candidate_power_product = ff_q_ftsv_shift_square_witness_candidate_power_product_partial * S ((S (ff_i_ftsv_shift_square_witness_candidate_power_product)) * ff_v_ftsv_shift_square_witness_candidate_power_product) + (ff_r_ftsv_shift_square_witness_candidate_power_product))) /\ ((((exists ff_h_ftsv_shift_square_witness_candidate_power_product_successor. ff_h_ftsv_shift_square_witness_candidate_power_product_successor + S (ff_s_ftsv_shift_square_witness_candidate_power_product) = S ((S (S ff_i_ftsv_shift_square_witness_candidate_power_product)) * ff_v_ftsv_shift_square_witness_candidate_power_product)) /\ exists ff_q_ftsv_shift_square_witness_candidate_power_product_successor. ff_u_ftsv_shift_square_witness_candidate_power_product = ff_q_ftsv_shift_square_witness_candidate_power_product_successor * S ((S (S ff_i_ftsv_shift_square_witness_candidate_power_product)) * ff_v_ftsv_shift_square_witness_candidate_power_product) + (ff_s_ftsv_shift_square_witness_candidate_power_product))) /\ ff_s_ftsv_shift_square_witness_candidate_power_product = ff_r_ftsv_shift_square_witness_candidate_power_product * ff_p_ftsv_shift_square_witness_candidate_power_product)))))))) /\ (exists bpv_factor_ftsv_shift_square_witness_candidate_divides. (z * z) = bpv_result_ftsv_shift_square_witness_candidate * bpv_factor_ftsv_shift_square_witness_candidate_divides))) -> (exists bpv_gap_ftsv_shift_square_witness_maximal. bpv_gap_ftsv_shift_square_witness_maximal + bpv_candidate_ftsv_shift_square_witness = E))
  14. 0014specialize power_valuation_exists p
  15. 0015specialize power_valuation_exists (z * z)
  16. 0016exact power_valuation_exists
  17. 0017cases hsquare
  18. 0018have hdoubled : x = e + e
  19. 0019specialize prime_power_valuation_square_even p
  20. 0020specialize prime_power_valuation_square_even z
  21. 0021specialize prime_power_valuation_square_even e
  22. 0022specialize prime_power_valuation_square_even x
  23. 0023apply prime_power_valuation_square_even
  24. 0024exact hprime
  25. 0025exact hfactor_nonzero
  26. 0026exact hfactor
  27. 0027exact hsquare_witness
  28. 0028have hsquare_nonzero : ~(z * z = 0)
  29. 0029specialize mul_ne_zero z
  30. 0030specialize mul_ne_zero z
  31. 0031intro hsquare_zero
  32. 0032apply mul_ne_zero
  33. 0033exact hfactor_nonzero
  34. 0034exact hfactor_nonzero
  35. 0035exact hsquare_zero
  36. 0036have hshift : g = x + f
  37. 0037specialize prime_power_valuation_mul p
  38. 0038specialize prime_power_valuation_mul (z * z)
  39. 0039specialize prime_power_valuation_mul n
  40. 0040specialize prime_power_valuation_mul x
  41. 0041specialize prime_power_valuation_mul f
  42. 0042specialize prime_power_valuation_mul g
  43. 0043apply prime_power_valuation_mul
  44. 0044exact hprime
  45. 0045exact hsquare_nonzero
  46. 0046exact hvalue_nonzero
  47. 0047exact hsquare_witness
  48. 0048exact hvalue
  49. 0049exact hproduct
  50. 0050rewrite hdoubled at hshift
  51. 0051exact hshift