PV000C

prime_exponent_entries_restore_prime_power

Restoring a removed full prime power preserves every old positive valuation, because its base prime is absent from the cofactor.

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

∀ n. ∀ u. ∀ p. ∀ k. ∀ P. ∀ pb. ∀ pc. ∀ eb. ∀ ec. ∀ vb. ∀ vc. ∀ l. Prime(p) → ¬u = 0 → n = P · u → Pow(p,k,P) → ¬Dvd(p,u) → PrimeExponentEntries(u,pb,pc,eb,ec,vb,vc,l) → PrimeExponentEntries(n,pb,pc,eb,ec,vb,vc,l)

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

Definition DAG

PrimeExponentEntries(n,pb,pc,eb,ec,vb,vc,l) · 2Dvd(d,n) · 2Prime(p) · 2BetaAt(b,c,i,x) · 3Pow(a,e,z) · 2BoundedPowerValuation(p,n,b,e) · 1

Actual proof prerequisites

power_valuation_nonzero_exponent_divides_base · checked external prerequisitepower_valuation_value_eq_transport · checked external prerequisiteprime_valuation_strip_other_prime
Original expanded first-order statement 
forall n u p k P pb pc eb ec vb vc l. (~((p) = 1) /\ forall pvs_left_restore_domain pvs_right_restore_domain. (p) = pvs_left_restore_domain * pvs_right_restore_domain -> pvs_left_restore_domain = 1 \/ pvs_right_restore_domain = 1) -> ~(u = 0) -> n = P * u -> (exists pa_b_pvs_restore_power pa_c_pvs_restore_power. ((forall pa_i_pvs_restore_power_repeat. (exists pa_lt_pvs_restore_power_repeat_bound. pa_lt_pvs_restore_power_repeat_bound + S pa_i_pvs_restore_power_repeat = k) -> (((exists pa_h_pvs_restore_power_repeat_decoded. pa_h_pvs_restore_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_restore_power_repeat)) * pa_c_pvs_restore_power)) /\ exists pa_q_pvs_restore_power_repeat_decoded. pa_b_pvs_restore_power = pa_q_pvs_restore_power_repeat_decoded * S ((S (pa_i_pvs_restore_power_repeat)) * pa_c_pvs_restore_power) + (p)))) /\ (exists pa_u_pvs_restore_power_product pa_v_pvs_restore_power_product. ((((exists pa_h_pvs_restore_power_product_start. pa_h_pvs_restore_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_restore_power_product)) /\ exists pa_q_pvs_restore_power_product_start. pa_u_pvs_restore_power_product = pa_q_pvs_restore_power_product_start * S ((S (0)) * pa_v_pvs_restore_power_product) + (1))) /\ ((((exists pa_h_pvs_restore_power_product_terminal. pa_h_pvs_restore_power_product_terminal + S (P) = S ((S (k)) * pa_v_pvs_restore_power_product)) /\ exists pa_q_pvs_restore_power_product_terminal. pa_u_pvs_restore_power_product = pa_q_pvs_restore_power_product_terminal * S ((S (k)) * pa_v_pvs_restore_power_product) + (P))) /\ forall pa_i_pvs_restore_power_product. (exists pa_lt_pvs_restore_power_product_bound. pa_lt_pvs_restore_power_product_bound + S pa_i_pvs_restore_power_product = k) -> exists pa_p_pvs_restore_power_product pa_r_pvs_restore_power_product pa_s_pvs_restore_power_product. ((((exists pa_h_pvs_restore_power_product_factor. pa_h_pvs_restore_power_product_factor + S (pa_p_pvs_restore_power_product) = S ((S (pa_i_pvs_restore_power_product)) * pa_c_pvs_restore_power)) /\ exists pa_q_pvs_restore_power_product_factor. pa_b_pvs_restore_power = pa_q_pvs_restore_power_product_factor * S ((S (pa_i_pvs_restore_power_product)) * pa_c_pvs_restore_power) + (pa_p_pvs_restore_power_product))) /\ ((((exists pa_h_pvs_restore_power_product_partial. pa_h_pvs_restore_power_product_partial + S (pa_r_pvs_restore_power_product) = S ((S (pa_i_pvs_restore_power_product)) * pa_v_pvs_restore_power_product)) /\ exists pa_q_pvs_restore_power_product_partial. pa_u_pvs_restore_power_product = pa_q_pvs_restore_power_product_partial * S ((S (pa_i_pvs_restore_power_product)) * pa_v_pvs_restore_power_product) + (pa_r_pvs_restore_power_product))) /\ ((((exists pa_h_pvs_restore_power_product_successor. pa_h_pvs_restore_power_product_successor + S (pa_s_pvs_restore_power_product) = S ((S (S pa_i_pvs_restore_power_product)) * pa_v_pvs_restore_power_product)) /\ exists pa_q_pvs_restore_power_product_successor. pa_u_pvs_restore_power_product = pa_q_pvs_restore_power_product_successor * S ((S (S pa_i_pvs_restore_power_product)) * pa_v_pvs_restore_power_product) + (pa_s_pvs_restore_power_product))) /\ pa_s_pvs_restore_power_product = pa_r_pvs_restore_power_product * pa_p_pvs_restore_power_product)))))))) -> ~(exists pvs_factor_restore_fresh. (u) = (p) * pvs_factor_restore_fresh) -> (forall pvs_index_restore_source. (exists pvs_gap_restore_sourceindex. pvs_gap_restore_sourceindex + S (pvs_index_restore_source) = (l)) -> exists pvs_prime_restore_source pvs_exponent_restore_source pvs_power_restore_source. (((((exists ff_h_pvs_restore_sourceprime. ff_h_pvs_restore_sourceprime + S (pvs_prime_restore_source) = S ((S (pvs_index_restore_source)) * pc)) /\ exists ff_q_pvs_restore_sourceprime. pb = ff_q_pvs_restore_sourceprime * S ((S (pvs_index_restore_source)) * pc) + (pvs_prime_restore_source))) /\ (((((exists ff_h_pvs_restore_sourceexponent. ff_h_pvs_restore_sourceexponent + S (pvs_exponent_restore_source) = S ((S (pvs_index_restore_source)) * ec)) /\ exists ff_q_pvs_restore_sourceexponent. eb = ff_q_pvs_restore_sourceexponent * S ((S (pvs_index_restore_source)) * ec) + (pvs_exponent_restore_source))) /\ (((((exists ff_h_pvs_restore_sourcepower. ff_h_pvs_restore_sourcepower + S (pvs_power_restore_source) = S ((S (pvs_index_restore_source)) * vc)) /\ exists ff_q_pvs_restore_sourcepower. vb = ff_q_pvs_restore_sourcepower * S ((S (pvs_index_restore_source)) * vc) + (pvs_power_restore_source))) /\ (((~((pvs_prime_restore_source) = 1) /\ forall pvs_left_restore_sourcedomain pvs_right_restore_sourcedomain. (pvs_prime_restore_source) = pvs_left_restore_sourcedomain * pvs_right_restore_sourcedomain -> pvs_left_restore_sourcedomain = 1 \/ pvs_right_restore_sourcedomain = 1) /\ (((~(pvs_exponent_restore_source = 0)) /\ (((((exists bpd_gap_pvs_restore_sourcevaluation_selected_bound. bpd_gap_pvs_restore_sourcevaluation_selected_bound + (pvs_exponent_restore_source) = (u)) /\ (exists bpvi_result_pvs_restore_sourcevaluation_selected. ((exists bpvi_b_pvs_restore_sourcevaluation_selected_power bpvi_c_pvs_restore_sourcevaluation_selected_power. ((forall bpvi_i_pvs_restore_sourcevaluation_selected_power. (exists bpvi_repeat_gap_pvs_restore_sourcevaluation_selected_power. bpvi_repeat_gap_pvs_restore_sourcevaluation_selected_power + S bpvi_i_pvs_restore_sourcevaluation_selected_power = pvs_exponent_restore_source) -> (((exists bpvi_h_pvs_restore_sourcevaluation_selected_power_repeat. bpvi_h_pvs_restore_sourcevaluation_selected_power_repeat + S (pvs_prime_restore_source) = S ((S (bpvi_i_pvs_restore_sourcevaluation_selected_power)) * bpvi_c_pvs_restore_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_selected_power_repeat. bpvi_b_pvs_restore_sourcevaluation_selected_power = bpvi_q_pvs_restore_sourcevaluation_selected_power_repeat * S ((S (bpvi_i_pvs_restore_sourcevaluation_selected_power)) * bpvi_c_pvs_restore_sourcevaluation_selected_power) + (pvs_prime_restore_source)))) /\ (exists bpvi_u_pvs_restore_sourcevaluation_selected_power bpvi_v_pvs_restore_sourcevaluation_selected_power. ((((exists bpvi_h_pvs_restore_sourcevaluation_selected_power_start. bpvi_h_pvs_restore_sourcevaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_restore_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_selected_power_start. bpvi_u_pvs_restore_sourcevaluation_selected_power = bpvi_q_pvs_restore_sourcevaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_restore_sourcevaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_restore_sourcevaluation_selected_power_terminal. bpvi_h_pvs_restore_sourcevaluation_selected_power_terminal + S (bpvi_result_pvs_restore_sourcevaluation_selected) = S ((S (pvs_exponent_restore_source)) * bpvi_v_pvs_restore_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_selected_power_terminal. bpvi_u_pvs_restore_sourcevaluation_selected_power = bpvi_q_pvs_restore_sourcevaluation_selected_power_terminal * S ((S (pvs_exponent_restore_source)) * bpvi_v_pvs_restore_sourcevaluation_selected_power) + (bpvi_result_pvs_restore_sourcevaluation_selected))) /\ forall bpvi_j_pvs_restore_sourcevaluation_selected_power. (exists bpvi_product_gap_pvs_restore_sourcevaluation_selected_power. bpvi_product_gap_pvs_restore_sourcevaluation_selected_power + S bpvi_j_pvs_restore_sourcevaluation_selected_power = pvs_exponent_restore_source) -> exists bpvi_factor_pvs_restore_sourcevaluation_selected_power bpvi_partial_pvs_restore_sourcevaluation_selected_power bpvi_successor_pvs_restore_sourcevaluation_selected_power. ((((exists bpvi_h_pvs_restore_sourcevaluation_selected_power_factor. bpvi_h_pvs_restore_sourcevaluation_selected_power_factor + S (bpvi_factor_pvs_restore_sourcevaluation_selected_power) = S ((S (bpvi_j_pvs_restore_sourcevaluation_selected_power)) * bpvi_c_pvs_restore_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_selected_power_factor. bpvi_b_pvs_restore_sourcevaluation_selected_power = bpvi_q_pvs_restore_sourcevaluation_selected_power_factor * S ((S (bpvi_j_pvs_restore_sourcevaluation_selected_power)) * bpvi_c_pvs_restore_sourcevaluation_selected_power) + (bpvi_factor_pvs_restore_sourcevaluation_selected_power))) /\ ((((exists bpvi_h_pvs_restore_sourcevaluation_selected_power_partial. bpvi_h_pvs_restore_sourcevaluation_selected_power_partial + S (bpvi_partial_pvs_restore_sourcevaluation_selected_power) = S ((S (bpvi_j_pvs_restore_sourcevaluation_selected_power)) * bpvi_v_pvs_restore_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_selected_power_partial. bpvi_u_pvs_restore_sourcevaluation_selected_power = bpvi_q_pvs_restore_sourcevaluation_selected_power_partial * S ((S (bpvi_j_pvs_restore_sourcevaluation_selected_power)) * bpvi_v_pvs_restore_sourcevaluation_selected_power) + (bpvi_partial_pvs_restore_sourcevaluation_selected_power))) /\ ((((exists bpvi_h_pvs_restore_sourcevaluation_selected_power_successor. bpvi_h_pvs_restore_sourcevaluation_selected_power_successor + S (bpvi_successor_pvs_restore_sourcevaluation_selected_power) = S ((S (S bpvi_j_pvs_restore_sourcevaluation_selected_power)) * bpvi_v_pvs_restore_sourcevaluation_selected_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_selected_power_successor. bpvi_u_pvs_restore_sourcevaluation_selected_power = bpvi_q_pvs_restore_sourcevaluation_selected_power_successor * S ((S (S bpvi_j_pvs_restore_sourcevaluation_selected_power)) * bpvi_v_pvs_restore_sourcevaluation_selected_power) + (bpvi_successor_pvs_restore_sourcevaluation_selected_power))) /\ bpvi_successor_pvs_restore_sourcevaluation_selected_power = bpvi_partial_pvs_restore_sourcevaluation_selected_power * bpvi_factor_pvs_restore_sourcevaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_restore_sourcevaluation_selected. u = bpvi_result_pvs_restore_sourcevaluation_selected * bpvi_divisor_factor_pvs_restore_sourcevaluation_selected))) /\ forall bpd_candidate_pvs_restore_sourcevaluation. (exists bpd_gap_pvs_restore_sourcevaluation_candidate_bound. bpd_gap_pvs_restore_sourcevaluation_candidate_bound + (bpd_candidate_pvs_restore_sourcevaluation) = (u)) -> (exists bpvi_result_pvs_restore_sourcevaluation_candidate. ((exists bpvi_b_pvs_restore_sourcevaluation_candidate_power bpvi_c_pvs_restore_sourcevaluation_candidate_power. ((forall bpvi_i_pvs_restore_sourcevaluation_candidate_power. (exists bpvi_repeat_gap_pvs_restore_sourcevaluation_candidate_power. bpvi_repeat_gap_pvs_restore_sourcevaluation_candidate_power + S bpvi_i_pvs_restore_sourcevaluation_candidate_power = bpd_candidate_pvs_restore_sourcevaluation) -> (((exists bpvi_h_pvs_restore_sourcevaluation_candidate_power_repeat. bpvi_h_pvs_restore_sourcevaluation_candidate_power_repeat + S (pvs_prime_restore_source) = S ((S (bpvi_i_pvs_restore_sourcevaluation_candidate_power)) * bpvi_c_pvs_restore_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_candidate_power_repeat. bpvi_b_pvs_restore_sourcevaluation_candidate_power = bpvi_q_pvs_restore_sourcevaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_restore_sourcevaluation_candidate_power)) * bpvi_c_pvs_restore_sourcevaluation_candidate_power) + (pvs_prime_restore_source)))) /\ (exists bpvi_u_pvs_restore_sourcevaluation_candidate_power bpvi_v_pvs_restore_sourcevaluation_candidate_power. ((((exists bpvi_h_pvs_restore_sourcevaluation_candidate_power_start. bpvi_h_pvs_restore_sourcevaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_restore_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_candidate_power_start. bpvi_u_pvs_restore_sourcevaluation_candidate_power = bpvi_q_pvs_restore_sourcevaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_restore_sourcevaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_restore_sourcevaluation_candidate_power_terminal. bpvi_h_pvs_restore_sourcevaluation_candidate_power_terminal + S (bpvi_result_pvs_restore_sourcevaluation_candidate) = S ((S (bpd_candidate_pvs_restore_sourcevaluation)) * bpvi_v_pvs_restore_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_candidate_power_terminal. bpvi_u_pvs_restore_sourcevaluation_candidate_power = bpvi_q_pvs_restore_sourcevaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_restore_sourcevaluation)) * bpvi_v_pvs_restore_sourcevaluation_candidate_power) + (bpvi_result_pvs_restore_sourcevaluation_candidate))) /\ forall bpvi_j_pvs_restore_sourcevaluation_candidate_power. (exists bpvi_product_gap_pvs_restore_sourcevaluation_candidate_power. bpvi_product_gap_pvs_restore_sourcevaluation_candidate_power + S bpvi_j_pvs_restore_sourcevaluation_candidate_power = bpd_candidate_pvs_restore_sourcevaluation) -> exists bpvi_factor_pvs_restore_sourcevaluation_candidate_power bpvi_partial_pvs_restore_sourcevaluation_candidate_power bpvi_successor_pvs_restore_sourcevaluation_candidate_power. ((((exists bpvi_h_pvs_restore_sourcevaluation_candidate_power_factor. bpvi_h_pvs_restore_sourcevaluation_candidate_power_factor + S (bpvi_factor_pvs_restore_sourcevaluation_candidate_power) = S ((S (bpvi_j_pvs_restore_sourcevaluation_candidate_power)) * bpvi_c_pvs_restore_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_candidate_power_factor. bpvi_b_pvs_restore_sourcevaluation_candidate_power = bpvi_q_pvs_restore_sourcevaluation_candidate_power_factor * S ((S (bpvi_j_pvs_restore_sourcevaluation_candidate_power)) * bpvi_c_pvs_restore_sourcevaluation_candidate_power) + (bpvi_factor_pvs_restore_sourcevaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_restore_sourcevaluation_candidate_power_partial. bpvi_h_pvs_restore_sourcevaluation_candidate_power_partial + S (bpvi_partial_pvs_restore_sourcevaluation_candidate_power) = S ((S (bpvi_j_pvs_restore_sourcevaluation_candidate_power)) * bpvi_v_pvs_restore_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_candidate_power_partial. bpvi_u_pvs_restore_sourcevaluation_candidate_power = bpvi_q_pvs_restore_sourcevaluation_candidate_power_partial * S ((S (bpvi_j_pvs_restore_sourcevaluation_candidate_power)) * bpvi_v_pvs_restore_sourcevaluation_candidate_power) + (bpvi_partial_pvs_restore_sourcevaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_restore_sourcevaluation_candidate_power_successor. bpvi_h_pvs_restore_sourcevaluation_candidate_power_successor + S (bpvi_successor_pvs_restore_sourcevaluation_candidate_power) = S ((S (S bpvi_j_pvs_restore_sourcevaluation_candidate_power)) * bpvi_v_pvs_restore_sourcevaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_sourcevaluation_candidate_power_successor. bpvi_u_pvs_restore_sourcevaluation_candidate_power = bpvi_q_pvs_restore_sourcevaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_restore_sourcevaluation_candidate_power)) * bpvi_v_pvs_restore_sourcevaluation_candidate_power) + (bpvi_successor_pvs_restore_sourcevaluation_candidate_power))) /\ bpvi_successor_pvs_restore_sourcevaluation_candidate_power = bpvi_partial_pvs_restore_sourcevaluation_candidate_power * bpvi_factor_pvs_restore_sourcevaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_restore_sourcevaluation_candidate. u = bpvi_result_pvs_restore_sourcevaluation_candidate * bpvi_divisor_factor_pvs_restore_sourcevaluation_candidate)) -> (exists bpd_gap_pvs_restore_sourcevaluation_maximal. bpd_gap_pvs_restore_sourcevaluation_maximal + (bpd_candidate_pvs_restore_sourcevaluation) = (pvs_exponent_restore_source))) /\ (exists pa_b_pvs_restore_sourcevalue pa_c_pvs_restore_sourcevalue. ((forall pa_i_pvs_restore_sourcevalue_repeat. (exists pa_lt_pvs_restore_sourcevalue_repeat_bound. pa_lt_pvs_restore_sourcevalue_repeat_bound + S pa_i_pvs_restore_sourcevalue_repeat = pvs_exponent_restore_source) -> (((exists pa_h_pvs_restore_sourcevalue_repeat_decoded. pa_h_pvs_restore_sourcevalue_repeat_decoded + S (pvs_prime_restore_source) = S ((S (pa_i_pvs_restore_sourcevalue_repeat)) * pa_c_pvs_restore_sourcevalue)) /\ exists pa_q_pvs_restore_sourcevalue_repeat_decoded. pa_b_pvs_restore_sourcevalue = pa_q_pvs_restore_sourcevalue_repeat_decoded * S ((S (pa_i_pvs_restore_sourcevalue_repeat)) * pa_c_pvs_restore_sourcevalue) + (pvs_prime_restore_source)))) /\ (exists pa_u_pvs_restore_sourcevalue_product pa_v_pvs_restore_sourcevalue_product. ((((exists pa_h_pvs_restore_sourcevalue_product_start. pa_h_pvs_restore_sourcevalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_restore_sourcevalue_product)) /\ exists pa_q_pvs_restore_sourcevalue_product_start. pa_u_pvs_restore_sourcevalue_product = pa_q_pvs_restore_sourcevalue_product_start * S ((S (0)) * pa_v_pvs_restore_sourcevalue_product) + (1))) /\ ((((exists pa_h_pvs_restore_sourcevalue_product_terminal. pa_h_pvs_restore_sourcevalue_product_terminal + S (pvs_power_restore_source) = S ((S (pvs_exponent_restore_source)) * pa_v_pvs_restore_sourcevalue_product)) /\ exists pa_q_pvs_restore_sourcevalue_product_terminal. pa_u_pvs_restore_sourcevalue_product = pa_q_pvs_restore_sourcevalue_product_terminal * S ((S (pvs_exponent_restore_source)) * pa_v_pvs_restore_sourcevalue_product) + (pvs_power_restore_source))) /\ forall pa_i_pvs_restore_sourcevalue_product. (exists pa_lt_pvs_restore_sourcevalue_product_bound. pa_lt_pvs_restore_sourcevalue_product_bound + S pa_i_pvs_restore_sourcevalue_product = pvs_exponent_restore_source) -> exists pa_p_pvs_restore_sourcevalue_product pa_r_pvs_restore_sourcevalue_product pa_s_pvs_restore_sourcevalue_product. ((((exists pa_h_pvs_restore_sourcevalue_product_factor. pa_h_pvs_restore_sourcevalue_product_factor + S (pa_p_pvs_restore_sourcevalue_product) = S ((S (pa_i_pvs_restore_sourcevalue_product)) * pa_c_pvs_restore_sourcevalue)) /\ exists pa_q_pvs_restore_sourcevalue_product_factor. pa_b_pvs_restore_sourcevalue = pa_q_pvs_restore_sourcevalue_product_factor * S ((S (pa_i_pvs_restore_sourcevalue_product)) * pa_c_pvs_restore_sourcevalue) + (pa_p_pvs_restore_sourcevalue_product))) /\ ((((exists pa_h_pvs_restore_sourcevalue_product_partial. pa_h_pvs_restore_sourcevalue_product_partial + S (pa_r_pvs_restore_sourcevalue_product) = S ((S (pa_i_pvs_restore_sourcevalue_product)) * pa_v_pvs_restore_sourcevalue_product)) /\ exists pa_q_pvs_restore_sourcevalue_product_partial. pa_u_pvs_restore_sourcevalue_product = pa_q_pvs_restore_sourcevalue_product_partial * S ((S (pa_i_pvs_restore_sourcevalue_product)) * pa_v_pvs_restore_sourcevalue_product) + (pa_r_pvs_restore_sourcevalue_product))) /\ ((((exists pa_h_pvs_restore_sourcevalue_product_successor. pa_h_pvs_restore_sourcevalue_product_successor + S (pa_s_pvs_restore_sourcevalue_product) = S ((S (S pa_i_pvs_restore_sourcevalue_product)) * pa_v_pvs_restore_sourcevalue_product)) /\ exists pa_q_pvs_restore_sourcevalue_product_successor. pa_u_pvs_restore_sourcevalue_product = pa_q_pvs_restore_sourcevalue_product_successor * S ((S (S pa_i_pvs_restore_sourcevalue_product)) * pa_v_pvs_restore_sourcevalue_product) + (pa_s_pvs_restore_sourcevalue_product))) /\ pa_s_pvs_restore_sourcevalue_product = pa_r_pvs_restore_sourcevalue_product * pa_p_pvs_restore_sourcevalue_product))))))))))))))))))))) -> (forall pvs_index_restore_target. (exists pvs_gap_restore_targetindex. pvs_gap_restore_targetindex + S (pvs_index_restore_target) = (l)) -> exists pvs_prime_restore_target pvs_exponent_restore_target pvs_power_restore_target. (((((exists ff_h_pvs_restore_targetprime. ff_h_pvs_restore_targetprime + S (pvs_prime_restore_target) = S ((S (pvs_index_restore_target)) * pc)) /\ exists ff_q_pvs_restore_targetprime. pb = ff_q_pvs_restore_targetprime * S ((S (pvs_index_restore_target)) * pc) + (pvs_prime_restore_target))) /\ (((((exists ff_h_pvs_restore_targetexponent. ff_h_pvs_restore_targetexponent + S (pvs_exponent_restore_target) = S ((S (pvs_index_restore_target)) * ec)) /\ exists ff_q_pvs_restore_targetexponent. eb = ff_q_pvs_restore_targetexponent * S ((S (pvs_index_restore_target)) * ec) + (pvs_exponent_restore_target))) /\ (((((exists ff_h_pvs_restore_targetpower. ff_h_pvs_restore_targetpower + S (pvs_power_restore_target) = S ((S (pvs_index_restore_target)) * vc)) /\ exists ff_q_pvs_restore_targetpower. vb = ff_q_pvs_restore_targetpower * S ((S (pvs_index_restore_target)) * vc) + (pvs_power_restore_target))) /\ (((~((pvs_prime_restore_target) = 1) /\ forall pvs_left_restore_targetdomain pvs_right_restore_targetdomain. (pvs_prime_restore_target) = pvs_left_restore_targetdomain * pvs_right_restore_targetdomain -> pvs_left_restore_targetdomain = 1 \/ pvs_right_restore_targetdomain = 1) /\ (((~(pvs_exponent_restore_target = 0)) /\ (((((exists bpd_gap_pvs_restore_targetvaluation_selected_bound. bpd_gap_pvs_restore_targetvaluation_selected_bound + (pvs_exponent_restore_target) = (n)) /\ (exists bpvi_result_pvs_restore_targetvaluation_selected. ((exists bpvi_b_pvs_restore_targetvaluation_selected_power bpvi_c_pvs_restore_targetvaluation_selected_power. ((forall bpvi_i_pvs_restore_targetvaluation_selected_power. (exists bpvi_repeat_gap_pvs_restore_targetvaluation_selected_power. bpvi_repeat_gap_pvs_restore_targetvaluation_selected_power + S bpvi_i_pvs_restore_targetvaluation_selected_power = pvs_exponent_restore_target) -> (((exists bpvi_h_pvs_restore_targetvaluation_selected_power_repeat. bpvi_h_pvs_restore_targetvaluation_selected_power_repeat + S (pvs_prime_restore_target) = S ((S (bpvi_i_pvs_restore_targetvaluation_selected_power)) * bpvi_c_pvs_restore_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_selected_power_repeat. bpvi_b_pvs_restore_targetvaluation_selected_power = bpvi_q_pvs_restore_targetvaluation_selected_power_repeat * S ((S (bpvi_i_pvs_restore_targetvaluation_selected_power)) * bpvi_c_pvs_restore_targetvaluation_selected_power) + (pvs_prime_restore_target)))) /\ (exists bpvi_u_pvs_restore_targetvaluation_selected_power bpvi_v_pvs_restore_targetvaluation_selected_power. ((((exists bpvi_h_pvs_restore_targetvaluation_selected_power_start. bpvi_h_pvs_restore_targetvaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_restore_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_selected_power_start. bpvi_u_pvs_restore_targetvaluation_selected_power = bpvi_q_pvs_restore_targetvaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_restore_targetvaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_restore_targetvaluation_selected_power_terminal. bpvi_h_pvs_restore_targetvaluation_selected_power_terminal + S (bpvi_result_pvs_restore_targetvaluation_selected) = S ((S (pvs_exponent_restore_target)) * bpvi_v_pvs_restore_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_selected_power_terminal. bpvi_u_pvs_restore_targetvaluation_selected_power = bpvi_q_pvs_restore_targetvaluation_selected_power_terminal * S ((S (pvs_exponent_restore_target)) * bpvi_v_pvs_restore_targetvaluation_selected_power) + (bpvi_result_pvs_restore_targetvaluation_selected))) /\ forall bpvi_j_pvs_restore_targetvaluation_selected_power. (exists bpvi_product_gap_pvs_restore_targetvaluation_selected_power. bpvi_product_gap_pvs_restore_targetvaluation_selected_power + S bpvi_j_pvs_restore_targetvaluation_selected_power = pvs_exponent_restore_target) -> exists bpvi_factor_pvs_restore_targetvaluation_selected_power bpvi_partial_pvs_restore_targetvaluation_selected_power bpvi_successor_pvs_restore_targetvaluation_selected_power. ((((exists bpvi_h_pvs_restore_targetvaluation_selected_power_factor. bpvi_h_pvs_restore_targetvaluation_selected_power_factor + S (bpvi_factor_pvs_restore_targetvaluation_selected_power) = S ((S (bpvi_j_pvs_restore_targetvaluation_selected_power)) * bpvi_c_pvs_restore_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_selected_power_factor. bpvi_b_pvs_restore_targetvaluation_selected_power = bpvi_q_pvs_restore_targetvaluation_selected_power_factor * S ((S (bpvi_j_pvs_restore_targetvaluation_selected_power)) * bpvi_c_pvs_restore_targetvaluation_selected_power) + (bpvi_factor_pvs_restore_targetvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_restore_targetvaluation_selected_power_partial. bpvi_h_pvs_restore_targetvaluation_selected_power_partial + S (bpvi_partial_pvs_restore_targetvaluation_selected_power) = S ((S (bpvi_j_pvs_restore_targetvaluation_selected_power)) * bpvi_v_pvs_restore_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_selected_power_partial. bpvi_u_pvs_restore_targetvaluation_selected_power = bpvi_q_pvs_restore_targetvaluation_selected_power_partial * S ((S (bpvi_j_pvs_restore_targetvaluation_selected_power)) * bpvi_v_pvs_restore_targetvaluation_selected_power) + (bpvi_partial_pvs_restore_targetvaluation_selected_power))) /\ ((((exists bpvi_h_pvs_restore_targetvaluation_selected_power_successor. bpvi_h_pvs_restore_targetvaluation_selected_power_successor + S (bpvi_successor_pvs_restore_targetvaluation_selected_power) = S ((S (S bpvi_j_pvs_restore_targetvaluation_selected_power)) * bpvi_v_pvs_restore_targetvaluation_selected_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_selected_power_successor. bpvi_u_pvs_restore_targetvaluation_selected_power = bpvi_q_pvs_restore_targetvaluation_selected_power_successor * S ((S (S bpvi_j_pvs_restore_targetvaluation_selected_power)) * bpvi_v_pvs_restore_targetvaluation_selected_power) + (bpvi_successor_pvs_restore_targetvaluation_selected_power))) /\ bpvi_successor_pvs_restore_targetvaluation_selected_power = bpvi_partial_pvs_restore_targetvaluation_selected_power * bpvi_factor_pvs_restore_targetvaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_restore_targetvaluation_selected. n = bpvi_result_pvs_restore_targetvaluation_selected * bpvi_divisor_factor_pvs_restore_targetvaluation_selected))) /\ forall bpd_candidate_pvs_restore_targetvaluation. (exists bpd_gap_pvs_restore_targetvaluation_candidate_bound. bpd_gap_pvs_restore_targetvaluation_candidate_bound + (bpd_candidate_pvs_restore_targetvaluation) = (n)) -> (exists bpvi_result_pvs_restore_targetvaluation_candidate. ((exists bpvi_b_pvs_restore_targetvaluation_candidate_power bpvi_c_pvs_restore_targetvaluation_candidate_power. ((forall bpvi_i_pvs_restore_targetvaluation_candidate_power. (exists bpvi_repeat_gap_pvs_restore_targetvaluation_candidate_power. bpvi_repeat_gap_pvs_restore_targetvaluation_candidate_power + S bpvi_i_pvs_restore_targetvaluation_candidate_power = bpd_candidate_pvs_restore_targetvaluation) -> (((exists bpvi_h_pvs_restore_targetvaluation_candidate_power_repeat. bpvi_h_pvs_restore_targetvaluation_candidate_power_repeat + S (pvs_prime_restore_target) = S ((S (bpvi_i_pvs_restore_targetvaluation_candidate_power)) * bpvi_c_pvs_restore_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_candidate_power_repeat. bpvi_b_pvs_restore_targetvaluation_candidate_power = bpvi_q_pvs_restore_targetvaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_restore_targetvaluation_candidate_power)) * bpvi_c_pvs_restore_targetvaluation_candidate_power) + (pvs_prime_restore_target)))) /\ (exists bpvi_u_pvs_restore_targetvaluation_candidate_power bpvi_v_pvs_restore_targetvaluation_candidate_power. ((((exists bpvi_h_pvs_restore_targetvaluation_candidate_power_start. bpvi_h_pvs_restore_targetvaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_restore_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_candidate_power_start. bpvi_u_pvs_restore_targetvaluation_candidate_power = bpvi_q_pvs_restore_targetvaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_restore_targetvaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_restore_targetvaluation_candidate_power_terminal. bpvi_h_pvs_restore_targetvaluation_candidate_power_terminal + S (bpvi_result_pvs_restore_targetvaluation_candidate) = S ((S (bpd_candidate_pvs_restore_targetvaluation)) * bpvi_v_pvs_restore_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_candidate_power_terminal. bpvi_u_pvs_restore_targetvaluation_candidate_power = bpvi_q_pvs_restore_targetvaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_restore_targetvaluation)) * bpvi_v_pvs_restore_targetvaluation_candidate_power) + (bpvi_result_pvs_restore_targetvaluation_candidate))) /\ forall bpvi_j_pvs_restore_targetvaluation_candidate_power. (exists bpvi_product_gap_pvs_restore_targetvaluation_candidate_power. bpvi_product_gap_pvs_restore_targetvaluation_candidate_power + S bpvi_j_pvs_restore_targetvaluation_candidate_power = bpd_candidate_pvs_restore_targetvaluation) -> exists bpvi_factor_pvs_restore_targetvaluation_candidate_power bpvi_partial_pvs_restore_targetvaluation_candidate_power bpvi_successor_pvs_restore_targetvaluation_candidate_power. ((((exists bpvi_h_pvs_restore_targetvaluation_candidate_power_factor. bpvi_h_pvs_restore_targetvaluation_candidate_power_factor + S (bpvi_factor_pvs_restore_targetvaluation_candidate_power) = S ((S (bpvi_j_pvs_restore_targetvaluation_candidate_power)) * bpvi_c_pvs_restore_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_candidate_power_factor. bpvi_b_pvs_restore_targetvaluation_candidate_power = bpvi_q_pvs_restore_targetvaluation_candidate_power_factor * S ((S (bpvi_j_pvs_restore_targetvaluation_candidate_power)) * bpvi_c_pvs_restore_targetvaluation_candidate_power) + (bpvi_factor_pvs_restore_targetvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_restore_targetvaluation_candidate_power_partial. bpvi_h_pvs_restore_targetvaluation_candidate_power_partial + S (bpvi_partial_pvs_restore_targetvaluation_candidate_power) = S ((S (bpvi_j_pvs_restore_targetvaluation_candidate_power)) * bpvi_v_pvs_restore_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_candidate_power_partial. bpvi_u_pvs_restore_targetvaluation_candidate_power = bpvi_q_pvs_restore_targetvaluation_candidate_power_partial * S ((S (bpvi_j_pvs_restore_targetvaluation_candidate_power)) * bpvi_v_pvs_restore_targetvaluation_candidate_power) + (bpvi_partial_pvs_restore_targetvaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_restore_targetvaluation_candidate_power_successor. bpvi_h_pvs_restore_targetvaluation_candidate_power_successor + S (bpvi_successor_pvs_restore_targetvaluation_candidate_power) = S ((S (S bpvi_j_pvs_restore_targetvaluation_candidate_power)) * bpvi_v_pvs_restore_targetvaluation_candidate_power)) /\ exists bpvi_q_pvs_restore_targetvaluation_candidate_power_successor. bpvi_u_pvs_restore_targetvaluation_candidate_power = bpvi_q_pvs_restore_targetvaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_restore_targetvaluation_candidate_power)) * bpvi_v_pvs_restore_targetvaluation_candidate_power) + (bpvi_successor_pvs_restore_targetvaluation_candidate_power))) /\ bpvi_successor_pvs_restore_targetvaluation_candidate_power = bpvi_partial_pvs_restore_targetvaluation_candidate_power * bpvi_factor_pvs_restore_targetvaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_restore_targetvaluation_candidate. n = bpvi_result_pvs_restore_targetvaluation_candidate * bpvi_divisor_factor_pvs_restore_targetvaluation_candidate)) -> (exists bpd_gap_pvs_restore_targetvaluation_maximal. bpd_gap_pvs_restore_targetvaluation_maximal + (bpd_candidate_pvs_restore_targetvaluation) = (pvs_exponent_restore_target))) /\ (exists pa_b_pvs_restore_targetvalue pa_c_pvs_restore_targetvalue. ((forall pa_i_pvs_restore_targetvalue_repeat. (exists pa_lt_pvs_restore_targetvalue_repeat_bound. pa_lt_pvs_restore_targetvalue_repeat_bound + S pa_i_pvs_restore_targetvalue_repeat = pvs_exponent_restore_target) -> (((exists pa_h_pvs_restore_targetvalue_repeat_decoded. pa_h_pvs_restore_targetvalue_repeat_decoded + S (pvs_prime_restore_target) = S ((S (pa_i_pvs_restore_targetvalue_repeat)) * pa_c_pvs_restore_targetvalue)) /\ exists pa_q_pvs_restore_targetvalue_repeat_decoded. pa_b_pvs_restore_targetvalue = pa_q_pvs_restore_targetvalue_repeat_decoded * S ((S (pa_i_pvs_restore_targetvalue_repeat)) * pa_c_pvs_restore_targetvalue) + (pvs_prime_restore_target)))) /\ (exists pa_u_pvs_restore_targetvalue_product pa_v_pvs_restore_targetvalue_product. ((((exists pa_h_pvs_restore_targetvalue_product_start. pa_h_pvs_restore_targetvalue_product_start + S (1) = S ((S (0)) * pa_v_pvs_restore_targetvalue_product)) /\ exists pa_q_pvs_restore_targetvalue_product_start. pa_u_pvs_restore_targetvalue_product = pa_q_pvs_restore_targetvalue_product_start * S ((S (0)) * pa_v_pvs_restore_targetvalue_product) + (1))) /\ ((((exists pa_h_pvs_restore_targetvalue_product_terminal. pa_h_pvs_restore_targetvalue_product_terminal + S (pvs_power_restore_target) = S ((S (pvs_exponent_restore_target)) * pa_v_pvs_restore_targetvalue_product)) /\ exists pa_q_pvs_restore_targetvalue_product_terminal. pa_u_pvs_restore_targetvalue_product = pa_q_pvs_restore_targetvalue_product_terminal * S ((S (pvs_exponent_restore_target)) * pa_v_pvs_restore_targetvalue_product) + (pvs_power_restore_target))) /\ forall pa_i_pvs_restore_targetvalue_product. (exists pa_lt_pvs_restore_targetvalue_product_bound. pa_lt_pvs_restore_targetvalue_product_bound + S pa_i_pvs_restore_targetvalue_product = pvs_exponent_restore_target) -> exists pa_p_pvs_restore_targetvalue_product pa_r_pvs_restore_targetvalue_product pa_s_pvs_restore_targetvalue_product. ((((exists pa_h_pvs_restore_targetvalue_product_factor. pa_h_pvs_restore_targetvalue_product_factor + S (pa_p_pvs_restore_targetvalue_product) = S ((S (pa_i_pvs_restore_targetvalue_product)) * pa_c_pvs_restore_targetvalue)) /\ exists pa_q_pvs_restore_targetvalue_product_factor. pa_b_pvs_restore_targetvalue = pa_q_pvs_restore_targetvalue_product_factor * S ((S (pa_i_pvs_restore_targetvalue_product)) * pa_c_pvs_restore_targetvalue) + (pa_p_pvs_restore_targetvalue_product))) /\ ((((exists pa_h_pvs_restore_targetvalue_product_partial. pa_h_pvs_restore_targetvalue_product_partial + S (pa_r_pvs_restore_targetvalue_product) = S ((S (pa_i_pvs_restore_targetvalue_product)) * pa_v_pvs_restore_targetvalue_product)) /\ exists pa_q_pvs_restore_targetvalue_product_partial. pa_u_pvs_restore_targetvalue_product = pa_q_pvs_restore_targetvalue_product_partial * S ((S (pa_i_pvs_restore_targetvalue_product)) * pa_v_pvs_restore_targetvalue_product) + (pa_r_pvs_restore_targetvalue_product))) /\ ((((exists pa_h_pvs_restore_targetvalue_product_successor. pa_h_pvs_restore_targetvalue_product_successor + S (pa_s_pvs_restore_targetvalue_product) = S ((S (S pa_i_pvs_restore_targetvalue_product)) * pa_v_pvs_restore_targetvalue_product)) /\ exists pa_q_pvs_restore_targetvalue_product_successor. pa_u_pvs_restore_targetvalue_product = pa_q_pvs_restore_targetvalue_product_successor * S ((S (S pa_i_pvs_restore_targetvalue_product)) * pa_v_pvs_restore_targetvalue_product) + (pa_s_pvs_restore_targetvalue_product))) /\ pa_s_pvs_restore_targetvalue_product = pa_r_pvs_restore_targetvalue_product * pa_p_pvs_restore_targetvalue_product)))))))))))))))))))))

Complete tactic proof in conservative notation

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

80 script commands · 22 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 (1)
prime valuation strip other prime
01Fix variables and assumptionsL1–10

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

  1. L1
    intro n
  2. L2
    intro u
  3. L3
    intro p
  4. L4
    intro k
  5. L5
    intro P
  6. L6
    intro pb
  7. L7
    intro pc
  8. L8
    intro eb
  9. L9
    intro ec
  10. L10
    intro vb
02Fix variables and assumptionsL11–20

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

  1. L11
    intro vc
  2. L12
    intro l
  3. L13
    intro hp
  4. L14
    intro hu
  5. L15
    intro hn
  6. L16
    intro hpow
  7. L17
    intro hfresh
  8. L18
    intro hentries
  9. L19
    intro i
  10. L20
    intro hi
03Establish hrowL21–24

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

  1. L21
    have hrow : ∃ p. ∃ e. ∃ v. BetaAt(pb,pc,i,p) ∧ (BetaAt(eb,ec,i,e) ∧ (BetaAt(vb,vc,i,v) ∧ (Prime(p) ∧ (¬e = 0 ∧ (BoundedPowerValuation(p,u,u,e) ∧ Pow(p,e,v))))))Definitions: BetaAt(pb,pc,i,p)BetaAt(eb,ec,i,e)BetaAt(vb,vc,i,v)Prime(p)BoundedPowerValuation(p,u,u,e)Pow(p,e,v)Original native command in the exact edition
  2. L22
    specialize hentries (i)
  3. L23
    apply hentries
  4. L24
    exact hi
04Separate the logical casesL25–33

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

  1. L25
    cases hrow
  2. L26
    cases hrow_witness
  3. L27
    cases hrow_witness_witness
  4. L28
    cases hrow_witness_witness_witness
  5. L29
    cases hrow_witness_witness_witness_right
  6. L30
    cases hrow_witness_witness_witness_right_right
  7. L31
    cases hrow_witness_witness_witness_right_right_right
  8. L32
    cases hrow_witness_witness_witness_right_right_right_right
  9. L33
    cases hrow_witness_witness_witness_right_right_right_right_right
05Establish hneqL34–35

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

  1. L34
    have hneq : ~(x = p)
  2. L35
    intro heq
06Establish hdivL36–45

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

  1. L36
  2. L37
    specialize power_valuation_nonzero_exponent_divides_base (x)
  3. L38
    specialize power_valuation_nonzero_exponent_divides_base (u)
  4. L39
    specialize power_valuation_nonzero_exponent_divides_base (x1)
  5. L40
    apply power_valuation_nonzero_exponent_divides_base
  6. L41
    exact hrow_witness_witness_witness_right_right_right_right_right_left
  7. L42
    exact hrow_witness_witness_witness_right_right_right_right_left
  8. L43
    rewrite heq at hdiv
  9. L44
    apply hfresh
  10. L45
    exact hdiv
07Construct an explicit witnessL46–48

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

  1. L46
    exists x
  2. L47
    exists x1
  3. L48
    exists x2
08Separate the logical casesL49–49

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

  1. L49
    split
09Use earlier factsL50–50

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

  1. L50
    exact hrow_witness_witness_witness_left
10Separate the logical casesL51–51

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

  1. L51
    split
11Use earlier factsL52–52

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

  1. L52
    exact hrow_witness_witness_witness_right_left
12Separate the logical casesL53–53

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

  1. L53
    split
13Use earlier factsL54–54

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

  1. L54
    exact hrow_witness_witness_witness_right_right_left
14Separate the logical casesL55–55

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

  1. L55
    split
15Use earlier factsL56–56

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

  1. L56
    exact hrow_witness_witness_witness_right_right_right_left
16Separate the logical casesL57–57

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

  1. L57
    split
17Use earlier factsL58–58

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

  1. L58
    exact hrow_witness_witness_witness_right_right_right_right_left
18Separate the logical casesL59–59

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

  1. L59
    split
19Use earlier factsL60–64

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

  1. L60
    specialize power_valuation_value_eq_transport (x)
  2. L61
    specialize power_valuation_value_eq_transport (P * u)
  3. L62
    specialize power_valuation_value_eq_transport (n)
  4. L63
    specialize power_valuation_value_eq_transport (x1)
  5. L64
    apply power_valuation_value_eq_transport
20Calculate and transport equalitiesL65–65

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

  1. L65
    symm
21Use earlier factsL66–75

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

  1. L66
    exact hn
  2. L67
    specialize prime_valuation_strip_other_prime (p)
  3. L68
    specialize prime_valuation_strip_other_prime (x)
  4. L69
    specialize prime_valuation_strip_other_prime (k)
  5. L70
    specialize prime_valuation_strip_other_prime (P)
  6. L71
    specialize prime_valuation_strip_other_prime (u)
  7. L72
    specialize prime_valuation_strip_other_prime (x1)
  8. L73
    apply prime_valuation_strip_other_prime
  9. L74
    exact hp
  10. L75
    exact hrow_witness_witness_witness_right_right_right_left
22Use earlier factsL76–80

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

  1. L76
    exact hneq
  2. L77
    exact hu
  3. L78
    exact hpow
  4. L79
    exact hrow_witness_witness_witness_right_right_right_right_right_left
  5. L80
    exact hrow_witness_witness_witness_right_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 80 lines
  1. 0001intro n
  2. 0002intro u
  3. 0003intro p
  4. 0004intro k
  5. 0005intro P
  6. 0006intro pb
  7. 0007intro pc
  8. 0008intro eb
  9. 0009intro ec
  10. 0010intro vb
  11. 0011intro vc
  12. 0012intro l
  13. 0013intro hp
  14. 0014intro hu
  15. 0015intro hn
  16. 0016intro hpow
  17. 0017intro hfresh
  18. 0018intro hentries
  19. 0019intro i
  20. 0020intro hi
  21. 0021have hrow : ∃ p. ∃ e. ∃ v. BetaAt(pb,pc,i,p) ∧ (BetaAt(eb,ec,i,e) ∧ (BetaAt(vb,vc,i,v) ∧ (Prime(p) ∧ (¬e = 0 ∧ (BoundedPowerValuation(p,u,u,e) ∧ Pow(p,e,v))))))
  22. 0022specialize hentries (i)
  23. 0023apply hentries
  24. 0024exact hi
  25. 0025cases hrow
  26. 0026cases hrow_witness
  27. 0027cases hrow_witness_witness
  28. 0028cases hrow_witness_witness_witness
  29. 0029cases hrow_witness_witness_witness_right
  30. 0030cases hrow_witness_witness_witness_right_right
  31. 0031cases hrow_witness_witness_witness_right_right_right
  32. 0032cases hrow_witness_witness_witness_right_right_right_right
  33. 0033cases hrow_witness_witness_witness_right_right_right_right_right
  34. 0034have hneq : ~(x = p)
  35. 0035intro heq
  36. 0036have hdiv : Dvd(x,u)
  37. 0037specialize power_valuation_nonzero_exponent_divides_base (x)
  38. 0038specialize power_valuation_nonzero_exponent_divides_base (u)
  39. 0039specialize power_valuation_nonzero_exponent_divides_base (x1)
  40. 0040apply power_valuation_nonzero_exponent_divides_base
  41. 0041exact hrow_witness_witness_witness_right_right_right_right_right_left
  42. 0042exact hrow_witness_witness_witness_right_right_right_right_left
  43. 0043rewrite heq at hdiv
  44. 0044apply hfresh
  45. 0045exact hdiv
  46. 0046exists x
  47. 0047exists x1
  48. 0048exists x2
  49. 0049split
  50. 0050exact hrow_witness_witness_witness_left
  51. 0051split
  52. 0052exact hrow_witness_witness_witness_right_left
  53. 0053split
  54. 0054exact hrow_witness_witness_witness_right_right_left
  55. 0055split
  56. 0056exact hrow_witness_witness_witness_right_right_right_left
  57. 0057split
  58. 0058exact hrow_witness_witness_witness_right_right_right_right_left
  59. 0059split
  60. 0060specialize power_valuation_value_eq_transport (x)
  61. 0061specialize power_valuation_value_eq_transport (P * u)
  62. 0062specialize power_valuation_value_eq_transport (n)
  63. 0063specialize power_valuation_value_eq_transport (x1)
  64. 0064apply power_valuation_value_eq_transport
  65. 0065symm
  66. 0066exact hn
  67. 0067specialize prime_valuation_strip_other_prime (p)
  68. 0068specialize prime_valuation_strip_other_prime (x)
  69. 0069specialize prime_valuation_strip_other_prime (k)
  70. 0070specialize prime_valuation_strip_other_prime (P)
  71. 0071specialize prime_valuation_strip_other_prime (u)
  72. 0072specialize prime_valuation_strip_other_prime (x1)
  73. 0073apply prime_valuation_strip_other_prime
  74. 0074exact hp
  75. 0075exact hrow_witness_witness_witness_right_right_right_left
  76. 0076exact hneq
  77. 0077exact hu
  78. 0078exact hpow
  79. 0079exact hrow_witness_witness_witness_right_right_right_right_right_left
  80. 0080exact hrow_witness_witness_witness_right_right_right_right_right_right