BT0106 · Bertrand theorem

prime_contribution_complete_exists

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

Every nonzero source has an exact supported contribution product.

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. ¬n = 0 → (∀ x. Prime(x) → Dvd(x,n) → Le(x,m)) → ∃ x. (∃ y. ∃ z. (∀ k. Lt(k,m) → ∃ i. BetaAt(y,z,k,i) ∧ (Prime(S k) ∧ (∃ j. PowerValuation(S k,n,j) ∧ Pow(S k,j,i)) ∨ ¬Prime(S k) ∧ i = 1)) ∧ Product(y,z,m,x)) ∧ n = x

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

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

10 occurrences

In local proof propositions

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

7 occurrences

Exact expanded native-PA statement
forall n m. ~(n = 0) -> (forall bpr_support_prime_bpcce_support. ((~(bpr_support_prime_bpcce_support = 1) /\ forall bpr_left_bpcce_support_prime bpr_right_bpcce_support_prime. bpr_support_prime_bpcce_support = bpr_left_bpcce_support_prime * bpr_right_bpcce_support_prime -> bpr_left_bpcce_support_prime = 1 \/ bpr_right_bpcce_support_prime = 1)) -> (exists bpr_divides_quotient_bpcce_support_divides. n = (bpr_support_prime_bpcce_support) * bpr_divides_quotient_bpcce_support_divides) -> (exists bpr_le_gap_bpcce_support_bound. bpr_le_gap_bpcce_support_bound + (bpr_support_prime_bpcce_support) = (m))) -> exists z. (exists bpr_product_code_bpcce_product bpr_product_scale_bpcce_product. ((forall bpr_prefix_index_bpcce_product_prefix. (exists bpr_gap_bpcce_product_prefix_bound. bpr_gap_bpcce_product_prefix_bound + S (bpr_prefix_index_bpcce_product_prefix) = m) -> exists bpr_prefix_value_bpcce_product_prefix. ((((exists bpr_height_bpcce_product_prefix_decoded. bpr_height_bpcce_product_prefix_decoded + S (bpr_prefix_value_bpcce_product_prefix) = S ((S (bpr_prefix_index_bpcce_product_prefix)) * bpr_product_scale_bpcce_product)) /\ exists bpr_quotient_bpcce_product_prefix_decoded. bpr_product_code_bpcce_product = bpr_quotient_bpcce_product_prefix_decoded * S ((S (bpr_prefix_index_bpcce_product_prefix)) * bpr_product_scale_bpcce_product) + (bpr_prefix_value_bpcce_product_prefix))) /\ (((((~(S (bpr_prefix_index_bpcce_product_prefix) = 1) /\ forall bpr_left_bpcce_product_prefix_choice_prime bpr_right_bpcce_product_prefix_choice_prime. S (bpr_prefix_index_bpcce_product_prefix) = bpr_left_bpcce_product_prefix_choice_prime * bpr_right_bpcce_product_prefix_choice_prime -> bpr_left_bpcce_product_prefix_choice_prime = 1 \/ bpr_right_bpcce_product_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcce_product_prefix_choice. ((((exists bpr_le_gap_bpcce_product_prefix_choice_valuation_selected_bound. bpr_le_gap_bpcce_product_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpcce_product_prefix_choice) = (n)) /\ (exists bpr_power_value_bpcce_product_prefix_choice_valuation_selected. ((exists bpr_power_code_bpcce_product_prefix_choice_valuation_selected_power bpr_power_scale_bpcce_product_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpcce_product_prefix_choice_valuation_selected_power. (exists bpr_gap_bpcce_product_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcce_product_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcce_product_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpcce_product_prefix_choice) -> (((exists bpr_height_bpcce_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpcce_product_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcce_product_prefix)) = S ((S (bpr_power_index_bpcce_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcce_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcce_product_prefix_choice_valuation_selected_power = bpr_quotient_bpcce_product_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcce_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcce_product_prefix))))) /\ (exists ff_u_bpcce_product_prefix_choice_valuation_selected_power_product ff_v_bpcce_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_start. ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_start. ff_u_bpcce_product_prefix_choice_valuation_selected_power_product = ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcce_product_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcce_product_prefix_choice)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpcce_product_prefix_choice_valuation_selected_power_product = ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcce_product_prefix_choice)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpcce_product_prefix_choice_valuation_selected))) /\ forall ff_i_bpcce_product_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpcce_product_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpcce_product_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpcce_product_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpcce_product_prefix_choice) -> exists ff_p_bpcce_product_prefix_choice_valuation_selected_power_product ff_r_bpcce_product_prefix_choice_valuation_selected_power_product ff_s_bpcce_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_factor. ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpcce_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpcce_product_prefix_choice_valuation_selected_power = ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_selected_power) + (ff_p_bpcce_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_partial. ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpcce_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_partial. ff_u_bpcce_product_prefix_choice_valuation_selected_power_product = ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product) + (ff_r_bpcce_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_successor. ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpcce_product_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_successor. ff_u_bpcce_product_prefix_choice_valuation_selected_power_product = ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product) + (ff_s_bpcce_product_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpcce_product_prefix_choice_valuation_selected_power_product = ff_r_bpcce_product_prefix_choice_valuation_selected_power_product * ff_p_bpcce_product_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcce_product_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpcce_product_prefix_choice_valuation_selected) * bpr_divides_quotient_bpcce_product_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcce_product_prefix_choice_valuation. (exists bpr_le_gap_bpcce_product_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpcce_product_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcce_product_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpcce_product_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpcce_product_prefix_choice_valuation_candidate_power bpr_power_scale_bpcce_product_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpcce_product_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpcce_product_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcce_product_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcce_product_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcce_product_prefix_choice_valuation) -> (((exists bpr_height_bpcce_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcce_product_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcce_product_prefix)) = S ((S (bpr_power_index_bpcce_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcce_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcce_product_prefix_choice_valuation_candidate_power = bpr_quotient_bpcce_product_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcce_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcce_product_prefix))))) /\ (exists ff_u_bpcce_product_prefix_choice_valuation_candidate_power_product ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_start. ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_start. ff_u_bpcce_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcce_product_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcce_product_prefix_choice_valuation)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpcce_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcce_product_prefix_choice_valuation)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpcce_product_prefix_choice_valuation_candidate))) /\ forall ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpcce_product_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpcce_product_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcce_product_prefix_choice_valuation) -> exists ff_p_bpcce_product_prefix_choice_valuation_candidate_power_product ff_r_bpcce_product_prefix_choice_valuation_candidate_power_product ff_s_bpcce_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpcce_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcce_product_prefix_choice_valuation_candidate_power = ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_candidate_power) + (ff_p_bpcce_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpcce_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpcce_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product) + (ff_r_bpcce_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpcce_product_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpcce_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product) + (ff_s_bpcce_product_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpcce_product_prefix_choice_valuation_candidate_power_product = ff_r_bpcce_product_prefix_choice_valuation_candidate_power_product * ff_p_bpcce_product_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcce_product_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpcce_product_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpcce_product_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcce_product_prefix_choice_valuation_candidate_below. bpr_le_gap_bpcce_product_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcce_product_prefix_choice_valuation) = (bpr_choice_exponent_bpcce_product_prefix_choice))) /\ (exists bpr_power_code_bpcce_product_prefix_choice_power bpr_power_scale_bpcce_product_prefix_choice_power. ((forall bpr_power_index_bpcce_product_prefix_choice_power. (exists bpr_gap_bpcce_product_prefix_choice_power_repeat_bound. bpr_gap_bpcce_product_prefix_choice_power_repeat_bound + S (bpr_power_index_bpcce_product_prefix_choice_power) = bpr_choice_exponent_bpcce_product_prefix_choice) -> (((exists bpr_height_bpcce_product_prefix_choice_power_repeat_entry. bpr_height_bpcce_product_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcce_product_prefix)) = S ((S (bpr_power_index_bpcce_product_prefix_choice_power)) * bpr_power_scale_bpcce_product_prefix_choice_power)) /\ exists bpr_quotient_bpcce_product_prefix_choice_power_repeat_entry. bpr_power_code_bpcce_product_prefix_choice_power = bpr_quotient_bpcce_product_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpcce_product_prefix_choice_power)) * bpr_power_scale_bpcce_product_prefix_choice_power) + (S (bpr_prefix_index_bpcce_product_prefix))))) /\ (exists ff_u_bpcce_product_prefix_choice_power_product ff_v_bpcce_product_prefix_choice_power_product. ((((exists ff_h_bpcce_product_prefix_choice_power_product_start. ff_h_bpcce_product_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_product_prefix_choice_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_power_product_start. ff_u_bpcce_product_prefix_choice_power_product = ff_q_bpcce_product_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpcce_product_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpcce_product_prefix_choice_power_product_terminal. ff_h_bpcce_product_prefix_choice_power_product_terminal + S (bpr_prefix_value_bpcce_product_prefix) = S ((S (bpr_choice_exponent_bpcce_product_prefix_choice)) * ff_v_bpcce_product_prefix_choice_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_power_product_terminal. ff_u_bpcce_product_prefix_choice_power_product = ff_q_bpcce_product_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcce_product_prefix_choice)) * ff_v_bpcce_product_prefix_choice_power_product) + (bpr_prefix_value_bpcce_product_prefix))) /\ forall ff_i_bpcce_product_prefix_choice_power_product. (exists ff_lt_bpcce_product_prefix_choice_power_product_bound. ff_lt_bpcce_product_prefix_choice_power_product_bound + S ff_i_bpcce_product_prefix_choice_power_product = bpr_choice_exponent_bpcce_product_prefix_choice) -> exists ff_p_bpcce_product_prefix_choice_power_product ff_r_bpcce_product_prefix_choice_power_product ff_s_bpcce_product_prefix_choice_power_product. ((((exists ff_h_bpcce_product_prefix_choice_power_product_factor. ff_h_bpcce_product_prefix_choice_power_product_factor + S (ff_p_bpcce_product_prefix_choice_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_power)) /\ exists ff_q_bpcce_product_prefix_choice_power_product_factor. bpr_power_code_bpcce_product_prefix_choice_power = ff_q_bpcce_product_prefix_choice_power_product_factor * S ((S (ff_i_bpcce_product_prefix_choice_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_power) + (ff_p_bpcce_product_prefix_choice_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_power_product_partial. ff_h_bpcce_product_prefix_choice_power_product_partial + S (ff_r_bpcce_product_prefix_choice_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_power_product)) * ff_v_bpcce_product_prefix_choice_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_power_product_partial. ff_u_bpcce_product_prefix_choice_power_product = ff_q_bpcce_product_prefix_choice_power_product_partial * S ((S (ff_i_bpcce_product_prefix_choice_power_product)) * ff_v_bpcce_product_prefix_choice_power_product) + (ff_r_bpcce_product_prefix_choice_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_power_product_successor. ff_h_bpcce_product_prefix_choice_power_product_successor + S (ff_s_bpcce_product_prefix_choice_power_product) = S ((S (S ff_i_bpcce_product_prefix_choice_power_product)) * ff_v_bpcce_product_prefix_choice_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_power_product_successor. ff_u_bpcce_product_prefix_choice_power_product = ff_q_bpcce_product_prefix_choice_power_product_successor * S ((S (S ff_i_bpcce_product_prefix_choice_power_product)) * ff_v_bpcce_product_prefix_choice_power_product) + (ff_s_bpcce_product_prefix_choice_power_product))) /\ ff_s_bpcce_product_prefix_choice_power_product = ff_r_bpcce_product_prefix_choice_power_product * ff_p_bpcce_product_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcce_product_prefix) = 1) /\ forall bpr_left_bpcce_product_prefix_choice_prime bpr_right_bpcce_product_prefix_choice_prime. S (bpr_prefix_index_bpcce_product_prefix) = bpr_left_bpcce_product_prefix_choice_prime * bpr_right_bpcce_product_prefix_choice_prime -> bpr_left_bpcce_product_prefix_choice_prime = 1 \/ bpr_right_bpcce_product_prefix_choice_prime = 1)) /\ bpr_prefix_value_bpcce_product_prefix = 1))))) /\ (exists ff_u_bpcce_product_product ff_v_bpcce_product_product. ((((exists ff_h_bpcce_product_product_start. ff_h_bpcce_product_product_start + S (1) = S ((S (0)) * ff_v_bpcce_product_product)) /\ exists ff_q_bpcce_product_product_start. ff_u_bpcce_product_product = ff_q_bpcce_product_product_start * S ((S (0)) * ff_v_bpcce_product_product) + (1))) /\ ((((exists ff_h_bpcce_product_product_terminal. ff_h_bpcce_product_product_terminal + S (z) = S ((S (m)) * ff_v_bpcce_product_product)) /\ exists ff_q_bpcce_product_product_terminal. ff_u_bpcce_product_product = ff_q_bpcce_product_product_terminal * S ((S (m)) * ff_v_bpcce_product_product) + (z))) /\ forall ff_i_bpcce_product_product. (exists ff_lt_bpcce_product_product_bound. ff_lt_bpcce_product_product_bound + S ff_i_bpcce_product_product = m) -> exists ff_p_bpcce_product_product ff_r_bpcce_product_product ff_s_bpcce_product_product. ((((exists ff_h_bpcce_product_product_factor. ff_h_bpcce_product_product_factor + S (ff_p_bpcce_product_product) = S ((S (ff_i_bpcce_product_product)) * bpr_product_scale_bpcce_product)) /\ exists ff_q_bpcce_product_product_factor. bpr_product_code_bpcce_product = ff_q_bpcce_product_product_factor * S ((S (ff_i_bpcce_product_product)) * bpr_product_scale_bpcce_product) + (ff_p_bpcce_product_product))) /\ ((((exists ff_h_bpcce_product_product_partial. ff_h_bpcce_product_product_partial + S (ff_r_bpcce_product_product) = S ((S (ff_i_bpcce_product_product)) * ff_v_bpcce_product_product)) /\ exists ff_q_bpcce_product_product_partial. ff_u_bpcce_product_product = ff_q_bpcce_product_product_partial * S ((S (ff_i_bpcce_product_product)) * ff_v_bpcce_product_product) + (ff_r_bpcce_product_product))) /\ ((((exists ff_h_bpcce_product_product_successor. ff_h_bpcce_product_product_successor + S (ff_s_bpcce_product_product) = S ((S (S ff_i_bpcce_product_product)) * ff_v_bpcce_product_product)) /\ exists ff_q_bpcce_product_product_successor. ff_u_bpcce_product_product = ff_q_bpcce_product_product_successor * S ((S (S ff_i_bpcce_product_product)) * ff_v_bpcce_product_product) + (ff_s_bpcce_product_product))) /\ ff_s_bpcce_product_product = ff_r_bpcce_product_product * ff_p_bpcce_product_product)))))))) /\ n = z

