TS003P · theorem body

prime_power_valuation_square_factor_shift

Alpha v34 checked-use · independently kernel and Lean verified; 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.

Statement with defined notation

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

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

Proof neighborhood

Direct theorem prerequisites

power_valuation_exists · Alpha closed TS003I prime_power_valuation_square_even mul_ne_zero · Stable closed prime_power_valuation_mul · Alpha closed

Direct theorem dependents

TS0036 square_factor_even_valuation_reflects_cofactor TS003Q prime_power_valuation_square_factor_preserves_evenness

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

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.

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 (1)
prime power valuation square even
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. PowerValuation(p,z · z,E)Definitions: PowerValuation(p,z · z,E)Original native command in the exact edition
  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 defined 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 : ∃ E. PowerValuation(p,z · z,E)
    Exact native replay linehave 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