BT00YY · Bertrand theorem

prime_contribution_product_divides

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Every finite complete-contribution Product divides its source.

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.

Statement with defined notation

∀ n. ∀ m. ∀ z. (∃ x. ∃ y. (∀ k. Lt(k,m) → ∃ i. BetaAt(x,y,k,i) ∧ (Prime(S k) ∧ (∃ j. PowerValuation(S k,n,j) ∧ Pow(S k,j,i)) ∨ ¬Prime(S k) ∧ i = 1)) ∧ Product(x,y,m,z)) → Dvd(z,n)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0003 Dvd PD0004 Prime PD0013 BetaAt PD0014 Product PD0020 Pow PD0046 PowerValuation

8 occurrences

In local proof propositions

PD0002 Lt PD0003 Dvd PD0004 Prime PD0005 Coprime PD0013 BetaAt PD0020 Pow PD0046 PowerValuation

14 occurrences

Exact expanded native-PA statement
forall n m z. (exists bpr_product_code_bpcpd_source bpr_product_scale_bpcpd_source. ((forall bpr_prefix_index_bpcpd_source_prefix. (exists bpr_gap_bpcpd_source_prefix_bound. bpr_gap_bpcpd_source_prefix_bound + S (bpr_prefix_index_bpcpd_source_prefix) = m) -> exists bpr_prefix_value_bpcpd_source_prefix. ((((exists bpr_height_bpcpd_source_prefix_decoded. bpr_height_bpcpd_source_prefix_decoded + S (bpr_prefix_value_bpcpd_source_prefix) = S ((S (bpr_prefix_index_bpcpd_source_prefix)) * bpr_product_scale_bpcpd_source)) /\ exists bpr_quotient_bpcpd_source_prefix_decoded. bpr_product_code_bpcpd_source = bpr_quotient_bpcpd_source_prefix_decoded * S ((S (bpr_prefix_index_bpcpd_source_prefix)) * bpr_product_scale_bpcpd_source) + (bpr_prefix_value_bpcpd_source_prefix))) /\ (((((~(S (bpr_prefix_index_bpcpd_source_prefix) = 1) /\ forall bpr_left_bpcpd_source_prefix_choice_prime bpr_right_bpcpd_source_prefix_choice_prime. S (bpr_prefix_index_bpcpd_source_prefix) = bpr_left_bpcpd_source_prefix_choice_prime * bpr_right_bpcpd_source_prefix_choice_prime -> bpr_left_bpcpd_source_prefix_choice_prime = 1 \/ bpr_right_bpcpd_source_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpd_source_prefix_choice. ((((exists bpr_le_gap_bpcpd_source_prefix_choice_valuation_selected_bound. bpr_le_gap_bpcpd_source_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpd_source_prefix_choice) = (n)) /\ (exists bpr_power_value_bpcpd_source_prefix_choice_valuation_selected. ((exists bpr_power_code_bpcpd_source_prefix_choice_valuation_selected_power bpr_power_scale_bpcpd_source_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpcpd_source_prefix_choice_valuation_selected_power. (exists bpr_gap_bpcpd_source_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpd_source_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpd_source_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpcpd_source_prefix_choice) -> (((exists bpr_height_bpcpd_source_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpd_source_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpd_source_prefix)) = S ((S (bpr_power_index_bpcpd_source_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpd_source_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpd_source_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpd_source_prefix_choice_valuation_selected_power = bpr_quotient_bpcpd_source_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpd_source_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpd_source_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpd_source_prefix))))) /\ (exists ff_u_bpcpd_source_prefix_choice_valuation_selected_power_product ff_v_bpcpd_source_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpd_source_prefix_choice_valuation_selected_power_product_start. ff_h_bpcpd_source_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpd_source_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_valuation_selected_power_product_start. ff_u_bpcpd_source_prefix_choice_valuation_selected_power_product = ff_q_bpcpd_source_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpd_source_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpd_source_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpcpd_source_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpd_source_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpd_source_prefix_choice)) * ff_v_bpcpd_source_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpcpd_source_prefix_choice_valuation_selected_power_product = ff_q_bpcpd_source_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpd_source_prefix_choice)) * ff_v_bpcpd_source_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpcpd_source_prefix_choice_valuation_selected))) /\ forall ff_i_bpcpd_source_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpcpd_source_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpcpd_source_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpcpd_source_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpd_source_prefix_choice) -> exists ff_p_bpcpd_source_prefix_choice_valuation_selected_power_product ff_r_bpcpd_source_prefix_choice_valuation_selected_power_product ff_s_bpcpd_source_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpd_source_prefix_choice_valuation_selected_power_product_factor. ff_h_bpcpd_source_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpcpd_source_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpd_source_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpd_source_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpcpd_source_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpd_source_prefix_choice_valuation_selected_power = ff_q_bpcpd_source_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpd_source_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpd_source_prefix_choice_valuation_selected_power) + (ff_p_bpcpd_source_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpd_source_prefix_choice_valuation_selected_power_product_partial. ff_h_bpcpd_source_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpcpd_source_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpd_source_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpd_source_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_valuation_selected_power_product_partial. ff_u_bpcpd_source_prefix_choice_valuation_selected_power_product = ff_q_bpcpd_source_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpd_source_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpd_source_prefix_choice_valuation_selected_power_product) + (ff_r_bpcpd_source_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpd_source_prefix_choice_valuation_selected_power_product_successor. ff_h_bpcpd_source_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpcpd_source_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpd_source_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpd_source_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_valuation_selected_power_product_successor. ff_u_bpcpd_source_prefix_choice_valuation_selected_power_product = ff_q_bpcpd_source_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpd_source_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpd_source_prefix_choice_valuation_selected_power_product) + (ff_s_bpcpd_source_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpcpd_source_prefix_choice_valuation_selected_power_product = ff_r_bpcpd_source_prefix_choice_valuation_selected_power_product * ff_p_bpcpd_source_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpd_source_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpcpd_source_prefix_choice_valuation_selected) * bpr_divides_quotient_bpcpd_source_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpd_source_prefix_choice_valuation. (exists bpr_le_gap_bpcpd_source_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpcpd_source_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpd_source_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpd_source_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpcpd_source_prefix_choice_valuation_candidate_power bpr_power_scale_bpcpd_source_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpd_source_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpcpd_source_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpd_source_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpd_source_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpd_source_prefix_choice_valuation) -> (((exists bpr_height_bpcpd_source_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpd_source_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpd_source_prefix)) = S ((S (bpr_power_index_bpcpd_source_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpd_source_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpd_source_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpd_source_prefix_choice_valuation_candidate_power = bpr_quotient_bpcpd_source_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpd_source_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpd_source_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpd_source_prefix))))) /\ (exists ff_u_bpcpd_source_prefix_choice_valuation_candidate_power_product ff_v_bpcpd_source_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpd_source_prefix_choice_valuation_candidate_power_product_start. ff_h_bpcpd_source_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpd_source_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_valuation_candidate_power_product_start. ff_u_bpcpd_source_prefix_choice_valuation_candidate_power_product = ff_q_bpcpd_source_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpd_source_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpd_source_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpcpd_source_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpd_source_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpd_source_prefix_choice_valuation)) * ff_v_bpcpd_source_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpcpd_source_prefix_choice_valuation_candidate_power_product = ff_q_bpcpd_source_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpd_source_prefix_choice_valuation)) * ff_v_bpcpd_source_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpd_source_prefix_choice_valuation_candidate))) /\ forall ff_i_bpcpd_source_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpcpd_source_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpcpd_source_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpcpd_source_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpd_source_prefix_choice_valuation) -> exists ff_p_bpcpd_source_prefix_choice_valuation_candidate_power_product ff_r_bpcpd_source_prefix_choice_valuation_candidate_power_product ff_s_bpcpd_source_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpd_source_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpcpd_source_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpd_source_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpd_source_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpd_source_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpcpd_source_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpd_source_prefix_choice_valuation_candidate_power = ff_q_bpcpd_source_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpd_source_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpd_source_prefix_choice_valuation_candidate_power) + (ff_p_bpcpd_source_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpd_source_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpcpd_source_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpd_source_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpd_source_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpd_source_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpcpd_source_prefix_choice_valuation_candidate_power_product = ff_q_bpcpd_source_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpd_source_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpd_source_prefix_choice_valuation_candidate_power_product) + (ff_r_bpcpd_source_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpd_source_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpcpd_source_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpd_source_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpd_source_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpd_source_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpcpd_source_prefix_choice_valuation_candidate_power_product = ff_q_bpcpd_source_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpd_source_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpd_source_prefix_choice_valuation_candidate_power_product) + (ff_s_bpcpd_source_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpcpd_source_prefix_choice_valuation_candidate_power_product = ff_r_bpcpd_source_prefix_choice_valuation_candidate_power_product * ff_p_bpcpd_source_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpd_source_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpd_source_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpcpd_source_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpd_source_prefix_choice_valuation_candidate_below. bpr_le_gap_bpcpd_source_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpd_source_prefix_choice_valuation) = (bpr_choice_exponent_bpcpd_source_prefix_choice))) /\ (exists bpr_power_code_bpcpd_source_prefix_choice_power bpr_power_scale_bpcpd_source_prefix_choice_power. ((forall bpr_power_index_bpcpd_source_prefix_choice_power. (exists bpr_gap_bpcpd_source_prefix_choice_power_repeat_bound. bpr_gap_bpcpd_source_prefix_choice_power_repeat_bound + S (bpr_power_index_bpcpd_source_prefix_choice_power) = bpr_choice_exponent_bpcpd_source_prefix_choice) -> (((exists bpr_height_bpcpd_source_prefix_choice_power_repeat_entry. bpr_height_bpcpd_source_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpd_source_prefix)) = S ((S (bpr_power_index_bpcpd_source_prefix_choice_power)) * bpr_power_scale_bpcpd_source_prefix_choice_power)) /\ exists bpr_quotient_bpcpd_source_prefix_choice_power_repeat_entry. bpr_power_code_bpcpd_source_prefix_choice_power = bpr_quotient_bpcpd_source_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpd_source_prefix_choice_power)) * bpr_power_scale_bpcpd_source_prefix_choice_power) + (S (bpr_prefix_index_bpcpd_source_prefix))))) /\ (exists ff_u_bpcpd_source_prefix_choice_power_product ff_v_bpcpd_source_prefix_choice_power_product. ((((exists ff_h_bpcpd_source_prefix_choice_power_product_start. ff_h_bpcpd_source_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpd_source_prefix_choice_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_power_product_start. ff_u_bpcpd_source_prefix_choice_power_product = ff_q_bpcpd_source_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpcpd_source_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpd_source_prefix_choice_power_product_terminal. ff_h_bpcpd_source_prefix_choice_power_product_terminal + S (bpr_prefix_value_bpcpd_source_prefix) = S ((S (bpr_choice_exponent_bpcpd_source_prefix_choice)) * ff_v_bpcpd_source_prefix_choice_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_power_product_terminal. ff_u_bpcpd_source_prefix_choice_power_product = ff_q_bpcpd_source_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpd_source_prefix_choice)) * ff_v_bpcpd_source_prefix_choice_power_product) + (bpr_prefix_value_bpcpd_source_prefix))) /\ forall ff_i_bpcpd_source_prefix_choice_power_product. (exists ff_lt_bpcpd_source_prefix_choice_power_product_bound. ff_lt_bpcpd_source_prefix_choice_power_product_bound + S ff_i_bpcpd_source_prefix_choice_power_product = bpr_choice_exponent_bpcpd_source_prefix_choice) -> exists ff_p_bpcpd_source_prefix_choice_power_product ff_r_bpcpd_source_prefix_choice_power_product ff_s_bpcpd_source_prefix_choice_power_product. ((((exists ff_h_bpcpd_source_prefix_choice_power_product_factor. ff_h_bpcpd_source_prefix_choice_power_product_factor + S (ff_p_bpcpd_source_prefix_choice_power_product) = S ((S (ff_i_bpcpd_source_prefix_choice_power_product)) * bpr_power_scale_bpcpd_source_prefix_choice_power)) /\ exists ff_q_bpcpd_source_prefix_choice_power_product_factor. bpr_power_code_bpcpd_source_prefix_choice_power = ff_q_bpcpd_source_prefix_choice_power_product_factor * S ((S (ff_i_bpcpd_source_prefix_choice_power_product)) * bpr_power_scale_bpcpd_source_prefix_choice_power) + (ff_p_bpcpd_source_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpd_source_prefix_choice_power_product_partial. ff_h_bpcpd_source_prefix_choice_power_product_partial + S (ff_r_bpcpd_source_prefix_choice_power_product) = S ((S (ff_i_bpcpd_source_prefix_choice_power_product)) * ff_v_bpcpd_source_prefix_choice_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_power_product_partial. ff_u_bpcpd_source_prefix_choice_power_product = ff_q_bpcpd_source_prefix_choice_power_product_partial * S ((S (ff_i_bpcpd_source_prefix_choice_power_product)) * ff_v_bpcpd_source_prefix_choice_power_product) + (ff_r_bpcpd_source_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpd_source_prefix_choice_power_product_successor. ff_h_bpcpd_source_prefix_choice_power_product_successor + S (ff_s_bpcpd_source_prefix_choice_power_product) = S ((S (S ff_i_bpcpd_source_prefix_choice_power_product)) * ff_v_bpcpd_source_prefix_choice_power_product)) /\ exists ff_q_bpcpd_source_prefix_choice_power_product_successor. ff_u_bpcpd_source_prefix_choice_power_product = ff_q_bpcpd_source_prefix_choice_power_product_successor * S ((S (S ff_i_bpcpd_source_prefix_choice_power_product)) * ff_v_bpcpd_source_prefix_choice_power_product) + (ff_s_bpcpd_source_prefix_choice_power_product))) /\ ff_s_bpcpd_source_prefix_choice_power_product = ff_r_bpcpd_source_prefix_choice_power_product * ff_p_bpcpd_source_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpd_source_prefix) = 1) /\ forall bpr_left_bpcpd_source_prefix_choice_prime bpr_right_bpcpd_source_prefix_choice_prime. S (bpr_prefix_index_bpcpd_source_prefix) = bpr_left_bpcpd_source_prefix_choice_prime * bpr_right_bpcpd_source_prefix_choice_prime -> bpr_left_bpcpd_source_prefix_choice_prime = 1 \/ bpr_right_bpcpd_source_prefix_choice_prime = 1)) /\ bpr_prefix_value_bpcpd_source_prefix = 1))))) /\ (exists ff_u_bpcpd_source_product ff_v_bpcpd_source_product. ((((exists ff_h_bpcpd_source_product_start. ff_h_bpcpd_source_product_start + S (1) = S ((S (0)) * ff_v_bpcpd_source_product)) /\ exists ff_q_bpcpd_source_product_start. ff_u_bpcpd_source_product = ff_q_bpcpd_source_product_start * S ((S (0)) * ff_v_bpcpd_source_product) + (1))) /\ ((((exists ff_h_bpcpd_source_product_terminal. ff_h_bpcpd_source_product_terminal + S (z) = S ((S (m)) * ff_v_bpcpd_source_product)) /\ exists ff_q_bpcpd_source_product_terminal. ff_u_bpcpd_source_product = ff_q_bpcpd_source_product_terminal * S ((S (m)) * ff_v_bpcpd_source_product) + (z))) /\ forall ff_i_bpcpd_source_product. (exists ff_lt_bpcpd_source_product_bound. ff_lt_bpcpd_source_product_bound + S ff_i_bpcpd_source_product = m) -> exists ff_p_bpcpd_source_product ff_r_bpcpd_source_product ff_s_bpcpd_source_product. ((((exists ff_h_bpcpd_source_product_factor. ff_h_bpcpd_source_product_factor + S (ff_p_bpcpd_source_product) = S ((S (ff_i_bpcpd_source_product)) * bpr_product_scale_bpcpd_source)) /\ exists ff_q_bpcpd_source_product_factor. bpr_product_code_bpcpd_source = ff_q_bpcpd_source_product_factor * S ((S (ff_i_bpcpd_source_product)) * bpr_product_scale_bpcpd_source) + (ff_p_bpcpd_source_product))) /\ ((((exists ff_h_bpcpd_source_product_partial. ff_h_bpcpd_source_product_partial + S (ff_r_bpcpd_source_product) = S ((S (ff_i_bpcpd_source_product)) * ff_v_bpcpd_source_product)) /\ exists ff_q_bpcpd_source_product_partial. ff_u_bpcpd_source_product = ff_q_bpcpd_source_product_partial * S ((S (ff_i_bpcpd_source_product)) * ff_v_bpcpd_source_product) + (ff_r_bpcpd_source_product))) /\ ((((exists ff_h_bpcpd_source_product_successor. ff_h_bpcpd_source_product_successor + S (ff_s_bpcpd_source_product) = S ((S (S ff_i_bpcpd_source_product)) * ff_v_bpcpd_source_product)) /\ exists ff_q_bpcpd_source_product_successor. ff_u_bpcpd_source_product = ff_q_bpcpd_source_product_successor * S ((S (S ff_i_bpcpd_source_product)) * ff_v_bpcpd_source_product) + (ff_s_bpcpd_source_product))) /\ ff_s_bpcpd_source_product = ff_r_bpcpd_source_product * ff_p_bpcpd_source_product)))))))) -> (exists bpr_divides_quotient_bpcpd_result. n = (z) * bpr_divides_quotient_bpcpd_result)

