PV0013

prime_valuation_support_bounded_exists

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

Ordinary natural induction on an explicit upper bound constructs the whole distinct-prime support; every recursive cofactor is strictly smaller.

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 B n. ~(n = 0) -> (exists pvs_gap_totality_bound. pvs_gap_totality_bound + S (n) = (B)) -> (exists pb pc eb ec vb vc l. (((~((n) = 0)) /\ (((forall pfp_i_pvs_totality_resultdistinct pfp_j_pvs_totality_resultdistinct pfp_a_pvs_totality_resultdistinct. (exists pfp_gap_pvs_totality_resultdistinctfirst. pfp_gap_pvs_totality_resultdistinctfirst + S (pfp_i_pvs_totality_resultdistinct) = (l)) -> (exists pfp_gap_pvs_totality_resultdistinctsecond. pfp_gap_pvs_totality_resultdistinctsecond + S (pfp_j_pvs_totality_resultdistinct) = (l)) -> (((exists ff_h_pfp_pvs_totality_resultdistinctleft. ff_h_pfp_pvs_totality_resultdistinctleft + S (pfp_a_pvs_totality_resultdistinct) = S ((S (pfp_i_pvs_totality_resultdistinct)) * pc)) /\ exists ff_q_pfp_pvs_totality_resultdistinctleft. pb = ff_q_pfp_pvs_totality_resultdistinctleft * S ((S (pfp_i_pvs_totality_resultdistinct)) * pc) + (pfp_a_pvs_totality_resultdistinct))) -> (((exists ff_h_pfp_pvs_totality_resultdistinctright. ff_h_pfp_pvs_totality_resultdistinctright + S (pfp_a_pvs_totality_resultdistinct) = S ((S (pfp_j_pvs_totality_resultdistinct)) * pc)) /\ exists ff_q_pfp_pvs_totality_resultdistinctright. pb = ff_q_pfp_pvs_totality_resultdistinctright * S ((S (pfp_j_pvs_totality_resultdistinct)) * pc) + (pfp_a_pvs_totality_resultdistinct))) -> pfp_i_pvs_totality_resultdistinct = pfp_j_pvs_totality_resultdistinct) /\ (((forall pvs_index_totality_resultentries. (exists pvs_gap_totality_resultentriesindex. pvs_gap_totality_resultentriesindex + S (pvs_index_totality_resultentries) = (l)) -> exists pvs_prime_totality_resultentries pvs_exponent_totality_resultentries pvs_power_totality_resultentries. (((((exists ff_h_pvs_totality_resultentriesprime. ff_h_pvs_totality_resultentriesprime + S (pvs_prime_totality_resultentries) = S ((S (pvs_index_totality_resultentries)) * pc)) /\ exists ff_q_pvs_totality_resultentriesprime. pb = ff_q_pvs_totality_resultentriesprime * S ((S (pvs_index_totality_resultentries)) * pc) + (pvs_prime_totality_resultentries))) /\ (((((exists ff_h_pvs_totality_resultentriesexponent. ff_h_pvs_totality_resultentriesexponent + S (pvs_exponent_totality_resultentries) = S ((S (pvs_index_totality_resultentries)) * ec)) /\ exists ff_q_pvs_totality_resultentriesexponent. eb = ff_q_pvs_totality_resultentriesexponent * S ((S (pvs_index_totality_resultentries)) * ec) + (pvs_exponent_totality_resultentries))) /\ (((((exists ff_h_pvs_totality_resultentriespower. ff_h_pvs_totality_resultentriespower + S (pvs_power_totality_resultentries) = S ((S (pvs_index_totality_resultentries)) * vc)) /\ exists ff_q_pvs_totality_resultentriespower. vb = ff_q_pvs_totality_resultentriespower * S ((S (pvs_index_totality_resultentries)) * vc) + (pvs_power_totality_resultentries))) /\ (((~((pvs_prime_totality_resultentries) = 1) /\ forall pvs_left_totality_resultentriesdomain pvs_right_totality_resultentriesdomain. (pvs_prime_totality_resultentries) = pvs_left_totality_resultentriesdomain * pvs_right_totality_resultentriesdomain -> pvs_left_totality_resultentriesdomain = 1 \/ pvs_right_totality_resultentriesdomain = 1) /\ (((~(pvs_exponent_totality_resultentries = 0)) /\ (((((exists bpd_gap_pvs_totality_resultentriesvaluation_selected_bound. bpd_gap_pvs_totality_resultentriesvaluation_selected_bound + (pvs_exponent_totality_resultentries) = (n)) /\ (exists bpvi_result_pvs_totality_resultentriesvaluation_selected. ((exists bpvi_b_pvs_totality_resultentriesvaluation_selected_power bpvi_c_pvs_totality_resultentriesvaluation_selected_power. ((forall bpvi_i_pvs_totality_resultentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_totality_resultentriesvaluation_selected_power. bpvi_repeat_gap_pvs_totality_resultentriesvaluation_selected_power + S bpvi_i_pvs_totality_resultentriesvaluation_selected_power = pvs_exponent_totality_resultentries) -> (((exists bpvi_h_pvs_totality_resultentriesvaluation_selected_power_repeat. bpvi_h_pvs_totality_resultentriesvaluation_selected_power_repeat + S (pvs_prime_totality_resultentries) = S ((S (bpvi_i_pvs_totality_resultentriesvaluation_selected_power)) * bpvi_c_pvs_totality_resultentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_selected_power_repeat. bpvi_b_pvs_totality_resultentriesvaluation_selected_power = bpvi_q_pvs_totality_resultentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_totality_resultentriesvaluation_selected_power)) * bpvi_c_pvs_totality_resultentriesvaluation_selected_power) + (pvs_prime_totality_resultentries)))) /\ (exists bpvi_u_pvs_totality_resultentriesvaluation_selected_power bpvi_v_pvs_totality_resultentriesvaluation_selected_power. ((((exists bpvi_h_pvs_totality_resultentriesvaluation_selected_power_start. bpvi_h_pvs_totality_resultentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_totality_resultentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_selected_power_start. bpvi_u_pvs_totality_resultentriesvaluation_selected_power = bpvi_q_pvs_totality_resultentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_totality_resultentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_totality_resultentriesvaluation_selected_power_terminal. bpvi_h_pvs_totality_resultentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_totality_resultentriesvaluation_selected) = S ((S (pvs_exponent_totality_resultentries)) * bpvi_v_pvs_totality_resultentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_selected_power_terminal. bpvi_u_pvs_totality_resultentriesvaluation_selected_power = bpvi_q_pvs_totality_resultentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_totality_resultentries)) * bpvi_v_pvs_totality_resultentriesvaluation_selected_power) + (bpvi_result_pvs_totality_resultentriesvaluation_selected))) /\ forall bpvi_j_pvs_totality_resultentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_totality_resultentriesvaluation_selected_power. bpvi_product_gap_pvs_totality_resultentriesvaluation_selected_power + S bpvi_j_pvs_totality_resultentriesvaluation_selected_power = pvs_exponent_totality_resultentries) -> exists bpvi_factor_pvs_totality_resultentriesvaluation_selected_power bpvi_partial_pvs_totality_resultentriesvaluation_selected_power bpvi_successor_pvs_totality_resultentriesvaluation_selected_power. ((((exists bpvi_h_pvs_totality_resultentriesvaluation_selected_power_factor. bpvi_h_pvs_totality_resultentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_totality_resultentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_totality_resultentriesvaluation_selected_power)) * bpvi_c_pvs_totality_resultentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_selected_power_factor. bpvi_b_pvs_totality_resultentriesvaluation_selected_power = bpvi_q_pvs_totality_resultentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_totality_resultentriesvaluation_selected_power)) * bpvi_c_pvs_totality_resultentriesvaluation_selected_power) + (bpvi_factor_pvs_totality_resultentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_totality_resultentriesvaluation_selected_power_partial. bpvi_h_pvs_totality_resultentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_totality_resultentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_totality_resultentriesvaluation_selected_power)) * bpvi_v_pvs_totality_resultentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_selected_power_partial. bpvi_u_pvs_totality_resultentriesvaluation_selected_power = bpvi_q_pvs_totality_resultentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_totality_resultentriesvaluation_selected_power)) * bpvi_v_pvs_totality_resultentriesvaluation_selected_power) + (bpvi_partial_pvs_totality_resultentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_totality_resultentriesvaluation_selected_power_successor. bpvi_h_pvs_totality_resultentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_totality_resultentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_totality_resultentriesvaluation_selected_power)) * bpvi_v_pvs_totality_resultentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_selected_power_successor. bpvi_u_pvs_totality_resultentriesvaluation_selected_power = bpvi_q_pvs_totality_resultentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_totality_resultentriesvaluation_selected_power)) * bpvi_v_pvs_totality_resultentriesvaluation_selected_power) + (bpvi_successor_pvs_totality_resultentriesvaluation_selected_power))) /\ bpvi_successor_pvs_totality_resultentriesvaluation_selected_power = bpvi_partial_pvs_totality_resultentriesvaluation_selected_power * bpvi_factor_pvs_totality_resultentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_totality_resultentriesvaluation_selected. n = bpvi_result_pvs_totality_resultentriesvaluation_selected * bpvi_divisor_factor_pvs_totality_resultentriesvaluation_selected))) /\ forall bpd_candidate_pvs_totality_resultentriesvaluation. (exists bpd_gap_pvs_totality_resultentriesvaluation_candidate_bound. bpd_gap_pvs_totality_resultentriesvaluation_candidate_bound + (bpd_candidate_pvs_totality_resultentriesvaluation) = (n)) -> (exists bpvi_result_pvs_totality_resultentriesvaluation_candidate. ((exists bpvi_b_pvs_totality_resultentriesvaluation_candidate_power bpvi_c_pvs_totality_resultentriesvaluation_candidate_power. ((forall bpvi_i_pvs_totality_resultentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_totality_resultentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_totality_resultentriesvaluation_candidate_power + S bpvi_i_pvs_totality_resultentriesvaluation_candidate_power = bpd_candidate_pvs_totality_resultentriesvaluation) -> (((exists bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_repeat. bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_repeat + S (pvs_prime_totality_resultentries) = S ((S (bpvi_i_pvs_totality_resultentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_resultentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_repeat. bpvi_b_pvs_totality_resultentriesvaluation_candidate_power = bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_totality_resultentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_resultentriesvaluation_candidate_power) + (pvs_prime_totality_resultentries)))) /\ (exists bpvi_u_pvs_totality_resultentriesvaluation_candidate_power bpvi_v_pvs_totality_resultentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_start. bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_totality_resultentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_start. bpvi_u_pvs_totality_resultentriesvaluation_candidate_power = bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_totality_resultentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_terminal. bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_totality_resultentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_totality_resultentriesvaluation)) * bpvi_v_pvs_totality_resultentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_terminal. bpvi_u_pvs_totality_resultentriesvaluation_candidate_power = bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_totality_resultentriesvaluation)) * bpvi_v_pvs_totality_resultentriesvaluation_candidate_power) + (bpvi_result_pvs_totality_resultentriesvaluation_candidate))) /\ forall bpvi_j_pvs_totality_resultentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_totality_resultentriesvaluation_candidate_power. bpvi_product_gap_pvs_totality_resultentriesvaluation_candidate_power + S bpvi_j_pvs_totality_resultentriesvaluation_candidate_power = bpd_candidate_pvs_totality_resultentriesvaluation) -> exists bpvi_factor_pvs_totality_resultentriesvaluation_candidate_power bpvi_partial_pvs_totality_resultentriesvaluation_candidate_power bpvi_successor_pvs_totality_resultentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_factor. bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_totality_resultentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_totality_resultentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_resultentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_factor. bpvi_b_pvs_totality_resultentriesvaluation_candidate_power = bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_totality_resultentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_resultentriesvaluation_candidate_power) + (bpvi_factor_pvs_totality_resultentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_partial. bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_totality_resultentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_totality_resultentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_resultentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_partial. bpvi_u_pvs_totality_resultentriesvaluation_candidate_power = bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_totality_resultentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_resultentriesvaluation_candidate_power) + (bpvi_partial_pvs_totality_resultentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_successor. bpvi_h_pvs_totality_resultentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_totality_resultentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_totality_resultentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_resultentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_successor. bpvi_u_pvs_totality_resultentriesvaluation_candidate_power = bpvi_q_pvs_totality_resultentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_totality_resultentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_resultentriesvaluation_candidate_power) + (bpvi_successor_pvs_totality_resultentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_totality_resultentriesvaluation_candidate_power = bpvi_partial_pvs_totality_resultentriesvaluation_candidate_power * bpvi_factor_pvs_totality_resultentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_totality_resultentriesvaluation_candidate. n = bpvi_result_pvs_totality_resultentriesvaluation_candidate * bpvi_divisor_factor_pvs_totality_resultentriesvaluation_candidate)) -> (exists bpd_gap_pvs_totality_resultentriesvaluation_maximal. bpd_gap_pvs_totality_resultentriesvaluation_maximal + (bpd_candidate_pvs_totality_resultentriesvaluation) = (pvs_exponent_totality_resultentries))) /\ (exists pa_b_pvs_totality_resultentriesvalue pa_c_pvs_totality_resultentriesvalue. ((forall pa_i_pvs_totality_resultentriesvalue_repeat. (exists pa_lt_pvs_totality_resultentriesvalue_repeat_bound. pa_lt_pvs_totality_resultentriesvalue_repeat_bound + S pa_i_pvs_totality_resultentriesvalue_repeat = pvs_exponent_totality_resultentries) -> (((exists pa_h_pvs_totality_resultentriesvalue_repeat_decoded. pa_h_pvs_totality_resultentriesvalue_repeat_decoded + S (pvs_prime_totality_resultentries) = S ((S (pa_i_pvs_totality_resultentriesvalue_repeat)) * pa_c_pvs_totality_resultentriesvalue)) /\ exists pa_q_pvs_totality_resultentriesvalue_repeat_decoded. pa_b_pvs_totality_resultentriesvalue = pa_q_pvs_totality_resultentriesvalue_repeat_decoded * S ((S (pa_i_pvs_totality_resultentriesvalue_repeat)) * pa_c_pvs_totality_resultentriesvalue) + (pvs_prime_totality_resultentries)))) /\ (exists pa_u_pvs_totality_resultentriesvalue_product pa_v_pvs_totality_resultentriesvalue_product. ((((exists pa_h_pvs_totality_resultentriesvalue_product_start. pa_h_pvs_totality_resultentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_totality_resultentriesvalue_product)) /\ exists pa_q_pvs_totality_resultentriesvalue_product_start. pa_u_pvs_totality_resultentriesvalue_product = pa_q_pvs_totality_resultentriesvalue_product_start * S ((S (0)) * pa_v_pvs_totality_resultentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_totality_resultentriesvalue_product_terminal. pa_h_pvs_totality_resultentriesvalue_product_terminal + S (pvs_power_totality_resultentries) = S ((S (pvs_exponent_totality_resultentries)) * pa_v_pvs_totality_resultentriesvalue_product)) /\ exists pa_q_pvs_totality_resultentriesvalue_product_terminal. pa_u_pvs_totality_resultentriesvalue_product = pa_q_pvs_totality_resultentriesvalue_product_terminal * S ((S (pvs_exponent_totality_resultentries)) * pa_v_pvs_totality_resultentriesvalue_product) + (pvs_power_totality_resultentries))) /\ forall pa_i_pvs_totality_resultentriesvalue_product. (exists pa_lt_pvs_totality_resultentriesvalue_product_bound. pa_lt_pvs_totality_resultentriesvalue_product_bound + S pa_i_pvs_totality_resultentriesvalue_product = pvs_exponent_totality_resultentries) -> exists pa_p_pvs_totality_resultentriesvalue_product pa_r_pvs_totality_resultentriesvalue_product pa_s_pvs_totality_resultentriesvalue_product. ((((exists pa_h_pvs_totality_resultentriesvalue_product_factor. pa_h_pvs_totality_resultentriesvalue_product_factor + S (pa_p_pvs_totality_resultentriesvalue_product) = S ((S (pa_i_pvs_totality_resultentriesvalue_product)) * pa_c_pvs_totality_resultentriesvalue)) /\ exists pa_q_pvs_totality_resultentriesvalue_product_factor. pa_b_pvs_totality_resultentriesvalue = pa_q_pvs_totality_resultentriesvalue_product_factor * S ((S (pa_i_pvs_totality_resultentriesvalue_product)) * pa_c_pvs_totality_resultentriesvalue) + (pa_p_pvs_totality_resultentriesvalue_product))) /\ ((((exists pa_h_pvs_totality_resultentriesvalue_product_partial. pa_h_pvs_totality_resultentriesvalue_product_partial + S (pa_r_pvs_totality_resultentriesvalue_product) = S ((S (pa_i_pvs_totality_resultentriesvalue_product)) * pa_v_pvs_totality_resultentriesvalue_product)) /\ exists pa_q_pvs_totality_resultentriesvalue_product_partial. pa_u_pvs_totality_resultentriesvalue_product = pa_q_pvs_totality_resultentriesvalue_product_partial * S ((S (pa_i_pvs_totality_resultentriesvalue_product)) * pa_v_pvs_totality_resultentriesvalue_product) + (pa_r_pvs_totality_resultentriesvalue_product))) /\ ((((exists pa_h_pvs_totality_resultentriesvalue_product_successor. pa_h_pvs_totality_resultentriesvalue_product_successor + S (pa_s_pvs_totality_resultentriesvalue_product) = S ((S (S pa_i_pvs_totality_resultentriesvalue_product)) * pa_v_pvs_totality_resultentriesvalue_product)) /\ exists pa_q_pvs_totality_resultentriesvalue_product_successor. pa_u_pvs_totality_resultentriesvalue_product = pa_q_pvs_totality_resultentriesvalue_product_successor * S ((S (S pa_i_pvs_totality_resultentriesvalue_product)) * pa_v_pvs_totality_resultentriesvalue_product) + (pa_s_pvs_totality_resultentriesvalue_product))) /\ pa_s_pvs_totality_resultentriesvalue_product = pa_r_pvs_totality_resultentriesvalue_product * pa_p_pvs_totality_resultentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_totality_resultcover. (~((pvs_divisor_totality_resultcover) = 1) /\ forall pvs_left_totality_resultcoverprime pvs_right_totality_resultcoverprime. (pvs_divisor_totality_resultcover) = pvs_left_totality_resultcoverprime * pvs_right_totality_resultcoverprime -> pvs_left_totality_resultcoverprime = 1 \/ pvs_right_totality_resultcoverprime = 1) -> (exists pvs_factor_totality_resultcoverdivides. (n) = (pvs_divisor_totality_resultcover) * pvs_factor_totality_resultcoverdivides) -> exists pvs_position_totality_resultcover. (exists pvs_gap_totality_resultcoverbound. pvs_gap_totality_resultcoverbound + S (pvs_position_totality_resultcover) = (l)) /\ (((exists ff_h_pvs_totality_resultcoverentry. ff_h_pvs_totality_resultcoverentry + S (pvs_divisor_totality_resultcover) = S ((S (pvs_position_totality_resultcover)) * pc)) /\ exists ff_q_pvs_totality_resultcoverentry. pb = ff_q_pvs_totality_resultcoverentry * S ((S (pvs_position_totality_resultcover)) * pc) + (pvs_divisor_totality_resultcover)))) /\ (exists ff_u_pvs_totality_resultproduct ff_v_pvs_totality_resultproduct. ((((exists ff_h_pvs_totality_resultproduct_start. ff_h_pvs_totality_resultproduct_start + S (1) = S ((S (0)) * ff_v_pvs_totality_resultproduct)) /\ exists ff_q_pvs_totality_resultproduct_start. ff_u_pvs_totality_resultproduct = ff_q_pvs_totality_resultproduct_start * S ((S (0)) * ff_v_pvs_totality_resultproduct) + (1))) /\ ((((exists ff_h_pvs_totality_resultproduct_terminal. ff_h_pvs_totality_resultproduct_terminal + S (n) = S ((S (l)) * ff_v_pvs_totality_resultproduct)) /\ exists ff_q_pvs_totality_resultproduct_terminal. ff_u_pvs_totality_resultproduct = ff_q_pvs_totality_resultproduct_terminal * S ((S (l)) * ff_v_pvs_totality_resultproduct) + (n))) /\ forall ff_i_pvs_totality_resultproduct. (exists ff_lt_pvs_totality_resultproduct_bound. ff_lt_pvs_totality_resultproduct_bound + S ff_i_pvs_totality_resultproduct = l) -> exists ff_p_pvs_totality_resultproduct ff_r_pvs_totality_resultproduct ff_s_pvs_totality_resultproduct. ((((exists ff_h_pvs_totality_resultproduct_factor. ff_h_pvs_totality_resultproduct_factor + S (ff_p_pvs_totality_resultproduct) = S ((S (ff_i_pvs_totality_resultproduct)) * vc)) /\ exists ff_q_pvs_totality_resultproduct_factor. vb = ff_q_pvs_totality_resultproduct_factor * S ((S (ff_i_pvs_totality_resultproduct)) * vc) + (ff_p_pvs_totality_resultproduct))) /\ ((((exists ff_h_pvs_totality_resultproduct_partial. ff_h_pvs_totality_resultproduct_partial + S (ff_r_pvs_totality_resultproduct) = S ((S (ff_i_pvs_totality_resultproduct)) * ff_v_pvs_totality_resultproduct)) /\ exists ff_q_pvs_totality_resultproduct_partial. ff_u_pvs_totality_resultproduct = ff_q_pvs_totality_resultproduct_partial * S ((S (ff_i_pvs_totality_resultproduct)) * ff_v_pvs_totality_resultproduct) + (ff_r_pvs_totality_resultproduct))) /\ ((((exists ff_h_pvs_totality_resultproduct_successor. ff_h_pvs_totality_resultproduct_successor + S (ff_s_pvs_totality_resultproduct) = S ((S (S ff_i_pvs_totality_resultproduct)) * ff_v_pvs_totality_resultproduct)) /\ exists ff_q_pvs_totality_resultproduct_successor. ff_u_pvs_totality_resultproduct = ff_q_pvs_totality_resultproduct_successor * S ((S (S ff_i_pvs_totality_resultproduct)) * ff_v_pvs_totality_resultproduct) + (ff_s_pvs_totality_resultproduct))) /\ ff_s_pvs_totality_resultproduct = ff_r_pvs_totality_resultproduct * ff_p_pvs_totality_resultproduct)))))))))))))))

Constructive proof overview

Generated structural guide

Ordinary natural induction on an explicit upper bound constructs the whole distinct-prime support; every recursive cofactor is strictly smaller.

The unchanged tactic script uses 8 declared prerequisites and contains 107 exact native proof lines.

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

Proof neighborhood

Direct dependencies

factor_permutation_below_zero_impossible Alpha theorem; checked-use authorized eq_decidable Stable theorem; checked-use authorized PV0010 prime_valuation_support_value_eq_transport PV000F prime_valuation_support_one PV0011 prime_valuation_strict_cofactor_exists lt_of_lt_of_le Stable theorem; checked-use authorized le_of_succ_le_succ Stable theorem; checked-use authorized PV0012 prime_valuation_support_append_full_power

Direct dependents

PV0014 prime_valuation_support_exists

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

107 script commands · 23 reading checkpoints · 3 local claims

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

Named ingredients (4)
prime valuation support value eq transportprime valuation support oneprime valuation strict cofactor existsprime valuation support append full power

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

01Fix variables and assumptionsL1–1

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

  1. L1
    intro B
02Induction on BL2–5

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction B
  2. L3
    intro n
  3. L4
    intro hn
  4. L5
    intro hbound
03Separate the logical casesL6–6

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

  1. L6
    exfalso
04Use earlier factsL7–9

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

  1. L7
    specialize factor_permutation_below_zero_impossible (n)
  2. L8
    apply factor_permutation_below_zero_impossible
  3. L9
    exact hbound
05Fix variables and assumptionsL10–12

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

  1. L10
    intro n
  2. L11
    intro hn
  3. L12
    intro hbound
06Use earlier factsL13–14

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

  1. L13
    specialize eq_decidable n
  2. L14
    specialize eq_decidable 1
07Separate the logical casesL15–15

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

  1. L15
    cases eq_decidable
08Construct an explicit witnessL16–22

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

  1. L16
    exists 0
  2. L17
    exists 0
  3. L18
    exists 0
  4. L19
    exists 0
  5. L20
    exists 0
  6. L21
    exists 0
  7. L22
    exists 0
09Use earlier factsL23–32

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

  1. L23
    specialize prime_valuation_support_value_eq_transport (1)
  2. L24
    specialize prime_valuation_support_value_eq_transport (n)
  3. L25
    specialize prime_valuation_support_value_eq_transport (0)
  4. L26
    specialize prime_valuation_support_value_eq_transport (0)
  5. L27
    specialize prime_valuation_support_value_eq_transport (0)
  6. L28
    specialize prime_valuation_support_value_eq_transport (0)
  7. L29
    specialize prime_valuation_support_value_eq_transport (0)
  8. L30
    specialize prime_valuation_support_value_eq_transport (0)
  9. L31
    specialize prime_valuation_support_value_eq_transport (0)
  10. L32
    apply prime_valuation_support_value_eq_transport
10Calculate and transport equalitiesL33–33

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

  1. L33
    symm
11Use earlier factsL34–35

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

  1. L34
    exact eq_decidable_left
  2. L35
    apply prime_valuation_support_one
12Establish hfactorL36–40

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

  1. L36
    have hfactor : ∃ p. ∃ e. ∃ P. ∃ u. Prime(p) ∧ (¬e = 0 ∧ (BoundedPowerValuation(p,n,n,e) ∧ (Pow(p,e,P) ∧ (n = P · u ∧ (¬u = 0 ∧ (¬Dvd(p,u) ∧ Lt(u,n)))))))Definitions: LtDvdPrimePowBoundedPowerValuation
  2. L37
    specialize prime_valuation_strict_cofactor_exists (n)
  3. L38
    apply prime_valuation_strict_cofactor_exists
  4. L39
    exact hn
  5. L40
    exact eq_decidable_right
13Separate the logical casesL41–50

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

  1. L41
    cases hfactor
  2. L42
    cases hfactor_witness
  3. L43
    cases hfactor_witness_witness
  4. L44
    cases hfactor_witness_witness_witness
  5. L45
    cases hfactor_witness_witness_witness_witness
  6. L46
    cases hfactor_witness_witness_witness_witness_right
  7. L47
    cases hfactor_witness_witness_witness_witness_right_right
  8. L48
    cases hfactor_witness_witness_witness_witness_right_right_right
  9. L49
    cases hfactor_witness_witness_witness_witness_right_right_right_right
  10. L50
    cases hfactor_witness_witness_witness_witness_right_right_right_right_right
14Separate the logical casesL51–51

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

  1. L51
    cases hfactor_witness_witness_witness_witness_right_right_right_right_right_right
15Establish hrecL52–61

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

  1. L52
    have hrec : ∃ pb. ∃ pc. ∃ eb. ∃ ec. ∃ vb. ∃ vc. ∃ l. PrimeValuationSupport(x3,pb,pc,eb,ec,vb,vc,l)Definitions: PrimeValuationSupport
  2. L53
    specialize IH (x3)
  3. L54
    apply IH
  4. L55
    exact hfactor_witness_witness_witness_witness_right_right_right_right_right_left
  5. L56
    specialize lt_of_lt_of_le (x3)
  6. L57
    specialize lt_of_lt_of_le (n)
  7. L58
    specialize lt_of_lt_of_le (B)
  8. L59
    apply lt_of_lt_of_le
  9. L60
    exact hfactor_witness_witness_witness_witness_right_right_right_right_right_right_right
  10. L61
    specialize le_of_succ_le_succ (n)
16Use earlier factsL62–64

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

  1. L62
    specialize le_of_succ_le_succ (B)
  2. L63
    apply le_of_succ_le_succ
  3. L64
    exact hbound
17Separate the logical casesL65–71

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

  1. L65
    cases hrec
  2. L66
    cases hrec_witness
  3. L67
    cases hrec_witness_witness
  4. L68
    cases hrec_witness_witness_witness
  5. L69
    cases hrec_witness_witness_witness_witness
  6. L70
    cases hrec_witness_witness_witness_witness_witness
  7. L71
    cases hrec_witness_witness_witness_witness_witness_witness
18Establish hextendedL72–81

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

  1. L72
    have hextended : ∃ a. ∃ b. ∃ c. ∃ d. ∃ e. ∃ f. PrimeValuationSupport(n,a,b,c,d,e,f,S x10)Definitions: PrimeValuationSupport
  2. L73
    specialize prime_valuation_support_append_full_power (n)
  3. L74
    specialize prime_valuation_support_append_full_power (x3)
  4. L75
    specialize prime_valuation_support_append_full_power (x)
  5. L76
    specialize prime_valuation_support_append_full_power (x1)
  6. L77
    specialize prime_valuation_support_append_full_power (x2)
  7. L78
    specialize prime_valuation_support_append_full_power (x4)
  8. L79
    specialize prime_valuation_support_append_full_power (x5)
  9. L80
    specialize prime_valuation_support_append_full_power (x6)
  10. L81
    specialize prime_valuation_support_append_full_power (x7)
19Use earlier factsL82–91

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

  1. L82
    specialize prime_valuation_support_append_full_power (x8)
  2. L83
    specialize prime_valuation_support_append_full_power (x9)
  3. L84
    specialize prime_valuation_support_append_full_power (x10)
  4. L85
    apply prime_valuation_support_append_full_power
  5. L86
    exact hn
  6. L87
    exact hfactor_witness_witness_witness_witness_left
  7. L88
    exact hfactor_witness_witness_witness_witness_right_left
  8. L89
    exact hfactor_witness_witness_witness_witness_right_right_left
  9. L90
    exact hfactor_witness_witness_witness_witness_right_right_right_left
  10. L91
    exact hfactor_witness_witness_witness_witness_right_right_right_right_right_right_left
20Use earlier factsL92–93

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

  1. L92
    exact hfactor_witness_witness_witness_witness_right_right_right_right_left
  2. L93
    exact hrec_witness_witness_witness_witness_witness_witness_witness
21Separate the logical casesL94–99

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

  1. L94
    cases hextended
  2. L95
    cases hextended_witness
  3. L96
    cases hextended_witness_witness
  4. L97
    cases hextended_witness_witness_witness
  5. L98
    cases hextended_witness_witness_witness_witness
  6. L99
    cases hextended_witness_witness_witness_witness_witness
22Construct an explicit witnessL100–106

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

  1. L100
    exists x11
  2. L101
    exists x12
  3. L102
    exists x13
  4. L103
    exists x14
  5. L104
    exists x15
  6. L105
    exists x16
  7. L106
    exists S x10
23Use earlier factsL107–107

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

  1. L107
    exact hextended_witness_witness_witness_witness_witness_witness

Library-wide reading audit

Original exact command ledger · 107 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro n
  4. 0004intro hn
  5. 0005intro hbound
  6. 0006exfalso
  7. 0007specialize factor_permutation_below_zero_impossible (n)
  8. 0008apply factor_permutation_below_zero_impossible
  9. 0009exact hbound
  10. 0010intro n
  11. 0011intro hn
  12. 0012intro hbound
  13. 0013specialize eq_decidable n
  14. 0014specialize eq_decidable 1
  15. 0015cases eq_decidable
  16. 0016exists 0
  17. 0017exists 0
  18. 0018exists 0
  19. 0019exists 0
  20. 0020exists 0
  21. 0021exists 0
  22. 0022exists 0
  23. 0023specialize prime_valuation_support_value_eq_transport (1)
  24. 0024specialize prime_valuation_support_value_eq_transport (n)
  25. 0025specialize prime_valuation_support_value_eq_transport (0)
  26. 0026specialize prime_valuation_support_value_eq_transport (0)
  27. 0027specialize prime_valuation_support_value_eq_transport (0)
  28. 0028specialize prime_valuation_support_value_eq_transport (0)
  29. 0029specialize prime_valuation_support_value_eq_transport (0)
  30. 0030specialize prime_valuation_support_value_eq_transport (0)
  31. 0031specialize prime_valuation_support_value_eq_transport (0)
  32. 0032apply prime_valuation_support_value_eq_transport
  33. 0033symm
  34. 0034exact eq_decidable_left
  35. 0035apply prime_valuation_support_one
  36. 0036have hfactor : exists p e P u. (((~((p) = 1) /\ forall pvs_left_totality_factorprime pvs_right_totality_factorprime. (p) = pvs_left_totality_factorprime * pvs_right_totality_factorprime -> pvs_left_totality_factorprime = 1 \/ pvs_right_totality_factorprime = 1) /\ (((~(e = 0)) /\ (((((exists bpd_gap_pvs_totality_factorvaluation_selected_bound. bpd_gap_pvs_totality_factorvaluation_selected_bound + (e) = (n)) /\ (exists bpvi_result_pvs_totality_factorvaluation_selected. ((exists bpvi_b_pvs_totality_factorvaluation_selected_power bpvi_c_pvs_totality_factorvaluation_selected_power. ((forall bpvi_i_pvs_totality_factorvaluation_selected_power. (exists bpvi_repeat_gap_pvs_totality_factorvaluation_selected_power. bpvi_repeat_gap_pvs_totality_factorvaluation_selected_power + S bpvi_i_pvs_totality_factorvaluation_selected_power = e) -> (((exists bpvi_h_pvs_totality_factorvaluation_selected_power_repeat. bpvi_h_pvs_totality_factorvaluation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_totality_factorvaluation_selected_power)) * bpvi_c_pvs_totality_factorvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_selected_power_repeat. bpvi_b_pvs_totality_factorvaluation_selected_power = bpvi_q_pvs_totality_factorvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_totality_factorvaluation_selected_power)) * bpvi_c_pvs_totality_factorvaluation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_totality_factorvaluation_selected_power bpvi_v_pvs_totality_factorvaluation_selected_power. ((((exists bpvi_h_pvs_totality_factorvaluation_selected_power_start. bpvi_h_pvs_totality_factorvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_totality_factorvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_selected_power_start. bpvi_u_pvs_totality_factorvaluation_selected_power = bpvi_q_pvs_totality_factorvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_totality_factorvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_totality_factorvaluation_selected_power_terminal. bpvi_h_pvs_totality_factorvaluation_selected_power_terminal + S (bpvi_result_pvs_totality_factorvaluation_selected) = S ((S (e)) * bpvi_v_pvs_totality_factorvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_selected_power_terminal. bpvi_u_pvs_totality_factorvaluation_selected_power = bpvi_q_pvs_totality_factorvaluation_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_totality_factorvaluation_selected_power) + (bpvi_result_pvs_totality_factorvaluation_selected))) /\ forall bpvi_j_pvs_totality_factorvaluation_selected_power. (exists bpvi_product_gap_pvs_totality_factorvaluation_selected_power. bpvi_product_gap_pvs_totality_factorvaluation_selected_power + S bpvi_j_pvs_totality_factorvaluation_selected_power = e) -> exists bpvi_factor_pvs_totality_factorvaluation_selected_power bpvi_partial_pvs_totality_factorvaluation_selected_power bpvi_successor_pvs_totality_factorvaluation_selected_power. ((((exists bpvi_h_pvs_totality_factorvaluation_selected_power_factor. bpvi_h_pvs_totality_factorvaluation_selected_power_factor + S (bpvi_factor_pvs_totality_factorvaluation_selected_power) = S ((S (bpvi_j_pvs_totality_factorvaluation_selected_power)) * bpvi_c_pvs_totality_factorvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_selected_power_factor. bpvi_b_pvs_totality_factorvaluation_selected_power = bpvi_q_pvs_totality_factorvaluation_selected_power_factor * S ((S (bpvi_j_pvs_totality_factorvaluation_selected_power)) * bpvi_c_pvs_totality_factorvaluation_selected_power) + (bpvi_factor_pvs_totality_factorvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_totality_factorvaluation_selected_power_partial. bpvi_h_pvs_totality_factorvaluation_selected_power_partial + S (bpvi_partial_pvs_totality_factorvaluation_selected_power) = S ((S (bpvi_j_pvs_totality_factorvaluation_selected_power)) * bpvi_v_pvs_totality_factorvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_selected_power_partial. bpvi_u_pvs_totality_factorvaluation_selected_power = bpvi_q_pvs_totality_factorvaluation_selected_power_partial * S ((S (bpvi_j_pvs_totality_factorvaluation_selected_power)) * bpvi_v_pvs_totality_factorvaluation_selected_power) + (bpvi_partial_pvs_totality_factorvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_totality_factorvaluation_selected_power_successor. bpvi_h_pvs_totality_factorvaluation_selected_power_successor + S (bpvi_successor_pvs_totality_factorvaluation_selected_power) = S ((S (S bpvi_j_pvs_totality_factorvaluation_selected_power)) * bpvi_v_pvs_totality_factorvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_selected_power_successor. bpvi_u_pvs_totality_factorvaluation_selected_power = bpvi_q_pvs_totality_factorvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_totality_factorvaluation_selected_power)) * bpvi_v_pvs_totality_factorvaluation_selected_power) + (bpvi_successor_pvs_totality_factorvaluation_selected_power))) /\ bpvi_successor_pvs_totality_factorvaluation_selected_power = bpvi_partial_pvs_totality_factorvaluation_selected_power * bpvi_factor_pvs_totality_factorvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_totality_factorvaluation_selected. n = bpvi_result_pvs_totality_factorvaluation_selected * bpvi_divisor_factor_pvs_totality_factorvaluation_selected))) /\ forall bpd_candidate_pvs_totality_factorvaluation. (exists bpd_gap_pvs_totality_factorvaluation_candidate_bound. bpd_gap_pvs_totality_factorvaluation_candidate_bound + (bpd_candidate_pvs_totality_factorvaluation) = (n)) -> (exists bpvi_result_pvs_totality_factorvaluation_candidate. ((exists bpvi_b_pvs_totality_factorvaluation_candidate_power bpvi_c_pvs_totality_factorvaluation_candidate_power. ((forall bpvi_i_pvs_totality_factorvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_totality_factorvaluation_candidate_power. bpvi_repeat_gap_pvs_totality_factorvaluation_candidate_power + S bpvi_i_pvs_totality_factorvaluation_candidate_power = bpd_candidate_pvs_totality_factorvaluation) -> (((exists bpvi_h_pvs_totality_factorvaluation_candidate_power_repeat. bpvi_h_pvs_totality_factorvaluation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_totality_factorvaluation_candidate_power)) * bpvi_c_pvs_totality_factorvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_candidate_power_repeat. bpvi_b_pvs_totality_factorvaluation_candidate_power = bpvi_q_pvs_totality_factorvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_totality_factorvaluation_candidate_power)) * bpvi_c_pvs_totality_factorvaluation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_totality_factorvaluation_candidate_power bpvi_v_pvs_totality_factorvaluation_candidate_power. ((((exists bpvi_h_pvs_totality_factorvaluation_candidate_power_start. bpvi_h_pvs_totality_factorvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_totality_factorvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_candidate_power_start. bpvi_u_pvs_totality_factorvaluation_candidate_power = bpvi_q_pvs_totality_factorvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_totality_factorvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_totality_factorvaluation_candidate_power_terminal. bpvi_h_pvs_totality_factorvaluation_candidate_power_terminal + S (bpvi_result_pvs_totality_factorvaluation_candidate) = S ((S (bpd_candidate_pvs_totality_factorvaluation)) * bpvi_v_pvs_totality_factorvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_candidate_power_terminal. bpvi_u_pvs_totality_factorvaluation_candidate_power = bpvi_q_pvs_totality_factorvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_totality_factorvaluation)) * bpvi_v_pvs_totality_factorvaluation_candidate_power) + (bpvi_result_pvs_totality_factorvaluation_candidate))) /\ forall bpvi_j_pvs_totality_factorvaluation_candidate_power. (exists bpvi_product_gap_pvs_totality_factorvaluation_candidate_power. bpvi_product_gap_pvs_totality_factorvaluation_candidate_power + S bpvi_j_pvs_totality_factorvaluation_candidate_power = bpd_candidate_pvs_totality_factorvaluation) -> exists bpvi_factor_pvs_totality_factorvaluation_candidate_power bpvi_partial_pvs_totality_factorvaluation_candidate_power bpvi_successor_pvs_totality_factorvaluation_candidate_power. ((((exists bpvi_h_pvs_totality_factorvaluation_candidate_power_factor. bpvi_h_pvs_totality_factorvaluation_candidate_power_factor + S (bpvi_factor_pvs_totality_factorvaluation_candidate_power) = S ((S (bpvi_j_pvs_totality_factorvaluation_candidate_power)) * bpvi_c_pvs_totality_factorvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_candidate_power_factor. bpvi_b_pvs_totality_factorvaluation_candidate_power = bpvi_q_pvs_totality_factorvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_totality_factorvaluation_candidate_power)) * bpvi_c_pvs_totality_factorvaluation_candidate_power) + (bpvi_factor_pvs_totality_factorvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_totality_factorvaluation_candidate_power_partial. bpvi_h_pvs_totality_factorvaluation_candidate_power_partial + S (bpvi_partial_pvs_totality_factorvaluation_candidate_power) = S ((S (bpvi_j_pvs_totality_factorvaluation_candidate_power)) * bpvi_v_pvs_totality_factorvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_candidate_power_partial. bpvi_u_pvs_totality_factorvaluation_candidate_power = bpvi_q_pvs_totality_factorvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_totality_factorvaluation_candidate_power)) * bpvi_v_pvs_totality_factorvaluation_candidate_power) + (bpvi_partial_pvs_totality_factorvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_totality_factorvaluation_candidate_power_successor. bpvi_h_pvs_totality_factorvaluation_candidate_power_successor + S (bpvi_successor_pvs_totality_factorvaluation_candidate_power) = S ((S (S bpvi_j_pvs_totality_factorvaluation_candidate_power)) * bpvi_v_pvs_totality_factorvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_factorvaluation_candidate_power_successor. bpvi_u_pvs_totality_factorvaluation_candidate_power = bpvi_q_pvs_totality_factorvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_totality_factorvaluation_candidate_power)) * bpvi_v_pvs_totality_factorvaluation_candidate_power) + (bpvi_successor_pvs_totality_factorvaluation_candidate_power))) /\ bpvi_successor_pvs_totality_factorvaluation_candidate_power = bpvi_partial_pvs_totality_factorvaluation_candidate_power * bpvi_factor_pvs_totality_factorvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_totality_factorvaluation_candidate. n = bpvi_result_pvs_totality_factorvaluation_candidate * bpvi_divisor_factor_pvs_totality_factorvaluation_candidate)) -> (exists bpd_gap_pvs_totality_factorvaluation_maximal. bpd_gap_pvs_totality_factorvaluation_maximal + (bpd_candidate_pvs_totality_factorvaluation) = (e))) /\ (((exists pa_b_pvs_totality_factorpower pa_c_pvs_totality_factorpower. ((forall pa_i_pvs_totality_factorpower_repeat. (exists pa_lt_pvs_totality_factorpower_repeat_bound. pa_lt_pvs_totality_factorpower_repeat_bound + S pa_i_pvs_totality_factorpower_repeat = e) -> (((exists pa_h_pvs_totality_factorpower_repeat_decoded. pa_h_pvs_totality_factorpower_repeat_decoded + S (p) = S ((S (pa_i_pvs_totality_factorpower_repeat)) * pa_c_pvs_totality_factorpower)) /\ exists pa_q_pvs_totality_factorpower_repeat_decoded. pa_b_pvs_totality_factorpower = pa_q_pvs_totality_factorpower_repeat_decoded * S ((S (pa_i_pvs_totality_factorpower_repeat)) * pa_c_pvs_totality_factorpower) + (p)))) /\ (exists pa_u_pvs_totality_factorpower_product pa_v_pvs_totality_factorpower_product. ((((exists pa_h_pvs_totality_factorpower_product_start. pa_h_pvs_totality_factorpower_product_start + S (1) = S ((S (0)) * pa_v_pvs_totality_factorpower_product)) /\ exists pa_q_pvs_totality_factorpower_product_start. pa_u_pvs_totality_factorpower_product = pa_q_pvs_totality_factorpower_product_start * S ((S (0)) * pa_v_pvs_totality_factorpower_product) + (1))) /\ ((((exists pa_h_pvs_totality_factorpower_product_terminal. pa_h_pvs_totality_factorpower_product_terminal + S (P) = S ((S (e)) * pa_v_pvs_totality_factorpower_product)) /\ exists pa_q_pvs_totality_factorpower_product_terminal. pa_u_pvs_totality_factorpower_product = pa_q_pvs_totality_factorpower_product_terminal * S ((S (e)) * pa_v_pvs_totality_factorpower_product) + (P))) /\ forall pa_i_pvs_totality_factorpower_product. (exists pa_lt_pvs_totality_factorpower_product_bound. pa_lt_pvs_totality_factorpower_product_bound + S pa_i_pvs_totality_factorpower_product = e) -> exists pa_p_pvs_totality_factorpower_product pa_r_pvs_totality_factorpower_product pa_s_pvs_totality_factorpower_product. ((((exists pa_h_pvs_totality_factorpower_product_factor. pa_h_pvs_totality_factorpower_product_factor + S (pa_p_pvs_totality_factorpower_product) = S ((S (pa_i_pvs_totality_factorpower_product)) * pa_c_pvs_totality_factorpower)) /\ exists pa_q_pvs_totality_factorpower_product_factor. pa_b_pvs_totality_factorpower = pa_q_pvs_totality_factorpower_product_factor * S ((S (pa_i_pvs_totality_factorpower_product)) * pa_c_pvs_totality_factorpower) + (pa_p_pvs_totality_factorpower_product))) /\ ((((exists pa_h_pvs_totality_factorpower_product_partial. pa_h_pvs_totality_factorpower_product_partial + S (pa_r_pvs_totality_factorpower_product) = S ((S (pa_i_pvs_totality_factorpower_product)) * pa_v_pvs_totality_factorpower_product)) /\ exists pa_q_pvs_totality_factorpower_product_partial. pa_u_pvs_totality_factorpower_product = pa_q_pvs_totality_factorpower_product_partial * S ((S (pa_i_pvs_totality_factorpower_product)) * pa_v_pvs_totality_factorpower_product) + (pa_r_pvs_totality_factorpower_product))) /\ ((((exists pa_h_pvs_totality_factorpower_product_successor. pa_h_pvs_totality_factorpower_product_successor + S (pa_s_pvs_totality_factorpower_product) = S ((S (S pa_i_pvs_totality_factorpower_product)) * pa_v_pvs_totality_factorpower_product)) /\ exists pa_q_pvs_totality_factorpower_product_successor. pa_u_pvs_totality_factorpower_product = pa_q_pvs_totality_factorpower_product_successor * S ((S (S pa_i_pvs_totality_factorpower_product)) * pa_v_pvs_totality_factorpower_product) + (pa_s_pvs_totality_factorpower_product))) /\ pa_s_pvs_totality_factorpower_product = pa_r_pvs_totality_factorpower_product * pa_p_pvs_totality_factorpower_product)))))))) /\ ((((n) = (P) * (u)) /\ (((~(u = 0)) /\ (((~(exists pvs_factor_totality_factornondivisor. (u) = (p) * pvs_factor_totality_factornondivisor)) /\ (exists pvs_gap_totality_factordescent. pvs_gap_totality_factordescent + S (u) = (n))))))))))))))))
  37. 0037specialize prime_valuation_strict_cofactor_exists (n)
  38. 0038apply prime_valuation_strict_cofactor_exists
  39. 0039exact hn
  40. 0040exact eq_decidable_right
  41. 0041cases hfactor
  42. 0042cases hfactor_witness
  43. 0043cases hfactor_witness_witness
  44. 0044cases hfactor_witness_witness_witness
  45. 0045cases hfactor_witness_witness_witness_witness
  46. 0046cases hfactor_witness_witness_witness_witness_right
  47. 0047cases hfactor_witness_witness_witness_witness_right_right
  48. 0048cases hfactor_witness_witness_witness_witness_right_right_right
  49. 0049cases hfactor_witness_witness_witness_witness_right_right_right_right
  50. 0050cases hfactor_witness_witness_witness_witness_right_right_right_right_right
  51. 0051cases hfactor_witness_witness_witness_witness_right_right_right_right_right_right
  52. 0052have hrec : exists pb pc eb ec vb vc l. (((~((x3) = 0)) /\ (((forall pfp_i_pvs_totality_recursivedistinct pfp_j_pvs_totality_recursivedistinct pfp_a_pvs_totality_recursivedistinct. (exists pfp_gap_pvs_totality_recursivedistinctfirst. pfp_gap_pvs_totality_recursivedistinctfirst + S (pfp_i_pvs_totality_recursivedistinct) = (l)) -> (exists pfp_gap_pvs_totality_recursivedistinctsecond. pfp_gap_pvs_totality_recursivedistinctsecond + S (pfp_j_pvs_totality_recursivedistinct) = (l)) -> (((exists ff_h_pfp_pvs_totality_recursivedistinctleft. ff_h_pfp_pvs_totality_recursivedistinctleft + S (pfp_a_pvs_totality_recursivedistinct) = S ((S (pfp_i_pvs_totality_recursivedistinct)) * pc)) /\ exists ff_q_pfp_pvs_totality_recursivedistinctleft. pb = ff_q_pfp_pvs_totality_recursivedistinctleft * S ((S (pfp_i_pvs_totality_recursivedistinct)) * pc) + (pfp_a_pvs_totality_recursivedistinct))) -> (((exists ff_h_pfp_pvs_totality_recursivedistinctright. ff_h_pfp_pvs_totality_recursivedistinctright + S (pfp_a_pvs_totality_recursivedistinct) = S ((S (pfp_j_pvs_totality_recursivedistinct)) * pc)) /\ exists ff_q_pfp_pvs_totality_recursivedistinctright. pb = ff_q_pfp_pvs_totality_recursivedistinctright * S ((S (pfp_j_pvs_totality_recursivedistinct)) * pc) + (pfp_a_pvs_totality_recursivedistinct))) -> pfp_i_pvs_totality_recursivedistinct = pfp_j_pvs_totality_recursivedistinct) /\ (((forall pvs_index_totality_recursiveentries. (exists pvs_gap_totality_recursiveentriesindex. pvs_gap_totality_recursiveentriesindex + S (pvs_index_totality_recursiveentries) = (l)) -> exists pvs_prime_totality_recursiveentries pvs_exponent_totality_recursiveentries pvs_power_totality_recursiveentries. (((((exists ff_h_pvs_totality_recursiveentriesprime. ff_h_pvs_totality_recursiveentriesprime + S (pvs_prime_totality_recursiveentries) = S ((S (pvs_index_totality_recursiveentries)) * pc)) /\ exists ff_q_pvs_totality_recursiveentriesprime. pb = ff_q_pvs_totality_recursiveentriesprime * S ((S (pvs_index_totality_recursiveentries)) * pc) + (pvs_prime_totality_recursiveentries))) /\ (((((exists ff_h_pvs_totality_recursiveentriesexponent. ff_h_pvs_totality_recursiveentriesexponent + S (pvs_exponent_totality_recursiveentries) = S ((S (pvs_index_totality_recursiveentries)) * ec)) /\ exists ff_q_pvs_totality_recursiveentriesexponent. eb = ff_q_pvs_totality_recursiveentriesexponent * S ((S (pvs_index_totality_recursiveentries)) * ec) + (pvs_exponent_totality_recursiveentries))) /\ (((((exists ff_h_pvs_totality_recursiveentriespower. ff_h_pvs_totality_recursiveentriespower + S (pvs_power_totality_recursiveentries) = S ((S (pvs_index_totality_recursiveentries)) * vc)) /\ exists ff_q_pvs_totality_recursiveentriespower. vb = ff_q_pvs_totality_recursiveentriespower * S ((S (pvs_index_totality_recursiveentries)) * vc) + (pvs_power_totality_recursiveentries))) /\ (((~((pvs_prime_totality_recursiveentries) = 1) /\ forall pvs_left_totality_recursiveentriesdomain pvs_right_totality_recursiveentriesdomain. (pvs_prime_totality_recursiveentries) = pvs_left_totality_recursiveentriesdomain * pvs_right_totality_recursiveentriesdomain -> pvs_left_totality_recursiveentriesdomain = 1 \/ pvs_right_totality_recursiveentriesdomain = 1) /\ (((~(pvs_exponent_totality_recursiveentries = 0)) /\ (((((exists bpd_gap_pvs_totality_recursiveentriesvaluation_selected_bound. bpd_gap_pvs_totality_recursiveentriesvaluation_selected_bound + (pvs_exponent_totality_recursiveentries) = (x3)) /\ (exists bpvi_result_pvs_totality_recursiveentriesvaluation_selected. ((exists bpvi_b_pvs_totality_recursiveentriesvaluation_selected_power bpvi_c_pvs_totality_recursiveentriesvaluation_selected_power. ((forall bpvi_i_pvs_totality_recursiveentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_totality_recursiveentriesvaluation_selected_power. bpvi_repeat_gap_pvs_totality_recursiveentriesvaluation_selected_power + S bpvi_i_pvs_totality_recursiveentriesvaluation_selected_power = pvs_exponent_totality_recursiveentries) -> (((exists bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_repeat. bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_repeat + S (pvs_prime_totality_recursiveentries) = S ((S (bpvi_i_pvs_totality_recursiveentriesvaluation_selected_power)) * bpvi_c_pvs_totality_recursiveentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_repeat. bpvi_b_pvs_totality_recursiveentriesvaluation_selected_power = bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_totality_recursiveentriesvaluation_selected_power)) * bpvi_c_pvs_totality_recursiveentriesvaluation_selected_power) + (pvs_prime_totality_recursiveentries)))) /\ (exists bpvi_u_pvs_totality_recursiveentriesvaluation_selected_power bpvi_v_pvs_totality_recursiveentriesvaluation_selected_power. ((((exists bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_start. bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_totality_recursiveentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_start. bpvi_u_pvs_totality_recursiveentriesvaluation_selected_power = bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_totality_recursiveentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_terminal. bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_totality_recursiveentriesvaluation_selected) = S ((S (pvs_exponent_totality_recursiveentries)) * bpvi_v_pvs_totality_recursiveentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_terminal. bpvi_u_pvs_totality_recursiveentriesvaluation_selected_power = bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_totality_recursiveentries)) * bpvi_v_pvs_totality_recursiveentriesvaluation_selected_power) + (bpvi_result_pvs_totality_recursiveentriesvaluation_selected))) /\ forall bpvi_j_pvs_totality_recursiveentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_totality_recursiveentriesvaluation_selected_power. bpvi_product_gap_pvs_totality_recursiveentriesvaluation_selected_power + S bpvi_j_pvs_totality_recursiveentriesvaluation_selected_power = pvs_exponent_totality_recursiveentries) -> exists bpvi_factor_pvs_totality_recursiveentriesvaluation_selected_power bpvi_partial_pvs_totality_recursiveentriesvaluation_selected_power bpvi_successor_pvs_totality_recursiveentriesvaluation_selected_power. ((((exists bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_factor. bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_totality_recursiveentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_totality_recursiveentriesvaluation_selected_power)) * bpvi_c_pvs_totality_recursiveentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_factor. bpvi_b_pvs_totality_recursiveentriesvaluation_selected_power = bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_totality_recursiveentriesvaluation_selected_power)) * bpvi_c_pvs_totality_recursiveentriesvaluation_selected_power) + (bpvi_factor_pvs_totality_recursiveentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_partial. bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_totality_recursiveentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_totality_recursiveentriesvaluation_selected_power)) * bpvi_v_pvs_totality_recursiveentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_partial. bpvi_u_pvs_totality_recursiveentriesvaluation_selected_power = bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_totality_recursiveentriesvaluation_selected_power)) * bpvi_v_pvs_totality_recursiveentriesvaluation_selected_power) + (bpvi_partial_pvs_totality_recursiveentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_successor. bpvi_h_pvs_totality_recursiveentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_totality_recursiveentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_totality_recursiveentriesvaluation_selected_power)) * bpvi_v_pvs_totality_recursiveentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_successor. bpvi_u_pvs_totality_recursiveentriesvaluation_selected_power = bpvi_q_pvs_totality_recursiveentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_totality_recursiveentriesvaluation_selected_power)) * bpvi_v_pvs_totality_recursiveentriesvaluation_selected_power) + (bpvi_successor_pvs_totality_recursiveentriesvaluation_selected_power))) /\ bpvi_successor_pvs_totality_recursiveentriesvaluation_selected_power = bpvi_partial_pvs_totality_recursiveentriesvaluation_selected_power * bpvi_factor_pvs_totality_recursiveentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_totality_recursiveentriesvaluation_selected. x3 = bpvi_result_pvs_totality_recursiveentriesvaluation_selected * bpvi_divisor_factor_pvs_totality_recursiveentriesvaluation_selected))) /\ forall bpd_candidate_pvs_totality_recursiveentriesvaluation. (exists bpd_gap_pvs_totality_recursiveentriesvaluation_candidate_bound. bpd_gap_pvs_totality_recursiveentriesvaluation_candidate_bound + (bpd_candidate_pvs_totality_recursiveentriesvaluation) = (x3)) -> (exists bpvi_result_pvs_totality_recursiveentriesvaluation_candidate. ((exists bpvi_b_pvs_totality_recursiveentriesvaluation_candidate_power bpvi_c_pvs_totality_recursiveentriesvaluation_candidate_power. ((forall bpvi_i_pvs_totality_recursiveentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_totality_recursiveentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_totality_recursiveentriesvaluation_candidate_power + S bpvi_i_pvs_totality_recursiveentriesvaluation_candidate_power = bpd_candidate_pvs_totality_recursiveentriesvaluation) -> (((exists bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_repeat. bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_repeat + S (pvs_prime_totality_recursiveentries) = S ((S (bpvi_i_pvs_totality_recursiveentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_recursiveentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_repeat. bpvi_b_pvs_totality_recursiveentriesvaluation_candidate_power = bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_totality_recursiveentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_recursiveentriesvaluation_candidate_power) + (pvs_prime_totality_recursiveentries)))) /\ (exists bpvi_u_pvs_totality_recursiveentriesvaluation_candidate_power bpvi_v_pvs_totality_recursiveentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_start. bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_totality_recursiveentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_start. bpvi_u_pvs_totality_recursiveentriesvaluation_candidate_power = bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_totality_recursiveentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_terminal. bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_totality_recursiveentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_totality_recursiveentriesvaluation)) * bpvi_v_pvs_totality_recursiveentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_terminal. bpvi_u_pvs_totality_recursiveentriesvaluation_candidate_power = bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_totality_recursiveentriesvaluation)) * bpvi_v_pvs_totality_recursiveentriesvaluation_candidate_power) + (bpvi_result_pvs_totality_recursiveentriesvaluation_candidate))) /\ forall bpvi_j_pvs_totality_recursiveentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_totality_recursiveentriesvaluation_candidate_power. bpvi_product_gap_pvs_totality_recursiveentriesvaluation_candidate_power + S bpvi_j_pvs_totality_recursiveentriesvaluation_candidate_power = bpd_candidate_pvs_totality_recursiveentriesvaluation) -> exists bpvi_factor_pvs_totality_recursiveentriesvaluation_candidate_power bpvi_partial_pvs_totality_recursiveentriesvaluation_candidate_power bpvi_successor_pvs_totality_recursiveentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_factor. bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_totality_recursiveentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_totality_recursiveentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_recursiveentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_factor. bpvi_b_pvs_totality_recursiveentriesvaluation_candidate_power = bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_totality_recursiveentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_recursiveentriesvaluation_candidate_power) + (bpvi_factor_pvs_totality_recursiveentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_partial. bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_totality_recursiveentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_totality_recursiveentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_recursiveentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_partial. bpvi_u_pvs_totality_recursiveentriesvaluation_candidate_power = bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_totality_recursiveentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_recursiveentriesvaluation_candidate_power) + (bpvi_partial_pvs_totality_recursiveentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_successor. bpvi_h_pvs_totality_recursiveentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_totality_recursiveentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_totality_recursiveentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_recursiveentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_successor. bpvi_u_pvs_totality_recursiveentriesvaluation_candidate_power = bpvi_q_pvs_totality_recursiveentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_totality_recursiveentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_recursiveentriesvaluation_candidate_power) + (bpvi_successor_pvs_totality_recursiveentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_totality_recursiveentriesvaluation_candidate_power = bpvi_partial_pvs_totality_recursiveentriesvaluation_candidate_power * bpvi_factor_pvs_totality_recursiveentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_totality_recursiveentriesvaluation_candidate. x3 = bpvi_result_pvs_totality_recursiveentriesvaluation_candidate * bpvi_divisor_factor_pvs_totality_recursiveentriesvaluation_candidate)) -> (exists bpd_gap_pvs_totality_recursiveentriesvaluation_maximal. bpd_gap_pvs_totality_recursiveentriesvaluation_maximal + (bpd_candidate_pvs_totality_recursiveentriesvaluation) = (pvs_exponent_totality_recursiveentries))) /\ (exists pa_b_pvs_totality_recursiveentriesvalue pa_c_pvs_totality_recursiveentriesvalue. ((forall pa_i_pvs_totality_recursiveentriesvalue_repeat. (exists pa_lt_pvs_totality_recursiveentriesvalue_repeat_bound. pa_lt_pvs_totality_recursiveentriesvalue_repeat_bound + S pa_i_pvs_totality_recursiveentriesvalue_repeat = pvs_exponent_totality_recursiveentries) -> (((exists pa_h_pvs_totality_recursiveentriesvalue_repeat_decoded. pa_h_pvs_totality_recursiveentriesvalue_repeat_decoded + S (pvs_prime_totality_recursiveentries) = S ((S (pa_i_pvs_totality_recursiveentriesvalue_repeat)) * pa_c_pvs_totality_recursiveentriesvalue)) /\ exists pa_q_pvs_totality_recursiveentriesvalue_repeat_decoded. pa_b_pvs_totality_recursiveentriesvalue = pa_q_pvs_totality_recursiveentriesvalue_repeat_decoded * S ((S (pa_i_pvs_totality_recursiveentriesvalue_repeat)) * pa_c_pvs_totality_recursiveentriesvalue) + (pvs_prime_totality_recursiveentries)))) /\ (exists pa_u_pvs_totality_recursiveentriesvalue_product pa_v_pvs_totality_recursiveentriesvalue_product. ((((exists pa_h_pvs_totality_recursiveentriesvalue_product_start. pa_h_pvs_totality_recursiveentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_totality_recursiveentriesvalue_product)) /\ exists pa_q_pvs_totality_recursiveentriesvalue_product_start. pa_u_pvs_totality_recursiveentriesvalue_product = pa_q_pvs_totality_recursiveentriesvalue_product_start * S ((S (0)) * pa_v_pvs_totality_recursiveentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_totality_recursiveentriesvalue_product_terminal. pa_h_pvs_totality_recursiveentriesvalue_product_terminal + S (pvs_power_totality_recursiveentries) = S ((S (pvs_exponent_totality_recursiveentries)) * pa_v_pvs_totality_recursiveentriesvalue_product)) /\ exists pa_q_pvs_totality_recursiveentriesvalue_product_terminal. pa_u_pvs_totality_recursiveentriesvalue_product = pa_q_pvs_totality_recursiveentriesvalue_product_terminal * S ((S (pvs_exponent_totality_recursiveentries)) * pa_v_pvs_totality_recursiveentriesvalue_product) + (pvs_power_totality_recursiveentries))) /\ forall pa_i_pvs_totality_recursiveentriesvalue_product. (exists pa_lt_pvs_totality_recursiveentriesvalue_product_bound. pa_lt_pvs_totality_recursiveentriesvalue_product_bound + S pa_i_pvs_totality_recursiveentriesvalue_product = pvs_exponent_totality_recursiveentries) -> exists pa_p_pvs_totality_recursiveentriesvalue_product pa_r_pvs_totality_recursiveentriesvalue_product pa_s_pvs_totality_recursiveentriesvalue_product. ((((exists pa_h_pvs_totality_recursiveentriesvalue_product_factor. pa_h_pvs_totality_recursiveentriesvalue_product_factor + S (pa_p_pvs_totality_recursiveentriesvalue_product) = S ((S (pa_i_pvs_totality_recursiveentriesvalue_product)) * pa_c_pvs_totality_recursiveentriesvalue)) /\ exists pa_q_pvs_totality_recursiveentriesvalue_product_factor. pa_b_pvs_totality_recursiveentriesvalue = pa_q_pvs_totality_recursiveentriesvalue_product_factor * S ((S (pa_i_pvs_totality_recursiveentriesvalue_product)) * pa_c_pvs_totality_recursiveentriesvalue) + (pa_p_pvs_totality_recursiveentriesvalue_product))) /\ ((((exists pa_h_pvs_totality_recursiveentriesvalue_product_partial. pa_h_pvs_totality_recursiveentriesvalue_product_partial + S (pa_r_pvs_totality_recursiveentriesvalue_product) = S ((S (pa_i_pvs_totality_recursiveentriesvalue_product)) * pa_v_pvs_totality_recursiveentriesvalue_product)) /\ exists pa_q_pvs_totality_recursiveentriesvalue_product_partial. pa_u_pvs_totality_recursiveentriesvalue_product = pa_q_pvs_totality_recursiveentriesvalue_product_partial * S ((S (pa_i_pvs_totality_recursiveentriesvalue_product)) * pa_v_pvs_totality_recursiveentriesvalue_product) + (pa_r_pvs_totality_recursiveentriesvalue_product))) /\ ((((exists pa_h_pvs_totality_recursiveentriesvalue_product_successor. pa_h_pvs_totality_recursiveentriesvalue_product_successor + S (pa_s_pvs_totality_recursiveentriesvalue_product) = S ((S (S pa_i_pvs_totality_recursiveentriesvalue_product)) * pa_v_pvs_totality_recursiveentriesvalue_product)) /\ exists pa_q_pvs_totality_recursiveentriesvalue_product_successor. pa_u_pvs_totality_recursiveentriesvalue_product = pa_q_pvs_totality_recursiveentriesvalue_product_successor * S ((S (S pa_i_pvs_totality_recursiveentriesvalue_product)) * pa_v_pvs_totality_recursiveentriesvalue_product) + (pa_s_pvs_totality_recursiveentriesvalue_product))) /\ pa_s_pvs_totality_recursiveentriesvalue_product = pa_r_pvs_totality_recursiveentriesvalue_product * pa_p_pvs_totality_recursiveentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_totality_recursivecover. (~((pvs_divisor_totality_recursivecover) = 1) /\ forall pvs_left_totality_recursivecoverprime pvs_right_totality_recursivecoverprime. (pvs_divisor_totality_recursivecover) = pvs_left_totality_recursivecoverprime * pvs_right_totality_recursivecoverprime -> pvs_left_totality_recursivecoverprime = 1 \/ pvs_right_totality_recursivecoverprime = 1) -> (exists pvs_factor_totality_recursivecoverdivides. (x3) = (pvs_divisor_totality_recursivecover) * pvs_factor_totality_recursivecoverdivides) -> exists pvs_position_totality_recursivecover. (exists pvs_gap_totality_recursivecoverbound. pvs_gap_totality_recursivecoverbound + S (pvs_position_totality_recursivecover) = (l)) /\ (((exists ff_h_pvs_totality_recursivecoverentry. ff_h_pvs_totality_recursivecoverentry + S (pvs_divisor_totality_recursivecover) = S ((S (pvs_position_totality_recursivecover)) * pc)) /\ exists ff_q_pvs_totality_recursivecoverentry. pb = ff_q_pvs_totality_recursivecoverentry * S ((S (pvs_position_totality_recursivecover)) * pc) + (pvs_divisor_totality_recursivecover)))) /\ (exists ff_u_pvs_totality_recursiveproduct ff_v_pvs_totality_recursiveproduct. ((((exists ff_h_pvs_totality_recursiveproduct_start. ff_h_pvs_totality_recursiveproduct_start + S (1) = S ((S (0)) * ff_v_pvs_totality_recursiveproduct)) /\ exists ff_q_pvs_totality_recursiveproduct_start. ff_u_pvs_totality_recursiveproduct = ff_q_pvs_totality_recursiveproduct_start * S ((S (0)) * ff_v_pvs_totality_recursiveproduct) + (1))) /\ ((((exists ff_h_pvs_totality_recursiveproduct_terminal. ff_h_pvs_totality_recursiveproduct_terminal + S (x3) = S ((S (l)) * ff_v_pvs_totality_recursiveproduct)) /\ exists ff_q_pvs_totality_recursiveproduct_terminal. ff_u_pvs_totality_recursiveproduct = ff_q_pvs_totality_recursiveproduct_terminal * S ((S (l)) * ff_v_pvs_totality_recursiveproduct) + (x3))) /\ forall ff_i_pvs_totality_recursiveproduct. (exists ff_lt_pvs_totality_recursiveproduct_bound. ff_lt_pvs_totality_recursiveproduct_bound + S ff_i_pvs_totality_recursiveproduct = l) -> exists ff_p_pvs_totality_recursiveproduct ff_r_pvs_totality_recursiveproduct ff_s_pvs_totality_recursiveproduct. ((((exists ff_h_pvs_totality_recursiveproduct_factor. ff_h_pvs_totality_recursiveproduct_factor + S (ff_p_pvs_totality_recursiveproduct) = S ((S (ff_i_pvs_totality_recursiveproduct)) * vc)) /\ exists ff_q_pvs_totality_recursiveproduct_factor. vb = ff_q_pvs_totality_recursiveproduct_factor * S ((S (ff_i_pvs_totality_recursiveproduct)) * vc) + (ff_p_pvs_totality_recursiveproduct))) /\ ((((exists ff_h_pvs_totality_recursiveproduct_partial. ff_h_pvs_totality_recursiveproduct_partial + S (ff_r_pvs_totality_recursiveproduct) = S ((S (ff_i_pvs_totality_recursiveproduct)) * ff_v_pvs_totality_recursiveproduct)) /\ exists ff_q_pvs_totality_recursiveproduct_partial. ff_u_pvs_totality_recursiveproduct = ff_q_pvs_totality_recursiveproduct_partial * S ((S (ff_i_pvs_totality_recursiveproduct)) * ff_v_pvs_totality_recursiveproduct) + (ff_r_pvs_totality_recursiveproduct))) /\ ((((exists ff_h_pvs_totality_recursiveproduct_successor. ff_h_pvs_totality_recursiveproduct_successor + S (ff_s_pvs_totality_recursiveproduct) = S ((S (S ff_i_pvs_totality_recursiveproduct)) * ff_v_pvs_totality_recursiveproduct)) /\ exists ff_q_pvs_totality_recursiveproduct_successor. ff_u_pvs_totality_recursiveproduct = ff_q_pvs_totality_recursiveproduct_successor * S ((S (S ff_i_pvs_totality_recursiveproduct)) * ff_v_pvs_totality_recursiveproduct) + (ff_s_pvs_totality_recursiveproduct))) /\ ff_s_pvs_totality_recursiveproduct = ff_r_pvs_totality_recursiveproduct * ff_p_pvs_totality_recursiveproduct))))))))))))))
  53. 0053specialize IH (x3)
  54. 0054apply IH
  55. 0055exact hfactor_witness_witness_witness_witness_right_right_right_right_right_left
  56. 0056specialize lt_of_lt_of_le (x3)
  57. 0057specialize lt_of_lt_of_le (n)
  58. 0058specialize lt_of_lt_of_le (B)
  59. 0059apply lt_of_lt_of_le
  60. 0060exact hfactor_witness_witness_witness_witness_right_right_right_right_right_right_right
  61. 0061specialize le_of_succ_le_succ (n)
  62. 0062specialize le_of_succ_le_succ (B)
  63. 0063apply le_of_succ_le_succ
  64. 0064exact hbound
  65. 0065cases hrec
  66. 0066cases hrec_witness
  67. 0067cases hrec_witness_witness
  68. 0068cases hrec_witness_witness_witness
  69. 0069cases hrec_witness_witness_witness_witness
  70. 0070cases hrec_witness_witness_witness_witness_witness
  71. 0071cases hrec_witness_witness_witness_witness_witness_witness
  72. 0072have hextended : exists a b c d e f. (((~((n) = 0)) /\ (((forall pfp_i_pvs_totality_extendeddistinct pfp_j_pvs_totality_extendeddistinct pfp_a_pvs_totality_extendeddistinct. (exists pfp_gap_pvs_totality_extendeddistinctfirst. pfp_gap_pvs_totality_extendeddistinctfirst + S (pfp_i_pvs_totality_extendeddistinct) = (S x10)) -> (exists pfp_gap_pvs_totality_extendeddistinctsecond. pfp_gap_pvs_totality_extendeddistinctsecond + S (pfp_j_pvs_totality_extendeddistinct) = (S x10)) -> (((exists ff_h_pfp_pvs_totality_extendeddistinctleft. ff_h_pfp_pvs_totality_extendeddistinctleft + S (pfp_a_pvs_totality_extendeddistinct) = S ((S (pfp_i_pvs_totality_extendeddistinct)) * b)) /\ exists ff_q_pfp_pvs_totality_extendeddistinctleft. a = ff_q_pfp_pvs_totality_extendeddistinctleft * S ((S (pfp_i_pvs_totality_extendeddistinct)) * b) + (pfp_a_pvs_totality_extendeddistinct))) -> (((exists ff_h_pfp_pvs_totality_extendeddistinctright. ff_h_pfp_pvs_totality_extendeddistinctright + S (pfp_a_pvs_totality_extendeddistinct) = S ((S (pfp_j_pvs_totality_extendeddistinct)) * b)) /\ exists ff_q_pfp_pvs_totality_extendeddistinctright. a = ff_q_pfp_pvs_totality_extendeddistinctright * S ((S (pfp_j_pvs_totality_extendeddistinct)) * b) + (pfp_a_pvs_totality_extendeddistinct))) -> pfp_i_pvs_totality_extendeddistinct = pfp_j_pvs_totality_extendeddistinct) /\ (((forall pvs_index_totality_extendedentries. (exists pvs_gap_totality_extendedentriesindex. pvs_gap_totality_extendedentriesindex + S (pvs_index_totality_extendedentries) = (S x10)) -> exists pvs_prime_totality_extendedentries pvs_exponent_totality_extendedentries pvs_power_totality_extendedentries. (((((exists ff_h_pvs_totality_extendedentriesprime. ff_h_pvs_totality_extendedentriesprime + S (pvs_prime_totality_extendedentries) = S ((S (pvs_index_totality_extendedentries)) * b)) /\ exists ff_q_pvs_totality_extendedentriesprime. a = ff_q_pvs_totality_extendedentriesprime * S ((S (pvs_index_totality_extendedentries)) * b) + (pvs_prime_totality_extendedentries))) /\ (((((exists ff_h_pvs_totality_extendedentriesexponent. ff_h_pvs_totality_extendedentriesexponent + S (pvs_exponent_totality_extendedentries) = S ((S (pvs_index_totality_extendedentries)) * d)) /\ exists ff_q_pvs_totality_extendedentriesexponent. c = ff_q_pvs_totality_extendedentriesexponent * S ((S (pvs_index_totality_extendedentries)) * d) + (pvs_exponent_totality_extendedentries))) /\ (((((exists ff_h_pvs_totality_extendedentriespower. ff_h_pvs_totality_extendedentriespower + S (pvs_power_totality_extendedentries) = S ((S (pvs_index_totality_extendedentries)) * f)) /\ exists ff_q_pvs_totality_extendedentriespower. e = ff_q_pvs_totality_extendedentriespower * S ((S (pvs_index_totality_extendedentries)) * f) + (pvs_power_totality_extendedentries))) /\ (((~((pvs_prime_totality_extendedentries) = 1) /\ forall pvs_left_totality_extendedentriesdomain pvs_right_totality_extendedentriesdomain. (pvs_prime_totality_extendedentries) = pvs_left_totality_extendedentriesdomain * pvs_right_totality_extendedentriesdomain -> pvs_left_totality_extendedentriesdomain = 1 \/ pvs_right_totality_extendedentriesdomain = 1) /\ (((~(pvs_exponent_totality_extendedentries = 0)) /\ (((((exists bpd_gap_pvs_totality_extendedentriesvaluation_selected_bound. bpd_gap_pvs_totality_extendedentriesvaluation_selected_bound + (pvs_exponent_totality_extendedentries) = (n)) /\ (exists bpvi_result_pvs_totality_extendedentriesvaluation_selected. ((exists bpvi_b_pvs_totality_extendedentriesvaluation_selected_power bpvi_c_pvs_totality_extendedentriesvaluation_selected_power. ((forall bpvi_i_pvs_totality_extendedentriesvaluation_selected_power. (exists bpvi_repeat_gap_pvs_totality_extendedentriesvaluation_selected_power. bpvi_repeat_gap_pvs_totality_extendedentriesvaluation_selected_power + S bpvi_i_pvs_totality_extendedentriesvaluation_selected_power = pvs_exponent_totality_extendedentries) -> (((exists bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_repeat. bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_repeat + S (pvs_prime_totality_extendedentries) = S ((S (bpvi_i_pvs_totality_extendedentriesvaluation_selected_power)) * bpvi_c_pvs_totality_extendedentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_repeat. bpvi_b_pvs_totality_extendedentriesvaluation_selected_power = bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_totality_extendedentriesvaluation_selected_power)) * bpvi_c_pvs_totality_extendedentriesvaluation_selected_power) + (pvs_prime_totality_extendedentries)))) /\ (exists bpvi_u_pvs_totality_extendedentriesvaluation_selected_power bpvi_v_pvs_totality_extendedentriesvaluation_selected_power. ((((exists bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_start. bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_totality_extendedentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_start. bpvi_u_pvs_totality_extendedentriesvaluation_selected_power = bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_totality_extendedentriesvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_terminal. bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_terminal + S (bpvi_result_pvs_totality_extendedentriesvaluation_selected) = S ((S (pvs_exponent_totality_extendedentries)) * bpvi_v_pvs_totality_extendedentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_terminal. bpvi_u_pvs_totality_extendedentriesvaluation_selected_power = bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_terminal * S ((S (pvs_exponent_totality_extendedentries)) * bpvi_v_pvs_totality_extendedentriesvaluation_selected_power) + (bpvi_result_pvs_totality_extendedentriesvaluation_selected))) /\ forall bpvi_j_pvs_totality_extendedentriesvaluation_selected_power. (exists bpvi_product_gap_pvs_totality_extendedentriesvaluation_selected_power. bpvi_product_gap_pvs_totality_extendedentriesvaluation_selected_power + S bpvi_j_pvs_totality_extendedentriesvaluation_selected_power = pvs_exponent_totality_extendedentries) -> exists bpvi_factor_pvs_totality_extendedentriesvaluation_selected_power bpvi_partial_pvs_totality_extendedentriesvaluation_selected_power bpvi_successor_pvs_totality_extendedentriesvaluation_selected_power. ((((exists bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_factor. bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_factor + S (bpvi_factor_pvs_totality_extendedentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_totality_extendedentriesvaluation_selected_power)) * bpvi_c_pvs_totality_extendedentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_factor. bpvi_b_pvs_totality_extendedentriesvaluation_selected_power = bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_factor * S ((S (bpvi_j_pvs_totality_extendedentriesvaluation_selected_power)) * bpvi_c_pvs_totality_extendedentriesvaluation_selected_power) + (bpvi_factor_pvs_totality_extendedentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_partial. bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_partial + S (bpvi_partial_pvs_totality_extendedentriesvaluation_selected_power) = S ((S (bpvi_j_pvs_totality_extendedentriesvaluation_selected_power)) * bpvi_v_pvs_totality_extendedentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_partial. bpvi_u_pvs_totality_extendedentriesvaluation_selected_power = bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_partial * S ((S (bpvi_j_pvs_totality_extendedentriesvaluation_selected_power)) * bpvi_v_pvs_totality_extendedentriesvaluation_selected_power) + (bpvi_partial_pvs_totality_extendedentriesvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_successor. bpvi_h_pvs_totality_extendedentriesvaluation_selected_power_successor + S (bpvi_successor_pvs_totality_extendedentriesvaluation_selected_power) = S ((S (S bpvi_j_pvs_totality_extendedentriesvaluation_selected_power)) * bpvi_v_pvs_totality_extendedentriesvaluation_selected_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_successor. bpvi_u_pvs_totality_extendedentriesvaluation_selected_power = bpvi_q_pvs_totality_extendedentriesvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_totality_extendedentriesvaluation_selected_power)) * bpvi_v_pvs_totality_extendedentriesvaluation_selected_power) + (bpvi_successor_pvs_totality_extendedentriesvaluation_selected_power))) /\ bpvi_successor_pvs_totality_extendedentriesvaluation_selected_power = bpvi_partial_pvs_totality_extendedentriesvaluation_selected_power * bpvi_factor_pvs_totality_extendedentriesvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_totality_extendedentriesvaluation_selected. n = bpvi_result_pvs_totality_extendedentriesvaluation_selected * bpvi_divisor_factor_pvs_totality_extendedentriesvaluation_selected))) /\ forall bpd_candidate_pvs_totality_extendedentriesvaluation. (exists bpd_gap_pvs_totality_extendedentriesvaluation_candidate_bound. bpd_gap_pvs_totality_extendedentriesvaluation_candidate_bound + (bpd_candidate_pvs_totality_extendedentriesvaluation) = (n)) -> (exists bpvi_result_pvs_totality_extendedentriesvaluation_candidate. ((exists bpvi_b_pvs_totality_extendedentriesvaluation_candidate_power bpvi_c_pvs_totality_extendedentriesvaluation_candidate_power. ((forall bpvi_i_pvs_totality_extendedentriesvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_totality_extendedentriesvaluation_candidate_power. bpvi_repeat_gap_pvs_totality_extendedentriesvaluation_candidate_power + S bpvi_i_pvs_totality_extendedentriesvaluation_candidate_power = bpd_candidate_pvs_totality_extendedentriesvaluation) -> (((exists bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_repeat. bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_repeat + S (pvs_prime_totality_extendedentries) = S ((S (bpvi_i_pvs_totality_extendedentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_extendedentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_repeat. bpvi_b_pvs_totality_extendedentriesvaluation_candidate_power = bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_totality_extendedentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_extendedentriesvaluation_candidate_power) + (pvs_prime_totality_extendedentries)))) /\ (exists bpvi_u_pvs_totality_extendedentriesvaluation_candidate_power bpvi_v_pvs_totality_extendedentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_start. bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_totality_extendedentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_start. bpvi_u_pvs_totality_extendedentriesvaluation_candidate_power = bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_totality_extendedentriesvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_terminal. bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_terminal + S (bpvi_result_pvs_totality_extendedentriesvaluation_candidate) = S ((S (bpd_candidate_pvs_totality_extendedentriesvaluation)) * bpvi_v_pvs_totality_extendedentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_terminal. bpvi_u_pvs_totality_extendedentriesvaluation_candidate_power = bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_totality_extendedentriesvaluation)) * bpvi_v_pvs_totality_extendedentriesvaluation_candidate_power) + (bpvi_result_pvs_totality_extendedentriesvaluation_candidate))) /\ forall bpvi_j_pvs_totality_extendedentriesvaluation_candidate_power. (exists bpvi_product_gap_pvs_totality_extendedentriesvaluation_candidate_power. bpvi_product_gap_pvs_totality_extendedentriesvaluation_candidate_power + S bpvi_j_pvs_totality_extendedentriesvaluation_candidate_power = bpd_candidate_pvs_totality_extendedentriesvaluation) -> exists bpvi_factor_pvs_totality_extendedentriesvaluation_candidate_power bpvi_partial_pvs_totality_extendedentriesvaluation_candidate_power bpvi_successor_pvs_totality_extendedentriesvaluation_candidate_power. ((((exists bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_factor. bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_factor + S (bpvi_factor_pvs_totality_extendedentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_totality_extendedentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_extendedentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_factor. bpvi_b_pvs_totality_extendedentriesvaluation_candidate_power = bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_totality_extendedentriesvaluation_candidate_power)) * bpvi_c_pvs_totality_extendedentriesvaluation_candidate_power) + (bpvi_factor_pvs_totality_extendedentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_partial. bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_partial + S (bpvi_partial_pvs_totality_extendedentriesvaluation_candidate_power) = S ((S (bpvi_j_pvs_totality_extendedentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_extendedentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_partial. bpvi_u_pvs_totality_extendedentriesvaluation_candidate_power = bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_totality_extendedentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_extendedentriesvaluation_candidate_power) + (bpvi_partial_pvs_totality_extendedentriesvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_successor. bpvi_h_pvs_totality_extendedentriesvaluation_candidate_power_successor + S (bpvi_successor_pvs_totality_extendedentriesvaluation_candidate_power) = S ((S (S bpvi_j_pvs_totality_extendedentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_extendedentriesvaluation_candidate_power)) /\ exists bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_successor. bpvi_u_pvs_totality_extendedentriesvaluation_candidate_power = bpvi_q_pvs_totality_extendedentriesvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_totality_extendedentriesvaluation_candidate_power)) * bpvi_v_pvs_totality_extendedentriesvaluation_candidate_power) + (bpvi_successor_pvs_totality_extendedentriesvaluation_candidate_power))) /\ bpvi_successor_pvs_totality_extendedentriesvaluation_candidate_power = bpvi_partial_pvs_totality_extendedentriesvaluation_candidate_power * bpvi_factor_pvs_totality_extendedentriesvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_totality_extendedentriesvaluation_candidate. n = bpvi_result_pvs_totality_extendedentriesvaluation_candidate * bpvi_divisor_factor_pvs_totality_extendedentriesvaluation_candidate)) -> (exists bpd_gap_pvs_totality_extendedentriesvaluation_maximal. bpd_gap_pvs_totality_extendedentriesvaluation_maximal + (bpd_candidate_pvs_totality_extendedentriesvaluation) = (pvs_exponent_totality_extendedentries))) /\ (exists pa_b_pvs_totality_extendedentriesvalue pa_c_pvs_totality_extendedentriesvalue. ((forall pa_i_pvs_totality_extendedentriesvalue_repeat. (exists pa_lt_pvs_totality_extendedentriesvalue_repeat_bound. pa_lt_pvs_totality_extendedentriesvalue_repeat_bound + S pa_i_pvs_totality_extendedentriesvalue_repeat = pvs_exponent_totality_extendedentries) -> (((exists pa_h_pvs_totality_extendedentriesvalue_repeat_decoded. pa_h_pvs_totality_extendedentriesvalue_repeat_decoded + S (pvs_prime_totality_extendedentries) = S ((S (pa_i_pvs_totality_extendedentriesvalue_repeat)) * pa_c_pvs_totality_extendedentriesvalue)) /\ exists pa_q_pvs_totality_extendedentriesvalue_repeat_decoded. pa_b_pvs_totality_extendedentriesvalue = pa_q_pvs_totality_extendedentriesvalue_repeat_decoded * S ((S (pa_i_pvs_totality_extendedentriesvalue_repeat)) * pa_c_pvs_totality_extendedentriesvalue) + (pvs_prime_totality_extendedentries)))) /\ (exists pa_u_pvs_totality_extendedentriesvalue_product pa_v_pvs_totality_extendedentriesvalue_product. ((((exists pa_h_pvs_totality_extendedentriesvalue_product_start. pa_h_pvs_totality_extendedentriesvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_totality_extendedentriesvalue_product)) /\ exists pa_q_pvs_totality_extendedentriesvalue_product_start. pa_u_pvs_totality_extendedentriesvalue_product = pa_q_pvs_totality_extendedentriesvalue_product_start * S ((S (0)) * pa_v_pvs_totality_extendedentriesvalue_product) + (1))) /\ ((((exists pa_h_pvs_totality_extendedentriesvalue_product_terminal. pa_h_pvs_totality_extendedentriesvalue_product_terminal + S (pvs_power_totality_extendedentries) = S ((S (pvs_exponent_totality_extendedentries)) * pa_v_pvs_totality_extendedentriesvalue_product)) /\ exists pa_q_pvs_totality_extendedentriesvalue_product_terminal. pa_u_pvs_totality_extendedentriesvalue_product = pa_q_pvs_totality_extendedentriesvalue_product_terminal * S ((S (pvs_exponent_totality_extendedentries)) * pa_v_pvs_totality_extendedentriesvalue_product) + (pvs_power_totality_extendedentries))) /\ forall pa_i_pvs_totality_extendedentriesvalue_product. (exists pa_lt_pvs_totality_extendedentriesvalue_product_bound. pa_lt_pvs_totality_extendedentriesvalue_product_bound + S pa_i_pvs_totality_extendedentriesvalue_product = pvs_exponent_totality_extendedentries) -> exists pa_p_pvs_totality_extendedentriesvalue_product pa_r_pvs_totality_extendedentriesvalue_product pa_s_pvs_totality_extendedentriesvalue_product. ((((exists pa_h_pvs_totality_extendedentriesvalue_product_factor. pa_h_pvs_totality_extendedentriesvalue_product_factor + S (pa_p_pvs_totality_extendedentriesvalue_product) = S ((S (pa_i_pvs_totality_extendedentriesvalue_product)) * pa_c_pvs_totality_extendedentriesvalue)) /\ exists pa_q_pvs_totality_extendedentriesvalue_product_factor. pa_b_pvs_totality_extendedentriesvalue = pa_q_pvs_totality_extendedentriesvalue_product_factor * S ((S (pa_i_pvs_totality_extendedentriesvalue_product)) * pa_c_pvs_totality_extendedentriesvalue) + (pa_p_pvs_totality_extendedentriesvalue_product))) /\ ((((exists pa_h_pvs_totality_extendedentriesvalue_product_partial. pa_h_pvs_totality_extendedentriesvalue_product_partial + S (pa_r_pvs_totality_extendedentriesvalue_product) = S ((S (pa_i_pvs_totality_extendedentriesvalue_product)) * pa_v_pvs_totality_extendedentriesvalue_product)) /\ exists pa_q_pvs_totality_extendedentriesvalue_product_partial. pa_u_pvs_totality_extendedentriesvalue_product = pa_q_pvs_totality_extendedentriesvalue_product_partial * S ((S (pa_i_pvs_totality_extendedentriesvalue_product)) * pa_v_pvs_totality_extendedentriesvalue_product) + (pa_r_pvs_totality_extendedentriesvalue_product))) /\ ((((exists pa_h_pvs_totality_extendedentriesvalue_product_successor. pa_h_pvs_totality_extendedentriesvalue_product_successor + S (pa_s_pvs_totality_extendedentriesvalue_product) = S ((S (S pa_i_pvs_totality_extendedentriesvalue_product)) * pa_v_pvs_totality_extendedentriesvalue_product)) /\ exists pa_q_pvs_totality_extendedentriesvalue_product_successor. pa_u_pvs_totality_extendedentriesvalue_product = pa_q_pvs_totality_extendedentriesvalue_product_successor * S ((S (S pa_i_pvs_totality_extendedentriesvalue_product)) * pa_v_pvs_totality_extendedentriesvalue_product) + (pa_s_pvs_totality_extendedentriesvalue_product))) /\ pa_s_pvs_totality_extendedentriesvalue_product = pa_r_pvs_totality_extendedentriesvalue_product * pa_p_pvs_totality_extendedentriesvalue_product))))))))))))))))))))) /\ (((forall pvs_divisor_totality_extendedcover. (~((pvs_divisor_totality_extendedcover) = 1) /\ forall pvs_left_totality_extendedcoverprime pvs_right_totality_extendedcoverprime. (pvs_divisor_totality_extendedcover) = pvs_left_totality_extendedcoverprime * pvs_right_totality_extendedcoverprime -> pvs_left_totality_extendedcoverprime = 1 \/ pvs_right_totality_extendedcoverprime = 1) -> (exists pvs_factor_totality_extendedcoverdivides. (n) = (pvs_divisor_totality_extendedcover) * pvs_factor_totality_extendedcoverdivides) -> exists pvs_position_totality_extendedcover. (exists pvs_gap_totality_extendedcoverbound. pvs_gap_totality_extendedcoverbound + S (pvs_position_totality_extendedcover) = (S x10)) /\ (((exists ff_h_pvs_totality_extendedcoverentry. ff_h_pvs_totality_extendedcoverentry + S (pvs_divisor_totality_extendedcover) = S ((S (pvs_position_totality_extendedcover)) * b)) /\ exists ff_q_pvs_totality_extendedcoverentry. a = ff_q_pvs_totality_extendedcoverentry * S ((S (pvs_position_totality_extendedcover)) * b) + (pvs_divisor_totality_extendedcover)))) /\ (exists ff_u_pvs_totality_extendedproduct ff_v_pvs_totality_extendedproduct. ((((exists ff_h_pvs_totality_extendedproduct_start. ff_h_pvs_totality_extendedproduct_start + S (1) = S ((S (0)) * ff_v_pvs_totality_extendedproduct)) /\ exists ff_q_pvs_totality_extendedproduct_start. ff_u_pvs_totality_extendedproduct = ff_q_pvs_totality_extendedproduct_start * S ((S (0)) * ff_v_pvs_totality_extendedproduct) + (1))) /\ ((((exists ff_h_pvs_totality_extendedproduct_terminal. ff_h_pvs_totality_extendedproduct_terminal + S (n) = S ((S (S x10)) * ff_v_pvs_totality_extendedproduct)) /\ exists ff_q_pvs_totality_extendedproduct_terminal. ff_u_pvs_totality_extendedproduct = ff_q_pvs_totality_extendedproduct_terminal * S ((S (S x10)) * ff_v_pvs_totality_extendedproduct) + (n))) /\ forall ff_i_pvs_totality_extendedproduct. (exists ff_lt_pvs_totality_extendedproduct_bound. ff_lt_pvs_totality_extendedproduct_bound + S ff_i_pvs_totality_extendedproduct = S x10) -> exists ff_p_pvs_totality_extendedproduct ff_r_pvs_totality_extendedproduct ff_s_pvs_totality_extendedproduct. ((((exists ff_h_pvs_totality_extendedproduct_factor. ff_h_pvs_totality_extendedproduct_factor + S (ff_p_pvs_totality_extendedproduct) = S ((S (ff_i_pvs_totality_extendedproduct)) * f)) /\ exists ff_q_pvs_totality_extendedproduct_factor. e = ff_q_pvs_totality_extendedproduct_factor * S ((S (ff_i_pvs_totality_extendedproduct)) * f) + (ff_p_pvs_totality_extendedproduct))) /\ ((((exists ff_h_pvs_totality_extendedproduct_partial. ff_h_pvs_totality_extendedproduct_partial + S (ff_r_pvs_totality_extendedproduct) = S ((S (ff_i_pvs_totality_extendedproduct)) * ff_v_pvs_totality_extendedproduct)) /\ exists ff_q_pvs_totality_extendedproduct_partial. ff_u_pvs_totality_extendedproduct = ff_q_pvs_totality_extendedproduct_partial * S ((S (ff_i_pvs_totality_extendedproduct)) * ff_v_pvs_totality_extendedproduct) + (ff_r_pvs_totality_extendedproduct))) /\ ((((exists ff_h_pvs_totality_extendedproduct_successor. ff_h_pvs_totality_extendedproduct_successor + S (ff_s_pvs_totality_extendedproduct) = S ((S (S ff_i_pvs_totality_extendedproduct)) * ff_v_pvs_totality_extendedproduct)) /\ exists ff_q_pvs_totality_extendedproduct_successor. ff_u_pvs_totality_extendedproduct = ff_q_pvs_totality_extendedproduct_successor * S ((S (S ff_i_pvs_totality_extendedproduct)) * ff_v_pvs_totality_extendedproduct) + (ff_s_pvs_totality_extendedproduct))) /\ ff_s_pvs_totality_extendedproduct = ff_r_pvs_totality_extendedproduct * ff_p_pvs_totality_extendedproduct))))))))))))))
  73. 0073specialize prime_valuation_support_append_full_power (n)
  74. 0074specialize prime_valuation_support_append_full_power (x3)
  75. 0075specialize prime_valuation_support_append_full_power (x)
  76. 0076specialize prime_valuation_support_append_full_power (x1)
  77. 0077specialize prime_valuation_support_append_full_power (x2)
  78. 0078specialize prime_valuation_support_append_full_power (x4)
  79. 0079specialize prime_valuation_support_append_full_power (x5)
  80. 0080specialize prime_valuation_support_append_full_power (x6)
  81. 0081specialize prime_valuation_support_append_full_power (x7)
  82. 0082specialize prime_valuation_support_append_full_power (x8)
  83. 0083specialize prime_valuation_support_append_full_power (x9)
  84. 0084specialize prime_valuation_support_append_full_power (x10)
  85. 0085apply prime_valuation_support_append_full_power
  86. 0086exact hn
  87. 0087exact hfactor_witness_witness_witness_witness_left
  88. 0088exact hfactor_witness_witness_witness_witness_right_left
  89. 0089exact hfactor_witness_witness_witness_witness_right_right_left
  90. 0090exact hfactor_witness_witness_witness_witness_right_right_right_left
  91. 0091exact hfactor_witness_witness_witness_witness_right_right_right_right_right_right_left
  92. 0092exact hfactor_witness_witness_witness_witness_right_right_right_right_left
  93. 0093exact hrec_witness_witness_witness_witness_witness_witness_witness
  94. 0094cases hextended
  95. 0095cases hextended_witness
  96. 0096cases hextended_witness_witness
  97. 0097cases hextended_witness_witness_witness
  98. 0098cases hextended_witness_witness_witness_witness
  99. 0099cases hextended_witness_witness_witness_witness_witness
  100. 0100exists x11
  101. 0101exists x12
  102. 0102exists x13
  103. 0103exists x14
  104. 0104exists x15
  105. 0105exists x16
  106. 0106exists S x10
  107. 0107exact hextended_witness_witness_witness_witness_witness_witness