PV000A

prime_valuation_strip_other_prime

Removing a full prime power does not change any other prime valuation of the remaining positive 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

∀ p. ∀ q. ∀ k. ∀ z. ∀ u. ∀ e. Prime(p) → Prime(q) → ¬q = p → ¬u = 0 → Pow(p,k,z) → BoundedPowerValuation(q,u,u,e) → BoundedPowerValuation(q,z · u,z · u,e)

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

Definition DAG

Prime(p) · 2Pow(a,e,z) · 1BoundedPowerValuation(p,n,b,e) · 2

Actual proof prerequisites

prime_valuation_product_zero_leftprime_nonzero · checked external prerequisiteone_le_of_ne_zero · checked external prerequisitepow_nonzero_of_one_le · checked external prerequisiteprime_valuation_distinct_prime_power_zero
Original expanded first-order statement 
forall p q k z u e. (~((p) = 1) /\ forall pvs_left_strip_base pvs_right_strip_base. (p) = pvs_left_strip_base * pvs_right_strip_base -> pvs_left_strip_base = 1 \/ pvs_right_strip_base = 1) -> (~((q) = 1) /\ forall pvs_left_strip_other pvs_right_strip_other. (q) = pvs_left_strip_other * pvs_right_strip_other -> pvs_left_strip_other = 1 \/ pvs_right_strip_other = 1) -> ~(q = p) -> ~(u = 0) -> (exists pa_b_pvs_strip_power pa_c_pvs_strip_power. ((forall pa_i_pvs_strip_power_repeat. (exists pa_lt_pvs_strip_power_repeat_bound. pa_lt_pvs_strip_power_repeat_bound + S pa_i_pvs_strip_power_repeat = k) -> (((exists pa_h_pvs_strip_power_repeat_decoded. pa_h_pvs_strip_power_repeat_decoded + S (p) = S ((S (pa_i_pvs_strip_power_repeat)) * pa_c_pvs_strip_power)) /\ exists pa_q_pvs_strip_power_repeat_decoded. pa_b_pvs_strip_power = pa_q_pvs_strip_power_repeat_decoded * S ((S (pa_i_pvs_strip_power_repeat)) * pa_c_pvs_strip_power) + (p)))) /\ (exists pa_u_pvs_strip_power_product pa_v_pvs_strip_power_product. ((((exists pa_h_pvs_strip_power_product_start. pa_h_pvs_strip_power_product_start + S (1) = S ((S (0)) * pa_v_pvs_strip_power_product)) /\ exists pa_q_pvs_strip_power_product_start. pa_u_pvs_strip_power_product = pa_q_pvs_strip_power_product_start * S ((S (0)) * pa_v_pvs_strip_power_product) + (1))) /\ ((((exists pa_h_pvs_strip_power_product_terminal. pa_h_pvs_strip_power_product_terminal + S (z) = S ((S (k)) * pa_v_pvs_strip_power_product)) /\ exists pa_q_pvs_strip_power_product_terminal. pa_u_pvs_strip_power_product = pa_q_pvs_strip_power_product_terminal * S ((S (k)) * pa_v_pvs_strip_power_product) + (z))) /\ forall pa_i_pvs_strip_power_product. (exists pa_lt_pvs_strip_power_product_bound. pa_lt_pvs_strip_power_product_bound + S pa_i_pvs_strip_power_product = k) -> exists pa_p_pvs_strip_power_product pa_r_pvs_strip_power_product pa_s_pvs_strip_power_product. ((((exists pa_h_pvs_strip_power_product_factor. pa_h_pvs_strip_power_product_factor + S (pa_p_pvs_strip_power_product) = S ((S (pa_i_pvs_strip_power_product)) * pa_c_pvs_strip_power)) /\ exists pa_q_pvs_strip_power_product_factor. pa_b_pvs_strip_power = pa_q_pvs_strip_power_product_factor * S ((S (pa_i_pvs_strip_power_product)) * pa_c_pvs_strip_power) + (pa_p_pvs_strip_power_product))) /\ ((((exists pa_h_pvs_strip_power_product_partial. pa_h_pvs_strip_power_product_partial + S (pa_r_pvs_strip_power_product) = S ((S (pa_i_pvs_strip_power_product)) * pa_v_pvs_strip_power_product)) /\ exists pa_q_pvs_strip_power_product_partial. pa_u_pvs_strip_power_product = pa_q_pvs_strip_power_product_partial * S ((S (pa_i_pvs_strip_power_product)) * pa_v_pvs_strip_power_product) + (pa_r_pvs_strip_power_product))) /\ ((((exists pa_h_pvs_strip_power_product_successor. pa_h_pvs_strip_power_product_successor + S (pa_s_pvs_strip_power_product) = S ((S (S pa_i_pvs_strip_power_product)) * pa_v_pvs_strip_power_product)) /\ exists pa_q_pvs_strip_power_product_successor. pa_u_pvs_strip_power_product = pa_q_pvs_strip_power_product_successor * S ((S (S pa_i_pvs_strip_power_product)) * pa_v_pvs_strip_power_product) + (pa_s_pvs_strip_power_product))) /\ pa_s_pvs_strip_power_product = pa_r_pvs_strip_power_product * pa_p_pvs_strip_power_product)))))))) -> (((exists bpd_gap_pvs_strip_source_selected_bound. bpd_gap_pvs_strip_source_selected_bound + (e) = (u)) /\ (exists bpvi_result_pvs_strip_source_selected. ((exists bpvi_b_pvs_strip_source_selected_power bpvi_c_pvs_strip_source_selected_power. ((forall bpvi_i_pvs_strip_source_selected_power. (exists bpvi_repeat_gap_pvs_strip_source_selected_power. bpvi_repeat_gap_pvs_strip_source_selected_power + S bpvi_i_pvs_strip_source_selected_power = e) -> (((exists bpvi_h_pvs_strip_source_selected_power_repeat. bpvi_h_pvs_strip_source_selected_power_repeat + S (q) = S ((S (bpvi_i_pvs_strip_source_selected_power)) * bpvi_c_pvs_strip_source_selected_power)) /\ exists bpvi_q_pvs_strip_source_selected_power_repeat. bpvi_b_pvs_strip_source_selected_power = bpvi_q_pvs_strip_source_selected_power_repeat * S ((S (bpvi_i_pvs_strip_source_selected_power)) * bpvi_c_pvs_strip_source_selected_power) + (q)))) /\ (exists bpvi_u_pvs_strip_source_selected_power bpvi_v_pvs_strip_source_selected_power. ((((exists bpvi_h_pvs_strip_source_selected_power_start. bpvi_h_pvs_strip_source_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_strip_source_selected_power)) /\ exists bpvi_q_pvs_strip_source_selected_power_start. bpvi_u_pvs_strip_source_selected_power = bpvi_q_pvs_strip_source_selected_power_start * S ((S (0)) * bpvi_v_pvs_strip_source_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_strip_source_selected_power_terminal. bpvi_h_pvs_strip_source_selected_power_terminal + S (bpvi_result_pvs_strip_source_selected) = S ((S (e)) * bpvi_v_pvs_strip_source_selected_power)) /\ exists bpvi_q_pvs_strip_source_selected_power_terminal. bpvi_u_pvs_strip_source_selected_power = bpvi_q_pvs_strip_source_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_strip_source_selected_power) + (bpvi_result_pvs_strip_source_selected))) /\ forall bpvi_j_pvs_strip_source_selected_power. (exists bpvi_product_gap_pvs_strip_source_selected_power. bpvi_product_gap_pvs_strip_source_selected_power + S bpvi_j_pvs_strip_source_selected_power = e) -> exists bpvi_factor_pvs_strip_source_selected_power bpvi_partial_pvs_strip_source_selected_power bpvi_successor_pvs_strip_source_selected_power. ((((exists bpvi_h_pvs_strip_source_selected_power_factor. bpvi_h_pvs_strip_source_selected_power_factor + S (bpvi_factor_pvs_strip_source_selected_power) = S ((S (bpvi_j_pvs_strip_source_selected_power)) * bpvi_c_pvs_strip_source_selected_power)) /\ exists bpvi_q_pvs_strip_source_selected_power_factor. bpvi_b_pvs_strip_source_selected_power = bpvi_q_pvs_strip_source_selected_power_factor * S ((S (bpvi_j_pvs_strip_source_selected_power)) * bpvi_c_pvs_strip_source_selected_power) + (bpvi_factor_pvs_strip_source_selected_power))) /\ ((((exists bpvi_h_pvs_strip_source_selected_power_partial. bpvi_h_pvs_strip_source_selected_power_partial + S (bpvi_partial_pvs_strip_source_selected_power) = S ((S (bpvi_j_pvs_strip_source_selected_power)) * bpvi_v_pvs_strip_source_selected_power)) /\ exists bpvi_q_pvs_strip_source_selected_power_partial. bpvi_u_pvs_strip_source_selected_power = bpvi_q_pvs_strip_source_selected_power_partial * S ((S (bpvi_j_pvs_strip_source_selected_power)) * bpvi_v_pvs_strip_source_selected_power) + (bpvi_partial_pvs_strip_source_selected_power))) /\ ((((exists bpvi_h_pvs_strip_source_selected_power_successor. bpvi_h_pvs_strip_source_selected_power_successor + S (bpvi_successor_pvs_strip_source_selected_power) = S ((S (S bpvi_j_pvs_strip_source_selected_power)) * bpvi_v_pvs_strip_source_selected_power)) /\ exists bpvi_q_pvs_strip_source_selected_power_successor. bpvi_u_pvs_strip_source_selected_power = bpvi_q_pvs_strip_source_selected_power_successor * S ((S (S bpvi_j_pvs_strip_source_selected_power)) * bpvi_v_pvs_strip_source_selected_power) + (bpvi_successor_pvs_strip_source_selected_power))) /\ bpvi_successor_pvs_strip_source_selected_power = bpvi_partial_pvs_strip_source_selected_power * bpvi_factor_pvs_strip_source_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_strip_source_selected. u = bpvi_result_pvs_strip_source_selected * bpvi_divisor_factor_pvs_strip_source_selected))) /\ forall bpd_candidate_pvs_strip_source. (exists bpd_gap_pvs_strip_source_candidate_bound. bpd_gap_pvs_strip_source_candidate_bound + (bpd_candidate_pvs_strip_source) = (u)) -> (exists bpvi_result_pvs_strip_source_candidate. ((exists bpvi_b_pvs_strip_source_candidate_power bpvi_c_pvs_strip_source_candidate_power. ((forall bpvi_i_pvs_strip_source_candidate_power. (exists bpvi_repeat_gap_pvs_strip_source_candidate_power. bpvi_repeat_gap_pvs_strip_source_candidate_power + S bpvi_i_pvs_strip_source_candidate_power = bpd_candidate_pvs_strip_source) -> (((exists bpvi_h_pvs_strip_source_candidate_power_repeat. bpvi_h_pvs_strip_source_candidate_power_repeat + S (q) = S ((S (bpvi_i_pvs_strip_source_candidate_power)) * bpvi_c_pvs_strip_source_candidate_power)) /\ exists bpvi_q_pvs_strip_source_candidate_power_repeat. bpvi_b_pvs_strip_source_candidate_power = bpvi_q_pvs_strip_source_candidate_power_repeat * S ((S (bpvi_i_pvs_strip_source_candidate_power)) * bpvi_c_pvs_strip_source_candidate_power) + (q)))) /\ (exists bpvi_u_pvs_strip_source_candidate_power bpvi_v_pvs_strip_source_candidate_power. ((((exists bpvi_h_pvs_strip_source_candidate_power_start. bpvi_h_pvs_strip_source_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_strip_source_candidate_power)) /\ exists bpvi_q_pvs_strip_source_candidate_power_start. bpvi_u_pvs_strip_source_candidate_power = bpvi_q_pvs_strip_source_candidate_power_start * S ((S (0)) * bpvi_v_pvs_strip_source_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_strip_source_candidate_power_terminal. bpvi_h_pvs_strip_source_candidate_power_terminal + S (bpvi_result_pvs_strip_source_candidate) = S ((S (bpd_candidate_pvs_strip_source)) * bpvi_v_pvs_strip_source_candidate_power)) /\ exists bpvi_q_pvs_strip_source_candidate_power_terminal. bpvi_u_pvs_strip_source_candidate_power = bpvi_q_pvs_strip_source_candidate_power_terminal * S ((S (bpd_candidate_pvs_strip_source)) * bpvi_v_pvs_strip_source_candidate_power) + (bpvi_result_pvs_strip_source_candidate))) /\ forall bpvi_j_pvs_strip_source_candidate_power. (exists bpvi_product_gap_pvs_strip_source_candidate_power. bpvi_product_gap_pvs_strip_source_candidate_power + S bpvi_j_pvs_strip_source_candidate_power = bpd_candidate_pvs_strip_source) -> exists bpvi_factor_pvs_strip_source_candidate_power bpvi_partial_pvs_strip_source_candidate_power bpvi_successor_pvs_strip_source_candidate_power. ((((exists bpvi_h_pvs_strip_source_candidate_power_factor. bpvi_h_pvs_strip_source_candidate_power_factor + S (bpvi_factor_pvs_strip_source_candidate_power) = S ((S (bpvi_j_pvs_strip_source_candidate_power)) * bpvi_c_pvs_strip_source_candidate_power)) /\ exists bpvi_q_pvs_strip_source_candidate_power_factor. bpvi_b_pvs_strip_source_candidate_power = bpvi_q_pvs_strip_source_candidate_power_factor * S ((S (bpvi_j_pvs_strip_source_candidate_power)) * bpvi_c_pvs_strip_source_candidate_power) + (bpvi_factor_pvs_strip_source_candidate_power))) /\ ((((exists bpvi_h_pvs_strip_source_candidate_power_partial. bpvi_h_pvs_strip_source_candidate_power_partial + S (bpvi_partial_pvs_strip_source_candidate_power) = S ((S (bpvi_j_pvs_strip_source_candidate_power)) * bpvi_v_pvs_strip_source_candidate_power)) /\ exists bpvi_q_pvs_strip_source_candidate_power_partial. bpvi_u_pvs_strip_source_candidate_power = bpvi_q_pvs_strip_source_candidate_power_partial * S ((S (bpvi_j_pvs_strip_source_candidate_power)) * bpvi_v_pvs_strip_source_candidate_power) + (bpvi_partial_pvs_strip_source_candidate_power))) /\ ((((exists bpvi_h_pvs_strip_source_candidate_power_successor. bpvi_h_pvs_strip_source_candidate_power_successor + S (bpvi_successor_pvs_strip_source_candidate_power) = S ((S (S bpvi_j_pvs_strip_source_candidate_power)) * bpvi_v_pvs_strip_source_candidate_power)) /\ exists bpvi_q_pvs_strip_source_candidate_power_successor. bpvi_u_pvs_strip_source_candidate_power = bpvi_q_pvs_strip_source_candidate_power_successor * S ((S (S bpvi_j_pvs_strip_source_candidate_power)) * bpvi_v_pvs_strip_source_candidate_power) + (bpvi_successor_pvs_strip_source_candidate_power))) /\ bpvi_successor_pvs_strip_source_candidate_power = bpvi_partial_pvs_strip_source_candidate_power * bpvi_factor_pvs_strip_source_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_strip_source_candidate. u = bpvi_result_pvs_strip_source_candidate * bpvi_divisor_factor_pvs_strip_source_candidate)) -> (exists bpd_gap_pvs_strip_source_maximal. bpd_gap_pvs_strip_source_maximal + (bpd_candidate_pvs_strip_source) = (e))) -> (((exists bpd_gap_pvs_strip_result_selected_bound. bpd_gap_pvs_strip_result_selected_bound + (e) = (z * u)) /\ (exists bpvi_result_pvs_strip_result_selected. ((exists bpvi_b_pvs_strip_result_selected_power bpvi_c_pvs_strip_result_selected_power. ((forall bpvi_i_pvs_strip_result_selected_power. (exists bpvi_repeat_gap_pvs_strip_result_selected_power. bpvi_repeat_gap_pvs_strip_result_selected_power + S bpvi_i_pvs_strip_result_selected_power = e) -> (((exists bpvi_h_pvs_strip_result_selected_power_repeat. bpvi_h_pvs_strip_result_selected_power_repeat + S (q) = S ((S (bpvi_i_pvs_strip_result_selected_power)) * bpvi_c_pvs_strip_result_selected_power)) /\ exists bpvi_q_pvs_strip_result_selected_power_repeat. bpvi_b_pvs_strip_result_selected_power = bpvi_q_pvs_strip_result_selected_power_repeat * S ((S (bpvi_i_pvs_strip_result_selected_power)) * bpvi_c_pvs_strip_result_selected_power) + (q)))) /\ (exists bpvi_u_pvs_strip_result_selected_power bpvi_v_pvs_strip_result_selected_power. ((((exists bpvi_h_pvs_strip_result_selected_power_start. bpvi_h_pvs_strip_result_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_strip_result_selected_power)) /\ exists bpvi_q_pvs_strip_result_selected_power_start. bpvi_u_pvs_strip_result_selected_power = bpvi_q_pvs_strip_result_selected_power_start * S ((S (0)) * bpvi_v_pvs_strip_result_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_strip_result_selected_power_terminal. bpvi_h_pvs_strip_result_selected_power_terminal + S (bpvi_result_pvs_strip_result_selected) = S ((S (e)) * bpvi_v_pvs_strip_result_selected_power)) /\ exists bpvi_q_pvs_strip_result_selected_power_terminal. bpvi_u_pvs_strip_result_selected_power = bpvi_q_pvs_strip_result_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_strip_result_selected_power) + (bpvi_result_pvs_strip_result_selected))) /\ forall bpvi_j_pvs_strip_result_selected_power. (exists bpvi_product_gap_pvs_strip_result_selected_power. bpvi_product_gap_pvs_strip_result_selected_power + S bpvi_j_pvs_strip_result_selected_power = e) -> exists bpvi_factor_pvs_strip_result_selected_power bpvi_partial_pvs_strip_result_selected_power bpvi_successor_pvs_strip_result_selected_power. ((((exists bpvi_h_pvs_strip_result_selected_power_factor. bpvi_h_pvs_strip_result_selected_power_factor + S (bpvi_factor_pvs_strip_result_selected_power) = S ((S (bpvi_j_pvs_strip_result_selected_power)) * bpvi_c_pvs_strip_result_selected_power)) /\ exists bpvi_q_pvs_strip_result_selected_power_factor. bpvi_b_pvs_strip_result_selected_power = bpvi_q_pvs_strip_result_selected_power_factor * S ((S (bpvi_j_pvs_strip_result_selected_power)) * bpvi_c_pvs_strip_result_selected_power) + (bpvi_factor_pvs_strip_result_selected_power))) /\ ((((exists bpvi_h_pvs_strip_result_selected_power_partial. bpvi_h_pvs_strip_result_selected_power_partial + S (bpvi_partial_pvs_strip_result_selected_power) = S ((S (bpvi_j_pvs_strip_result_selected_power)) * bpvi_v_pvs_strip_result_selected_power)) /\ exists bpvi_q_pvs_strip_result_selected_power_partial. bpvi_u_pvs_strip_result_selected_power = bpvi_q_pvs_strip_result_selected_power_partial * S ((S (bpvi_j_pvs_strip_result_selected_power)) * bpvi_v_pvs_strip_result_selected_power) + (bpvi_partial_pvs_strip_result_selected_power))) /\ ((((exists bpvi_h_pvs_strip_result_selected_power_successor. bpvi_h_pvs_strip_result_selected_power_successor + S (bpvi_successor_pvs_strip_result_selected_power) = S ((S (S bpvi_j_pvs_strip_result_selected_power)) * bpvi_v_pvs_strip_result_selected_power)) /\ exists bpvi_q_pvs_strip_result_selected_power_successor. bpvi_u_pvs_strip_result_selected_power = bpvi_q_pvs_strip_result_selected_power_successor * S ((S (S bpvi_j_pvs_strip_result_selected_power)) * bpvi_v_pvs_strip_result_selected_power) + (bpvi_successor_pvs_strip_result_selected_power))) /\ bpvi_successor_pvs_strip_result_selected_power = bpvi_partial_pvs_strip_result_selected_power * bpvi_factor_pvs_strip_result_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_strip_result_selected. z * u = bpvi_result_pvs_strip_result_selected * bpvi_divisor_factor_pvs_strip_result_selected))) /\ forall bpd_candidate_pvs_strip_result. (exists bpd_gap_pvs_strip_result_candidate_bound. bpd_gap_pvs_strip_result_candidate_bound + (bpd_candidate_pvs_strip_result) = (z * u)) -> (exists bpvi_result_pvs_strip_result_candidate. ((exists bpvi_b_pvs_strip_result_candidate_power bpvi_c_pvs_strip_result_candidate_power. ((forall bpvi_i_pvs_strip_result_candidate_power. (exists bpvi_repeat_gap_pvs_strip_result_candidate_power. bpvi_repeat_gap_pvs_strip_result_candidate_power + S bpvi_i_pvs_strip_result_candidate_power = bpd_candidate_pvs_strip_result) -> (((exists bpvi_h_pvs_strip_result_candidate_power_repeat. bpvi_h_pvs_strip_result_candidate_power_repeat + S (q) = S ((S (bpvi_i_pvs_strip_result_candidate_power)) * bpvi_c_pvs_strip_result_candidate_power)) /\ exists bpvi_q_pvs_strip_result_candidate_power_repeat. bpvi_b_pvs_strip_result_candidate_power = bpvi_q_pvs_strip_result_candidate_power_repeat * S ((S (bpvi_i_pvs_strip_result_candidate_power)) * bpvi_c_pvs_strip_result_candidate_power) + (q)))) /\ (exists bpvi_u_pvs_strip_result_candidate_power bpvi_v_pvs_strip_result_candidate_power. ((((exists bpvi_h_pvs_strip_result_candidate_power_start. bpvi_h_pvs_strip_result_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_strip_result_candidate_power)) /\ exists bpvi_q_pvs_strip_result_candidate_power_start. bpvi_u_pvs_strip_result_candidate_power = bpvi_q_pvs_strip_result_candidate_power_start * S ((S (0)) * bpvi_v_pvs_strip_result_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_strip_result_candidate_power_terminal. bpvi_h_pvs_strip_result_candidate_power_terminal + S (bpvi_result_pvs_strip_result_candidate) = S ((S (bpd_candidate_pvs_strip_result)) * bpvi_v_pvs_strip_result_candidate_power)) /\ exists bpvi_q_pvs_strip_result_candidate_power_terminal. bpvi_u_pvs_strip_result_candidate_power = bpvi_q_pvs_strip_result_candidate_power_terminal * S ((S (bpd_candidate_pvs_strip_result)) * bpvi_v_pvs_strip_result_candidate_power) + (bpvi_result_pvs_strip_result_candidate))) /\ forall bpvi_j_pvs_strip_result_candidate_power. (exists bpvi_product_gap_pvs_strip_result_candidate_power. bpvi_product_gap_pvs_strip_result_candidate_power + S bpvi_j_pvs_strip_result_candidate_power = bpd_candidate_pvs_strip_result) -> exists bpvi_factor_pvs_strip_result_candidate_power bpvi_partial_pvs_strip_result_candidate_power bpvi_successor_pvs_strip_result_candidate_power. ((((exists bpvi_h_pvs_strip_result_candidate_power_factor. bpvi_h_pvs_strip_result_candidate_power_factor + S (bpvi_factor_pvs_strip_result_candidate_power) = S ((S (bpvi_j_pvs_strip_result_candidate_power)) * bpvi_c_pvs_strip_result_candidate_power)) /\ exists bpvi_q_pvs_strip_result_candidate_power_factor. bpvi_b_pvs_strip_result_candidate_power = bpvi_q_pvs_strip_result_candidate_power_factor * S ((S (bpvi_j_pvs_strip_result_candidate_power)) * bpvi_c_pvs_strip_result_candidate_power) + (bpvi_factor_pvs_strip_result_candidate_power))) /\ ((((exists bpvi_h_pvs_strip_result_candidate_power_partial. bpvi_h_pvs_strip_result_candidate_power_partial + S (bpvi_partial_pvs_strip_result_candidate_power) = S ((S (bpvi_j_pvs_strip_result_candidate_power)) * bpvi_v_pvs_strip_result_candidate_power)) /\ exists bpvi_q_pvs_strip_result_candidate_power_partial. bpvi_u_pvs_strip_result_candidate_power = bpvi_q_pvs_strip_result_candidate_power_partial * S ((S (bpvi_j_pvs_strip_result_candidate_power)) * bpvi_v_pvs_strip_result_candidate_power) + (bpvi_partial_pvs_strip_result_candidate_power))) /\ ((((exists bpvi_h_pvs_strip_result_candidate_power_successor. bpvi_h_pvs_strip_result_candidate_power_successor + S (bpvi_successor_pvs_strip_result_candidate_power) = S ((S (S bpvi_j_pvs_strip_result_candidate_power)) * bpvi_v_pvs_strip_result_candidate_power)) /\ exists bpvi_q_pvs_strip_result_candidate_power_successor. bpvi_u_pvs_strip_result_candidate_power = bpvi_q_pvs_strip_result_candidate_power_successor * S ((S (S bpvi_j_pvs_strip_result_candidate_power)) * bpvi_v_pvs_strip_result_candidate_power) + (bpvi_successor_pvs_strip_result_candidate_power))) /\ bpvi_successor_pvs_strip_result_candidate_power = bpvi_partial_pvs_strip_result_candidate_power * bpvi_factor_pvs_strip_result_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_strip_result_candidate. z * u = bpvi_result_pvs_strip_result_candidate * bpvi_divisor_factor_pvs_strip_result_candidate)) -> (exists bpd_gap_pvs_strip_result_maximal. bpd_gap_pvs_strip_result_maximal + (bpd_candidate_pvs_strip_result) = (e)))

Complete tactic proof in conservative notation

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

43 script commands · 8 reading checkpoints · 0 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 (2)
prime valuation product zero leftprime valuation distinct prime power zero
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro k
  4. L4
    intro z
  5. L5
    intro u
  6. L6
    intro e
  7. L7
    intro hp
  8. L8
    intro hq
  9. L9
    intro hne
  10. L10
    intro hu
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hpow
  2. L12
    intro hval
03Use earlier factsL13–18

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

  1. L13
    specialize prime_valuation_product_zero_left (q)
  2. L14
    specialize prime_valuation_product_zero_left (z)
  3. L15
    specialize prime_valuation_product_zero_left (u)
  4. L16
    specialize prime_valuation_product_zero_left (e)
  5. L17
    apply prime_valuation_product_zero_left
  6. L18
    exact hq
04Fix variables and assumptionsL19–19

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

  1. L19
    intro hz
05Use earlier factsL20–25

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

  1. L20
    specialize pow_nonzero_of_one_le (p)
  2. L21
    specialize pow_nonzero_of_one_le (k)
  3. L22
    specialize pow_nonzero_of_one_le (z)
  4. L23
    apply pow_nonzero_of_one_le
  5. L24
    specialize one_le_of_ne_zero (p)
  6. L25
    apply one_le_of_ne_zero
06Fix variables and assumptionsL26–26

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

  1. L26
    intro hpzero
07Use earlier factsL27–36

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

  1. L27
    specialize prime_nonzero (p)
  2. L28
    apply prime_nonzero
  3. L29
    exact hp
  4. L30
    exact hpzero
  5. L31
    exact hpow
  6. L32
    exact hz
  7. L33
    exact hu
  8. L34
    specialize prime_valuation_distinct_prime_power_zero (p)
  9. L35
    specialize prime_valuation_distinct_prime_power_zero (q)
  10. L36
    specialize prime_valuation_distinct_prime_power_zero (k)
08Use earlier factsL37–43

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

  1. L37
    specialize prime_valuation_distinct_prime_power_zero (z)
  2. L38
    apply prime_valuation_distinct_prime_power_zero
  3. L39
    exact hp
  4. L40
    exact hq
  5. L41
    exact hne
  6. L42
    exact hpow
  7. L43
    exact hval

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro k
  4. 0004intro z
  5. 0005intro u
  6. 0006intro e
  7. 0007intro hp
  8. 0008intro hq
  9. 0009intro hne
  10. 0010intro hu
  11. 0011intro hpow
  12. 0012intro hval
  13. 0013specialize prime_valuation_product_zero_left (q)
  14. 0014specialize prime_valuation_product_zero_left (z)
  15. 0015specialize prime_valuation_product_zero_left (u)
  16. 0016specialize prime_valuation_product_zero_left (e)
  17. 0017apply prime_valuation_product_zero_left
  18. 0018exact hq
  19. 0019intro hz
  20. 0020specialize pow_nonzero_of_one_le (p)
  21. 0021specialize pow_nonzero_of_one_le (k)
  22. 0022specialize pow_nonzero_of_one_le (z)
  23. 0023apply pow_nonzero_of_one_le
  24. 0024specialize one_le_of_ne_zero (p)
  25. 0025apply one_le_of_ne_zero
  26. 0026intro hpzero
  27. 0027specialize prime_nonzero (p)
  28. 0028apply prime_nonzero
  29. 0029exact hp
  30. 0030exact hpzero
  31. 0031exact hpow
  32. 0032exact hz
  33. 0033exact hu
  34. 0034specialize prime_valuation_distinct_prime_power_zero (p)
  35. 0035specialize prime_valuation_distinct_prime_power_zero (q)
  36. 0036specialize prime_valuation_distinct_prime_power_zero (k)
  37. 0037specialize prime_valuation_distinct_prime_power_zero (z)
  38. 0038apply prime_valuation_distinct_prime_power_zero
  39. 0039exact hp
  40. 0040exact hq
  41. 0041exact hne
  42. 0042exact hpow
  43. 0043exact hval