Proof neighborhood

Direct theorem prerequisites

BT0042 beta_at_unique BT00VD beta_pairwise_coprime_product_divides_common_multiple BT00YW prime_contribution_prefix_pairwise_coprime BT00YX prime_contribution_factor_divides

Direct theorem dependents

BT0104 prime_contribution_reverse_divides BT0105 prime_contribution_product_eq

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

Read the argument

Proof checkpoints

40 script commands · 12 reading checkpoints · 5 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)
beta at uniquebeta pairwise coprime product divides common multipleprime contribution prefix pairwise coprimeprime contribution factor divides
01Fix variables and assumptionsL1–4

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

  1. L1
    intro n
  2. L2
    intro m
  3. L3
    intro z
  4. L4
    intro hsource
02Separate the logical casesL5–7

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

  1. L5
    cases hsource
  2. L6
    cases hsource_witness
  3. L7
    cases hsource_witness_witness
03Establish hpairwiseL8–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution prefix pairwise coprime.

  1. L8
    have hpairwise : ∀ bpr_pair_left_index_bpcpd_pairwise. ∀ bpr_pair_right_index_bpcpd_pairwise. ∀ bpr_pair_left_bpcpd_pairwise. ∀ bpr_pair_right_bpcpd_pairwise. Lt(bpr_pair_left_index_bpcpd_pairwise,m) → Lt(bpr_pair_right_index_bpcpd_pairwise,m) → BetaAt(x,x1,bpr_pair_left_index_bpcpd_pairwise,bpr_pair_left_bpcpd_pairwise) → BetaAt(x,x1,bpr_pair_right_index_bpcpd_pairwise,bpr_pair_right_bpcpd_pairwise) → ¬bpr_pair_left_index_bpcpd_pairwise = bpr_pair_right_index_bpcpd_pairwise → Coprime(bpr_pair_left_bpcpd_pairwise,bpr_pair_right_bpcpd_pairwise)Definitions: Lt(bpr_pair_left_index_bpcpd_pairwise,m)Lt(bpr_pair_right_index_bpcpd_pairwise,m)BetaAt(x,x1,bpr_pair_left_index_bpcpd_pairwise,bpr_pair_left_bpcpd_pairwise)BetaAt(x,x1,bpr_pair_right_index_bpcpd_pairwise,bpr_pair_right_bpcpd_pairwise)Coprime(bpr_pair_left_bpcpd_pairwise,bpr_pair_right_bpcpd_pairwise)Original native command in the exact edition
  2. L9
    apply prime_contribution_prefix_pairwise_coprime
  3. L10
    exact hsource_witness_witness_left