Proof neighborhood

Direct theorem prerequisites

BT00YS prime_contribution_product_exists BT0105 prime_contribution_product_eq

Direct theorem dependents

BT0107 central_binom_prime_contribution_product_exists

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

21 script commands · 7 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
prime contribution product existsprime contribution product eq
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 hn
  4. L4
    intro hsupport
02Establish hproductL5–8

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

  1. L5
    have hproduct : ∃ 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)Definitions: Lt(k,m)BetaAt(x,y,k,i)Prime(S k)PowerValuation(S k,n,j)Pow(S k,j,i)Product(x,y,m,z)Original native command in the exact edition
  2. L6
    specialize prime_contribution_product_exists n
  3. L7
    specialize prime_contribution_product_exists m
  4. L8
    exact prime_contribution_product_exists
03Separate the logical casesL9–9

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

  1. L9
    cases hproduct
04Establish heqL10–17

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

  1. L10
    have heq : n = x
  2. L11
    specialize prime_contribution_product_eq n
  3. L12
    specialize prime_contribution_product_eq m
  4. L13
    specialize prime_contribution_product_eq x
  5. L14
    apply prime_contribution_product_eq
  6. L15
    exact hn
  7. L16
    exact hsupport
  8. L17
    exact hproduct_witness
05Construct an explicit witnessL18–18

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

  1. L18
    exists x
