PV0013

prime_valuation_support_bounded_exists

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

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

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.

This is a shared constructive tool, not an additional major blueprint goal. The list covers every prime divisor, has no repeated primes, and contains actual prime-power values. One uses the empty support; zero is excluded.

Exact theorem in conservative defined notation

∀ B. ∀ n. ¬n = 0 → Lt(n,B) → ∃ x. ∃ y. ∃ z. ∃ m. ∃ k. ∃ i. ∃ j. PrimeValuationSupport(n,x,y,z,m,k,i,j)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PrimeValuationSupport(n,pb,pc,eb,ec,vb,vc,l) · 3Lt(a,b) · 2Dvd(d,n) · 1Prime(p) · 1Pow(a,e,z) · 1BoundedPowerValuation(p,n,b,e) · 1

Actual proof prerequisites

factor_permutation_below_zero_impossible · checked external prerequisiteeq_decidable · checked external prerequisiteprime_valuation_support_value_eq_transportprime_valuation_support_oneprime_valuation_strict_cofactor_existslt_of_lt_of_le · checked external prerequisitele_of_succ_le_succ · checked external prerequisiteprime_valuation_support_append_full_power
Original expanded first-order 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)))))))))))))))

Complete tactic proof in conservative notation

All 107 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

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

Named ingredients (4)
prime valuation support value eq transportprime valuation support oneprime valuation strict cofactor existsprime valuation support append full power
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: Prime(p)BoundedPowerValuation(p,n,n,e)Pow(p,e,P)Dvd(p,u)Lt(u,n)Original native command in the exact edition
  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(x3,pb,pc,eb,ec,vb,vc,l)Original native command in the exact edition
  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(n,a,b,c,d,e,f,S x10)Original native command in the exact edition
  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 defined 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 : ∃ 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)))))))
  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 : ∃ pb. ∃ pc. ∃ eb. ∃ ec. ∃ vb. ∃ vc. ∃ l. PrimeValuationSupport(x3,pb,pc,eb,ec,vb,vc,l)
  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 : ∃ a. ∃ b. ∃ c. ∃ d. ∃ e. ∃ f. PrimeValuationSupport(n,a,b,c,d,e,f,S x10)
  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