BT0102

prime_contribution_cofactor_prime_contradiction

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

A prime divisor of the remaining cofactor contradicts maximality.

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.

Exact expanded PA statement

forall n m z q p. ~(n = 0) -> (forall bpr_support_prime_bpccpc_support. ((~(bpr_support_prime_bpccpc_support = 1) /\ forall bpr_left_bpccpc_support_prime bpr_right_bpccpc_support_prime. bpr_support_prime_bpccpc_support = bpr_left_bpccpc_support_prime * bpr_right_bpccpc_support_prime -> bpr_left_bpccpc_support_prime = 1 \/ bpr_right_bpccpc_support_prime = 1)) -> (exists bpr_divides_quotient_bpccpc_support_divides. n = (bpr_support_prime_bpccpc_support) * bpr_divides_quotient_bpccpc_support_divides) -> (exists bpr_le_gap_bpccpc_support_bound. bpr_le_gap_bpccpc_support_bound + (bpr_support_prime_bpccpc_support) = (m))) -> (exists bpr_product_code_bpccpc_product bpr_product_scale_bpccpc_product. ((forall bpr_prefix_index_bpccpc_product_prefix. (exists bpr_gap_bpccpc_product_prefix_bound. bpr_gap_bpccpc_product_prefix_bound + S (bpr_prefix_index_bpccpc_product_prefix) = m) -> exists bpr_prefix_value_bpccpc_product_prefix. ((((exists bpr_height_bpccpc_product_prefix_decoded. bpr_height_bpccpc_product_prefix_decoded + S (bpr_prefix_value_bpccpc_product_prefix) = S ((S (bpr_prefix_index_bpccpc_product_prefix)) * bpr_product_scale_bpccpc_product)) /\ exists bpr_quotient_bpccpc_product_prefix_decoded. bpr_product_code_bpccpc_product = bpr_quotient_bpccpc_product_prefix_decoded * S ((S (bpr_prefix_index_bpccpc_product_prefix)) * bpr_product_scale_bpccpc_product) + (bpr_prefix_value_bpccpc_product_prefix))) /\ (((((~(S (bpr_prefix_index_bpccpc_product_prefix) = 1) /\ forall bpr_left_bpccpc_product_prefix_choice_prime bpr_right_bpccpc_product_prefix_choice_prime. S (bpr_prefix_index_bpccpc_product_prefix) = bpr_left_bpccpc_product_prefix_choice_prime * bpr_right_bpccpc_product_prefix_choice_prime -> bpr_left_bpccpc_product_prefix_choice_prime = 1 \/ bpr_right_bpccpc_product_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpccpc_product_prefix_choice. ((((exists bpr_le_gap_bpccpc_product_prefix_choice_valuation_selected_bound. bpr_le_gap_bpccpc_product_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpccpc_product_prefix_choice) = (n)) /\ (exists bpr_power_value_bpccpc_product_prefix_choice_valuation_selected. ((exists bpr_power_code_bpccpc_product_prefix_choice_valuation_selected_power bpr_power_scale_bpccpc_product_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpccpc_product_prefix_choice_valuation_selected_power. (exists bpr_gap_bpccpc_product_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpccpc_product_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpccpc_product_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpccpc_product_prefix_choice) -> (((exists bpr_height_bpccpc_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpccpc_product_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpccpc_product_prefix)) = S ((S (bpr_power_index_bpccpc_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpccpc_product_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpccpc_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpccpc_product_prefix_choice_valuation_selected_power = bpr_quotient_bpccpc_product_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpccpc_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpccpc_product_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_bpccpc_product_prefix))))) /\ (exists ff_u_bpccpc_product_prefix_choice_valuation_selected_power_product ff_v_bpccpc_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpccpc_product_prefix_choice_valuation_selected_power_product_start. ff_h_bpccpc_product_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpccpc_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_valuation_selected_power_product_start. ff_u_bpccpc_product_prefix_choice_valuation_selected_power_product = ff_q_bpccpc_product_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpccpc_product_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpccpc_product_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpccpc_product_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpccpc_product_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpccpc_product_prefix_choice)) * ff_v_bpccpc_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpccpc_product_prefix_choice_valuation_selected_power_product = ff_q_bpccpc_product_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpccpc_product_prefix_choice)) * ff_v_bpccpc_product_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpccpc_product_prefix_choice_valuation_selected))) /\ forall ff_i_bpccpc_product_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpccpc_product_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpccpc_product_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpccpc_product_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpccpc_product_prefix_choice) -> exists ff_p_bpccpc_product_prefix_choice_valuation_selected_power_product ff_r_bpccpc_product_prefix_choice_valuation_selected_power_product ff_s_bpccpc_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpccpc_product_prefix_choice_valuation_selected_power_product_factor. ff_h_bpccpc_product_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpccpc_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpccpc_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpccpc_product_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpccpc_product_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpccpc_product_prefix_choice_valuation_selected_power = ff_q_bpccpc_product_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpccpc_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpccpc_product_prefix_choice_valuation_selected_power) + (ff_p_bpccpc_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpccpc_product_prefix_choice_valuation_selected_power_product_partial. ff_h_bpccpc_product_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpccpc_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpccpc_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpccpc_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_valuation_selected_power_product_partial. ff_u_bpccpc_product_prefix_choice_valuation_selected_power_product = ff_q_bpccpc_product_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpccpc_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpccpc_product_prefix_choice_valuation_selected_power_product) + (ff_r_bpccpc_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpccpc_product_prefix_choice_valuation_selected_power_product_successor. ff_h_bpccpc_product_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpccpc_product_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpccpc_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpccpc_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_valuation_selected_power_product_successor. ff_u_bpccpc_product_prefix_choice_valuation_selected_power_product = ff_q_bpccpc_product_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpccpc_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpccpc_product_prefix_choice_valuation_selected_power_product) + (ff_s_bpccpc_product_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpccpc_product_prefix_choice_valuation_selected_power_product = ff_r_bpccpc_product_prefix_choice_valuation_selected_power_product * ff_p_bpccpc_product_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpccpc_product_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpccpc_product_prefix_choice_valuation_selected) * bpr_divides_quotient_bpccpc_product_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpccpc_product_prefix_choice_valuation. (exists bpr_le_gap_bpccpc_product_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpccpc_product_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpccpc_product_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpccpc_product_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpccpc_product_prefix_choice_valuation_candidate_power bpr_power_scale_bpccpc_product_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpccpc_product_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpccpc_product_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpccpc_product_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpccpc_product_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpccpc_product_prefix_choice_valuation) -> (((exists bpr_height_bpccpc_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpccpc_product_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpccpc_product_prefix)) = S ((S (bpr_power_index_bpccpc_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpccpc_product_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpccpc_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpccpc_product_prefix_choice_valuation_candidate_power = bpr_quotient_bpccpc_product_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpccpc_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpccpc_product_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpccpc_product_prefix))))) /\ (exists ff_u_bpccpc_product_prefix_choice_valuation_candidate_power_product ff_v_bpccpc_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpccpc_product_prefix_choice_valuation_candidate_power_product_start. ff_h_bpccpc_product_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpccpc_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_valuation_candidate_power_product_start. ff_u_bpccpc_product_prefix_choice_valuation_candidate_power_product = ff_q_bpccpc_product_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpccpc_product_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpccpc_product_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpccpc_product_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpccpc_product_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpccpc_product_prefix_choice_valuation)) * ff_v_bpccpc_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpccpc_product_prefix_choice_valuation_candidate_power_product = ff_q_bpccpc_product_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpccpc_product_prefix_choice_valuation)) * ff_v_bpccpc_product_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpccpc_product_prefix_choice_valuation_candidate))) /\ forall ff_i_bpccpc_product_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpccpc_product_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpccpc_product_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpccpc_product_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpccpc_product_prefix_choice_valuation) -> exists ff_p_bpccpc_product_prefix_choice_valuation_candidate_power_product ff_r_bpccpc_product_prefix_choice_valuation_candidate_power_product ff_s_bpccpc_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpccpc_product_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpccpc_product_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpccpc_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpccpc_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpccpc_product_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpccpc_product_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpccpc_product_prefix_choice_valuation_candidate_power = ff_q_bpccpc_product_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpccpc_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpccpc_product_prefix_choice_valuation_candidate_power) + (ff_p_bpccpc_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpccpc_product_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpccpc_product_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpccpc_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpccpc_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpccpc_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpccpc_product_prefix_choice_valuation_candidate_power_product = ff_q_bpccpc_product_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpccpc_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpccpc_product_prefix_choice_valuation_candidate_power_product) + (ff_r_bpccpc_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpccpc_product_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpccpc_product_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpccpc_product_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpccpc_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpccpc_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpccpc_product_prefix_choice_valuation_candidate_power_product = ff_q_bpccpc_product_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpccpc_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpccpc_product_prefix_choice_valuation_candidate_power_product) + (ff_s_bpccpc_product_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpccpc_product_prefix_choice_valuation_candidate_power_product = ff_r_bpccpc_product_prefix_choice_valuation_candidate_power_product * ff_p_bpccpc_product_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpccpc_product_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpccpc_product_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpccpc_product_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpccpc_product_prefix_choice_valuation_candidate_below. bpr_le_gap_bpccpc_product_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpccpc_product_prefix_choice_valuation) = (bpr_choice_exponent_bpccpc_product_prefix_choice))) /\ (exists bpr_power_code_bpccpc_product_prefix_choice_power bpr_power_scale_bpccpc_product_prefix_choice_power. ((forall bpr_power_index_bpccpc_product_prefix_choice_power. (exists bpr_gap_bpccpc_product_prefix_choice_power_repeat_bound. bpr_gap_bpccpc_product_prefix_choice_power_repeat_bound + S (bpr_power_index_bpccpc_product_prefix_choice_power) = bpr_choice_exponent_bpccpc_product_prefix_choice) -> (((exists bpr_height_bpccpc_product_prefix_choice_power_repeat_entry. bpr_height_bpccpc_product_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_bpccpc_product_prefix)) = S ((S (bpr_power_index_bpccpc_product_prefix_choice_power)) * bpr_power_scale_bpccpc_product_prefix_choice_power)) /\ exists bpr_quotient_bpccpc_product_prefix_choice_power_repeat_entry. bpr_power_code_bpccpc_product_prefix_choice_power = bpr_quotient_bpccpc_product_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpccpc_product_prefix_choice_power)) * bpr_power_scale_bpccpc_product_prefix_choice_power) + (S (bpr_prefix_index_bpccpc_product_prefix))))) /\ (exists ff_u_bpccpc_product_prefix_choice_power_product ff_v_bpccpc_product_prefix_choice_power_product. ((((exists ff_h_bpccpc_product_prefix_choice_power_product_start. ff_h_bpccpc_product_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpccpc_product_prefix_choice_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_power_product_start. ff_u_bpccpc_product_prefix_choice_power_product = ff_q_bpccpc_product_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpccpc_product_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpccpc_product_prefix_choice_power_product_terminal. ff_h_bpccpc_product_prefix_choice_power_product_terminal + S (bpr_prefix_value_bpccpc_product_prefix) = S ((S (bpr_choice_exponent_bpccpc_product_prefix_choice)) * ff_v_bpccpc_product_prefix_choice_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_power_product_terminal. ff_u_bpccpc_product_prefix_choice_power_product = ff_q_bpccpc_product_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpccpc_product_prefix_choice)) * ff_v_bpccpc_product_prefix_choice_power_product) + (bpr_prefix_value_bpccpc_product_prefix))) /\ forall ff_i_bpccpc_product_prefix_choice_power_product. (exists ff_lt_bpccpc_product_prefix_choice_power_product_bound. ff_lt_bpccpc_product_prefix_choice_power_product_bound + S ff_i_bpccpc_product_prefix_choice_power_product = bpr_choice_exponent_bpccpc_product_prefix_choice) -> exists ff_p_bpccpc_product_prefix_choice_power_product ff_r_bpccpc_product_prefix_choice_power_product ff_s_bpccpc_product_prefix_choice_power_product. ((((exists ff_h_bpccpc_product_prefix_choice_power_product_factor. ff_h_bpccpc_product_prefix_choice_power_product_factor + S (ff_p_bpccpc_product_prefix_choice_power_product) = S ((S (ff_i_bpccpc_product_prefix_choice_power_product)) * bpr_power_scale_bpccpc_product_prefix_choice_power)) /\ exists ff_q_bpccpc_product_prefix_choice_power_product_factor. bpr_power_code_bpccpc_product_prefix_choice_power = ff_q_bpccpc_product_prefix_choice_power_product_factor * S ((S (ff_i_bpccpc_product_prefix_choice_power_product)) * bpr_power_scale_bpccpc_product_prefix_choice_power) + (ff_p_bpccpc_product_prefix_choice_power_product))) /\ ((((exists ff_h_bpccpc_product_prefix_choice_power_product_partial. ff_h_bpccpc_product_prefix_choice_power_product_partial + S (ff_r_bpccpc_product_prefix_choice_power_product) = S ((S (ff_i_bpccpc_product_prefix_choice_power_product)) * ff_v_bpccpc_product_prefix_choice_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_power_product_partial. ff_u_bpccpc_product_prefix_choice_power_product = ff_q_bpccpc_product_prefix_choice_power_product_partial * S ((S (ff_i_bpccpc_product_prefix_choice_power_product)) * ff_v_bpccpc_product_prefix_choice_power_product) + (ff_r_bpccpc_product_prefix_choice_power_product))) /\ ((((exists ff_h_bpccpc_product_prefix_choice_power_product_successor. ff_h_bpccpc_product_prefix_choice_power_product_successor + S (ff_s_bpccpc_product_prefix_choice_power_product) = S ((S (S ff_i_bpccpc_product_prefix_choice_power_product)) * ff_v_bpccpc_product_prefix_choice_power_product)) /\ exists ff_q_bpccpc_product_prefix_choice_power_product_successor. ff_u_bpccpc_product_prefix_choice_power_product = ff_q_bpccpc_product_prefix_choice_power_product_successor * S ((S (S ff_i_bpccpc_product_prefix_choice_power_product)) * ff_v_bpccpc_product_prefix_choice_power_product) + (ff_s_bpccpc_product_prefix_choice_power_product))) /\ ff_s_bpccpc_product_prefix_choice_power_product = ff_r_bpccpc_product_prefix_choice_power_product * ff_p_bpccpc_product_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpccpc_product_prefix) = 1) /\ forall bpr_left_bpccpc_product_prefix_choice_prime bpr_right_bpccpc_product_prefix_choice_prime. S (bpr_prefix_index_bpccpc_product_prefix) = bpr_left_bpccpc_product_prefix_choice_prime * bpr_right_bpccpc_product_prefix_choice_prime -> bpr_left_bpccpc_product_prefix_choice_prime = 1 \/ bpr_right_bpccpc_product_prefix_choice_prime = 1)) /\ bpr_prefix_value_bpccpc_product_prefix = 1))))) /\ (exists ff_u_bpccpc_product_product ff_v_bpccpc_product_product. ((((exists ff_h_bpccpc_product_product_start. ff_h_bpccpc_product_product_start + S (1) = S ((S (0)) * ff_v_bpccpc_product_product)) /\ exists ff_q_bpccpc_product_product_start. ff_u_bpccpc_product_product = ff_q_bpccpc_product_product_start * S ((S (0)) * ff_v_bpccpc_product_product) + (1))) /\ ((((exists ff_h_bpccpc_product_product_terminal. ff_h_bpccpc_product_product_terminal + S (z) = S ((S (m)) * ff_v_bpccpc_product_product)) /\ exists ff_q_bpccpc_product_product_terminal. ff_u_bpccpc_product_product = ff_q_bpccpc_product_product_terminal * S ((S (m)) * ff_v_bpccpc_product_product) + (z))) /\ forall ff_i_bpccpc_product_product. (exists ff_lt_bpccpc_product_product_bound. ff_lt_bpccpc_product_product_bound + S ff_i_bpccpc_product_product = m) -> exists ff_p_bpccpc_product_product ff_r_bpccpc_product_product ff_s_bpccpc_product_product. ((((exists ff_h_bpccpc_product_product_factor. ff_h_bpccpc_product_product_factor + S (ff_p_bpccpc_product_product) = S ((S (ff_i_bpccpc_product_product)) * bpr_product_scale_bpccpc_product)) /\ exists ff_q_bpccpc_product_product_factor. bpr_product_code_bpccpc_product = ff_q_bpccpc_product_product_factor * S ((S (ff_i_bpccpc_product_product)) * bpr_product_scale_bpccpc_product) + (ff_p_bpccpc_product_product))) /\ ((((exists ff_h_bpccpc_product_product_partial. ff_h_bpccpc_product_product_partial + S (ff_r_bpccpc_product_product) = S ((S (ff_i_bpccpc_product_product)) * ff_v_bpccpc_product_product)) /\ exists ff_q_bpccpc_product_product_partial. ff_u_bpccpc_product_product = ff_q_bpccpc_product_product_partial * S ((S (ff_i_bpccpc_product_product)) * ff_v_bpccpc_product_product) + (ff_r_bpccpc_product_product))) /\ ((((exists ff_h_bpccpc_product_product_successor. ff_h_bpccpc_product_product_successor + S (ff_s_bpccpc_product_product) = S ((S (S ff_i_bpccpc_product_product)) * ff_v_bpccpc_product_product)) /\ exists ff_q_bpccpc_product_product_successor. ff_u_bpccpc_product_product = ff_q_bpccpc_product_product_successor * S ((S (S ff_i_bpccpc_product_product)) * ff_v_bpccpc_product_product) + (ff_s_bpccpc_product_product))) /\ ff_s_bpccpc_product_product = ff_r_bpccpc_product_product * ff_p_bpccpc_product_product)))))))) -> n = z * q -> ((~(p = 1) /\ forall bpr_left_bpccpc_prime bpr_right_bpccpc_prime. p = bpr_left_bpccpc_prime * bpr_right_bpccpc_prime -> bpr_left_bpccpc_prime = 1 \/ bpr_right_bpccpc_prime = 1)) -> (exists bpr_divides_quotient_bpccpc_divides. q = (p) * bpr_divides_quotient_bpccpc_divides) -> false