04Establish hpointwiseL11–15

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

  1. L11
    have hpointwise : ∀ bpr_divide_index_bpcpd_pointwise. ∀ bpr_divide_value_bpcpd_pointwise. Lt(bpr_divide_index_bpcpd_pointwise,m) → BetaAt(x,x1,bpr_divide_index_bpcpd_pointwise,bpr_divide_value_bpcpd_pointwise) → Dvd(bpr_divide_value_bpcpd_pointwise,n)Definitions: Lt(bpr_divide_index_bpcpd_pointwise,m)BetaAt(x,x1,bpr_divide_index_bpcpd_pointwise,bpr_divide_value_bpcpd_pointwise)Dvd(bpr_divide_value_bpcpd_pointwise,n)Original native command in the exact edition
  2. L12
    intro i
  3. L13
    intro a
  4. L14
    intro hi
  5. L15
    intro ha
05Establish hentryL16–18

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

  1. L16
    have hentry : ∃ q. BetaAt(x,x1,i,q) ∧ (Prime(S i) ∧ (∃ y. PowerValuation(S i,n,y) ∧ Pow(S i,y,q)) ∨ ¬Prime(S i) ∧ q = 1)Definitions: BetaAt(x,x1,i,q)Prime(S i)PowerValuation(S i,n,y)Pow(S i,y,q)Original native command in the exact edition
  2. L17
    apply hsource_witness_witness_left
  3. L18
    exact hi
