EL0020

lte_prime_power_iteration

Ordinary HA induction constructs every prime-power exponent and its power difference, raising the valuation by exactly the number of prime steps.

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.

All displayed hypotheses are required. Powers and positive differences are actual existential outputs. The proof constructs second-order correction identities and iterates the prime step; no binomial expansion or LTE oracle is assumed. The 2-adic variants remain separate open targets.

Exact theorem in conservative defined notation

∀ p. ∀ a. ∀ b. ∀ d. ∀ e. ∀ k. ¬p = 1 ∧ (∀ x. ∀ y. p = x · y → x = 1 ∨ y = 1) → ¬p = 2 → a = b + d → ¬d = 0 → Dvd(p,d) → ¬Dvd(p,b) → BoundedPowerValuation(p,d,d,e) → ∃ x. ∃ y. ∃ z. ∃ n. Pow(p,k,x) ∧ LiftedPowerDifference(p,a,b,x,e + k,y,z,n)

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

Definition DAG

LiftedPowerDifference(p,a,b,n,e,A,B,D) · 3Dvd(d,n) · 2Pow(a,e,z) · 2BoundedPowerValuation(p,n,b,e) · 1

Actual proof prerequisites

lte_power_zero_exactlte_power_one_exactprime_valuation_exponent_eq_transport · checked external prerequisitelte_odd_prime_power_steppow_successor_compose · checked external prerequisitelte_power_iteration_construct
Original expanded first-order statement 
forall p a b d e k. (~((p) = 1) /\ forall pvs_left_tower_prime pvs_right_tower_prime. (p) = pvs_left_tower_prime * pvs_right_tower_prime -> pvs_left_tower_prime = 1 \/ pvs_right_tower_prime = 1) -> ~(p = 2) -> a = b + d -> ~(d = 0) -> (exists olte_factor_tower_divisor. (d) = (p) * olte_factor_tower_divisor) -> ~(exists olte_factor_tower_unit. (b) = (p) * olte_factor_tower_unit) -> (((exists bpd_gap_pvs_tower_input_selected_bound. bpd_gap_pvs_tower_input_selected_bound + (e) = (d)) /\ (exists bpvi_result_pvs_tower_input_selected. ((exists bpvi_b_pvs_tower_input_selected_power bpvi_c_pvs_tower_input_selected_power. ((forall bpvi_i_pvs_tower_input_selected_power. (exists bpvi_repeat_gap_pvs_tower_input_selected_power. bpvi_repeat_gap_pvs_tower_input_selected_power + S bpvi_i_pvs_tower_input_selected_power = e) -> (((exists bpvi_h_pvs_tower_input_selected_power_repeat. bpvi_h_pvs_tower_input_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_tower_input_selected_power)) * bpvi_c_pvs_tower_input_selected_power)) /\ exists bpvi_q_pvs_tower_input_selected_power_repeat. bpvi_b_pvs_tower_input_selected_power = bpvi_q_pvs_tower_input_selected_power_repeat * S ((S (bpvi_i_pvs_tower_input_selected_power)) * bpvi_c_pvs_tower_input_selected_power) + (p)))) /\ (exists bpvi_u_pvs_tower_input_selected_power bpvi_v_pvs_tower_input_selected_power. ((((exists bpvi_h_pvs_tower_input_selected_power_start. bpvi_h_pvs_tower_input_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_tower_input_selected_power)) /\ exists bpvi_q_pvs_tower_input_selected_power_start. bpvi_u_pvs_tower_input_selected_power = bpvi_q_pvs_tower_input_selected_power_start * S ((S (0)) * bpvi_v_pvs_tower_input_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_tower_input_selected_power_terminal. bpvi_h_pvs_tower_input_selected_power_terminal + S (bpvi_result_pvs_tower_input_selected) = S ((S (e)) * bpvi_v_pvs_tower_input_selected_power)) /\ exists bpvi_q_pvs_tower_input_selected_power_terminal. bpvi_u_pvs_tower_input_selected_power = bpvi_q_pvs_tower_input_selected_power_terminal * S ((S (e)) * bpvi_v_pvs_tower_input_selected_power) + (bpvi_result_pvs_tower_input_selected))) /\ forall bpvi_j_pvs_tower_input_selected_power. (exists bpvi_product_gap_pvs_tower_input_selected_power. bpvi_product_gap_pvs_tower_input_selected_power + S bpvi_j_pvs_tower_input_selected_power = e) -> exists bpvi_factor_pvs_tower_input_selected_power bpvi_partial_pvs_tower_input_selected_power bpvi_successor_pvs_tower_input_selected_power. ((((exists bpvi_h_pvs_tower_input_selected_power_factor. bpvi_h_pvs_tower_input_selected_power_factor + S (bpvi_factor_pvs_tower_input_selected_power) = S ((S (bpvi_j_pvs_tower_input_selected_power)) * bpvi_c_pvs_tower_input_selected_power)) /\ exists bpvi_q_pvs_tower_input_selected_power_factor. bpvi_b_pvs_tower_input_selected_power = bpvi_q_pvs_tower_input_selected_power_factor * S ((S (bpvi_j_pvs_tower_input_selected_power)) * bpvi_c_pvs_tower_input_selected_power) + (bpvi_factor_pvs_tower_input_selected_power))) /\ ((((exists bpvi_h_pvs_tower_input_selected_power_partial. bpvi_h_pvs_tower_input_selected_power_partial + S (bpvi_partial_pvs_tower_input_selected_power) = S ((S (bpvi_j_pvs_tower_input_selected_power)) * bpvi_v_pvs_tower_input_selected_power)) /\ exists bpvi_q_pvs_tower_input_selected_power_partial. bpvi_u_pvs_tower_input_selected_power = bpvi_q_pvs_tower_input_selected_power_partial * S ((S (bpvi_j_pvs_tower_input_selected_power)) * bpvi_v_pvs_tower_input_selected_power) + (bpvi_partial_pvs_tower_input_selected_power))) /\ ((((exists bpvi_h_pvs_tower_input_selected_power_successor. bpvi_h_pvs_tower_input_selected_power_successor + S (bpvi_successor_pvs_tower_input_selected_power) = S ((S (S bpvi_j_pvs_tower_input_selected_power)) * bpvi_v_pvs_tower_input_selected_power)) /\ exists bpvi_q_pvs_tower_input_selected_power_successor. bpvi_u_pvs_tower_input_selected_power = bpvi_q_pvs_tower_input_selected_power_successor * S ((S (S bpvi_j_pvs_tower_input_selected_power)) * bpvi_v_pvs_tower_input_selected_power) + (bpvi_successor_pvs_tower_input_selected_power))) /\ bpvi_successor_pvs_tower_input_selected_power = bpvi_partial_pvs_tower_input_selected_power * bpvi_factor_pvs_tower_input_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_tower_input_selected. d = bpvi_result_pvs_tower_input_selected * bpvi_divisor_factor_pvs_tower_input_selected))) /\ forall bpd_candidate_pvs_tower_input. (exists bpd_gap_pvs_tower_input_candidate_bound. bpd_gap_pvs_tower_input_candidate_bound + (bpd_candidate_pvs_tower_input) = (d)) -> (exists bpvi_result_pvs_tower_input_candidate. ((exists bpvi_b_pvs_tower_input_candidate_power bpvi_c_pvs_tower_input_candidate_power. ((forall bpvi_i_pvs_tower_input_candidate_power. (exists bpvi_repeat_gap_pvs_tower_input_candidate_power. bpvi_repeat_gap_pvs_tower_input_candidate_power + S bpvi_i_pvs_tower_input_candidate_power = bpd_candidate_pvs_tower_input) -> (((exists bpvi_h_pvs_tower_input_candidate_power_repeat. bpvi_h_pvs_tower_input_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_tower_input_candidate_power)) * bpvi_c_pvs_tower_input_candidate_power)) /\ exists bpvi_q_pvs_tower_input_candidate_power_repeat. bpvi_b_pvs_tower_input_candidate_power = bpvi_q_pvs_tower_input_candidate_power_repeat * S ((S (bpvi_i_pvs_tower_input_candidate_power)) * bpvi_c_pvs_tower_input_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_tower_input_candidate_power bpvi_v_pvs_tower_input_candidate_power. ((((exists bpvi_h_pvs_tower_input_candidate_power_start. bpvi_h_pvs_tower_input_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_tower_input_candidate_power)) /\ exists bpvi_q_pvs_tower_input_candidate_power_start. bpvi_u_pvs_tower_input_candidate_power = bpvi_q_pvs_tower_input_candidate_power_start * S ((S (0)) * bpvi_v_pvs_tower_input_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_tower_input_candidate_power_terminal. bpvi_h_pvs_tower_input_candidate_power_terminal + S (bpvi_result_pvs_tower_input_candidate) = S ((S (bpd_candidate_pvs_tower_input)) * bpvi_v_pvs_tower_input_candidate_power)) /\ exists bpvi_q_pvs_tower_input_candidate_power_terminal. bpvi_u_pvs_tower_input_candidate_power = bpvi_q_pvs_tower_input_candidate_power_terminal * S ((S (bpd_candidate_pvs_tower_input)) * bpvi_v_pvs_tower_input_candidate_power) + (bpvi_result_pvs_tower_input_candidate))) /\ forall bpvi_j_pvs_tower_input_candidate_power. (exists bpvi_product_gap_pvs_tower_input_candidate_power. bpvi_product_gap_pvs_tower_input_candidate_power + S bpvi_j_pvs_tower_input_candidate_power = bpd_candidate_pvs_tower_input) -> exists bpvi_factor_pvs_tower_input_candidate_power bpvi_partial_pvs_tower_input_candidate_power bpvi_successor_pvs_tower_input_candidate_power. ((((exists bpvi_h_pvs_tower_input_candidate_power_factor. bpvi_h_pvs_tower_input_candidate_power_factor + S (bpvi_factor_pvs_tower_input_candidate_power) = S ((S (bpvi_j_pvs_tower_input_candidate_power)) * bpvi_c_pvs_tower_input_candidate_power)) /\ exists bpvi_q_pvs_tower_input_candidate_power_factor. bpvi_b_pvs_tower_input_candidate_power = bpvi_q_pvs_tower_input_candidate_power_factor * S ((S (bpvi_j_pvs_tower_input_candidate_power)) * bpvi_c_pvs_tower_input_candidate_power) + (bpvi_factor_pvs_tower_input_candidate_power))) /\ ((((exists bpvi_h_pvs_tower_input_candidate_power_partial. bpvi_h_pvs_tower_input_candidate_power_partial + S (bpvi_partial_pvs_tower_input_candidate_power) = S ((S (bpvi_j_pvs_tower_input_candidate_power)) * bpvi_v_pvs_tower_input_candidate_power)) /\ exists bpvi_q_pvs_tower_input_candidate_power_partial. bpvi_u_pvs_tower_input_candidate_power = bpvi_q_pvs_tower_input_candidate_power_partial * S ((S (bpvi_j_pvs_tower_input_candidate_power)) * bpvi_v_pvs_tower_input_candidate_power) + (bpvi_partial_pvs_tower_input_candidate_power))) /\ ((((exists bpvi_h_pvs_tower_input_candidate_power_successor. bpvi_h_pvs_tower_input_candidate_power_successor + S (bpvi_successor_pvs_tower_input_candidate_power) = S ((S (S bpvi_j_pvs_tower_input_candidate_power)) * bpvi_v_pvs_tower_input_candidate_power)) /\ exists bpvi_q_pvs_tower_input_candidate_power_successor. bpvi_u_pvs_tower_input_candidate_power = bpvi_q_pvs_tower_input_candidate_power_successor * S ((S (S bpvi_j_pvs_tower_input_candidate_power)) * bpvi_v_pvs_tower_input_candidate_power) + (bpvi_successor_pvs_tower_input_candidate_power))) /\ bpvi_successor_pvs_tower_input_candidate_power = bpvi_partial_pvs_tower_input_candidate_power * bpvi_factor_pvs_tower_input_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_tower_input_candidate. d = bpvi_result_pvs_tower_input_candidate * bpvi_divisor_factor_pvs_tower_input_candidate)) -> (exists bpd_gap_pvs_tower_input_maximal. bpd_gap_pvs_tower_input_maximal + (bpd_candidate_pvs_tower_input) = (e))) -> exists q A B D. (((exists pa_b_olte_tower_resultexponent pa_c_olte_tower_resultexponent. ((forall pa_i_olte_tower_resultexponent_repeat. (exists pa_lt_olte_tower_resultexponent_repeat_bound. pa_lt_olte_tower_resultexponent_repeat_bound + S pa_i_olte_tower_resultexponent_repeat = k) -> (((exists pa_h_olte_tower_resultexponent_repeat_decoded. pa_h_olte_tower_resultexponent_repeat_decoded + S (p) = S ((S (pa_i_olte_tower_resultexponent_repeat)) * pa_c_olte_tower_resultexponent)) /\ exists pa_q_olte_tower_resultexponent_repeat_decoded. pa_b_olte_tower_resultexponent = pa_q_olte_tower_resultexponent_repeat_decoded * S ((S (pa_i_olte_tower_resultexponent_repeat)) * pa_c_olte_tower_resultexponent) + (p)))) /\ (exists pa_u_olte_tower_resultexponent_product pa_v_olte_tower_resultexponent_product. ((((exists pa_h_olte_tower_resultexponent_product_start. pa_h_olte_tower_resultexponent_product_start + S (1) = S ((S (0)) * pa_v_olte_tower_resultexponent_product)) /\ exists pa_q_olte_tower_resultexponent_product_start. pa_u_olte_tower_resultexponent_product = pa_q_olte_tower_resultexponent_product_start * S ((S (0)) * pa_v_olte_tower_resultexponent_product) + (1))) /\ ((((exists pa_h_olte_tower_resultexponent_product_terminal. pa_h_olte_tower_resultexponent_product_terminal + S (q) = S ((S (k)) * pa_v_olte_tower_resultexponent_product)) /\ exists pa_q_olte_tower_resultexponent_product_terminal. pa_u_olte_tower_resultexponent_product = pa_q_olte_tower_resultexponent_product_terminal * S ((S (k)) * pa_v_olte_tower_resultexponent_product) + (q))) /\ forall pa_i_olte_tower_resultexponent_product. (exists pa_lt_olte_tower_resultexponent_product_bound. pa_lt_olte_tower_resultexponent_product_bound + S pa_i_olte_tower_resultexponent_product = k) -> exists pa_p_olte_tower_resultexponent_product pa_r_olte_tower_resultexponent_product pa_s_olte_tower_resultexponent_product. ((((exists pa_h_olte_tower_resultexponent_product_factor. pa_h_olte_tower_resultexponent_product_factor + S (pa_p_olte_tower_resultexponent_product) = S ((S (pa_i_olte_tower_resultexponent_product)) * pa_c_olte_tower_resultexponent)) /\ exists pa_q_olte_tower_resultexponent_product_factor. pa_b_olte_tower_resultexponent = pa_q_olte_tower_resultexponent_product_factor * S ((S (pa_i_olte_tower_resultexponent_product)) * pa_c_olte_tower_resultexponent) + (pa_p_olte_tower_resultexponent_product))) /\ ((((exists pa_h_olte_tower_resultexponent_product_partial. pa_h_olte_tower_resultexponent_product_partial + S (pa_r_olte_tower_resultexponent_product) = S ((S (pa_i_olte_tower_resultexponent_product)) * pa_v_olte_tower_resultexponent_product)) /\ exists pa_q_olte_tower_resultexponent_product_partial. pa_u_olte_tower_resultexponent_product = pa_q_olte_tower_resultexponent_product_partial * S ((S (pa_i_olte_tower_resultexponent_product)) * pa_v_olte_tower_resultexponent_product) + (pa_r_olte_tower_resultexponent_product))) /\ ((((exists pa_h_olte_tower_resultexponent_product_successor. pa_h_olte_tower_resultexponent_product_successor + S (pa_s_olte_tower_resultexponent_product) = S ((S (S pa_i_olte_tower_resultexponent_product)) * pa_v_olte_tower_resultexponent_product)) /\ exists pa_q_olte_tower_resultexponent_product_successor. pa_u_olte_tower_resultexponent_product = pa_q_olte_tower_resultexponent_product_successor * S ((S (S pa_i_olte_tower_resultexponent_product)) * pa_v_olte_tower_resultexponent_product) + (pa_s_olte_tower_resultexponent_product))) /\ pa_s_olte_tower_resultexponent_product = pa_r_olte_tower_resultexponent_product * pa_p_olte_tower_resultexponent_product)))))))) /\ (((exists pa_b_olte_tower_resultdifferenceA pa_c_olte_tower_resultdifferenceA. ((forall pa_i_olte_tower_resultdifferenceA_repeat. (exists pa_lt_olte_tower_resultdifferenceA_repeat_bound. pa_lt_olte_tower_resultdifferenceA_repeat_bound + S pa_i_olte_tower_resultdifferenceA_repeat = q) -> (((exists pa_h_olte_tower_resultdifferenceA_repeat_decoded. pa_h_olte_tower_resultdifferenceA_repeat_decoded + S (a) = S ((S (pa_i_olte_tower_resultdifferenceA_repeat)) * pa_c_olte_tower_resultdifferenceA)) /\ exists pa_q_olte_tower_resultdifferenceA_repeat_decoded. pa_b_olte_tower_resultdifferenceA = pa_q_olte_tower_resultdifferenceA_repeat_decoded * S ((S (pa_i_olte_tower_resultdifferenceA_repeat)) * pa_c_olte_tower_resultdifferenceA) + (a)))) /\ (exists pa_u_olte_tower_resultdifferenceA_product pa_v_olte_tower_resultdifferenceA_product. ((((exists pa_h_olte_tower_resultdifferenceA_product_start. pa_h_olte_tower_resultdifferenceA_product_start + S (1) = S ((S (0)) * pa_v_olte_tower_resultdifferenceA_product)) /\ exists pa_q_olte_tower_resultdifferenceA_product_start. pa_u_olte_tower_resultdifferenceA_product = pa_q_olte_tower_resultdifferenceA_product_start * S ((S (0)) * pa_v_olte_tower_resultdifferenceA_product) + (1))) /\ ((((exists pa_h_olte_tower_resultdifferenceA_product_terminal. pa_h_olte_tower_resultdifferenceA_product_terminal + S (A) = S ((S (q)) * pa_v_olte_tower_resultdifferenceA_product)) /\ exists pa_q_olte_tower_resultdifferenceA_product_terminal. pa_u_olte_tower_resultdifferenceA_product = pa_q_olte_tower_resultdifferenceA_product_terminal * S ((S (q)) * pa_v_olte_tower_resultdifferenceA_product) + (A))) /\ forall pa_i_olte_tower_resultdifferenceA_product. (exists pa_lt_olte_tower_resultdifferenceA_product_bound. pa_lt_olte_tower_resultdifferenceA_product_bound + S pa_i_olte_tower_resultdifferenceA_product = q) -> exists pa_p_olte_tower_resultdifferenceA_product pa_r_olte_tower_resultdifferenceA_product pa_s_olte_tower_resultdifferenceA_product. ((((exists pa_h_olte_tower_resultdifferenceA_product_factor. pa_h_olte_tower_resultdifferenceA_product_factor + S (pa_p_olte_tower_resultdifferenceA_product) = S ((S (pa_i_olte_tower_resultdifferenceA_product)) * pa_c_olte_tower_resultdifferenceA)) /\ exists pa_q_olte_tower_resultdifferenceA_product_factor. pa_b_olte_tower_resultdifferenceA = pa_q_olte_tower_resultdifferenceA_product_factor * S ((S (pa_i_olte_tower_resultdifferenceA_product)) * pa_c_olte_tower_resultdifferenceA) + (pa_p_olte_tower_resultdifferenceA_product))) /\ ((((exists pa_h_olte_tower_resultdifferenceA_product_partial. pa_h_olte_tower_resultdifferenceA_product_partial + S (pa_r_olte_tower_resultdifferenceA_product) = S ((S (pa_i_olte_tower_resultdifferenceA_product)) * pa_v_olte_tower_resultdifferenceA_product)) /\ exists pa_q_olte_tower_resultdifferenceA_product_partial. pa_u_olte_tower_resultdifferenceA_product = pa_q_olte_tower_resultdifferenceA_product_partial * S ((S (pa_i_olte_tower_resultdifferenceA_product)) * pa_v_olte_tower_resultdifferenceA_product) + (pa_r_olte_tower_resultdifferenceA_product))) /\ ((((exists pa_h_olte_tower_resultdifferenceA_product_successor. pa_h_olte_tower_resultdifferenceA_product_successor + S (pa_s_olte_tower_resultdifferenceA_product) = S ((S (S pa_i_olte_tower_resultdifferenceA_product)) * pa_v_olte_tower_resultdifferenceA_product)) /\ exists pa_q_olte_tower_resultdifferenceA_product_successor. pa_u_olte_tower_resultdifferenceA_product = pa_q_olte_tower_resultdifferenceA_product_successor * S ((S (S pa_i_olte_tower_resultdifferenceA_product)) * pa_v_olte_tower_resultdifferenceA_product) + (pa_s_olte_tower_resultdifferenceA_product))) /\ pa_s_olte_tower_resultdifferenceA_product = pa_r_olte_tower_resultdifferenceA_product * pa_p_olte_tower_resultdifferenceA_product)))))))) /\ (((exists pa_b_olte_tower_resultdifferenceB pa_c_olte_tower_resultdifferenceB. ((forall pa_i_olte_tower_resultdifferenceB_repeat. (exists pa_lt_olte_tower_resultdifferenceB_repeat_bound. pa_lt_olte_tower_resultdifferenceB_repeat_bound + S pa_i_olte_tower_resultdifferenceB_repeat = q) -> (((exists pa_h_olte_tower_resultdifferenceB_repeat_decoded. pa_h_olte_tower_resultdifferenceB_repeat_decoded + S (b) = S ((S (pa_i_olte_tower_resultdifferenceB_repeat)) * pa_c_olte_tower_resultdifferenceB)) /\ exists pa_q_olte_tower_resultdifferenceB_repeat_decoded. pa_b_olte_tower_resultdifferenceB = pa_q_olte_tower_resultdifferenceB_repeat_decoded * S ((S (pa_i_olte_tower_resultdifferenceB_repeat)) * pa_c_olte_tower_resultdifferenceB) + (b)))) /\ (exists pa_u_olte_tower_resultdifferenceB_product pa_v_olte_tower_resultdifferenceB_product. ((((exists pa_h_olte_tower_resultdifferenceB_product_start. pa_h_olte_tower_resultdifferenceB_product_start + S (1) = S ((S (0)) * pa_v_olte_tower_resultdifferenceB_product)) /\ exists pa_q_olte_tower_resultdifferenceB_product_start. pa_u_olte_tower_resultdifferenceB_product = pa_q_olte_tower_resultdifferenceB_product_start * S ((S (0)) * pa_v_olte_tower_resultdifferenceB_product) + (1))) /\ ((((exists pa_h_olte_tower_resultdifferenceB_product_terminal. pa_h_olte_tower_resultdifferenceB_product_terminal + S (B) = S ((S (q)) * pa_v_olte_tower_resultdifferenceB_product)) /\ exists pa_q_olte_tower_resultdifferenceB_product_terminal. pa_u_olte_tower_resultdifferenceB_product = pa_q_olte_tower_resultdifferenceB_product_terminal * S ((S (q)) * pa_v_olte_tower_resultdifferenceB_product) + (B))) /\ forall pa_i_olte_tower_resultdifferenceB_product. (exists pa_lt_olte_tower_resultdifferenceB_product_bound. pa_lt_olte_tower_resultdifferenceB_product_bound + S pa_i_olte_tower_resultdifferenceB_product = q) -> exists pa_p_olte_tower_resultdifferenceB_product pa_r_olte_tower_resultdifferenceB_product pa_s_olte_tower_resultdifferenceB_product. ((((exists pa_h_olte_tower_resultdifferenceB_product_factor. pa_h_olte_tower_resultdifferenceB_product_factor + S (pa_p_olte_tower_resultdifferenceB_product) = S ((S (pa_i_olte_tower_resultdifferenceB_product)) * pa_c_olte_tower_resultdifferenceB)) /\ exists pa_q_olte_tower_resultdifferenceB_product_factor. pa_b_olte_tower_resultdifferenceB = pa_q_olte_tower_resultdifferenceB_product_factor * S ((S (pa_i_olte_tower_resultdifferenceB_product)) * pa_c_olte_tower_resultdifferenceB) + (pa_p_olte_tower_resultdifferenceB_product))) /\ ((((exists pa_h_olte_tower_resultdifferenceB_product_partial. pa_h_olte_tower_resultdifferenceB_product_partial + S (pa_r_olte_tower_resultdifferenceB_product) = S ((S (pa_i_olte_tower_resultdifferenceB_product)) * pa_v_olte_tower_resultdifferenceB_product)) /\ exists pa_q_olte_tower_resultdifferenceB_product_partial. pa_u_olte_tower_resultdifferenceB_product = pa_q_olte_tower_resultdifferenceB_product_partial * S ((S (pa_i_olte_tower_resultdifferenceB_product)) * pa_v_olte_tower_resultdifferenceB_product) + (pa_r_olte_tower_resultdifferenceB_product))) /\ ((((exists pa_h_olte_tower_resultdifferenceB_product_successor. pa_h_olte_tower_resultdifferenceB_product_successor + S (pa_s_olte_tower_resultdifferenceB_product) = S ((S (S pa_i_olte_tower_resultdifferenceB_product)) * pa_v_olte_tower_resultdifferenceB_product)) /\ exists pa_q_olte_tower_resultdifferenceB_product_successor. pa_u_olte_tower_resultdifferenceB_product = pa_q_olte_tower_resultdifferenceB_product_successor * S ((S (S pa_i_olte_tower_resultdifferenceB_product)) * pa_v_olte_tower_resultdifferenceB_product) + (pa_s_olte_tower_resultdifferenceB_product))) /\ pa_s_olte_tower_resultdifferenceB_product = pa_r_olte_tower_resultdifferenceB_product * pa_p_olte_tower_resultdifferenceB_product)))))))) /\ ((((A) = (B) + (D)) /\ (((~((D) = 0)) /\ (((exists olte_factor_tower_resultdifferencedivides. (D) = (p) * olte_factor_tower_resultdifferencedivides) /\ (((~(exists olte_factor_tower_resultdifferenceunit. (B) = (p) * olte_factor_tower_resultdifferenceunit)) /\ (((exists bpd_gap_pvs_olte_tower_resultdifferencevaluation_selected_bound. bpd_gap_pvs_olte_tower_resultdifferencevaluation_selected_bound + ((e) + (k)) = (D)) /\ (exists bpvi_result_pvs_olte_tower_resultdifferencevaluation_selected. ((exists bpvi_b_pvs_olte_tower_resultdifferencevaluation_selected_power bpvi_c_pvs_olte_tower_resultdifferencevaluation_selected_power. ((forall bpvi_i_pvs_olte_tower_resultdifferencevaluation_selected_power. (exists bpvi_repeat_gap_pvs_olte_tower_resultdifferencevaluation_selected_power. bpvi_repeat_gap_pvs_olte_tower_resultdifferencevaluation_selected_power + S bpvi_i_pvs_olte_tower_resultdifferencevaluation_selected_power = (e) + (k)) -> (((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_repeat. bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_repeat + S (p) = S ((S (bpvi_i_pvs_olte_tower_resultdifferencevaluation_selected_power)) * bpvi_c_pvs_olte_tower_resultdifferencevaluation_selected_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_repeat. bpvi_b_pvs_olte_tower_resultdifferencevaluation_selected_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_repeat * S ((S (bpvi_i_pvs_olte_tower_resultdifferencevaluation_selected_power)) * bpvi_c_pvs_olte_tower_resultdifferencevaluation_selected_power) + (p)))) /\ (exists bpvi_u_pvs_olte_tower_resultdifferencevaluation_selected_power bpvi_v_pvs_olte_tower_resultdifferencevaluation_selected_power. ((((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_start. bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_selected_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_start. bpvi_u_pvs_olte_tower_resultdifferencevaluation_selected_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_start * S ((S (0)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_selected_power) + (1))) /\ ((((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_terminal. bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_terminal + S (bpvi_result_pvs_olte_tower_resultdifferencevaluation_selected) = S ((S ((e) + (k))) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_selected_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_terminal. bpvi_u_pvs_olte_tower_resultdifferencevaluation_selected_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_terminal * S ((S ((e) + (k))) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_selected_power) + (bpvi_result_pvs_olte_tower_resultdifferencevaluation_selected))) /\ forall bpvi_j_pvs_olte_tower_resultdifferencevaluation_selected_power. (exists bpvi_product_gap_pvs_olte_tower_resultdifferencevaluation_selected_power. bpvi_product_gap_pvs_olte_tower_resultdifferencevaluation_selected_power + S bpvi_j_pvs_olte_tower_resultdifferencevaluation_selected_power = (e) + (k)) -> exists bpvi_factor_pvs_olte_tower_resultdifferencevaluation_selected_power bpvi_partial_pvs_olte_tower_resultdifferencevaluation_selected_power bpvi_successor_pvs_olte_tower_resultdifferencevaluation_selected_power. ((((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_factor. bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_factor + S (bpvi_factor_pvs_olte_tower_resultdifferencevaluation_selected_power) = S ((S (bpvi_j_pvs_olte_tower_resultdifferencevaluation_selected_power)) * bpvi_c_pvs_olte_tower_resultdifferencevaluation_selected_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_factor. bpvi_b_pvs_olte_tower_resultdifferencevaluation_selected_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_factor * S ((S (bpvi_j_pvs_olte_tower_resultdifferencevaluation_selected_power)) * bpvi_c_pvs_olte_tower_resultdifferencevaluation_selected_power) + (bpvi_factor_pvs_olte_tower_resultdifferencevaluation_selected_power))) /\ ((((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_partial. bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_partial + S (bpvi_partial_pvs_olte_tower_resultdifferencevaluation_selected_power) = S ((S (bpvi_j_pvs_olte_tower_resultdifferencevaluation_selected_power)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_selected_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_partial. bpvi_u_pvs_olte_tower_resultdifferencevaluation_selected_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_partial * S ((S (bpvi_j_pvs_olte_tower_resultdifferencevaluation_selected_power)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_selected_power) + (bpvi_partial_pvs_olte_tower_resultdifferencevaluation_selected_power))) /\ ((((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_successor. bpvi_h_pvs_olte_tower_resultdifferencevaluation_selected_power_successor + S (bpvi_successor_pvs_olte_tower_resultdifferencevaluation_selected_power) = S ((S (S bpvi_j_pvs_olte_tower_resultdifferencevaluation_selected_power)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_selected_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_successor. bpvi_u_pvs_olte_tower_resultdifferencevaluation_selected_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_selected_power_successor * S ((S (S bpvi_j_pvs_olte_tower_resultdifferencevaluation_selected_power)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_selected_power) + (bpvi_successor_pvs_olte_tower_resultdifferencevaluation_selected_power))) /\ bpvi_successor_pvs_olte_tower_resultdifferencevaluation_selected_power = bpvi_partial_pvs_olte_tower_resultdifferencevaluation_selected_power * bpvi_factor_pvs_olte_tower_resultdifferencevaluation_selected_power)))))))) /\ exists bpvi_divisor_factor_pvs_olte_tower_resultdifferencevaluation_selected. D = bpvi_result_pvs_olte_tower_resultdifferencevaluation_selected * bpvi_divisor_factor_pvs_olte_tower_resultdifferencevaluation_selected))) /\ forall bpd_candidate_pvs_olte_tower_resultdifferencevaluation. (exists bpd_gap_pvs_olte_tower_resultdifferencevaluation_candidate_bound. bpd_gap_pvs_olte_tower_resultdifferencevaluation_candidate_bound + (bpd_candidate_pvs_olte_tower_resultdifferencevaluation) = (D)) -> (exists bpvi_result_pvs_olte_tower_resultdifferencevaluation_candidate. ((exists bpvi_b_pvs_olte_tower_resultdifferencevaluation_candidate_power bpvi_c_pvs_olte_tower_resultdifferencevaluation_candidate_power. ((forall bpvi_i_pvs_olte_tower_resultdifferencevaluation_candidate_power. (exists bpvi_repeat_gap_pvs_olte_tower_resultdifferencevaluation_candidate_power. bpvi_repeat_gap_pvs_olte_tower_resultdifferencevaluation_candidate_power + S bpvi_i_pvs_olte_tower_resultdifferencevaluation_candidate_power = bpd_candidate_pvs_olte_tower_resultdifferencevaluation) -> (((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_repeat. bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_repeat + S (p) = S ((S (bpvi_i_pvs_olte_tower_resultdifferencevaluation_candidate_power)) * bpvi_c_pvs_olte_tower_resultdifferencevaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_repeat. bpvi_b_pvs_olte_tower_resultdifferencevaluation_candidate_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_repeat * S ((S (bpvi_i_pvs_olte_tower_resultdifferencevaluation_candidate_power)) * bpvi_c_pvs_olte_tower_resultdifferencevaluation_candidate_power) + (p)))) /\ (exists bpvi_u_pvs_olte_tower_resultdifferencevaluation_candidate_power bpvi_v_pvs_olte_tower_resultdifferencevaluation_candidate_power. ((((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_start. bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_start. bpvi_u_pvs_olte_tower_resultdifferencevaluation_candidate_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_start * S ((S (0)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_candidate_power) + (1))) /\ ((((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_terminal. bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_terminal + S (bpvi_result_pvs_olte_tower_resultdifferencevaluation_candidate) = S ((S (bpd_candidate_pvs_olte_tower_resultdifferencevaluation)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_terminal. bpvi_u_pvs_olte_tower_resultdifferencevaluation_candidate_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_terminal * S ((S (bpd_candidate_pvs_olte_tower_resultdifferencevaluation)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_candidate_power) + (bpvi_result_pvs_olte_tower_resultdifferencevaluation_candidate))) /\ forall bpvi_j_pvs_olte_tower_resultdifferencevaluation_candidate_power. (exists bpvi_product_gap_pvs_olte_tower_resultdifferencevaluation_candidate_power. bpvi_product_gap_pvs_olte_tower_resultdifferencevaluation_candidate_power + S bpvi_j_pvs_olte_tower_resultdifferencevaluation_candidate_power = bpd_candidate_pvs_olte_tower_resultdifferencevaluation) -> exists bpvi_factor_pvs_olte_tower_resultdifferencevaluation_candidate_power bpvi_partial_pvs_olte_tower_resultdifferencevaluation_candidate_power bpvi_successor_pvs_olte_tower_resultdifferencevaluation_candidate_power. ((((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_factor. bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_factor + S (bpvi_factor_pvs_olte_tower_resultdifferencevaluation_candidate_power) = S ((S (bpvi_j_pvs_olte_tower_resultdifferencevaluation_candidate_power)) * bpvi_c_pvs_olte_tower_resultdifferencevaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_factor. bpvi_b_pvs_olte_tower_resultdifferencevaluation_candidate_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_factor * S ((S (bpvi_j_pvs_olte_tower_resultdifferencevaluation_candidate_power)) * bpvi_c_pvs_olte_tower_resultdifferencevaluation_candidate_power) + (bpvi_factor_pvs_olte_tower_resultdifferencevaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_partial. bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_partial + S (bpvi_partial_pvs_olte_tower_resultdifferencevaluation_candidate_power) = S ((S (bpvi_j_pvs_olte_tower_resultdifferencevaluation_candidate_power)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_partial. bpvi_u_pvs_olte_tower_resultdifferencevaluation_candidate_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_partial * S ((S (bpvi_j_pvs_olte_tower_resultdifferencevaluation_candidate_power)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_candidate_power) + (bpvi_partial_pvs_olte_tower_resultdifferencevaluation_candidate_power))) /\ ((((exists bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_successor. bpvi_h_pvs_olte_tower_resultdifferencevaluation_candidate_power_successor + S (bpvi_successor_pvs_olte_tower_resultdifferencevaluation_candidate_power) = S ((S (S bpvi_j_pvs_olte_tower_resultdifferencevaluation_candidate_power)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_candidate_power)) /\ exists bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_successor. bpvi_u_pvs_olte_tower_resultdifferencevaluation_candidate_power = bpvi_q_pvs_olte_tower_resultdifferencevaluation_candidate_power_successor * S ((S (S bpvi_j_pvs_olte_tower_resultdifferencevaluation_candidate_power)) * bpvi_v_pvs_olte_tower_resultdifferencevaluation_candidate_power) + (bpvi_successor_pvs_olte_tower_resultdifferencevaluation_candidate_power))) /\ bpvi_successor_pvs_olte_tower_resultdifferencevaluation_candidate_power = bpvi_partial_pvs_olte_tower_resultdifferencevaluation_candidate_power * bpvi_factor_pvs_olte_tower_resultdifferencevaluation_candidate_power)))))))) /\ exists bpvi_divisor_factor_pvs_olte_tower_resultdifferencevaluation_candidate. D = bpvi_result_pvs_olte_tower_resultdifferencevaluation_candidate * bpvi_divisor_factor_pvs_olte_tower_resultdifferencevaluation_candidate)) -> (exists bpd_gap_pvs_olte_tower_resultdifferencevaluation_maximal. bpd_gap_pvs_olte_tower_resultdifferencevaluation_maximal + (bpd_candidate_pvs_olte_tower_resultdifferencevaluation) = ((e) + (k))))))))))))))))))

Complete tactic proof in conservative notation

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

142 script commands · 48 reading checkpoints · 2 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)
lte power zero exactlte power one exactlte odd prime power steplte power iteration construct
01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro d
  5. L5
    intro e
02Induction on kL6–13

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

  1. L6
    induction k
  2. L7
    intro hp
  3. L8
    intro hne
  4. L9
    intro ha
  5. L10
    intro hdzero
  6. L11
    intro hd
  7. L12
    intro hb
  8. L13
    intro hval
03Construct an explicit witnessL14–17

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

  1. L14
    exists 1
  2. L15
    exists a
  3. L16
    exists b
  4. L17
    exists d
04Separate the logical casesL18–18

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

  1. L18
    split
05Use earlier factsL19–20

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

  1. L19
    specialize lte_power_zero_exact (p)
  2. L20
    apply lte_power_zero_exact
06Separate the logical casesL21–21

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

  1. L21
    split
07Use earlier factsL22–23

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

  1. L22
    specialize lte_power_one_exact (a)
  2. L23
    apply lte_power_one_exact
08Separate the logical casesL24–24

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

  1. L24
    split
09Use earlier factsL25–26

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

  1. L25
    specialize lte_power_one_exact (b)
  2. L26
    apply lte_power_one_exact
10Separate the logical casesL27–27

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

  1. L27
    split
11Use earlier factsL28–28

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

  1. L28
    exact ha
12Separate the logical casesL29–29

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

  1. L29
    split
13Use earlier factsL30–30

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

  1. L30
    exact hdzero
14Separate the logical casesL31–31

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

  1. L31
    split
15Use earlier factsL32–32

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

  1. L32
    exact hd
16Separate the logical casesL33–33

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

  1. L33
    split
17Use earlier factsL34–39

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

  1. L34
    exact hb
  2. L35
    specialize prime_valuation_exponent_eq_transport (p)
  3. L36
    specialize prime_valuation_exponent_eq_transport (d)
  4. L37
    specialize prime_valuation_exponent_eq_transport (e)
  5. L38
    specialize prime_valuation_exponent_eq_transport (e + 0)
  6. L39
    apply prime_valuation_exponent_eq_transport
18Calculate and transport equalitiesL40–40

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

  1. L40
    symm
19Use earlier factsL41–42

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

  1. L41
    apply PA3
  2. L42
    exact hval
20Fix variables and assumptionsL43–49

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

  1. L43
    intro hp
  2. L44
    intro hne
  3. L45
    intro ha
  4. L46
    intro hdzero
  5. L47
    intro hd
  6. L48
    intro hb
  7. L49
    intro hval
21Establish hpreviousL50–58

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

  1. L50
    have hprevious : ∃ q. ∃ A. ∃ B. ∃ D. Pow(p,k,q) ∧ LiftedPowerDifference(p,a,b,q,e + k,A,B,D)Definitions: Pow(p,k,q)LiftedPowerDifference(p,a,b,q,e + k,A,B,D)Original native command in the exact edition
  2. L51
    apply IH
  3. L52
    exact hp
  4. L53
    exact hne
  5. L54
    exact ha
  6. L55
    exact hdzero
  7. L56
    exact hd
  8. L57
    exact hb
  9. L58
    exact hval
22Separate the logical casesL59–68

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

  1. L59
    cases hprevious
  2. L60
    cases hprevious_witness
  3. L61
    cases hprevious_witness_witness
  4. L62
    cases hprevious_witness_witness_witness
  5. L63
    cases hprevious_witness_witness_witness_witness
  6. L64
    cases hprevious_witness_witness_witness_witness_right
  7. L65
    cases hprevious_witness_witness_witness_witness_right_right
  8. L66
    cases hprevious_witness_witness_witness_witness_right_right_right
  9. L67
    cases hprevious_witness_witness_witness_witness_right_right_right_right
  10. L68
    cases hprevious_witness_witness_witness_witness_right_right_right_right_right
23Separate the logical casesL69–69

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

  1. L69
    cases hprevious_witness_witness_witness_witness_right_right_right_right_right_right
24Establish hstepL70–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lte odd prime power step.

  1. L70
    have hstep : ∃ A. ∃ B. ∃ D. LiftedPowerDifference(p,x1,x2,p,S (e + k),A,B,D)Definitions: LiftedPowerDifference(p,x1,x2,p,S (e + k),A,B,D)Original native command in the exact edition
  2. L71
    specialize lte_odd_prime_power_step (p)
  3. L72
    specialize lte_odd_prime_power_step (x1)
  4. L73
    specialize lte_odd_prime_power_step (x2)
  5. L74
    specialize lte_odd_prime_power_step (x3)
  6. L75
    specialize lte_odd_prime_power_step (e + k)
  7. L76
    apply lte_odd_prime_power_step
  8. L77
    exact hp
  9. L78
    exact hne
  10. L79
    exact hprevious_witness_witness_witness_witness_right_right_right_left
25Use earlier factsL80–83

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

  1. L80
    exact hprevious_witness_witness_witness_witness_right_right_right_right_left
  2. L81
    exact hprevious_witness_witness_witness_witness_right_right_right_right_right_left
  3. L82
    exact hprevious_witness_witness_witness_witness_right_right_right_right_right_right_left
  4. L83
    exact hprevious_witness_witness_witness_witness_right_right_right_right_right_right_right
26Separate the logical casesL84–92

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

  1. L84
    cases hstep
  2. L85
    cases hstep_witness
  3. L86
    cases hstep_witness_witness
  4. L87
    cases hstep_witness_witness_witness
  5. L88
    cases hstep_witness_witness_witness_right
  6. L89
    cases hstep_witness_witness_witness_right_right
  7. L90
    cases hstep_witness_witness_witness_right_right_right
  8. L91
    cases hstep_witness_witness_witness_right_right_right_right
  9. L92
    cases hstep_witness_witness_witness_right_right_right_right_right
27Construct an explicit witnessL93–96

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

  1. L93
    exists x * p
  2. L94
    exists x4
  3. L95
    exists x5
  4. L96
    exists x6
28Separate the logical casesL97–97

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

  1. L97
    split
29Use earlier factsL98–103

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

  1. L98
    specialize pow_successor_compose (p)
  2. L99
    specialize pow_successor_compose (k)
  3. L100
    specialize pow_successor_compose (x)
  4. L101
    specialize pow_successor_compose (x * p)
  5. L102
    apply pow_successor_compose
  6. L103
    exact hprevious_witness_witness_witness_witness_left
30Calculate and transport equalitiesL104–104

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

  1. L104
    refl
31Separate the logical casesL105–105

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

  1. L105
    split
32Use earlier factsL106–112

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

  1. L106
    specialize lte_power_iteration_construct (a)
  2. L107
    specialize lte_power_iteration_construct (x)
  3. L108
    specialize lte_power_iteration_construct (p)
  4. L109
    specialize lte_power_iteration_construct (x * p)
  5. L110
    specialize lte_power_iteration_construct (x1)
  6. L111
    specialize lte_power_iteration_construct (x4)
  7. L112
    apply lte_power_iteration_construct
33Calculate and transport equalitiesL113–113

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

  1. L113
    refl
34Use earlier factsL114–115

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

  1. L114
    exact hprevious_witness_witness_witness_witness_right_left
  2. L115
    exact hstep_witness_witness_witness_left
35Separate the logical casesL116–116

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

  1. L116
    split
36Use earlier factsL117–123

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

  1. L117
    specialize lte_power_iteration_construct (b)
  2. L118
    specialize lte_power_iteration_construct (x)
  3. L119
    specialize lte_power_iteration_construct (p)
  4. L120
    specialize lte_power_iteration_construct (x * p)
  5. L121
    specialize lte_power_iteration_construct (x2)
  6. L122
    specialize lte_power_iteration_construct (x5)
  7. L123
    apply lte_power_iteration_construct
37Calculate and transport equalitiesL124–124

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

  1. L124
    refl
38Use earlier factsL125–126

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

  1. L125
    exact hprevious_witness_witness_witness_witness_right_right_left
  2. L126
    exact hstep_witness_witness_witness_right_left
39Separate the logical casesL127–127

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

  1. L127
    split
40Use earlier factsL128–128

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

  1. L128
    exact hstep_witness_witness_witness_right_right_left
41Separate the logical casesL129–129

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

  1. L129
    split
42Use earlier factsL130–130

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

  1. L130
    exact hstep_witness_witness_witness_right_right_right_left
43Separate the logical casesL131–131

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

  1. L131
    split
44Use earlier factsL132–132

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

  1. L132
    exact hstep_witness_witness_witness_right_right_right_right_left
45Separate the logical casesL133–133

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

  1. L133
    split
46Use earlier factsL134–139

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

  1. L134
    exact hstep_witness_witness_witness_right_right_right_right_right_left
  2. L135
    specialize prime_valuation_exponent_eq_transport (p)
  3. L136
    specialize prime_valuation_exponent_eq_transport (x6)
  4. L137
    specialize prime_valuation_exponent_eq_transport (S (e + k))
  5. L138
    specialize prime_valuation_exponent_eq_transport (e + S k)
  6. L139
    apply prime_valuation_exponent_eq_transport
47Calculate and transport equalitiesL140–140

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

  1. L140
    symm
48Use earlier factsL141–142

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

  1. L141
    apply PA4
  2. L142
    exact hstep_witness_witness_witness_right_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 142 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro d
  5. 0005intro e
  6. 0006induction k
  7. 0007intro hp
  8. 0008intro hne
  9. 0009intro ha
  10. 0010intro hdzero
  11. 0011intro hd
  12. 0012intro hb
  13. 0013intro hval
  14. 0014exists 1
  15. 0015exists a
  16. 0016exists b
  17. 0017exists d
  18. 0018split
  19. 0019specialize lte_power_zero_exact (p)
  20. 0020apply lte_power_zero_exact
  21. 0021split
  22. 0022specialize lte_power_one_exact (a)
  23. 0023apply lte_power_one_exact
  24. 0024split
  25. 0025specialize lte_power_one_exact (b)
  26. 0026apply lte_power_one_exact
  27. 0027split
  28. 0028exact ha
  29. 0029split
  30. 0030exact hdzero
  31. 0031split
  32. 0032exact hd
  33. 0033split
  34. 0034exact hb
  35. 0035specialize prime_valuation_exponent_eq_transport (p)
  36. 0036specialize prime_valuation_exponent_eq_transport (d)
  37. 0037specialize prime_valuation_exponent_eq_transport (e)
  38. 0038specialize prime_valuation_exponent_eq_transport (e + 0)
  39. 0039apply prime_valuation_exponent_eq_transport
  40. 0040symm
  41. 0041apply PA3
  42. 0042exact hval
  43. 0043intro hp
  44. 0044intro hne
  45. 0045intro ha
  46. 0046intro hdzero
  47. 0047intro hd
  48. 0048intro hb
  49. 0049intro hval
  50. 0050have hprevious : ∃ q. ∃ A. ∃ B. ∃ D. Pow(p,k,q) ∧ LiftedPowerDifference(p,a,b,q,e + k,A,B,D)
  51. 0051apply IH
  52. 0052exact hp
  53. 0053exact hne
  54. 0054exact ha
  55. 0055exact hdzero
  56. 0056exact hd
  57. 0057exact hb
  58. 0058exact hval
  59. 0059cases hprevious
  60. 0060cases hprevious_witness
  61. 0061cases hprevious_witness_witness
  62. 0062cases hprevious_witness_witness_witness
  63. 0063cases hprevious_witness_witness_witness_witness
  64. 0064cases hprevious_witness_witness_witness_witness_right
  65. 0065cases hprevious_witness_witness_witness_witness_right_right
  66. 0066cases hprevious_witness_witness_witness_witness_right_right_right
  67. 0067cases hprevious_witness_witness_witness_witness_right_right_right_right
  68. 0068cases hprevious_witness_witness_witness_witness_right_right_right_right_right
  69. 0069cases hprevious_witness_witness_witness_witness_right_right_right_right_right_right
  70. 0070have hstep : ∃ A. ∃ B. ∃ D. LiftedPowerDifference(p,x1,x2,p,S (e + k),A,B,D)
  71. 0071specialize lte_odd_prime_power_step (p)
  72. 0072specialize lte_odd_prime_power_step (x1)
  73. 0073specialize lte_odd_prime_power_step (x2)
  74. 0074specialize lte_odd_prime_power_step (x3)
  75. 0075specialize lte_odd_prime_power_step (e + k)
  76. 0076apply lte_odd_prime_power_step
  77. 0077exact hp
  78. 0078exact hne
  79. 0079exact hprevious_witness_witness_witness_witness_right_right_right_left
  80. 0080exact hprevious_witness_witness_witness_witness_right_right_right_right_left
  81. 0081exact hprevious_witness_witness_witness_witness_right_right_right_right_right_left
  82. 0082exact hprevious_witness_witness_witness_witness_right_right_right_right_right_right_left
  83. 0083exact hprevious_witness_witness_witness_witness_right_right_right_right_right_right_right
  84. 0084cases hstep
  85. 0085cases hstep_witness
  86. 0086cases hstep_witness_witness
  87. 0087cases hstep_witness_witness_witness
  88. 0088cases hstep_witness_witness_witness_right
  89. 0089cases hstep_witness_witness_witness_right_right
  90. 0090cases hstep_witness_witness_witness_right_right_right
  91. 0091cases hstep_witness_witness_witness_right_right_right_right
  92. 0092cases hstep_witness_witness_witness_right_right_right_right_right
  93. 0093exists x * p
  94. 0094exists x4
  95. 0095exists x5
  96. 0096exists x6
  97. 0097split
  98. 0098specialize pow_successor_compose (p)
  99. 0099specialize pow_successor_compose (k)
  100. 0100specialize pow_successor_compose (x)
  101. 0101specialize pow_successor_compose (x * p)
  102. 0102apply pow_successor_compose
  103. 0103exact hprevious_witness_witness_witness_witness_left
  104. 0104refl
  105. 0105split
  106. 0106specialize lte_power_iteration_construct (a)
  107. 0107specialize lte_power_iteration_construct (x)
  108. 0108specialize lte_power_iteration_construct (p)
  109. 0109specialize lte_power_iteration_construct (x * p)
  110. 0110specialize lte_power_iteration_construct (x1)
  111. 0111specialize lte_power_iteration_construct (x4)
  112. 0112apply lte_power_iteration_construct
  113. 0113refl
  114. 0114exact hprevious_witness_witness_witness_witness_right_left
  115. 0115exact hstep_witness_witness_witness_left
  116. 0116split
  117. 0117specialize lte_power_iteration_construct (b)
  118. 0118specialize lte_power_iteration_construct (x)
  119. 0119specialize lte_power_iteration_construct (p)
  120. 0120specialize lte_power_iteration_construct (x * p)
  121. 0121specialize lte_power_iteration_construct (x2)
  122. 0122specialize lte_power_iteration_construct (x5)
  123. 0123apply lte_power_iteration_construct
  124. 0124refl
  125. 0125exact hprevious_witness_witness_witness_witness_right_right_left
  126. 0126exact hstep_witness_witness_witness_right_left
  127. 0127split
  128. 0128exact hstep_witness_witness_witness_right_right_left
  129. 0129split
  130. 0130exact hstep_witness_witness_witness_right_right_right_left
  131. 0131split
  132. 0132exact hstep_witness_witness_witness_right_right_right_right_left
  133. 0133split
  134. 0134exact hstep_witness_witness_witness_right_right_right_right_right_left
  135. 0135specialize prime_valuation_exponent_eq_transport (p)
  136. 0136specialize prime_valuation_exponent_eq_transport (x6)
  137. 0137specialize prime_valuation_exponent_eq_transport (S (e + k))
  138. 0138specialize prime_valuation_exponent_eq_transport (e + S k)
  139. 0139apply prime_valuation_exponent_eq_transport
  140. 0140symm
  141. 0141apply PA4
  142. 0142exact hstep_witness_witness_witness_right_right_right_right_right_right