Structural proof guide

A prime divisor of the remaining cofactor contradicts maximality.

Direct prerequisites: prime_is_succ_succ, multiple_mul_left, prime_contribution_selected_entry, prime_contribution_selected_successor_divides, power_valuation_successor_not_divides. The authored body proceeds by case analysis (6), intermediate claims (6), equality transport (4).

Proof neighborhood

Direct dependencies

BT00AW prime_is_succ_succ BT002B multiple_mul_left BT0100 prime_contribution_selected_entry BT0101 prime_contribution_selected_successor_divides BT00QH power_valuation_successor_not_divides

Direct dependents

BT0103 prime_contribution_cofactor_eq_one

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

70 script commands · 16 reading checkpoints · 6 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.

Named ingredients (5)
prime is succ succmultiple mul leftprime contribution selected entryprime contribution selected successor dividespower valuation successor not divides

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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 q
  5. L5
    intro p
  6. L6
    intro hn
  7. L7
    intro hsupport
  8. L8
    intro hproduct
  9. L9
    intro hfactor
  10. L10
    intro hp
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hprime
03Establish hscaledL12–17

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

  1. L12
    have hscaled : exists bpr_divides_quotient_bpccpc_scaled. z * q = (p) * bpr_divides_quotient_bpccpc_scaled
  2. L13
    specialize multiple_mul_left p
  3. L14
    specialize multiple_mul_left q
  4. L15
    specialize multiple_mul_left z
  5. L16
    apply multiple_mul_left
  6. L17
    exact hprime
