MK0006

beta_prime_product_valuation_eq_sum

For a prime and any nonzero finite factor list, the exact product valuation equals the finite sum of its actual factor valuations.

Alpha v34 checked-use · first admitted v27 · 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.

The carry relation contains actual quotient columns and carry bits, not the desired valuation. The theorem includes all finite lists and zero parts. It uses sequential binary-column carries; a separate simultaneous-grid or permutation-invariance theorem is not asserted.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ vb. ∀ vc. ∀ l. ∀ z. ∀ e. ∀ g. Prime(p) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → ¬y = 0) → BetaValuationPrefix(p,b,c,vb,vc,l) → Product(b,c,l,z) → Sum(vb,vc,l,e) → BoundedPowerValuation(p,z,z,g) → g = e

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

Definition DAG

BetaValuationPrefix(p,b,c,vb,vc,l) · 2Lt(a,b) · 2Prime(p) · 1BetaAt(b,c,i,x) · 4Product(b,c,l,z) · 2Sum(b,c,l,z) · 2BoundedPowerValuation(p,n,b,e) · 3

Actual proof prerequisites

beta_sum_zero · checked external prerequisitebeta_product_zero · checked external prerequisiteprime_power_valuation_one_zero · checked external prerequisitebeta_product_succ_decompose · checked external prerequisitebeta_sum_succ_decompose · checked external prerequisitecrt_positive_moduli_prefix_drop_last · checked external prerequisitebeta_valuation_prefix_drop_lastpower_valuation_exists · checked external prerequisitebeta_valuation_prefix_lastcrt_positive_moduli_prefix_product_nonzero · checked external prerequisitecrt_positive_moduli_prefix_last_nonzero · checked external prerequisiteprime_power_valuation_mul · checked external prerequisite
Original expanded first-order statement 
forall p b c vb vc l z e g. ((~(p = 1) /\ forall frm_prime_left_mkm_product_prime frm_prime_right_mkm_product_prime. p = frm_prime_left_mkm_product_prime * frm_prime_right_mkm_product_prime -> frm_prime_left_mkm_product_prime = 1 \/ frm_prime_right_mkm_product_prime = 1)) -> (forall gcrt_positive_index_mkm_product_nonzero gcrt_positive_value_mkm_product_nonzero. (exists ff_lt_gcrt_mkm_product_nonzero_bound. ff_lt_gcrt_mkm_product_nonzero_bound + S gcrt_positive_index_mkm_product_nonzero = l) -> (((exists ff_h_gcrt_mkm_product_nonzero_entry. ff_h_gcrt_mkm_product_nonzero_entry + S (gcrt_positive_value_mkm_product_nonzero) = S ((S (gcrt_positive_index_mkm_product_nonzero)) * c)) /\ exists ff_q_gcrt_mkm_product_nonzero_entry. b = ff_q_gcrt_mkm_product_nonzero_entry * S ((S (gcrt_positive_index_mkm_product_nonzero)) * c) + (gcrt_positive_value_mkm_product_nonzero))) -> ~(gcrt_positive_value_mkm_product_nonzero = 0)) -> (forall mkm_index_product_valuations. (exists mkm_lt_product_valuations_bound. mkm_lt_product_valuations_bound + S (mkm_index_product_valuations) = (l)) -> (exists mkm_value_product_valuations_point mkm_exponent_product_valuations_point. (((exists fs_h_mkm_product_valuations_point_source. fs_h_mkm_product_valuations_point_source + S (mkm_value_product_valuations_point) = S ((S (mkm_index_product_valuations)) * c)) /\ exists fs_q_mkm_product_valuations_point_source. b = fs_q_mkm_product_valuations_point_source * S ((S (mkm_index_product_valuations)) * c) + (mkm_value_product_valuations_point))) /\ ((((exists fs_h_mkm_product_valuations_point_decoded. fs_h_mkm_product_valuations_point_decoded + S (mkm_exponent_product_valuations_point) = S ((S (mkm_index_product_valuations)) * vc)) /\ exists fs_q_mkm_product_valuations_point_decoded. vb = fs_q_mkm_product_valuations_point_decoded * S ((S (mkm_index_product_valuations)) * vc) + (mkm_exponent_product_valuations_point))) /\ (((exists bpv_gap_mkm_product_valuations_point_valuation_exponent_bound. bpv_gap_mkm_product_valuations_point_valuation_exponent_bound + mkm_exponent_product_valuations_point = (mkm_value_product_valuations_point)) /\ (exists bpv_result_mkm_product_valuations_point_valuation_selected. ((exists ff_b_mkm_product_valuations_point_valuation_selected_power ff_c_mkm_product_valuations_point_valuation_selected_power. ((forall ff_i_mkm_product_valuations_point_valuation_selected_power_repeat. (exists ff_lt_mkm_product_valuations_point_valuation_selected_power_repeat_bound. ff_lt_mkm_product_valuations_point_valuation_selected_power_repeat_bound + S ff_i_mkm_product_valuations_point_valuation_selected_power_repeat = mkm_exponent_product_valuations_point) -> (((exists ff_h_mkm_product_valuations_point_valuation_selected_power_repeat_decoded. ff_h_mkm_product_valuations_point_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_repeat)) * ff_c_mkm_product_valuations_point_valuation_selected_power)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_repeat_decoded. ff_b_mkm_product_valuations_point_valuation_selected_power = ff_q_mkm_product_valuations_point_valuation_selected_power_repeat_decoded * S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_repeat)) * ff_c_mkm_product_valuations_point_valuation_selected_power) + (p)))) /\ (exists ff_u_mkm_product_valuations_point_valuation_selected_power_product ff_v_mkm_product_valuations_point_valuation_selected_power_product. ((((exists ff_h_mkm_product_valuations_point_valuation_selected_power_product_start. ff_h_mkm_product_valuations_point_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_product_start. ff_u_mkm_product_valuations_point_valuation_selected_power_product = ff_q_mkm_product_valuations_point_valuation_selected_power_product_start * S ((S (0)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_selected_power_product_terminal. ff_h_mkm_product_valuations_point_valuation_selected_power_product_terminal + S (bpv_result_mkm_product_valuations_point_valuation_selected) = S ((S (mkm_exponent_product_valuations_point)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_product_terminal. ff_u_mkm_product_valuations_point_valuation_selected_power_product = ff_q_mkm_product_valuations_point_valuation_selected_power_product_terminal * S ((S (mkm_exponent_product_valuations_point)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product) + (bpv_result_mkm_product_valuations_point_valuation_selected))) /\ forall ff_i_mkm_product_valuations_point_valuation_selected_power_product. (exists ff_lt_mkm_product_valuations_point_valuation_selected_power_product_bound. ff_lt_mkm_product_valuations_point_valuation_selected_power_product_bound + S ff_i_mkm_product_valuations_point_valuation_selected_power_product = mkm_exponent_product_valuations_point) -> exists ff_p_mkm_product_valuations_point_valuation_selected_power_product ff_r_mkm_product_valuations_point_valuation_selected_power_product ff_s_mkm_product_valuations_point_valuation_selected_power_product. ((((exists ff_h_mkm_product_valuations_point_valuation_selected_power_product_factor. ff_h_mkm_product_valuations_point_valuation_selected_power_product_factor + S (ff_p_mkm_product_valuations_point_valuation_selected_power_product) = S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_c_mkm_product_valuations_point_valuation_selected_power)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_product_factor. ff_b_mkm_product_valuations_point_valuation_selected_power = ff_q_mkm_product_valuations_point_valuation_selected_power_product_factor * S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_c_mkm_product_valuations_point_valuation_selected_power) + (ff_p_mkm_product_valuations_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_selected_power_product_partial. ff_h_mkm_product_valuations_point_valuation_selected_power_product_partial + S (ff_r_mkm_product_valuations_point_valuation_selected_power_product) = S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_product_partial. ff_u_mkm_product_valuations_point_valuation_selected_power_product = ff_q_mkm_product_valuations_point_valuation_selected_power_product_partial * S ((S (ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product) + (ff_r_mkm_product_valuations_point_valuation_selected_power_product))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_selected_power_product_successor. ff_h_mkm_product_valuations_point_valuation_selected_power_product_successor + S (ff_s_mkm_product_valuations_point_valuation_selected_power_product) = S ((S (S ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_selected_power_product_successor. ff_u_mkm_product_valuations_point_valuation_selected_power_product = ff_q_mkm_product_valuations_point_valuation_selected_power_product_successor * S ((S (S ff_i_mkm_product_valuations_point_valuation_selected_power_product)) * ff_v_mkm_product_valuations_point_valuation_selected_power_product) + (ff_s_mkm_product_valuations_point_valuation_selected_power_product))) /\ ff_s_mkm_product_valuations_point_valuation_selected_power_product = ff_r_mkm_product_valuations_point_valuation_selected_power_product * ff_p_mkm_product_valuations_point_valuation_selected_power_product)))))))) /\ (exists bpv_factor_mkm_product_valuations_point_valuation_selected_divides. (mkm_value_product_valuations_point) = bpv_result_mkm_product_valuations_point_valuation_selected * bpv_factor_mkm_product_valuations_point_valuation_selected_divides)))) /\ forall bpv_candidate_mkm_product_valuations_point_valuation. (exists bpv_gap_mkm_product_valuations_point_valuation_candidate_bound. bpv_gap_mkm_product_valuations_point_valuation_candidate_bound + bpv_candidate_mkm_product_valuations_point_valuation = (mkm_value_product_valuations_point)) -> (exists bpv_result_mkm_product_valuations_point_valuation_candidate. ((exists ff_b_mkm_product_valuations_point_valuation_candidate_power ff_c_mkm_product_valuations_point_valuation_candidate_power. ((forall ff_i_mkm_product_valuations_point_valuation_candidate_power_repeat. (exists ff_lt_mkm_product_valuations_point_valuation_candidate_power_repeat_bound. ff_lt_mkm_product_valuations_point_valuation_candidate_power_repeat_bound + S ff_i_mkm_product_valuations_point_valuation_candidate_power_repeat = bpv_candidate_mkm_product_valuations_point_valuation) -> (((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_repeat_decoded. ff_h_mkm_product_valuations_point_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_repeat)) * ff_c_mkm_product_valuations_point_valuation_candidate_power)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_repeat_decoded. ff_b_mkm_product_valuations_point_valuation_candidate_power = ff_q_mkm_product_valuations_point_valuation_candidate_power_repeat_decoded * S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_repeat)) * ff_c_mkm_product_valuations_point_valuation_candidate_power) + (p)))) /\ (exists ff_u_mkm_product_valuations_point_valuation_candidate_power_product ff_v_mkm_product_valuations_point_valuation_candidate_power_product. ((((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_product_start. ff_h_mkm_product_valuations_point_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_product_start. ff_u_mkm_product_valuations_point_valuation_candidate_power_product = ff_q_mkm_product_valuations_point_valuation_candidate_power_product_start * S ((S (0)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_product_terminal. ff_h_mkm_product_valuations_point_valuation_candidate_power_product_terminal + S (bpv_result_mkm_product_valuations_point_valuation_candidate) = S ((S (bpv_candidate_mkm_product_valuations_point_valuation)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_product_terminal. ff_u_mkm_product_valuations_point_valuation_candidate_power_product = ff_q_mkm_product_valuations_point_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_product_valuations_point_valuation)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product) + (bpv_result_mkm_product_valuations_point_valuation_candidate))) /\ forall ff_i_mkm_product_valuations_point_valuation_candidate_power_product. (exists ff_lt_mkm_product_valuations_point_valuation_candidate_power_product_bound. ff_lt_mkm_product_valuations_point_valuation_candidate_power_product_bound + S ff_i_mkm_product_valuations_point_valuation_candidate_power_product = bpv_candidate_mkm_product_valuations_point_valuation) -> exists ff_p_mkm_product_valuations_point_valuation_candidate_power_product ff_r_mkm_product_valuations_point_valuation_candidate_power_product ff_s_mkm_product_valuations_point_valuation_candidate_power_product. ((((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_product_factor. ff_h_mkm_product_valuations_point_valuation_candidate_power_product_factor + S (ff_p_mkm_product_valuations_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_c_mkm_product_valuations_point_valuation_candidate_power)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_product_factor. ff_b_mkm_product_valuations_point_valuation_candidate_power = ff_q_mkm_product_valuations_point_valuation_candidate_power_product_factor * S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_c_mkm_product_valuations_point_valuation_candidate_power) + (ff_p_mkm_product_valuations_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_product_partial. ff_h_mkm_product_valuations_point_valuation_candidate_power_product_partial + S (ff_r_mkm_product_valuations_point_valuation_candidate_power_product) = S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_product_partial. ff_u_mkm_product_valuations_point_valuation_candidate_power_product = ff_q_mkm_product_valuations_point_valuation_candidate_power_product_partial * S ((S (ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product) + (ff_r_mkm_product_valuations_point_valuation_candidate_power_product))) /\ ((((exists ff_h_mkm_product_valuations_point_valuation_candidate_power_product_successor. ff_h_mkm_product_valuations_point_valuation_candidate_power_product_successor + S (ff_s_mkm_product_valuations_point_valuation_candidate_power_product) = S ((S (S ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product)) /\ exists ff_q_mkm_product_valuations_point_valuation_candidate_power_product_successor. ff_u_mkm_product_valuations_point_valuation_candidate_power_product = ff_q_mkm_product_valuations_point_valuation_candidate_power_product_successor * S ((S (S ff_i_mkm_product_valuations_point_valuation_candidate_power_product)) * ff_v_mkm_product_valuations_point_valuation_candidate_power_product) + (ff_s_mkm_product_valuations_point_valuation_candidate_power_product))) /\ ff_s_mkm_product_valuations_point_valuation_candidate_power_product = ff_r_mkm_product_valuations_point_valuation_candidate_power_product * ff_p_mkm_product_valuations_point_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_product_valuations_point_valuation_candidate_divides. (mkm_value_product_valuations_point) = bpv_result_mkm_product_valuations_point_valuation_candidate * bpv_factor_mkm_product_valuations_point_valuation_candidate_divides))) -> (exists bpv_gap_mkm_product_valuations_point_valuation_maximal. bpv_gap_mkm_product_valuations_point_valuation_maximal + bpv_candidate_mkm_product_valuations_point_valuation = mkm_exponent_product_valuations_point))))) -> (exists ff_u_mkm_product_value ff_v_mkm_product_value. ((((exists ff_h_mkm_product_value_start. ff_h_mkm_product_value_start + S (1) = S ((S (0)) * ff_v_mkm_product_value)) /\ exists ff_q_mkm_product_value_start. ff_u_mkm_product_value = ff_q_mkm_product_value_start * S ((S (0)) * ff_v_mkm_product_value) + (1))) /\ ((((exists ff_h_mkm_product_value_terminal. ff_h_mkm_product_value_terminal + S (z) = S ((S (l)) * ff_v_mkm_product_value)) /\ exists ff_q_mkm_product_value_terminal. ff_u_mkm_product_value = ff_q_mkm_product_value_terminal * S ((S (l)) * ff_v_mkm_product_value) + (z))) /\ forall ff_i_mkm_product_value. (exists ff_lt_mkm_product_value_bound. ff_lt_mkm_product_value_bound + S ff_i_mkm_product_value = l) -> exists ff_p_mkm_product_value ff_r_mkm_product_value ff_s_mkm_product_value. ((((exists ff_h_mkm_product_value_factor. ff_h_mkm_product_value_factor + S (ff_p_mkm_product_value) = S ((S (ff_i_mkm_product_value)) * c)) /\ exists ff_q_mkm_product_value_factor. b = ff_q_mkm_product_value_factor * S ((S (ff_i_mkm_product_value)) * c) + (ff_p_mkm_product_value))) /\ ((((exists ff_h_mkm_product_value_partial. ff_h_mkm_product_value_partial + S (ff_r_mkm_product_value) = S ((S (ff_i_mkm_product_value)) * ff_v_mkm_product_value)) /\ exists ff_q_mkm_product_value_partial. ff_u_mkm_product_value = ff_q_mkm_product_value_partial * S ((S (ff_i_mkm_product_value)) * ff_v_mkm_product_value) + (ff_r_mkm_product_value))) /\ ((((exists ff_h_mkm_product_value_successor. ff_h_mkm_product_value_successor + S (ff_s_mkm_product_value) = S ((S (S ff_i_mkm_product_value)) * ff_v_mkm_product_value)) /\ exists ff_q_mkm_product_value_successor. ff_u_mkm_product_value = ff_q_mkm_product_value_successor * S ((S (S ff_i_mkm_product_value)) * ff_v_mkm_product_value) + (ff_s_mkm_product_value))) /\ ff_s_mkm_product_value = ff_r_mkm_product_value * ff_p_mkm_product_value)))))) -> (exists fs_u_mkm_product_sum fs_v_mkm_product_sum. ((((exists fs_h_mkm_product_sum_body_start. fs_h_mkm_product_sum_body_start + S (0) = S ((S (0)) * fs_v_mkm_product_sum)) /\ exists fs_q_mkm_product_sum_body_start. fs_u_mkm_product_sum = fs_q_mkm_product_sum_body_start * S ((S (0)) * fs_v_mkm_product_sum) + (0))) /\ ((((exists fs_h_mkm_product_sum_body_terminal. fs_h_mkm_product_sum_body_terminal + S (e) = S ((S (l)) * fs_v_mkm_product_sum)) /\ exists fs_q_mkm_product_sum_body_terminal. fs_u_mkm_product_sum = fs_q_mkm_product_sum_body_terminal * S ((S (l)) * fs_v_mkm_product_sum) + (e))) /\ forall fs_i_mkm_product_sum_body_steps. (exists fs_lt_mkm_product_sum_body_steps_bound. fs_lt_mkm_product_sum_body_steps_bound + S fs_i_mkm_product_sum_body_steps = l) -> exists fs_a_mkm_product_sum_body_steps fs_r_mkm_product_sum_body_steps fs_s_mkm_product_sum_body_steps. ((((exists fs_h_mkm_product_sum_body_steps_summand. fs_h_mkm_product_sum_body_steps_summand + S (fs_a_mkm_product_sum_body_steps) = S ((S (fs_i_mkm_product_sum_body_steps)) * vc)) /\ exists fs_q_mkm_product_sum_body_steps_summand. vb = fs_q_mkm_product_sum_body_steps_summand * S ((S (fs_i_mkm_product_sum_body_steps)) * vc) + (fs_a_mkm_product_sum_body_steps))) /\ ((((exists fs_h_mkm_product_sum_body_steps_partial. fs_h_mkm_product_sum_body_steps_partial + S (fs_r_mkm_product_sum_body_steps) = S ((S (fs_i_mkm_product_sum_body_steps)) * fs_v_mkm_product_sum)) /\ exists fs_q_mkm_product_sum_body_steps_partial. fs_u_mkm_product_sum = fs_q_mkm_product_sum_body_steps_partial * S ((S (fs_i_mkm_product_sum_body_steps)) * fs_v_mkm_product_sum) + (fs_r_mkm_product_sum_body_steps))) /\ ((((exists fs_h_mkm_product_sum_body_steps_successor. fs_h_mkm_product_sum_body_steps_successor + S (fs_s_mkm_product_sum_body_steps) = S ((S (S fs_i_mkm_product_sum_body_steps)) * fs_v_mkm_product_sum)) /\ exists fs_q_mkm_product_sum_body_steps_successor. fs_u_mkm_product_sum = fs_q_mkm_product_sum_body_steps_successor * S ((S (S fs_i_mkm_product_sum_body_steps)) * fs_v_mkm_product_sum) + (fs_s_mkm_product_sum_body_steps))) /\ fs_s_mkm_product_sum_body_steps = fs_r_mkm_product_sum_body_steps + fs_a_mkm_product_sum_body_steps)))))) -> (((exists bpv_gap_mkm_product_val_exponent_bound. bpv_gap_mkm_product_val_exponent_bound + g = (z)) /\ (exists bpv_result_mkm_product_val_selected. ((exists ff_b_mkm_product_val_selected_power ff_c_mkm_product_val_selected_power. ((forall ff_i_mkm_product_val_selected_power_repeat. (exists ff_lt_mkm_product_val_selected_power_repeat_bound. ff_lt_mkm_product_val_selected_power_repeat_bound + S ff_i_mkm_product_val_selected_power_repeat = g) -> (((exists ff_h_mkm_product_val_selected_power_repeat_decoded. ff_h_mkm_product_val_selected_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_val_selected_power_repeat)) * ff_c_mkm_product_val_selected_power)) /\ exists ff_q_mkm_product_val_selected_power_repeat_decoded. ff_b_mkm_product_val_selected_power = ff_q_mkm_product_val_selected_power_repeat_decoded * S ((S (ff_i_mkm_product_val_selected_power_repeat)) * ff_c_mkm_product_val_selected_power) + (p)))) /\ (exists ff_u_mkm_product_val_selected_power_product ff_v_mkm_product_val_selected_power_product. ((((exists ff_h_mkm_product_val_selected_power_product_start. ff_h_mkm_product_val_selected_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_val_selected_power_product)) /\ exists ff_q_mkm_product_val_selected_power_product_start. ff_u_mkm_product_val_selected_power_product = ff_q_mkm_product_val_selected_power_product_start * S ((S (0)) * ff_v_mkm_product_val_selected_power_product) + (1))) /\ ((((exists ff_h_mkm_product_val_selected_power_product_terminal. ff_h_mkm_product_val_selected_power_product_terminal + S (bpv_result_mkm_product_val_selected) = S ((S (g)) * ff_v_mkm_product_val_selected_power_product)) /\ exists ff_q_mkm_product_val_selected_power_product_terminal. ff_u_mkm_product_val_selected_power_product = ff_q_mkm_product_val_selected_power_product_terminal * S ((S (g)) * ff_v_mkm_product_val_selected_power_product) + (bpv_result_mkm_product_val_selected))) /\ forall ff_i_mkm_product_val_selected_power_product. (exists ff_lt_mkm_product_val_selected_power_product_bound. ff_lt_mkm_product_val_selected_power_product_bound + S ff_i_mkm_product_val_selected_power_product = g) -> exists ff_p_mkm_product_val_selected_power_product ff_r_mkm_product_val_selected_power_product ff_s_mkm_product_val_selected_power_product. ((((exists ff_h_mkm_product_val_selected_power_product_factor. ff_h_mkm_product_val_selected_power_product_factor + S (ff_p_mkm_product_val_selected_power_product) = S ((S (ff_i_mkm_product_val_selected_power_product)) * ff_c_mkm_product_val_selected_power)) /\ exists ff_q_mkm_product_val_selected_power_product_factor. ff_b_mkm_product_val_selected_power = ff_q_mkm_product_val_selected_power_product_factor * S ((S (ff_i_mkm_product_val_selected_power_product)) * ff_c_mkm_product_val_selected_power) + (ff_p_mkm_product_val_selected_power_product))) /\ ((((exists ff_h_mkm_product_val_selected_power_product_partial. ff_h_mkm_product_val_selected_power_product_partial + S (ff_r_mkm_product_val_selected_power_product) = S ((S (ff_i_mkm_product_val_selected_power_product)) * ff_v_mkm_product_val_selected_power_product)) /\ exists ff_q_mkm_product_val_selected_power_product_partial. ff_u_mkm_product_val_selected_power_product = ff_q_mkm_product_val_selected_power_product_partial * S ((S (ff_i_mkm_product_val_selected_power_product)) * ff_v_mkm_product_val_selected_power_product) + (ff_r_mkm_product_val_selected_power_product))) /\ ((((exists ff_h_mkm_product_val_selected_power_product_successor. ff_h_mkm_product_val_selected_power_product_successor + S (ff_s_mkm_product_val_selected_power_product) = S ((S (S ff_i_mkm_product_val_selected_power_product)) * ff_v_mkm_product_val_selected_power_product)) /\ exists ff_q_mkm_product_val_selected_power_product_successor. ff_u_mkm_product_val_selected_power_product = ff_q_mkm_product_val_selected_power_product_successor * S ((S (S ff_i_mkm_product_val_selected_power_product)) * ff_v_mkm_product_val_selected_power_product) + (ff_s_mkm_product_val_selected_power_product))) /\ ff_s_mkm_product_val_selected_power_product = ff_r_mkm_product_val_selected_power_product * ff_p_mkm_product_val_selected_power_product)))))))) /\ (exists bpv_factor_mkm_product_val_selected_divides. (z) = bpv_result_mkm_product_val_selected * bpv_factor_mkm_product_val_selected_divides)))) /\ forall bpv_candidate_mkm_product_val. (exists bpv_gap_mkm_product_val_candidate_bound. bpv_gap_mkm_product_val_candidate_bound + bpv_candidate_mkm_product_val = (z)) -> (exists bpv_result_mkm_product_val_candidate. ((exists ff_b_mkm_product_val_candidate_power ff_c_mkm_product_val_candidate_power. ((forall ff_i_mkm_product_val_candidate_power_repeat. (exists ff_lt_mkm_product_val_candidate_power_repeat_bound. ff_lt_mkm_product_val_candidate_power_repeat_bound + S ff_i_mkm_product_val_candidate_power_repeat = bpv_candidate_mkm_product_val) -> (((exists ff_h_mkm_product_val_candidate_power_repeat_decoded. ff_h_mkm_product_val_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_mkm_product_val_candidate_power_repeat)) * ff_c_mkm_product_val_candidate_power)) /\ exists ff_q_mkm_product_val_candidate_power_repeat_decoded. ff_b_mkm_product_val_candidate_power = ff_q_mkm_product_val_candidate_power_repeat_decoded * S ((S (ff_i_mkm_product_val_candidate_power_repeat)) * ff_c_mkm_product_val_candidate_power) + (p)))) /\ (exists ff_u_mkm_product_val_candidate_power_product ff_v_mkm_product_val_candidate_power_product. ((((exists ff_h_mkm_product_val_candidate_power_product_start. ff_h_mkm_product_val_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_mkm_product_val_candidate_power_product)) /\ exists ff_q_mkm_product_val_candidate_power_product_start. ff_u_mkm_product_val_candidate_power_product = ff_q_mkm_product_val_candidate_power_product_start * S ((S (0)) * ff_v_mkm_product_val_candidate_power_product) + (1))) /\ ((((exists ff_h_mkm_product_val_candidate_power_product_terminal. ff_h_mkm_product_val_candidate_power_product_terminal + S (bpv_result_mkm_product_val_candidate) = S ((S (bpv_candidate_mkm_product_val)) * ff_v_mkm_product_val_candidate_power_product)) /\ exists ff_q_mkm_product_val_candidate_power_product_terminal. ff_u_mkm_product_val_candidate_power_product = ff_q_mkm_product_val_candidate_power_product_terminal * S ((S (bpv_candidate_mkm_product_val)) * ff_v_mkm_product_val_candidate_power_product) + (bpv_result_mkm_product_val_candidate))) /\ forall ff_i_mkm_product_val_candidate_power_product. (exists ff_lt_mkm_product_val_candidate_power_product_bound. ff_lt_mkm_product_val_candidate_power_product_bound + S ff_i_mkm_product_val_candidate_power_product = bpv_candidate_mkm_product_val) -> exists ff_p_mkm_product_val_candidate_power_product ff_r_mkm_product_val_candidate_power_product ff_s_mkm_product_val_candidate_power_product. ((((exists ff_h_mkm_product_val_candidate_power_product_factor. ff_h_mkm_product_val_candidate_power_product_factor + S (ff_p_mkm_product_val_candidate_power_product) = S ((S (ff_i_mkm_product_val_candidate_power_product)) * ff_c_mkm_product_val_candidate_power)) /\ exists ff_q_mkm_product_val_candidate_power_product_factor. ff_b_mkm_product_val_candidate_power = ff_q_mkm_product_val_candidate_power_product_factor * S ((S (ff_i_mkm_product_val_candidate_power_product)) * ff_c_mkm_product_val_candidate_power) + (ff_p_mkm_product_val_candidate_power_product))) /\ ((((exists ff_h_mkm_product_val_candidate_power_product_partial. ff_h_mkm_product_val_candidate_power_product_partial + S (ff_r_mkm_product_val_candidate_power_product) = S ((S (ff_i_mkm_product_val_candidate_power_product)) * ff_v_mkm_product_val_candidate_power_product)) /\ exists ff_q_mkm_product_val_candidate_power_product_partial. ff_u_mkm_product_val_candidate_power_product = ff_q_mkm_product_val_candidate_power_product_partial * S ((S (ff_i_mkm_product_val_candidate_power_product)) * ff_v_mkm_product_val_candidate_power_product) + (ff_r_mkm_product_val_candidate_power_product))) /\ ((((exists ff_h_mkm_product_val_candidate_power_product_successor. ff_h_mkm_product_val_candidate_power_product_successor + S (ff_s_mkm_product_val_candidate_power_product) = S ((S (S ff_i_mkm_product_val_candidate_power_product)) * ff_v_mkm_product_val_candidate_power_product)) /\ exists ff_q_mkm_product_val_candidate_power_product_successor. ff_u_mkm_product_val_candidate_power_product = ff_q_mkm_product_val_candidate_power_product_successor * S ((S (S ff_i_mkm_product_val_candidate_power_product)) * ff_v_mkm_product_val_candidate_power_product) + (ff_s_mkm_product_val_candidate_power_product))) /\ ff_s_mkm_product_val_candidate_power_product = ff_r_mkm_product_val_candidate_power_product * ff_p_mkm_product_val_candidate_power_product)))))))) /\ (exists bpv_factor_mkm_product_val_candidate_divides. (z) = bpv_result_mkm_product_val_candidate * bpv_factor_mkm_product_val_candidate_divides))) -> (exists bpv_gap_mkm_product_val_maximal. bpv_gap_mkm_product_val_maximal + bpv_candidate_mkm_product_val = g)) -> g = e

Complete tactic proof in conservative notation

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

150 script commands · 27 reading checkpoints · 8 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)
beta valuation prefix drop lastbeta valuation prefix last
01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro vb
  5. L5
    intro vc
02Induction on lL6–15

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

  1. L6
    induction l
  2. L7
    intro z
  3. L8
    intro e
  4. L9
    intro g
  5. L10
    intro hp
  6. L11
    intro hn
  7. L12
    intro hv
  8. L13
    intro hprod
  9. L14
    intro hsum
  10. L15
    intro hg
03Establish hezeroL16–25

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

  1. L16
    have hezero : e = 0
  2. L17
    specialize beta_sum_zero vb
  3. L18
    specialize beta_sum_zero vc
  4. L19
    specialize beta_sum_zero e
  5. L20
    apply beta_sum_zero
  6. L21
    exact hsum
  7. L22
    rewrite hezero
  8. L23
    specialize prime_power_valuation_one_zero p
  9. L24
    specialize prime_power_valuation_one_zero z
  10. L25
    specialize prime_power_valuation_one_zero g
04Use earlier factsL26–33

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

  1. L26
    apply prime_power_valuation_one_zero
  2. L27
    specialize beta_product_zero b
  3. L28
    specialize beta_product_zero c
  4. L29
    specialize beta_product_zero z
  5. L30
    apply beta_product_zero
  6. L31
    exact hprod
  7. L32
    exact hp
  8. L33
    exact hg
05Fix variables and assumptionsL34–42

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

  1. L34
    intro z
  2. L35
    intro e
  3. L36
    intro g
  4. L37
    intro hp
  5. L38
    intro hn
  6. L39
    intro hv
  7. L40
    intro hprod
  8. L41
    intro hsum
  9. L42
    intro hg
06Establish hprodpartL43–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L43
    have hprodpart : ∃ a. ∃ w. BetaAt(b,c,l,a) ∧ (Product(b,c,l,w) ∧ z = w · a)Definitions: BetaAt(b,c,l,a)Product(b,c,l,w)Original native command in the exact edition
  2. L44
    specialize beta_product_succ_decompose b
  3. L45
    specialize beta_product_succ_decompose c
  4. L46
    specialize beta_product_succ_decompose l
  5. L47
    specialize beta_product_succ_decompose z
  6. L48
    apply beta_product_succ_decompose
  7. L49
    exact hprod
07Separate the logical casesL50–53

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

  1. L50
    cases hprodpart
  2. L51
    cases hprodpart_witness
  3. L52
    cases hprodpart_witness_witness
  4. L53
    cases hprodpart_witness_witness_right
08Establish hsumpartL54–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum succ decompose.

  1. L54
    have hsumpart : ∃ v. ∃ E. BetaAt(vb,vc,l,v) ∧ (Sum(vb,vc,l,E) ∧ e = E + v)Definitions: BetaAt(vb,vc,l,v)Sum(vb,vc,l,E)Original native command in the exact edition
  2. L55
    specialize beta_sum_succ_decompose vb
  3. L56
    specialize beta_sum_succ_decompose vc
  4. L57
    specialize beta_sum_succ_decompose l
  5. L58
    specialize beta_sum_succ_decompose e
  6. L59
    apply beta_sum_succ_decompose
  7. L60
    exact hsum
09Separate the logical casesL61–64

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

  1. L61
    cases hsumpart
  2. L62
    cases hsumpart_witness
  3. L63
    cases hsumpart_witness_witness
  4. L64
    cases hsumpart_witness_witness_right
10Establish hnprevL65–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply crt positive moduli prefix drop last.

  1. L65
    have hnprev : ∀ gcrt_positive_index_mkm_product_previous_nonzero. ∀ gcrt_positive_value_mkm_product_previous_nonzero. Lt(gcrt_positive_index_mkm_product_previous_nonzero,l) → BetaAt(b,c,gcrt_positive_index_mkm_product_previous_nonzero,gcrt_positive_value_mkm_product_previous_nonzero) → ¬gcrt_positive_value_mkm_product_previous_nonzero = 0Definitions: Lt(gcrt_positive_index_mkm_product_previous_nonzero,l)BetaAt(b,c,gcrt_positive_index_mkm_product_previous_nonzero,gcrt_positive_value_mkm_product_previous_nonzero)Original native command in the exact edition
  2. L66
    specialize crt_positive_moduli_prefix_drop_last b
  3. L67
    specialize crt_positive_moduli_prefix_drop_last c
  4. L68
    specialize crt_positive_moduli_prefix_drop_last l
  5. L69
    apply crt_positive_moduli_prefix_drop_last
  6. L70
    exact hn
11Establish hvprevL71–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta valuation prefix drop last.

  1. L71
    have hvprev : BetaValuationPrefix(p,b,c,vb,vc,l)Definitions: BetaValuationPrefix(p,b,c,vb,vc,l)Original native command in the exact edition
  2. L72
    specialize beta_valuation_prefix_drop_last p
  3. L73
    specialize beta_valuation_prefix_drop_last b
  4. L74
    specialize beta_valuation_prefix_drop_last c
  5. L75
    specialize beta_valuation_prefix_drop_last vb
  6. L76
    specialize beta_valuation_prefix_drop_last vc
  7. L77
    specialize beta_valuation_prefix_drop_last l
  8. L78
    apply beta_valuation_prefix_drop_last
  9. L79
    exact hv
12Establish hpreviousL80–83

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

  1. L80
    have hprevious : ∃ v. BoundedPowerValuation(p,x1,x1,v)Definitions: BoundedPowerValuation(p,x1,x1,v)Original native command in the exact edition
  2. L81
    specialize power_valuation_exists p
  3. L82
    specialize power_valuation_exists x1
  4. L83
    apply power_valuation_exists
13Separate the logical casesL84–84

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

  1. L84
    cases hprevious
14Establish hprevious_valueL85–94

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

  1. L85
    have hprevious_value : x4 = x3
  2. L86
    specialize IH x1
  3. L87
    specialize IH x3
  4. L88
    specialize IH x4
  5. L89
    apply IH
  6. L90
    exact hp
  7. L91
    exact hnprev
  8. L92
    exact hvprev
  9. L93
    exact hprodpart_witness_witness_right_left
  10. L94
    exact hsumpart_witness_witness_right_left
15Use earlier factsL95–95

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

  1. L95
    exact hprevious_witness
16Calculate and transport equalitiesL96–101

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

  1. L96
    rewrite hprevious_value at hprevious_witness
  2. L97
    rewrite hprevious_value at hprevious_witness
  3. L98
    rewrite hprevious_value at hprevious_witness
  4. L99
    rewrite hprevious_value at hprevious_witness
  5. L100
    rewrite hprevious_value at hprevious_witness
  6. L101
    rewrite hprevious_value at hprevious_witness
17Establish hlastL102–111

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta valuation prefix last.

  1. L102
    have hlast : BoundedPowerValuation(p,x,x,x2)Definitions: BoundedPowerValuation(p,x,x,x2)Original native command in the exact edition
  2. L103
    specialize beta_valuation_prefix_last p
  3. L104
    specialize beta_valuation_prefix_last b
  4. L105
    specialize beta_valuation_prefix_last c
  5. L106
    specialize beta_valuation_prefix_last vb
  6. L107
    specialize beta_valuation_prefix_last vc
  7. L108
    specialize beta_valuation_prefix_last l
  8. L109
    specialize beta_valuation_prefix_last x
  9. L110
    specialize beta_valuation_prefix_last x2
  10. L111
    apply beta_valuation_prefix_last
18Use earlier factsL112–114

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

  1. L112
    exact hv
  2. L113
    exact hprodpart_witness_witness_left
  3. L114
    exact hsumpart_witness_witness_left
19Calculate and transport equalitiesL115–119

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

  1. L115
    rewrite hprodpart_witness_witness_right_right at hg
  2. L116
    rewrite hprodpart_witness_witness_right_right at hg
  3. L117
    rewrite hprodpart_witness_witness_right_right at hg
  4. L118
    rewrite hprodpart_witness_witness_right_right at hg
  5. L119
    trans x3 + x2
20Use earlier factsL120–127

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

  1. L120
    specialize prime_power_valuation_mul p
  2. L121
    specialize prime_power_valuation_mul x1
  3. L122
    specialize prime_power_valuation_mul x
  4. L123
    specialize prime_power_valuation_mul x3
  5. L124
    specialize prime_power_valuation_mul x2
  6. L125
    specialize prime_power_valuation_mul g
  7. L126
    apply prime_power_valuation_mul
  8. L127
    exact hp
21Fix variables and assumptionsL128–128

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

  1. L128
    intro hzero
22Use earlier factsL129–136

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

  1. L129
    specialize crt_positive_moduli_prefix_product_nonzero b
  2. L130
    specialize crt_positive_moduli_prefix_product_nonzero c
  3. L131
    specialize crt_positive_moduli_prefix_product_nonzero l
  4. L132
    specialize crt_positive_moduli_prefix_product_nonzero x1
  5. L133
    apply crt_positive_moduli_prefix_product_nonzero
  6. L134
    exact hnprev
  7. L135
    exact hprodpart_witness_witness_right_left
  8. L136
    exact hzero
23Fix variables and assumptionsL137–137

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

  1. L137
    intro hzero
24Use earlier factsL138–147

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

  1. L138
    specialize crt_positive_moduli_prefix_last_nonzero b
  2. L139
    specialize crt_positive_moduli_prefix_last_nonzero c
  3. L140
    specialize crt_positive_moduli_prefix_last_nonzero l
  4. L141
    specialize crt_positive_moduli_prefix_last_nonzero x
  5. L142
    apply crt_positive_moduli_prefix_last_nonzero
  6. L143
    exact hn
  7. L144
    exact hprodpart_witness_witness_left
  8. L145
    exact hzero
  9. L146
    exact hprevious_witness
  10. L147
    exact hlast
25Use earlier factsL148–148

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

  1. L148
    exact hg
26Calculate and transport equalitiesL149–149

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

  1. L149
    symm
27Use earlier factsL150–150

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

  1. L150
    exact hsumpart_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 150 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro vb
  5. 0005intro vc
  6. 0006induction l
  7. 0007intro z
  8. 0008intro e
  9. 0009intro g
  10. 0010intro hp
  11. 0011intro hn
  12. 0012intro hv
  13. 0013intro hprod
  14. 0014intro hsum
  15. 0015intro hg
  16. 0016have hezero : e = 0
  17. 0017specialize beta_sum_zero vb
  18. 0018specialize beta_sum_zero vc
  19. 0019specialize beta_sum_zero e
  20. 0020apply beta_sum_zero
  21. 0021exact hsum
  22. 0022rewrite hezero
  23. 0023specialize prime_power_valuation_one_zero p
  24. 0024specialize prime_power_valuation_one_zero z
  25. 0025specialize prime_power_valuation_one_zero g
  26. 0026apply prime_power_valuation_one_zero
  27. 0027specialize beta_product_zero b
  28. 0028specialize beta_product_zero c
  29. 0029specialize beta_product_zero z
  30. 0030apply beta_product_zero
  31. 0031exact hprod
  32. 0032exact hp
  33. 0033exact hg
  34. 0034intro z
  35. 0035intro e
  36. 0036intro g
  37. 0037intro hp
  38. 0038intro hn
  39. 0039intro hv
  40. 0040intro hprod
  41. 0041intro hsum
  42. 0042intro hg
  43. 0043have hprodpart : ∃ a. ∃ w. BetaAt(b,c,l,a) ∧ (Product(b,c,l,w) ∧ z = w · a)
  44. 0044specialize beta_product_succ_decompose b
  45. 0045specialize beta_product_succ_decompose c
  46. 0046specialize beta_product_succ_decompose l
  47. 0047specialize beta_product_succ_decompose z
  48. 0048apply beta_product_succ_decompose
  49. 0049exact hprod
  50. 0050cases hprodpart
  51. 0051cases hprodpart_witness
  52. 0052cases hprodpart_witness_witness
  53. 0053cases hprodpart_witness_witness_right
  54. 0054have hsumpart : ∃ v. ∃ E. BetaAt(vb,vc,l,v) ∧ (Sum(vb,vc,l,E) ∧ e = E + v)
  55. 0055specialize beta_sum_succ_decompose vb
  56. 0056specialize beta_sum_succ_decompose vc
  57. 0057specialize beta_sum_succ_decompose l
  58. 0058specialize beta_sum_succ_decompose e
  59. 0059apply beta_sum_succ_decompose
  60. 0060exact hsum
  61. 0061cases hsumpart
  62. 0062cases hsumpart_witness
  63. 0063cases hsumpart_witness_witness
  64. 0064cases hsumpart_witness_witness_right
  65. 0065have hnprev : ∀ gcrt_positive_index_mkm_product_previous_nonzero. ∀ gcrt_positive_value_mkm_product_previous_nonzero. Lt(gcrt_positive_index_mkm_product_previous_nonzero,l) → BetaAt(b,c,gcrt_positive_index_mkm_product_previous_nonzero,gcrt_positive_value_mkm_product_previous_nonzero) → ¬gcrt_positive_value_mkm_product_previous_nonzero = 0
  66. 0066specialize crt_positive_moduli_prefix_drop_last b
  67. 0067specialize crt_positive_moduli_prefix_drop_last c
  68. 0068specialize crt_positive_moduli_prefix_drop_last l
  69. 0069apply crt_positive_moduli_prefix_drop_last
  70. 0070exact hn
  71. 0071have hvprev : BetaValuationPrefix(p,b,c,vb,vc,l)
  72. 0072specialize beta_valuation_prefix_drop_last p
  73. 0073specialize beta_valuation_prefix_drop_last b
  74. 0074specialize beta_valuation_prefix_drop_last c
  75. 0075specialize beta_valuation_prefix_drop_last vb
  76. 0076specialize beta_valuation_prefix_drop_last vc
  77. 0077specialize beta_valuation_prefix_drop_last l
  78. 0078apply beta_valuation_prefix_drop_last
  79. 0079exact hv
  80. 0080have hprevious : ∃ v. BoundedPowerValuation(p,x1,x1,v)
  81. 0081specialize power_valuation_exists p
  82. 0082specialize power_valuation_exists x1
  83. 0083apply power_valuation_exists
  84. 0084cases hprevious
  85. 0085have hprevious_value : x4 = x3
  86. 0086specialize IH x1
  87. 0087specialize IH x3
  88. 0088specialize IH x4
  89. 0089apply IH
  90. 0090exact hp
  91. 0091exact hnprev
  92. 0092exact hvprev
  93. 0093exact hprodpart_witness_witness_right_left
  94. 0094exact hsumpart_witness_witness_right_left
  95. 0095exact hprevious_witness
  96. 0096rewrite hprevious_value at hprevious_witness
  97. 0097rewrite hprevious_value at hprevious_witness
  98. 0098rewrite hprevious_value at hprevious_witness
  99. 0099rewrite hprevious_value at hprevious_witness
  100. 0100rewrite hprevious_value at hprevious_witness
  101. 0101rewrite hprevious_value at hprevious_witness
  102. 0102have hlast : BoundedPowerValuation(p,x,x,x2)
  103. 0103specialize beta_valuation_prefix_last p
  104. 0104specialize beta_valuation_prefix_last b
  105. 0105specialize beta_valuation_prefix_last c
  106. 0106specialize beta_valuation_prefix_last vb
  107. 0107specialize beta_valuation_prefix_last vc
  108. 0108specialize beta_valuation_prefix_last l
  109. 0109specialize beta_valuation_prefix_last x
  110. 0110specialize beta_valuation_prefix_last x2
  111. 0111apply beta_valuation_prefix_last
  112. 0112exact hv
  113. 0113exact hprodpart_witness_witness_left
  114. 0114exact hsumpart_witness_witness_left
  115. 0115rewrite hprodpart_witness_witness_right_right at hg
  116. 0116rewrite hprodpart_witness_witness_right_right at hg
  117. 0117rewrite hprodpart_witness_witness_right_right at hg
  118. 0118rewrite hprodpart_witness_witness_right_right at hg
  119. 0119trans x3 + x2
  120. 0120specialize prime_power_valuation_mul p
  121. 0121specialize prime_power_valuation_mul x1
  122. 0122specialize prime_power_valuation_mul x
  123. 0123specialize prime_power_valuation_mul x3
  124. 0124specialize prime_power_valuation_mul x2
  125. 0125specialize prime_power_valuation_mul g
  126. 0126apply prime_power_valuation_mul
  127. 0127exact hp
  128. 0128intro hzero
  129. 0129specialize crt_positive_moduli_prefix_product_nonzero b
  130. 0130specialize crt_positive_moduli_prefix_product_nonzero c
  131. 0131specialize crt_positive_moduli_prefix_product_nonzero l
  132. 0132specialize crt_positive_moduli_prefix_product_nonzero x1
  133. 0133apply crt_positive_moduli_prefix_product_nonzero
  134. 0134exact hnprev
  135. 0135exact hprodpart_witness_witness_right_left
  136. 0136exact hzero
  137. 0137intro hzero
  138. 0138specialize crt_positive_moduli_prefix_last_nonzero b
  139. 0139specialize crt_positive_moduli_prefix_last_nonzero c
  140. 0140specialize crt_positive_moduli_prefix_last_nonzero l
  141. 0141specialize crt_positive_moduli_prefix_last_nonzero x
  142. 0142apply crt_positive_moduli_prefix_last_nonzero
  143. 0143exact hn
  144. 0144exact hprodpart_witness_witness_left
  145. 0145exact hzero
  146. 0146exact hprevious_witness
  147. 0147exact hlast
  148. 0148exact hg
  149. 0149symm
  150. 0150exact hsumpart_witness_witness_right_right