06Separate the logical casesL19–20

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

  1. L19
    cases hentry
  2. L20
    cases hentry_witness
07Establish haqL21–24

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

  1. L21
    have haq : a = x2
  2. L22
    apply beta_at_unique
  3. L23
    exact ha
  4. L24
    exact hentry_witness_left
08Establish hdividesL25–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution factor divides.

  1. L25
    have hdivides : Dvd(x2,n)Definitions: Dvd(x2,n)Original native command in the exact edition
  2. L26
    apply prime_contribution_factor_divides
  3. L27
    exact hentry_witness_right
09Separate the logical casesL28–28

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

  1. L28
    cases hdivides
10Construct an explicit witnessL29–29

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

  1. L29
    exists x3
11Calculate and transport equalitiesL30–30

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

  1. L30
    rewrite haq
12Use earlier factsL31–40

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

  1. L31
    exact hdivides_witness
  2. L32
    specialize beta_pairwise_coprime_product_divides_common_multiple x
  3. L33
    specialize beta_pairwise_coprime_product_divides_common_multiple x1
  4. L34
    specialize beta_pairwise_coprime_product_divides_common_multiple m
  5. L35
    specialize beta_pairwise_coprime_product_divides_common_multiple z
  6. L36
    specialize beta_pairwise_coprime_product_divides_common_multiple n
  7. L37
    apply beta_pairwise_coprime_product_divides_common_multiple
  8. L38
    exact hpairwise
  9. L39
    exact hpointwise
  10. L40
    exact hsource_witness_witness_right

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro n
  2. 0002intro m
  3. 0003intro z
  4. 0004intro hsource
  5. 0005cases hsource
  6. 0006cases hsource_witness
  7. 0007cases hsource_witness_witness
  8. 0008have hpairwise : ∀ bpr_pair_left_index_bpcpd_pairwise. ∀ bpr_pair_right_index_bpcpd_pairwise. ∀ bpr_pair_left_bpcpd_pairwise. ∀ bpr_pair_right_bpcpd_pairwise. Lt(bpr_pair_left_index_bpcpd_pairwise,m) → Lt(bpr_pair_right_index_bpcpd_pairwise,m) → BetaAt(x,x1,bpr_pair_left_index_bpcpd_pairwise,bpr_pair_left_bpcpd_pairwise) → BetaAt(x,x1,bpr_pair_right_index_bpcpd_pairwise,bpr_pair_right_bpcpd_pairwise) → ¬bpr_pair_left_index_bpcpd_pairwise = bpr_pair_right_index_bpcpd_pairwise → Coprime(bpr_pair_left_bpcpd_pairwise,bpr_pair_right_bpcpd_pairwise)
    Exact native replay linehave hpairwise : forall bpr_pair_left_index_bpcpd_pairwise bpr_pair_right_index_bpcpd_pairwise bpr_pair_left_bpcpd_pairwise bpr_pair_right_bpcpd_pairwise. (exists bpr_gap_bpcpd_pairwise_left_bound. bpr_gap_bpcpd_pairwise_left_bound + S (bpr_pair_left_index_bpcpd_pairwise) = m) -> (exists bpr_gap_bpcpd_pairwise_right_bound. bpr_gap_bpcpd_pairwise_right_bound + S (bpr_pair_right_index_bpcpd_pairwise) = m) -> (((exists bpr_height_bpcpd_pairwise_left_entry. bpr_height_bpcpd_pairwise_left_entry + S (bpr_pair_left_bpcpd_pairwise) = S ((S (bpr_pair_left_index_bpcpd_pairwise)) * x1)) /\ exists bpr_quotient_bpcpd_pairwise_left_entry. x = bpr_quotient_bpcpd_pairwise_left_entry * S ((S (bpr_pair_left_index_bpcpd_pairwise)) * x1) + (bpr_pair_left_bpcpd_pairwise))) -> (((exists bpr_height_bpcpd_pairwise_right_entry. bpr_height_bpcpd_pairwise_right_entry + S (bpr_pair_right_bpcpd_pairwise) = S ((S (bpr_pair_right_index_bpcpd_pairwise)) * x1)) /\ exists bpr_quotient_bpcpd_pairwise_right_entry. x = bpr_quotient_bpcpd_pairwise_right_entry * S ((S (bpr_pair_right_index_bpcpd_pairwise)) * x1) + (bpr_pair_right_bpcpd_pairwise))) -> ~(bpr_pair_left_index_bpcpd_pairwise = bpr_pair_right_index_bpcpd_pairwise) -> (forall bpr_coprime_divisor_bpcpd_pairwise_coprime. (exists bpr_coprime_left_bpcpd_pairwise_coprime. bpr_pair_left_bpcpd_pairwise = bpr_coprime_divisor_bpcpd_pairwise_coprime * bpr_coprime_left_bpcpd_pairwise_coprime) -> (exists bpr_coprime_right_bpcpd_pairwise_coprime. bpr_pair_right_bpcpd_pairwise = bpr_coprime_divisor_bpcpd_pairwise_coprime * bpr_coprime_right_bpcpd_pairwise_coprime) -> bpr_coprime_divisor_bpcpd_pairwise_coprime = 1)
  9. 0009apply prime_contribution_prefix_pairwise_coprime
  10. 0010exact hsource_witness_witness_left
  11. 0011have hpointwise : ∀ bpr_divide_index_bpcpd_pointwise. ∀ bpr_divide_value_bpcpd_pointwise. Lt(bpr_divide_index_bpcpd_pointwise,m) → BetaAt(x,x1,bpr_divide_index_bpcpd_pointwise,bpr_divide_value_bpcpd_pointwise) → Dvd(bpr_divide_value_bpcpd_pointwise,n)
    Exact native replay linehave hpointwise : forall bpr_divide_index_bpcpd_pointwise bpr_divide_value_bpcpd_pointwise. (exists bpr_gap_bpcpd_pointwise_bound. bpr_gap_bpcpd_pointwise_bound + S (bpr_divide_index_bpcpd_pointwise) = m) -> (((exists bpr_height_bpcpd_pointwise_entry. bpr_height_bpcpd_pointwise_entry + S (bpr_divide_value_bpcpd_pointwise) = S ((S (bpr_divide_index_bpcpd_pointwise)) * x1)) /\ exists bpr_quotient_bpcpd_pointwise_entry. x = bpr_quotient_bpcpd_pointwise_entry * S ((S (bpr_divide_index_bpcpd_pointwise)) * x1) + (bpr_divide_value_bpcpd_pointwise))) -> (exists bpr_divides_quotient_bpcpd_pointwise_divides. n = (bpr_divide_value_bpcpd_pointwise) * bpr_divides_quotient_bpcpd_pointwise_divides)
  12. 0012intro i
  13. 0013intro a
  14. 0014intro hi
  15. 0015intro ha
  16. 0016have hentry : ∃ q. BetaAt(x,x1,i,q) ∧ (Prime(S i) ∧ (∃ y. PowerValuation(S i,n,y) ∧ Pow(S i,y,q)) ∨ ¬Prime(S i) ∧ q = 1)
    Exact native replay linehave hentry : exists q. (((exists bpr_height_bpcpd_entry. bpr_height_bpcpd_entry + S (q) = S ((S (i)) * x1)) /\ exists bpr_quotient_bpcpd_entry. x = bpr_quotient_bpcpd_entry * S ((S (i)) * x1) + (q))) /\ (((((~(S (i) = 1) /\ forall bpr_left_bpcpd_choice_prime bpr_right_bpcpd_choice_prime. S (i) = bpr_left_bpcpd_choice_prime * bpr_right_bpcpd_choice_prime -> bpr_left_bpcpd_choice_prime = 1 \/ bpr_right_bpcpd_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpd_choice. ((((exists bpr_le_gap_bpcpd_choice_valuation_selected_bound. bpr_le_gap_bpcpd_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpd_choice) = (n)) /\ (exists bpr_power_value_bpcpd_choice_valuation_selected. ((exists bpr_power_code_bpcpd_choice_valuation_selected_power bpr_power_scale_bpcpd_choice_valuation_selected_power. ((forall bpr_power_index_bpcpd_choice_valuation_selected_power. (exists bpr_gap_bpcpd_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpd_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpd_choice_valuation_selected_power) = bpr_choice_exponent_bpcpd_choice) -> (((exists bpr_height_bpcpd_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpd_choice_valuation_selected_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcpd_choice_valuation_selected_power)) * bpr_power_scale_bpcpd_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpd_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpd_choice_valuation_selected_power = bpr_quotient_bpcpd_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpd_choice_valuation_selected_power)) * bpr_power_scale_bpcpd_choice_valuation_selected_power) + (S (i))))) /\ (exists ff_u_bpcpd_choice_valuation_selected_power_product ff_v_bpcpd_choice_valuation_selected_power_product. ((((exists ff_h_bpcpd_choice_valuation_selected_power_product_start. ff_h_bpcpd_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpd_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpd_choice_valuation_selected_power_product_start. ff_u_bpcpd_choice_valuation_selected_power_product = ff_q_bpcpd_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpd_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpd_choice_valuation_selected_power_product_terminal. ff_h_bpcpd_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpd_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpd_choice)) * ff_v_bpcpd_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpd_choice_valuation_selected_power_product_terminal. ff_u_bpcpd_choice_valuation_selected_power_product = ff_q_bpcpd_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpd_choice)) * ff_v_bpcpd_choice_valuation_selected_power_product) + (bpr_power_value_bpcpd_choice_valuation_selected))) /\ forall ff_i_bpcpd_choice_valuation_selected_power_product. (exists ff_lt_bpcpd_choice_valuation_selected_power_product_bound. ff_lt_bpcpd_choice_valuation_selected_power_product_bound + S ff_i_bpcpd_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpd_choice) -> exists ff_p_bpcpd_choice_valuation_selected_power_product ff_r_bpcpd_choice_valuation_selected_power_product ff_s_bpcpd_choice_valuation_selected_power_product. ((((exists ff_h_bpcpd_choice_valuation_selected_power_product_factor. ff_h_bpcpd_choice_valuation_selected_power_product_factor + S (ff_p_bpcpd_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpd_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpd_choice_valuation_selected_power)) /\ exists ff_q_bpcpd_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpd_choice_valuation_selected_power = ff_q_bpcpd_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpd_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpd_choice_valuation_selected_power) + (ff_p_bpcpd_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpd_choice_valuation_selected_power_product_partial. ff_h_bpcpd_choice_valuation_selected_power_product_partial + S (ff_r_bpcpd_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpd_choice_valuation_selected_power_product)) * ff_v_bpcpd_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpd_choice_valuation_selected_power_product_partial. ff_u_bpcpd_choice_valuation_selected_power_product = ff_q_bpcpd_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpd_choice_valuation_selected_power_product)) * ff_v_bpcpd_choice_valuation_selected_power_product) + (ff_r_bpcpd_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpd_choice_valuation_selected_power_product_successor. ff_h_bpcpd_choice_valuation_selected_power_product_successor + S (ff_s_bpcpd_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpd_choice_valuation_selected_power_product)) * ff_v_bpcpd_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpd_choice_valuation_selected_power_product_successor. ff_u_bpcpd_choice_valuation_selected_power_product = ff_q_bpcpd_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpd_choice_valuation_selected_power_product)) * ff_v_bpcpd_choice_valuation_selected_power_product) + (ff_s_bpcpd_choice_valuation_selected_power_product))) /\ ff_s_bpcpd_choice_valuation_selected_power_product = ff_r_bpcpd_choice_valuation_selected_power_product * ff_p_bpcpd_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpd_choice_valuation_selected_divides. n = (bpr_power_value_bpcpd_choice_valuation_selected) * bpr_divides_quotient_bpcpd_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpd_choice_valuation. (exists bpr_le_gap_bpcpd_choice_valuation_candidate_bound. bpr_le_gap_bpcpd_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpd_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpd_choice_valuation_candidate. ((exists bpr_power_code_bpcpd_choice_valuation_candidate_power bpr_power_scale_bpcpd_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpd_choice_valuation_candidate_power. (exists bpr_gap_bpcpd_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpd_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpd_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpd_choice_valuation) -> (((exists bpr_height_bpcpd_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpd_choice_valuation_candidate_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcpd_choice_valuation_candidate_power)) * bpr_power_scale_bpcpd_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpd_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpd_choice_valuation_candidate_power = bpr_quotient_bpcpd_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpd_choice_valuation_candidate_power)) * bpr_power_scale_bpcpd_choice_valuation_candidate_power) + (S (i))))) /\ (exists ff_u_bpcpd_choice_valuation_candidate_power_product ff_v_bpcpd_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpd_choice_valuation_candidate_power_product_start. ff_h_bpcpd_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpd_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpd_choice_valuation_candidate_power_product_start. ff_u_bpcpd_choice_valuation_candidate_power_product = ff_q_bpcpd_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpd_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpd_choice_valuation_candidate_power_product_terminal. ff_h_bpcpd_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpd_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpd_choice_valuation)) * ff_v_bpcpd_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpd_choice_valuation_candidate_power_product_terminal. ff_u_bpcpd_choice_valuation_candidate_power_product = ff_q_bpcpd_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpd_choice_valuation)) * ff_v_bpcpd_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpd_choice_valuation_candidate))) /\ forall ff_i_bpcpd_choice_valuation_candidate_power_product. (exists ff_lt_bpcpd_choice_valuation_candidate_power_product_bound. ff_lt_bpcpd_choice_valuation_candidate_power_product_bound + S ff_i_bpcpd_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpd_choice_valuation) -> exists ff_p_bpcpd_choice_valuation_candidate_power_product ff_r_bpcpd_choice_valuation_candidate_power_product ff_s_bpcpd_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpd_choice_valuation_candidate_power_product_factor. ff_h_bpcpd_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpd_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpd_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpd_choice_valuation_candidate_power)) /\ exists ff_q_bpcpd_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpd_choice_valuation_candidate_power = ff_q_bpcpd_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpd_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpd_choice_valuation_candidate_power) + (ff_p_bpcpd_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpd_choice_valuation_candidate_power_product_partial. ff_h_bpcpd_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpd_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpd_choice_valuation_candidate_power_product)) * ff_v_bpcpd_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpd_choice_valuation_candidate_power_product_partial. ff_u_bpcpd_choice_valuation_candidate_power_product = ff_q_bpcpd_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpd_choice_valuation_candidate_power_product)) * ff_v_bpcpd_choice_valuation_candidate_power_product) + (ff_r_bpcpd_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpd_choice_valuation_candidate_power_product_successor. ff_h_bpcpd_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpd_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpd_choice_valuation_candidate_power_product)) * ff_v_bpcpd_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpd_choice_valuation_candidate_power_product_successor. ff_u_bpcpd_choice_valuation_candidate_power_product = ff_q_bpcpd_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpd_choice_valuation_candidate_power_product)) * ff_v_bpcpd_choice_valuation_candidate_power_product) + (ff_s_bpcpd_choice_valuation_candidate_power_product))) /\ ff_s_bpcpd_choice_valuation_candidate_power_product = ff_r_bpcpd_choice_valuation_candidate_power_product * ff_p_bpcpd_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpd_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpd_choice_valuation_candidate) * bpr_divides_quotient_bpcpd_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpd_choice_valuation_candidate_below. bpr_le_gap_bpcpd_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpd_choice_valuation) = (bpr_choice_exponent_bpcpd_choice))) /\ (exists bpr_power_code_bpcpd_choice_power bpr_power_scale_bpcpd_choice_power. ((forall bpr_power_index_bpcpd_choice_power. (exists bpr_gap_bpcpd_choice_power_repeat_bound. bpr_gap_bpcpd_choice_power_repeat_bound + S (bpr_power_index_bpcpd_choice_power) = bpr_choice_exponent_bpcpd_choice) -> (((exists bpr_height_bpcpd_choice_power_repeat_entry. bpr_height_bpcpd_choice_power_repeat_entry + S (S (i)) = S ((S (bpr_power_index_bpcpd_choice_power)) * bpr_power_scale_bpcpd_choice_power)) /\ exists bpr_quotient_bpcpd_choice_power_repeat_entry. bpr_power_code_bpcpd_choice_power = bpr_quotient_bpcpd_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpd_choice_power)) * bpr_power_scale_bpcpd_choice_power) + (S (i))))) /\ (exists ff_u_bpcpd_choice_power_product ff_v_bpcpd_choice_power_product. ((((exists ff_h_bpcpd_choice_power_product_start. ff_h_bpcpd_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpd_choice_power_product)) /\ exists ff_q_bpcpd_choice_power_product_start. ff_u_bpcpd_choice_power_product = ff_q_bpcpd_choice_power_product_start * S ((S (0)) * ff_v_bpcpd_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpd_choice_power_product_terminal. ff_h_bpcpd_choice_power_product_terminal + S (q) = S ((S (bpr_choice_exponent_bpcpd_choice)) * ff_v_bpcpd_choice_power_product)) /\ exists ff_q_bpcpd_choice_power_product_terminal. ff_u_bpcpd_choice_power_product = ff_q_bpcpd_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpd_choice)) * ff_v_bpcpd_choice_power_product) + (q))) /\ forall ff_i_bpcpd_choice_power_product. (exists ff_lt_bpcpd_choice_power_product_bound. ff_lt_bpcpd_choice_power_product_bound + S ff_i_bpcpd_choice_power_product = bpr_choice_exponent_bpcpd_choice) -> exists ff_p_bpcpd_choice_power_product ff_r_bpcpd_choice_power_product ff_s_bpcpd_choice_power_product. ((((exists ff_h_bpcpd_choice_power_product_factor. ff_h_bpcpd_choice_power_product_factor + S (ff_p_bpcpd_choice_power_product) = S ((S (ff_i_bpcpd_choice_power_product)) * bpr_power_scale_bpcpd_choice_power)) /\ exists ff_q_bpcpd_choice_power_product_factor. bpr_power_code_bpcpd_choice_power = ff_q_bpcpd_choice_power_product_factor * S ((S (ff_i_bpcpd_choice_power_product)) * bpr_power_scale_bpcpd_choice_power) + (ff_p_bpcpd_choice_power_product))) /\ ((((exists ff_h_bpcpd_choice_power_product_partial. ff_h_bpcpd_choice_power_product_partial + S (ff_r_bpcpd_choice_power_product) = S ((S (ff_i_bpcpd_choice_power_product)) * ff_v_bpcpd_choice_power_product)) /\ exists ff_q_bpcpd_choice_power_product_partial. ff_u_bpcpd_choice_power_product = ff_q_bpcpd_choice_power_product_partial * S ((S (ff_i_bpcpd_choice_power_product)) * ff_v_bpcpd_choice_power_product) + (ff_r_bpcpd_choice_power_product))) /\ ((((exists ff_h_bpcpd_choice_power_product_successor. ff_h_bpcpd_choice_power_product_successor + S (ff_s_bpcpd_choice_power_product) = S ((S (S ff_i_bpcpd_choice_power_product)) * ff_v_bpcpd_choice_power_product)) /\ exists ff_q_bpcpd_choice_power_product_successor. ff_u_bpcpd_choice_power_product = ff_q_bpcpd_choice_power_product_successor * S ((S (S ff_i_bpcpd_choice_power_product)) * ff_v_bpcpd_choice_power_product) + (ff_s_bpcpd_choice_power_product))) /\ ff_s_bpcpd_choice_power_product = ff_r_bpcpd_choice_power_product * ff_p_bpcpd_choice_power_product)))))))))) \/ (~((~(S (i) = 1) /\ forall bpr_left_bpcpd_choice_prime bpr_right_bpcpd_choice_prime. S (i) = bpr_left_bpcpd_choice_prime * bpr_right_bpcpd_choice_prime -> bpr_left_bpcpd_choice_prime = 1 \/ bpr_right_bpcpd_choice_prime = 1)) /\ q = 1)))
  17. 0017apply hsource_witness_witness_left
  18. 0018exact hi
  19. 0019cases hentry
  20. 0020cases hentry_witness
  21. 0021have haq : a = x2
  22. 0022apply beta_at_unique
  23. 0023exact ha
  24. 0024exact hentry_witness_left
  25. 0025have hdivides : Dvd(x2,n)
    Exact native replay linehave hdivides : exists q. n = x2 * q
  26. 0026apply prime_contribution_factor_divides
  27. 0027exact hentry_witness_right
  28. 0028cases hdivides
  29. 0029exists x3
  30. 0030rewrite haq
  31. 0031exact hdivides_witness
  32. 0032specialize beta_pairwise_coprime_product_divides_common_multiple x
  33. 0033specialize beta_pairwise_coprime_product_divides_common_multiple x1
  34. 0034specialize beta_pairwise_coprime_product_divides_common_multiple m
  35. 0035specialize beta_pairwise_coprime_product_divides_common_multiple z
  36. 0036specialize beta_pairwise_coprime_product_divides_common_multiple n
  37. 0037apply beta_pairwise_coprime_product_divides_common_multiple
  38. 0038exact hpairwise
  39. 0039exact hpointwise
  40. 0040exact hsource_witness_witness_right