04Establish hsourceL18–18

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

  1. L18
    have hsource : exists bpr_divides_quotient_bpccpc_source_divides. n = (p) * bpr_divides_quotient_bpccpc_source_divides
05Separate the logical casesL19–19

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

  1. L19
    cases hscaled
06Construct an explicit witnessL20–20

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

  1. L20
    exists x
07Calculate and transport equalitiesL21–21

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

  1. L21
    trans z * q
08Use earlier factsL22–23

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

  1. L22
    exact hfactor
  2. L23
    exact hscaled_witness
09Establish hboundL24–28

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

  1. L24
    have hbound : exists bpr_le_gap_bpccpc_bound. bpr_le_gap_bpccpc_bound + (p) = (m)
  2. L25
    specialize hsupport p
  3. L26
    apply hsupport
  4. L27
    exact hp
  5. L28
    exact hsource
10Establish hshapeL29–32

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

  1. L29
    have hshape : exists k. p = S (S k)
  2. L30
    specialize prime_is_succ_succ p
  3. L31
    apply prime_is_succ_succ
  4. L32
    exact hp
11Separate the logical casesL33–33

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

  1. L33
    cases hshape
12Calculate and transport equalitiesL34–37

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

  1. L34
    rewrite hshape_witness at hp
  2. L35
    rewrite hshape_witness at hp
  3. L36
    rewrite hshape_witness at hbound
  4. L37
    rewrite hshape_witness at hprime