06Separate the logical casesL19–19

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

  1. L19
    split
07Use earlier factsL20–21

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

  1. L20
    exact hproduct_witness
  2. L21
    exact heq

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro n
  2. 0002intro m
  3. 0003intro hn
  4. 0004intro hsupport
  5. 0005have hproduct : ∃ 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)
    Exact native replay linehave hproduct : exists z. (exists bpr_product_code_bpcce_product bpr_product_scale_bpcce_product. ((forall bpr_prefix_index_bpcce_product_prefix. (exists bpr_gap_bpcce_product_prefix_bound. bpr_gap_bpcce_product_prefix_bound + S (bpr_prefix_index_bpcce_product_prefix) = m) -> exists bpr_prefix_value_bpcce_product_prefix. ((((exists bpr_height_bpcce_product_prefix_decoded. bpr_height_bpcce_product_prefix_decoded + S (bpr_prefix_value_bpcce_product_prefix) = S ((S (bpr_prefix_index_bpcce_product_prefix)) * bpr_product_scale_bpcce_product)) /\ exists bpr_quotient_bpcce_product_prefix_decoded. bpr_product_code_bpcce_product = bpr_quotient_bpcce_product_prefix_decoded * S ((S (bpr_prefix_index_bpcce_product_prefix)) * bpr_product_scale_bpcce_product) + (bpr_prefix_value_bpcce_product_prefix))) /\ (((((~(S (bpr_prefix_index_bpcce_product_prefix) = 1) /\ forall bpr_left_bpcce_product_prefix_choice_prime bpr_right_bpcce_product_prefix_choice_prime. S (bpr_prefix_index_bpcce_product_prefix) = bpr_left_bpcce_product_prefix_choice_prime * bpr_right_bpcce_product_prefix_choice_prime -> bpr_left_bpcce_product_prefix_choice_prime = 1 \/ bpr_right_bpcce_product_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcce_product_prefix_choice. ((((exists bpr_le_gap_bpcce_product_prefix_choice_valuation_selected_bound. bpr_le_gap_bpcce_product_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpcce_product_prefix_choice) = (n)) /\ (exists bpr_power_value_bpcce_product_prefix_choice_valuation_selected. ((exists bpr_power_code_bpcce_product_prefix_choice_valuation_selected_power bpr_power_scale_bpcce_product_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpcce_product_prefix_choice_valuation_selected_power. (exists bpr_gap_bpcce_product_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcce_product_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcce_product_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpcce_product_prefix_choice) -> (((exists bpr_height_bpcce_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpcce_product_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcce_product_prefix)) = S ((S (bpr_power_index_bpcce_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcce_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcce_product_prefix_choice_valuation_selected_power = bpr_quotient_bpcce_product_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcce_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcce_product_prefix))))) /\ (exists ff_u_bpcce_product_prefix_choice_valuation_selected_power_product ff_v_bpcce_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_start. ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_start. ff_u_bpcce_product_prefix_choice_valuation_selected_power_product = ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcce_product_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcce_product_prefix_choice)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpcce_product_prefix_choice_valuation_selected_power_product = ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcce_product_prefix_choice)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpcce_product_prefix_choice_valuation_selected))) /\ forall ff_i_bpcce_product_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpcce_product_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpcce_product_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpcce_product_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpcce_product_prefix_choice) -> exists ff_p_bpcce_product_prefix_choice_valuation_selected_power_product ff_r_bpcce_product_prefix_choice_valuation_selected_power_product ff_s_bpcce_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_factor. ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpcce_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpcce_product_prefix_choice_valuation_selected_power = ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_selected_power) + (ff_p_bpcce_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_partial. ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpcce_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_partial. ff_u_bpcce_product_prefix_choice_valuation_selected_power_product = ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product) + (ff_r_bpcce_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_successor. ff_h_bpcce_product_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpcce_product_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_successor. ff_u_bpcce_product_prefix_choice_valuation_selected_power_product = ff_q_bpcce_product_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcce_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_selected_power_product) + (ff_s_bpcce_product_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpcce_product_prefix_choice_valuation_selected_power_product = ff_r_bpcce_product_prefix_choice_valuation_selected_power_product * ff_p_bpcce_product_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcce_product_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpcce_product_prefix_choice_valuation_selected) * bpr_divides_quotient_bpcce_product_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcce_product_prefix_choice_valuation. (exists bpr_le_gap_bpcce_product_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpcce_product_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcce_product_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpcce_product_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpcce_product_prefix_choice_valuation_candidate_power bpr_power_scale_bpcce_product_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpcce_product_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpcce_product_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcce_product_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcce_product_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcce_product_prefix_choice_valuation) -> (((exists bpr_height_bpcce_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcce_product_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcce_product_prefix)) = S ((S (bpr_power_index_bpcce_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcce_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcce_product_prefix_choice_valuation_candidate_power = bpr_quotient_bpcce_product_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcce_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcce_product_prefix))))) /\ (exists ff_u_bpcce_product_prefix_choice_valuation_candidate_power_product ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_start. ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_start. ff_u_bpcce_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcce_product_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcce_product_prefix_choice_valuation)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpcce_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcce_product_prefix_choice_valuation)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpcce_product_prefix_choice_valuation_candidate))) /\ forall ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpcce_product_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpcce_product_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcce_product_prefix_choice_valuation) -> exists ff_p_bpcce_product_prefix_choice_valuation_candidate_power_product ff_r_bpcce_product_prefix_choice_valuation_candidate_power_product ff_s_bpcce_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpcce_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcce_product_prefix_choice_valuation_candidate_power = ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_valuation_candidate_power) + (ff_p_bpcce_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpcce_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpcce_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product) + (ff_r_bpcce_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpcce_product_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpcce_product_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpcce_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcce_product_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcce_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcce_product_prefix_choice_valuation_candidate_power_product) + (ff_s_bpcce_product_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpcce_product_prefix_choice_valuation_candidate_power_product = ff_r_bpcce_product_prefix_choice_valuation_candidate_power_product * ff_p_bpcce_product_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcce_product_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpcce_product_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpcce_product_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcce_product_prefix_choice_valuation_candidate_below. bpr_le_gap_bpcce_product_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcce_product_prefix_choice_valuation) = (bpr_choice_exponent_bpcce_product_prefix_choice))) /\ (exists bpr_power_code_bpcce_product_prefix_choice_power bpr_power_scale_bpcce_product_prefix_choice_power. ((forall bpr_power_index_bpcce_product_prefix_choice_power. (exists bpr_gap_bpcce_product_prefix_choice_power_repeat_bound. bpr_gap_bpcce_product_prefix_choice_power_repeat_bound + S (bpr_power_index_bpcce_product_prefix_choice_power) = bpr_choice_exponent_bpcce_product_prefix_choice) -> (((exists bpr_height_bpcce_product_prefix_choice_power_repeat_entry. bpr_height_bpcce_product_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcce_product_prefix)) = S ((S (bpr_power_index_bpcce_product_prefix_choice_power)) * bpr_power_scale_bpcce_product_prefix_choice_power)) /\ exists bpr_quotient_bpcce_product_prefix_choice_power_repeat_entry. bpr_power_code_bpcce_product_prefix_choice_power = bpr_quotient_bpcce_product_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpcce_product_prefix_choice_power)) * bpr_power_scale_bpcce_product_prefix_choice_power) + (S (bpr_prefix_index_bpcce_product_prefix))))) /\ (exists ff_u_bpcce_product_prefix_choice_power_product ff_v_bpcce_product_prefix_choice_power_product. ((((exists ff_h_bpcce_product_prefix_choice_power_product_start. ff_h_bpcce_product_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcce_product_prefix_choice_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_power_product_start. ff_u_bpcce_product_prefix_choice_power_product = ff_q_bpcce_product_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpcce_product_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpcce_product_prefix_choice_power_product_terminal. ff_h_bpcce_product_prefix_choice_power_product_terminal + S (bpr_prefix_value_bpcce_product_prefix) = S ((S (bpr_choice_exponent_bpcce_product_prefix_choice)) * ff_v_bpcce_product_prefix_choice_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_power_product_terminal. ff_u_bpcce_product_prefix_choice_power_product = ff_q_bpcce_product_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcce_product_prefix_choice)) * ff_v_bpcce_product_prefix_choice_power_product) + (bpr_prefix_value_bpcce_product_prefix))) /\ forall ff_i_bpcce_product_prefix_choice_power_product. (exists ff_lt_bpcce_product_prefix_choice_power_product_bound. ff_lt_bpcce_product_prefix_choice_power_product_bound + S ff_i_bpcce_product_prefix_choice_power_product = bpr_choice_exponent_bpcce_product_prefix_choice) -> exists ff_p_bpcce_product_prefix_choice_power_product ff_r_bpcce_product_prefix_choice_power_product ff_s_bpcce_product_prefix_choice_power_product. ((((exists ff_h_bpcce_product_prefix_choice_power_product_factor. ff_h_bpcce_product_prefix_choice_power_product_factor + S (ff_p_bpcce_product_prefix_choice_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_power)) /\ exists ff_q_bpcce_product_prefix_choice_power_product_factor. bpr_power_code_bpcce_product_prefix_choice_power = ff_q_bpcce_product_prefix_choice_power_product_factor * S ((S (ff_i_bpcce_product_prefix_choice_power_product)) * bpr_power_scale_bpcce_product_prefix_choice_power) + (ff_p_bpcce_product_prefix_choice_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_power_product_partial. ff_h_bpcce_product_prefix_choice_power_product_partial + S (ff_r_bpcce_product_prefix_choice_power_product) = S ((S (ff_i_bpcce_product_prefix_choice_power_product)) * ff_v_bpcce_product_prefix_choice_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_power_product_partial. ff_u_bpcce_product_prefix_choice_power_product = ff_q_bpcce_product_prefix_choice_power_product_partial * S ((S (ff_i_bpcce_product_prefix_choice_power_product)) * ff_v_bpcce_product_prefix_choice_power_product) + (ff_r_bpcce_product_prefix_choice_power_product))) /\ ((((exists ff_h_bpcce_product_prefix_choice_power_product_successor. ff_h_bpcce_product_prefix_choice_power_product_successor + S (ff_s_bpcce_product_prefix_choice_power_product) = S ((S (S ff_i_bpcce_product_prefix_choice_power_product)) * ff_v_bpcce_product_prefix_choice_power_product)) /\ exists ff_q_bpcce_product_prefix_choice_power_product_successor. ff_u_bpcce_product_prefix_choice_power_product = ff_q_bpcce_product_prefix_choice_power_product_successor * S ((S (S ff_i_bpcce_product_prefix_choice_power_product)) * ff_v_bpcce_product_prefix_choice_power_product) + (ff_s_bpcce_product_prefix_choice_power_product))) /\ ff_s_bpcce_product_prefix_choice_power_product = ff_r_bpcce_product_prefix_choice_power_product * ff_p_bpcce_product_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcce_product_prefix) = 1) /\ forall bpr_left_bpcce_product_prefix_choice_prime bpr_right_bpcce_product_prefix_choice_prime. S (bpr_prefix_index_bpcce_product_prefix) = bpr_left_bpcce_product_prefix_choice_prime * bpr_right_bpcce_product_prefix_choice_prime -> bpr_left_bpcce_product_prefix_choice_prime = 1 \/ bpr_right_bpcce_product_prefix_choice_prime = 1)) /\ bpr_prefix_value_bpcce_product_prefix = 1))))) /\ (exists ff_u_bpcce_product_product ff_v_bpcce_product_product. ((((exists ff_h_bpcce_product_product_start. ff_h_bpcce_product_product_start + S (1) = S ((S (0)) * ff_v_bpcce_product_product)) /\ exists ff_q_bpcce_product_product_start. ff_u_bpcce_product_product = ff_q_bpcce_product_product_start * S ((S (0)) * ff_v_bpcce_product_product) + (1))) /\ ((((exists ff_h_bpcce_product_product_terminal. ff_h_bpcce_product_product_terminal + S (z) = S ((S (m)) * ff_v_bpcce_product_product)) /\ exists ff_q_bpcce_product_product_terminal. ff_u_bpcce_product_product = ff_q_bpcce_product_product_terminal * S ((S (m)) * ff_v_bpcce_product_product) + (z))) /\ forall ff_i_bpcce_product_product. (exists ff_lt_bpcce_product_product_bound. ff_lt_bpcce_product_product_bound + S ff_i_bpcce_product_product = m) -> exists ff_p_bpcce_product_product ff_r_bpcce_product_product ff_s_bpcce_product_product. ((((exists ff_h_bpcce_product_product_factor. ff_h_bpcce_product_product_factor + S (ff_p_bpcce_product_product) = S ((S (ff_i_bpcce_product_product)) * bpr_product_scale_bpcce_product)) /\ exists ff_q_bpcce_product_product_factor. bpr_product_code_bpcce_product = ff_q_bpcce_product_product_factor * S ((S (ff_i_bpcce_product_product)) * bpr_product_scale_bpcce_product) + (ff_p_bpcce_product_product))) /\ ((((exists ff_h_bpcce_product_product_partial. ff_h_bpcce_product_product_partial + S (ff_r_bpcce_product_product) = S ((S (ff_i_bpcce_product_product)) * ff_v_bpcce_product_product)) /\ exists ff_q_bpcce_product_product_partial. ff_u_bpcce_product_product = ff_q_bpcce_product_product_partial * S ((S (ff_i_bpcce_product_product)) * ff_v_bpcce_product_product) + (ff_r_bpcce_product_product))) /\ ((((exists ff_h_bpcce_product_product_successor. ff_h_bpcce_product_product_successor + S (ff_s_bpcce_product_product) = S ((S (S ff_i_bpcce_product_product)) * ff_v_bpcce_product_product)) /\ exists ff_q_bpcce_product_product_successor. ff_u_bpcce_product_product = ff_q_bpcce_product_product_successor * S ((S (S ff_i_bpcce_product_product)) * ff_v_bpcce_product_product) + (ff_s_bpcce_product_product))) /\ ff_s_bpcce_product_product = ff_r_bpcce_product_product * ff_p_bpcce_product_product))))))))
  6. 0006specialize prime_contribution_product_exists n
  7. 0007specialize prime_contribution_product_exists m
  8. 0008exact prime_contribution_product_exists
  9. 0009cases hproduct
  10. 0010have heq : n = x
  11. 0011specialize prime_contribution_product_eq n
  12. 0012specialize prime_contribution_product_eq m
  13. 0013specialize prime_contribution_product_eq x
  14. 0014apply prime_contribution_product_eq
  15. 0015exact hn
  16. 0016exact hsupport
  17. 0017exact hproduct_witness
  18. 0018exists x
  19. 0019split
  20. 0020exact hproduct_witness
  21. 0021exact heq