13Establish hselectedL38–46

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

  1. L38
    have hselected : ∃ e. ∃ a. BoundedPowerValuation(S S x,n,n,e) ∧ (Pow(S S x,e,a) ∧ Dvd(a,z))Definitions: DvdPowBoundedPowerValuation
  2. L39
    specialize prime_contribution_selected_entry n
  3. L40
    specialize prime_contribution_selected_entry m
  4. L41
    specialize prime_contribution_selected_entry z
  5. L42
    specialize prime_contribution_selected_entry (S x)
  6. L43
    apply prime_contribution_selected_entry
  7. L44
    exact hp
  8. L45
    exact hbound
  9. L46
    exact hproduct
14Separate the logical casesL47–50

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

  1. L47
    cases hselected
  2. L48
    cases hselected_witness
  3. L49
    cases hselected_witness_witness
  4. L50
    cases hselected_witness_witness_right
15Establish hsuccessorL51–60

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

  1. L51
    have hsuccessor : PowerDivides(S S x,S x1,n)Definitions: PowerDivides
  2. L52
    specialize prime_contribution_selected_successor_divides (S (S x))
  3. L53
    specialize prime_contribution_selected_successor_divides x1
  4. L54
    specialize prime_contribution_selected_successor_divides x2
  5. L55
    specialize prime_contribution_selected_successor_divides z
  6. L56
    specialize prime_contribution_selected_successor_divides q
  7. L57
    specialize prime_contribution_selected_successor_divides n
  8. L58
    apply prime_contribution_selected_successor_divides
  9. L59
    exact hselected_witness_witness_right_left
  10. L60
    exact hselected_witness_witness_right_right
16Use earlier factsL61–70

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

  1. L61
    exact hprime
  2. L62
    exact hfactor
  3. L63
    specialize power_valuation_successor_not_divides (S (S x))
  4. L64
    specialize power_valuation_successor_not_divides n
  5. L65
    specialize power_valuation_successor_not_divides x1
  6. L66
    apply power_valuation_successor_not_divides
  7. L67
    exact hp
  8. L68
    exact hn
  9. L69
    exact hselected_witness_witness_left
  10. L70
    exact hsuccessor

Library-wide reading audit

Original exact command ledger · 70 lines
  1. 0001intro n
  2. 0002intro m
  3. 0003intro z
  4. 0004intro q
  5. 0005intro p
  6. 0006intro hn
  7. 0007intro hsupport
  8. 0008intro hproduct
  9. 0009intro hfactor
  10. 0010intro hp
  11. 0011intro hprime
  12. 0012have hscaled : exists bpr_divides_quotient_bpccpc_scaled. z * q = (p) * bpr_divides_quotient_bpccpc_scaled
  13. 0013specialize multiple_mul_left p
  14. 0014specialize multiple_mul_left q
  15. 0015specialize multiple_mul_left z
  16. 0016apply multiple_mul_left
  17. 0017exact hprime
  18. 0018have hsource : exists bpr_divides_quotient_bpccpc_source_divides. n = (p) * bpr_divides_quotient_bpccpc_source_divides
  19. 0019cases hscaled
  20. 0020exists x
  21. 0021trans z * q
  22. 0022exact hfactor
  23. 0023exact hscaled_witness
  24. 0024have hbound : exists bpr_le_gap_bpccpc_bound. bpr_le_gap_bpccpc_bound + (p) = (m)
  25. 0025specialize hsupport p
  26. 0026apply hsupport
  27. 0027exact hp
  28. 0028exact hsource
  29. 0029have hshape : exists k. p = S (S k)
  30. 0030specialize prime_is_succ_succ p
  31. 0031apply prime_is_succ_succ
  32. 0032exact hp
  33. 0033cases hshape
  34. 0034rewrite hshape_witness at hp
  35. 0035rewrite hshape_witness at hp
  36. 0036rewrite hshape_witness at hbound
  37. 0037rewrite hshape_witness at hprime
  38. 0038have hselected : exists e a. (((exists bpr_le_gap_bpccpc_selected_valuation_selected_bound. bpr_le_gap_bpccpc_selected_valuation_selected_bound + (e) = (n)) /\ (exists bpr_power_value_bpccpc_selected_valuation_selected. ((exists bpr_power_code_bpccpc_selected_valuation_selected_power bpr_power_scale_bpccpc_selected_valuation_selected_power. ((forall bpr_power_index_bpccpc_selected_valuation_selected_power. (exists bpr_gap_bpccpc_selected_valuation_selected_power_repeat_bound. bpr_gap_bpccpc_selected_valuation_selected_power_repeat_bound + S (bpr_power_index_bpccpc_selected_valuation_selected_power) = e) -> (((exists bpr_height_bpccpc_selected_valuation_selected_power_repeat_entry. bpr_height_bpccpc_selected_valuation_selected_power_repeat_entry + S (S (S x)) = S ((S (bpr_power_index_bpccpc_selected_valuation_selected_power)) * bpr_power_scale_bpccpc_selected_valuation_selected_power)) /\ exists bpr_quotient_bpccpc_selected_valuation_selected_power_repeat_entry. bpr_power_code_bpccpc_selected_valuation_selected_power = bpr_quotient_bpccpc_selected_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpccpc_selected_valuation_selected_power)) * bpr_power_scale_bpccpc_selected_valuation_selected_power) + (S (S x))))) /\ (exists ff_u_bpccpc_selected_valuation_selected_power_product ff_v_bpccpc_selected_valuation_selected_power_product. ((((exists ff_h_bpccpc_selected_valuation_selected_power_product_start. ff_h_bpccpc_selected_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpccpc_selected_valuation_selected_power_product)) /\ exists ff_q_bpccpc_selected_valuation_selected_power_product_start. ff_u_bpccpc_selected_valuation_selected_power_product = ff_q_bpccpc_selected_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpccpc_selected_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpccpc_selected_valuation_selected_power_product_terminal. ff_h_bpccpc_selected_valuation_selected_power_product_terminal + S (bpr_power_value_bpccpc_selected_valuation_selected) = S ((S (e)) * ff_v_bpccpc_selected_valuation_selected_power_product)) /\ exists ff_q_bpccpc_selected_valuation_selected_power_product_terminal. ff_u_bpccpc_selected_valuation_selected_power_product = ff_q_bpccpc_selected_valuation_selected_power_product_terminal * S ((S (e)) * ff_v_bpccpc_selected_valuation_selected_power_product) + (bpr_power_value_bpccpc_selected_valuation_selected))) /\ forall ff_i_bpccpc_selected_valuation_selected_power_product. (exists ff_lt_bpccpc_selected_valuation_selected_power_product_bound. ff_lt_bpccpc_selected_valuation_selected_power_product_bound + S ff_i_bpccpc_selected_valuation_selected_power_product = e) -> exists ff_p_bpccpc_selected_valuation_selected_power_product ff_r_bpccpc_selected_valuation_selected_power_product ff_s_bpccpc_selected_valuation_selected_power_product. ((((exists ff_h_bpccpc_selected_valuation_selected_power_product_factor. ff_h_bpccpc_selected_valuation_selected_power_product_factor + S (ff_p_bpccpc_selected_valuation_selected_power_product) = S ((S (ff_i_bpccpc_selected_valuation_selected_power_product)) * bpr_power_scale_bpccpc_selected_valuation_selected_power)) /\ exists ff_q_bpccpc_selected_valuation_selected_power_product_factor. bpr_power_code_bpccpc_selected_valuation_selected_power = ff_q_bpccpc_selected_valuation_selected_power_product_factor * S ((S (ff_i_bpccpc_selected_valuation_selected_power_product)) * bpr_power_scale_bpccpc_selected_valuation_selected_power) + (ff_p_bpccpc_selected_valuation_selected_power_product))) /\ ((((exists ff_h_bpccpc_selected_valuation_selected_power_product_partial. ff_h_bpccpc_selected_valuation_selected_power_product_partial + S (ff_r_bpccpc_selected_valuation_selected_power_product) = S ((S (ff_i_bpccpc_selected_valuation_selected_power_product)) * ff_v_bpccpc_selected_valuation_selected_power_product)) /\ exists ff_q_bpccpc_selected_valuation_selected_power_product_partial. ff_u_bpccpc_selected_valuation_selected_power_product = ff_q_bpccpc_selected_valuation_selected_power_product_partial * S ((S (ff_i_bpccpc_selected_valuation_selected_power_product)) * ff_v_bpccpc_selected_valuation_selected_power_product) + (ff_r_bpccpc_selected_valuation_selected_power_product))) /\ ((((exists ff_h_bpccpc_selected_valuation_selected_power_product_successor. ff_h_bpccpc_selected_valuation_selected_power_product_successor + S (ff_s_bpccpc_selected_valuation_selected_power_product) = S ((S (S ff_i_bpccpc_selected_valuation_selected_power_product)) * ff_v_bpccpc_selected_valuation_selected_power_product)) /\ exists ff_q_bpccpc_selected_valuation_selected_power_product_successor. ff_u_bpccpc_selected_valuation_selected_power_product = ff_q_bpccpc_selected_valuation_selected_power_product_successor * S ((S (S ff_i_bpccpc_selected_valuation_selected_power_product)) * ff_v_bpccpc_selected_valuation_selected_power_product) + (ff_s_bpccpc_selected_valuation_selected_power_product))) /\ ff_s_bpccpc_selected_valuation_selected_power_product = ff_r_bpccpc_selected_valuation_selected_power_product * ff_p_bpccpc_selected_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpccpc_selected_valuation_selected_divides. n = (bpr_power_value_bpccpc_selected_valuation_selected) * bpr_divides_quotient_bpccpc_selected_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpccpc_selected_valuation. (exists bpr_le_gap_bpccpc_selected_valuation_candidate_bound. bpr_le_gap_bpccpc_selected_valuation_candidate_bound + (bpr_valuation_candidate_bpccpc_selected_valuation) = (n)) -> (exists bpr_power_value_bpccpc_selected_valuation_candidate. ((exists bpr_power_code_bpccpc_selected_valuation_candidate_power bpr_power_scale_bpccpc_selected_valuation_candidate_power. ((forall bpr_power_index_bpccpc_selected_valuation_candidate_power. (exists bpr_gap_bpccpc_selected_valuation_candidate_power_repeat_bound. bpr_gap_bpccpc_selected_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpccpc_selected_valuation_candidate_power) = bpr_valuation_candidate_bpccpc_selected_valuation) -> (((exists bpr_height_bpccpc_selected_valuation_candidate_power_repeat_entry. bpr_height_bpccpc_selected_valuation_candidate_power_repeat_entry + S (S (S x)) = S ((S (bpr_power_index_bpccpc_selected_valuation_candidate_power)) * bpr_power_scale_bpccpc_selected_valuation_candidate_power)) /\ exists bpr_quotient_bpccpc_selected_valuation_candidate_power_repeat_entry. bpr_power_code_bpccpc_selected_valuation_candidate_power = bpr_quotient_bpccpc_selected_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpccpc_selected_valuation_candidate_power)) * bpr_power_scale_bpccpc_selected_valuation_candidate_power) + (S (S x))))) /\ (exists ff_u_bpccpc_selected_valuation_candidate_power_product ff_v_bpccpc_selected_valuation_candidate_power_product. ((((exists ff_h_bpccpc_selected_valuation_candidate_power_product_start. ff_h_bpccpc_selected_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpccpc_selected_valuation_candidate_power_product)) /\ exists ff_q_bpccpc_selected_valuation_candidate_power_product_start. ff_u_bpccpc_selected_valuation_candidate_power_product = ff_q_bpccpc_selected_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpccpc_selected_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpccpc_selected_valuation_candidate_power_product_terminal. ff_h_bpccpc_selected_valuation_candidate_power_product_terminal + S (bpr_power_value_bpccpc_selected_valuation_candidate) = S ((S (bpr_valuation_candidate_bpccpc_selected_valuation)) * ff_v_bpccpc_selected_valuation_candidate_power_product)) /\ exists ff_q_bpccpc_selected_valuation_candidate_power_product_terminal. ff_u_bpccpc_selected_valuation_candidate_power_product = ff_q_bpccpc_selected_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpccpc_selected_valuation)) * ff_v_bpccpc_selected_valuation_candidate_power_product) + (bpr_power_value_bpccpc_selected_valuation_candidate))) /\ forall ff_i_bpccpc_selected_valuation_candidate_power_product. (exists ff_lt_bpccpc_selected_valuation_candidate_power_product_bound. ff_lt_bpccpc_selected_valuation_candidate_power_product_bound + S ff_i_bpccpc_selected_valuation_candidate_power_product = bpr_valuation_candidate_bpccpc_selected_valuation) -> exists ff_p_bpccpc_selected_valuation_candidate_power_product ff_r_bpccpc_selected_valuation_candidate_power_product ff_s_bpccpc_selected_valuation_candidate_power_product. ((((exists ff_h_bpccpc_selected_valuation_candidate_power_product_factor. ff_h_bpccpc_selected_valuation_candidate_power_product_factor + S (ff_p_bpccpc_selected_valuation_candidate_power_product) = S ((S (ff_i_bpccpc_selected_valuation_candidate_power_product)) * bpr_power_scale_bpccpc_selected_valuation_candidate_power)) /\ exists ff_q_bpccpc_selected_valuation_candidate_power_product_factor. bpr_power_code_bpccpc_selected_valuation_candidate_power = ff_q_bpccpc_selected_valuation_candidate_power_product_factor * S ((S (ff_i_bpccpc_selected_valuation_candidate_power_product)) * bpr_power_scale_bpccpc_selected_valuation_candidate_power) + (ff_p_bpccpc_selected_valuation_candidate_power_product))) /\ ((((exists ff_h_bpccpc_selected_valuation_candidate_power_product_partial. ff_h_bpccpc_selected_valuation_candidate_power_product_partial + S (ff_r_bpccpc_selected_valuation_candidate_power_product) = S ((S (ff_i_bpccpc_selected_valuation_candidate_power_product)) * ff_v_bpccpc_selected_valuation_candidate_power_product)) /\ exists ff_q_bpccpc_selected_valuation_candidate_power_product_partial. ff_u_bpccpc_selected_valuation_candidate_power_product = ff_q_bpccpc_selected_valuation_candidate_power_product_partial * S ((S (ff_i_bpccpc_selected_valuation_candidate_power_product)) * ff_v_bpccpc_selected_valuation_candidate_power_product) + (ff_r_bpccpc_selected_valuation_candidate_power_product))) /\ ((((exists ff_h_bpccpc_selected_valuation_candidate_power_product_successor. ff_h_bpccpc_selected_valuation_candidate_power_product_successor + S (ff_s_bpccpc_selected_valuation_candidate_power_product) = S ((S (S ff_i_bpccpc_selected_valuation_candidate_power_product)) * ff_v_bpccpc_selected_valuation_candidate_power_product)) /\ exists ff_q_bpccpc_selected_valuation_candidate_power_product_successor. ff_u_bpccpc_selected_valuation_candidate_power_product = ff_q_bpccpc_selected_valuation_candidate_power_product_successor * S ((S (S ff_i_bpccpc_selected_valuation_candidate_power_product)) * ff_v_bpccpc_selected_valuation_candidate_power_product) + (ff_s_bpccpc_selected_valuation_candidate_power_product))) /\ ff_s_bpccpc_selected_valuation_candidate_power_product = ff_r_bpccpc_selected_valuation_candidate_power_product * ff_p_bpccpc_selected_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpccpc_selected_valuation_candidate_divides. n = (bpr_power_value_bpccpc_selected_valuation_candidate) * bpr_divides_quotient_bpccpc_selected_valuation_candidate_divides))) -> (exists bpr_le_gap_bpccpc_selected_valuation_candidate_below. bpr_le_gap_bpccpc_selected_valuation_candidate_below + (bpr_valuation_candidate_bpccpc_selected_valuation) = (e))) /\ ((exists bpr_power_code_bpccpc_selected_power bpr_power_scale_bpccpc_selected_power. ((forall bpr_power_index_bpccpc_selected_power. (exists bpr_gap_bpccpc_selected_power_repeat_bound. bpr_gap_bpccpc_selected_power_repeat_bound + S (bpr_power_index_bpccpc_selected_power) = e) -> (((exists bpr_height_bpccpc_selected_power_repeat_entry. bpr_height_bpccpc_selected_power_repeat_entry + S (S (S x)) = S ((S (bpr_power_index_bpccpc_selected_power)) * bpr_power_scale_bpccpc_selected_power)) /\ exists bpr_quotient_bpccpc_selected_power_repeat_entry. bpr_power_code_bpccpc_selected_power = bpr_quotient_bpccpc_selected_power_repeat_entry * S ((S (bpr_power_index_bpccpc_selected_power)) * bpr_power_scale_bpccpc_selected_power) + (S (S x))))) /\ (exists ff_u_bpccpc_selected_power_product ff_v_bpccpc_selected_power_product. ((((exists ff_h_bpccpc_selected_power_product_start. ff_h_bpccpc_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpccpc_selected_power_product)) /\ exists ff_q_bpccpc_selected_power_product_start. ff_u_bpccpc_selected_power_product = ff_q_bpccpc_selected_power_product_start * S ((S (0)) * ff_v_bpccpc_selected_power_product) + (1))) /\ ((((exists ff_h_bpccpc_selected_power_product_terminal. ff_h_bpccpc_selected_power_product_terminal + S (a) = S ((S (e)) * ff_v_bpccpc_selected_power_product)) /\ exists ff_q_bpccpc_selected_power_product_terminal. ff_u_bpccpc_selected_power_product = ff_q_bpccpc_selected_power_product_terminal * S ((S (e)) * ff_v_bpccpc_selected_power_product) + (a))) /\ forall ff_i_bpccpc_selected_power_product. (exists ff_lt_bpccpc_selected_power_product_bound. ff_lt_bpccpc_selected_power_product_bound + S ff_i_bpccpc_selected_power_product = e) -> exists ff_p_bpccpc_selected_power_product ff_r_bpccpc_selected_power_product ff_s_bpccpc_selected_power_product. ((((exists ff_h_bpccpc_selected_power_product_factor. ff_h_bpccpc_selected_power_product_factor + S (ff_p_bpccpc_selected_power_product) = S ((S (ff_i_bpccpc_selected_power_product)) * bpr_power_scale_bpccpc_selected_power)) /\ exists ff_q_bpccpc_selected_power_product_factor. bpr_power_code_bpccpc_selected_power = ff_q_bpccpc_selected_power_product_factor * S ((S (ff_i_bpccpc_selected_power_product)) * bpr_power_scale_bpccpc_selected_power) + (ff_p_bpccpc_selected_power_product))) /\ ((((exists ff_h_bpccpc_selected_power_product_partial. ff_h_bpccpc_selected_power_product_partial + S (ff_r_bpccpc_selected_power_product) = S ((S (ff_i_bpccpc_selected_power_product)) * ff_v_bpccpc_selected_power_product)) /\ exists ff_q_bpccpc_selected_power_product_partial. ff_u_bpccpc_selected_power_product = ff_q_bpccpc_selected_power_product_partial * S ((S (ff_i_bpccpc_selected_power_product)) * ff_v_bpccpc_selected_power_product) + (ff_r_bpccpc_selected_power_product))) /\ ((((exists ff_h_bpccpc_selected_power_product_successor. ff_h_bpccpc_selected_power_product_successor + S (ff_s_bpccpc_selected_power_product) = S ((S (S ff_i_bpccpc_selected_power_product)) * ff_v_bpccpc_selected_power_product)) /\ exists ff_q_bpccpc_selected_power_product_successor. ff_u_bpccpc_selected_power_product = ff_q_bpccpc_selected_power_product_successor * S ((S (S ff_i_bpccpc_selected_power_product)) * ff_v_bpccpc_selected_power_product) + (ff_s_bpccpc_selected_power_product))) /\ ff_s_bpccpc_selected_power_product = ff_r_bpccpc_selected_power_product * ff_p_bpccpc_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpccpc_selected_divides. z = (a) * bpr_divides_quotient_bpccpc_selected_divides))
  39. 0039specialize prime_contribution_selected_entry n
  40. 0040specialize prime_contribution_selected_entry m
  41. 0041specialize prime_contribution_selected_entry z
  42. 0042specialize prime_contribution_selected_entry (S x)
  43. 0043apply prime_contribution_selected_entry
  44. 0044exact hp
  45. 0045exact hbound
  46. 0046exact hproduct
  47. 0047cases hselected
  48. 0048cases hselected_witness
  49. 0049cases hselected_witness_witness
  50. 0050cases hselected_witness_witness_right
  51. 0051have hsuccessor : exists bpr_power_value_bpccpc_successor. ((exists bpr_power_code_bpccpc_successor_power bpr_power_scale_bpccpc_successor_power. ((forall bpr_power_index_bpccpc_successor_power. (exists bpr_gap_bpccpc_successor_power_repeat_bound. bpr_gap_bpccpc_successor_power_repeat_bound + S (bpr_power_index_bpccpc_successor_power) = S x1) -> (((exists bpr_height_bpccpc_successor_power_repeat_entry. bpr_height_bpccpc_successor_power_repeat_entry + S (S (S x)) = S ((S (bpr_power_index_bpccpc_successor_power)) * bpr_power_scale_bpccpc_successor_power)) /\ exists bpr_quotient_bpccpc_successor_power_repeat_entry. bpr_power_code_bpccpc_successor_power = bpr_quotient_bpccpc_successor_power_repeat_entry * S ((S (bpr_power_index_bpccpc_successor_power)) * bpr_power_scale_bpccpc_successor_power) + (S (S x))))) /\ (exists ff_u_bpccpc_successor_power_product ff_v_bpccpc_successor_power_product. ((((exists ff_h_bpccpc_successor_power_product_start. ff_h_bpccpc_successor_power_product_start + S (1) = S ((S (0)) * ff_v_bpccpc_successor_power_product)) /\ exists ff_q_bpccpc_successor_power_product_start. ff_u_bpccpc_successor_power_product = ff_q_bpccpc_successor_power_product_start * S ((S (0)) * ff_v_bpccpc_successor_power_product) + (1))) /\ ((((exists ff_h_bpccpc_successor_power_product_terminal. ff_h_bpccpc_successor_power_product_terminal + S (bpr_power_value_bpccpc_successor) = S ((S (S x1)) * ff_v_bpccpc_successor_power_product)) /\ exists ff_q_bpccpc_successor_power_product_terminal. ff_u_bpccpc_successor_power_product = ff_q_bpccpc_successor_power_product_terminal * S ((S (S x1)) * ff_v_bpccpc_successor_power_product) + (bpr_power_value_bpccpc_successor))) /\ forall ff_i_bpccpc_successor_power_product. (exists ff_lt_bpccpc_successor_power_product_bound. ff_lt_bpccpc_successor_power_product_bound + S ff_i_bpccpc_successor_power_product = S x1) -> exists ff_p_bpccpc_successor_power_product ff_r_bpccpc_successor_power_product ff_s_bpccpc_successor_power_product. ((((exists ff_h_bpccpc_successor_power_product_factor. ff_h_bpccpc_successor_power_product_factor + S (ff_p_bpccpc_successor_power_product) = S ((S (ff_i_bpccpc_successor_power_product)) * bpr_power_scale_bpccpc_successor_power)) /\ exists ff_q_bpccpc_successor_power_product_factor. bpr_power_code_bpccpc_successor_power = ff_q_bpccpc_successor_power_product_factor * S ((S (ff_i_bpccpc_successor_power_product)) * bpr_power_scale_bpccpc_successor_power) + (ff_p_bpccpc_successor_power_product))) /\ ((((exists ff_h_bpccpc_successor_power_product_partial. ff_h_bpccpc_successor_power_product_partial + S (ff_r_bpccpc_successor_power_product) = S ((S (ff_i_bpccpc_successor_power_product)) * ff_v_bpccpc_successor_power_product)) /\ exists ff_q_bpccpc_successor_power_product_partial. ff_u_bpccpc_successor_power_product = ff_q_bpccpc_successor_power_product_partial * S ((S (ff_i_bpccpc_successor_power_product)) * ff_v_bpccpc_successor_power_product) + (ff_r_bpccpc_successor_power_product))) /\ ((((exists ff_h_bpccpc_successor_power_product_successor. ff_h_bpccpc_successor_power_product_successor + S (ff_s_bpccpc_successor_power_product) = S ((S (S ff_i_bpccpc_successor_power_product)) * ff_v_bpccpc_successor_power_product)) /\ exists ff_q_bpccpc_successor_power_product_successor. ff_u_bpccpc_successor_power_product = ff_q_bpccpc_successor_power_product_successor * S ((S (S ff_i_bpccpc_successor_power_product)) * ff_v_bpccpc_successor_power_product) + (ff_s_bpccpc_successor_power_product))) /\ ff_s_bpccpc_successor_power_product = ff_r_bpccpc_successor_power_product * ff_p_bpccpc_successor_power_product)))))))) /\ (exists bpr_divides_quotient_bpccpc_successor_divides. n = (bpr_power_value_bpccpc_successor) * bpr_divides_quotient_bpccpc_successor_divides))
  52. 0052specialize prime_contribution_selected_successor_divides (S (S x))
  53. 0053specialize prime_contribution_selected_successor_divides x1
  54. 0054specialize prime_contribution_selected_successor_divides x2
  55. 0055specialize prime_contribution_selected_successor_divides z
  56. 0056specialize prime_contribution_selected_successor_divides q
  57. 0057specialize prime_contribution_selected_successor_divides n
  58. 0058apply prime_contribution_selected_successor_divides
  59. 0059exact hselected_witness_witness_right_left
  60. 0060exact hselected_witness_witness_right_right
  61. 0061exact hprime
  62. 0062exact hfactor
  63. 0063specialize power_valuation_successor_not_divides (S (S x))
  64. 0064specialize power_valuation_successor_not_divides n
  65. 0065specialize power_valuation_successor_not_divides x1
  66. 0066apply power_valuation_successor_not_divides
  67. 0067exact hp
  68. 0068exact hn
  69. 0069exact hselected_witness_witness_left
  70. 0070exact hsuccessor