Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Statement with defined notation
∀ n. ∀ m. ∀ z. ¬n = 0 → (∀ x. Prime(x) → Dvd(x,n) → Le(x,m)) → (∃ 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)) → n = zEvery 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 PowerValuation10 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall n m z. ~(n = 0) -> (forall bpr_support_prime_bpcpeq_support. ((~(bpr_support_prime_bpcpeq_support = 1) /\ forall bpr_left_bpcpeq_support_prime bpr_right_bpcpeq_support_prime. bpr_support_prime_bpcpeq_support = bpr_left_bpcpeq_support_prime * bpr_right_bpcpeq_support_prime -> bpr_left_bpcpeq_support_prime = 1 \/ bpr_right_bpcpeq_support_prime = 1)) -> (exists bpr_divides_quotient_bpcpeq_support_divides. n = (bpr_support_prime_bpcpeq_support) * bpr_divides_quotient_bpcpeq_support_divides) -> (exists bpr_le_gap_bpcpeq_support_bound. bpr_le_gap_bpcpeq_support_bound + (bpr_support_prime_bpcpeq_support) = (m))) -> (exists bpr_product_code_bpcpeq_product bpr_product_scale_bpcpeq_product. ((forall bpr_prefix_index_bpcpeq_product_prefix. (exists bpr_gap_bpcpeq_product_prefix_bound. bpr_gap_bpcpeq_product_prefix_bound + S (bpr_prefix_index_bpcpeq_product_prefix) = m) -> exists bpr_prefix_value_bpcpeq_product_prefix. ((((exists bpr_height_bpcpeq_product_prefix_decoded. bpr_height_bpcpeq_product_prefix_decoded + S (bpr_prefix_value_bpcpeq_product_prefix) = S ((S (bpr_prefix_index_bpcpeq_product_prefix)) * bpr_product_scale_bpcpeq_product)) /\ exists bpr_quotient_bpcpeq_product_prefix_decoded. bpr_product_code_bpcpeq_product = bpr_quotient_bpcpeq_product_prefix_decoded * S ((S (bpr_prefix_index_bpcpeq_product_prefix)) * bpr_product_scale_bpcpeq_product) + (bpr_prefix_value_bpcpeq_product_prefix))) /\ (((((~(S (bpr_prefix_index_bpcpeq_product_prefix) = 1) /\ forall bpr_left_bpcpeq_product_prefix_choice_prime bpr_right_bpcpeq_product_prefix_choice_prime. S (bpr_prefix_index_bpcpeq_product_prefix) = bpr_left_bpcpeq_product_prefix_choice_prime * bpr_right_bpcpeq_product_prefix_choice_prime -> bpr_left_bpcpeq_product_prefix_choice_prime = 1 \/ bpr_right_bpcpeq_product_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcpeq_product_prefix_choice. ((((exists bpr_le_gap_bpcpeq_product_prefix_choice_valuation_selected_bound. bpr_le_gap_bpcpeq_product_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpcpeq_product_prefix_choice) = (n)) /\ (exists bpr_power_value_bpcpeq_product_prefix_choice_valuation_selected. ((exists bpr_power_code_bpcpeq_product_prefix_choice_valuation_selected_power bpr_power_scale_bpcpeq_product_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpcpeq_product_prefix_choice_valuation_selected_power. (exists bpr_gap_bpcpeq_product_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcpeq_product_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcpeq_product_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpcpeq_product_prefix_choice) -> (((exists bpr_height_bpcpeq_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpcpeq_product_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcpeq_product_prefix)) = S ((S (bpr_power_index_bpcpeq_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpeq_product_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcpeq_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcpeq_product_prefix_choice_valuation_selected_power = bpr_quotient_bpcpeq_product_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcpeq_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcpeq_product_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcpeq_product_prefix))))) /\ (exists ff_u_bpcpeq_product_prefix_choice_valuation_selected_power_product ff_v_bpcpeq_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpeq_product_prefix_choice_valuation_selected_power_product_start. ff_h_bpcpeq_product_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpeq_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_valuation_selected_power_product_start. ff_u_bpcpeq_product_prefix_choice_valuation_selected_power_product = ff_q_bpcpeq_product_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcpeq_product_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcpeq_product_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpcpeq_product_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcpeq_product_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcpeq_product_prefix_choice)) * ff_v_bpcpeq_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpcpeq_product_prefix_choice_valuation_selected_power_product = ff_q_bpcpeq_product_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcpeq_product_prefix_choice)) * ff_v_bpcpeq_product_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpcpeq_product_prefix_choice_valuation_selected))) /\ forall ff_i_bpcpeq_product_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpcpeq_product_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpcpeq_product_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpcpeq_product_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpcpeq_product_prefix_choice) -> exists ff_p_bpcpeq_product_prefix_choice_valuation_selected_power_product ff_r_bpcpeq_product_prefix_choice_valuation_selected_power_product ff_s_bpcpeq_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcpeq_product_prefix_choice_valuation_selected_power_product_factor. ff_h_bpcpeq_product_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpcpeq_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpeq_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpeq_product_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpcpeq_product_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpcpeq_product_prefix_choice_valuation_selected_power = ff_q_bpcpeq_product_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcpeq_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcpeq_product_prefix_choice_valuation_selected_power) + (ff_p_bpcpeq_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpeq_product_prefix_choice_valuation_selected_power_product_partial. ff_h_bpcpeq_product_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpcpeq_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcpeq_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpeq_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_valuation_selected_power_product_partial. ff_u_bpcpeq_product_prefix_choice_valuation_selected_power_product = ff_q_bpcpeq_product_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcpeq_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpeq_product_prefix_choice_valuation_selected_power_product) + (ff_r_bpcpeq_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcpeq_product_prefix_choice_valuation_selected_power_product_successor. ff_h_bpcpeq_product_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpcpeq_product_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcpeq_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpeq_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_valuation_selected_power_product_successor. ff_u_bpcpeq_product_prefix_choice_valuation_selected_power_product = ff_q_bpcpeq_product_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcpeq_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcpeq_product_prefix_choice_valuation_selected_power_product) + (ff_s_bpcpeq_product_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpcpeq_product_prefix_choice_valuation_selected_power_product = ff_r_bpcpeq_product_prefix_choice_valuation_selected_power_product * ff_p_bpcpeq_product_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpeq_product_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpcpeq_product_prefix_choice_valuation_selected) * bpr_divides_quotient_bpcpeq_product_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcpeq_product_prefix_choice_valuation. (exists bpr_le_gap_bpcpeq_product_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpcpeq_product_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcpeq_product_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpcpeq_product_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpcpeq_product_prefix_choice_valuation_candidate_power bpr_power_scale_bpcpeq_product_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpcpeq_product_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpcpeq_product_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcpeq_product_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcpeq_product_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcpeq_product_prefix_choice_valuation) -> (((exists bpr_height_bpcpeq_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcpeq_product_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcpeq_product_prefix)) = S ((S (bpr_power_index_bpcpeq_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpeq_product_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcpeq_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcpeq_product_prefix_choice_valuation_candidate_power = bpr_quotient_bpcpeq_product_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcpeq_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcpeq_product_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcpeq_product_prefix))))) /\ (exists ff_u_bpcpeq_product_prefix_choice_valuation_candidate_power_product ff_v_bpcpeq_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpeq_product_prefix_choice_valuation_candidate_power_product_start. ff_h_bpcpeq_product_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpeq_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_valuation_candidate_power_product_start. ff_u_bpcpeq_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcpeq_product_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcpeq_product_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcpeq_product_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpcpeq_product_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcpeq_product_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcpeq_product_prefix_choice_valuation)) * ff_v_bpcpeq_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpcpeq_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcpeq_product_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcpeq_product_prefix_choice_valuation)) * ff_v_bpcpeq_product_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpcpeq_product_prefix_choice_valuation_candidate))) /\ forall ff_i_bpcpeq_product_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpcpeq_product_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpcpeq_product_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpcpeq_product_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcpeq_product_prefix_choice_valuation) -> exists ff_p_bpcpeq_product_prefix_choice_valuation_candidate_power_product ff_r_bpcpeq_product_prefix_choice_valuation_candidate_power_product ff_s_bpcpeq_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcpeq_product_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpcpeq_product_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpcpeq_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpeq_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpeq_product_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpcpeq_product_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcpeq_product_prefix_choice_valuation_candidate_power = ff_q_bpcpeq_product_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcpeq_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcpeq_product_prefix_choice_valuation_candidate_power) + (ff_p_bpcpeq_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpeq_product_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpcpeq_product_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpcpeq_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcpeq_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpeq_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpcpeq_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcpeq_product_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcpeq_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpeq_product_prefix_choice_valuation_candidate_power_product) + (ff_r_bpcpeq_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcpeq_product_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpcpeq_product_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpcpeq_product_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcpeq_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpeq_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpcpeq_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcpeq_product_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcpeq_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcpeq_product_prefix_choice_valuation_candidate_power_product) + (ff_s_bpcpeq_product_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpcpeq_product_prefix_choice_valuation_candidate_power_product = ff_r_bpcpeq_product_prefix_choice_valuation_candidate_power_product * ff_p_bpcpeq_product_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcpeq_product_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpcpeq_product_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpcpeq_product_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcpeq_product_prefix_choice_valuation_candidate_below. bpr_le_gap_bpcpeq_product_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcpeq_product_prefix_choice_valuation) = (bpr_choice_exponent_bpcpeq_product_prefix_choice))) /\ (exists bpr_power_code_bpcpeq_product_prefix_choice_power bpr_power_scale_bpcpeq_product_prefix_choice_power. ((forall bpr_power_index_bpcpeq_product_prefix_choice_power. (exists bpr_gap_bpcpeq_product_prefix_choice_power_repeat_bound. bpr_gap_bpcpeq_product_prefix_choice_power_repeat_bound + S (bpr_power_index_bpcpeq_product_prefix_choice_power) = bpr_choice_exponent_bpcpeq_product_prefix_choice) -> (((exists bpr_height_bpcpeq_product_prefix_choice_power_repeat_entry. bpr_height_bpcpeq_product_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcpeq_product_prefix)) = S ((S (bpr_power_index_bpcpeq_product_prefix_choice_power)) * bpr_power_scale_bpcpeq_product_prefix_choice_power)) /\ exists bpr_quotient_bpcpeq_product_prefix_choice_power_repeat_entry. bpr_power_code_bpcpeq_product_prefix_choice_power = bpr_quotient_bpcpeq_product_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpcpeq_product_prefix_choice_power)) * bpr_power_scale_bpcpeq_product_prefix_choice_power) + (S (bpr_prefix_index_bpcpeq_product_prefix))))) /\ (exists ff_u_bpcpeq_product_prefix_choice_power_product ff_v_bpcpeq_product_prefix_choice_power_product. ((((exists ff_h_bpcpeq_product_prefix_choice_power_product_start. ff_h_bpcpeq_product_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcpeq_product_prefix_choice_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_power_product_start. ff_u_bpcpeq_product_prefix_choice_power_product = ff_q_bpcpeq_product_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpcpeq_product_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpcpeq_product_prefix_choice_power_product_terminal. ff_h_bpcpeq_product_prefix_choice_power_product_terminal + S (bpr_prefix_value_bpcpeq_product_prefix) = S ((S (bpr_choice_exponent_bpcpeq_product_prefix_choice)) * ff_v_bpcpeq_product_prefix_choice_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_power_product_terminal. ff_u_bpcpeq_product_prefix_choice_power_product = ff_q_bpcpeq_product_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcpeq_product_prefix_choice)) * ff_v_bpcpeq_product_prefix_choice_power_product) + (bpr_prefix_value_bpcpeq_product_prefix))) /\ forall ff_i_bpcpeq_product_prefix_choice_power_product. (exists ff_lt_bpcpeq_product_prefix_choice_power_product_bound. ff_lt_bpcpeq_product_prefix_choice_power_product_bound + S ff_i_bpcpeq_product_prefix_choice_power_product = bpr_choice_exponent_bpcpeq_product_prefix_choice) -> exists ff_p_bpcpeq_product_prefix_choice_power_product ff_r_bpcpeq_product_prefix_choice_power_product ff_s_bpcpeq_product_prefix_choice_power_product. ((((exists ff_h_bpcpeq_product_prefix_choice_power_product_factor. ff_h_bpcpeq_product_prefix_choice_power_product_factor + S (ff_p_bpcpeq_product_prefix_choice_power_product) = S ((S (ff_i_bpcpeq_product_prefix_choice_power_product)) * bpr_power_scale_bpcpeq_product_prefix_choice_power)) /\ exists ff_q_bpcpeq_product_prefix_choice_power_product_factor. bpr_power_code_bpcpeq_product_prefix_choice_power = ff_q_bpcpeq_product_prefix_choice_power_product_factor * S ((S (ff_i_bpcpeq_product_prefix_choice_power_product)) * bpr_power_scale_bpcpeq_product_prefix_choice_power) + (ff_p_bpcpeq_product_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpeq_product_prefix_choice_power_product_partial. ff_h_bpcpeq_product_prefix_choice_power_product_partial + S (ff_r_bpcpeq_product_prefix_choice_power_product) = S ((S (ff_i_bpcpeq_product_prefix_choice_power_product)) * ff_v_bpcpeq_product_prefix_choice_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_power_product_partial. ff_u_bpcpeq_product_prefix_choice_power_product = ff_q_bpcpeq_product_prefix_choice_power_product_partial * S ((S (ff_i_bpcpeq_product_prefix_choice_power_product)) * ff_v_bpcpeq_product_prefix_choice_power_product) + (ff_r_bpcpeq_product_prefix_choice_power_product))) /\ ((((exists ff_h_bpcpeq_product_prefix_choice_power_product_successor. ff_h_bpcpeq_product_prefix_choice_power_product_successor + S (ff_s_bpcpeq_product_prefix_choice_power_product) = S ((S (S ff_i_bpcpeq_product_prefix_choice_power_product)) * ff_v_bpcpeq_product_prefix_choice_power_product)) /\ exists ff_q_bpcpeq_product_prefix_choice_power_product_successor. ff_u_bpcpeq_product_prefix_choice_power_product = ff_q_bpcpeq_product_prefix_choice_power_product_successor * S ((S (S ff_i_bpcpeq_product_prefix_choice_power_product)) * ff_v_bpcpeq_product_prefix_choice_power_product) + (ff_s_bpcpeq_product_prefix_choice_power_product))) /\ ff_s_bpcpeq_product_prefix_choice_power_product = ff_r_bpcpeq_product_prefix_choice_power_product * ff_p_bpcpeq_product_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcpeq_product_prefix) = 1) /\ forall bpr_left_bpcpeq_product_prefix_choice_prime bpr_right_bpcpeq_product_prefix_choice_prime. S (bpr_prefix_index_bpcpeq_product_prefix) = bpr_left_bpcpeq_product_prefix_choice_prime * bpr_right_bpcpeq_product_prefix_choice_prime -> bpr_left_bpcpeq_product_prefix_choice_prime = 1 \/ bpr_right_bpcpeq_product_prefix_choice_prime = 1)) /\ bpr_prefix_value_bpcpeq_product_prefix = 1))))) /\ (exists ff_u_bpcpeq_product_product ff_v_bpcpeq_product_product. ((((exists ff_h_bpcpeq_product_product_start. ff_h_bpcpeq_product_product_start + S (1) = S ((S (0)) * ff_v_bpcpeq_product_product)) /\ exists ff_q_bpcpeq_product_product_start. ff_u_bpcpeq_product_product = ff_q_bpcpeq_product_product_start * S ((S (0)) * ff_v_bpcpeq_product_product) + (1))) /\ ((((exists ff_h_bpcpeq_product_product_terminal. ff_h_bpcpeq_product_product_terminal + S (z) = S ((S (m)) * ff_v_bpcpeq_product_product)) /\ exists ff_q_bpcpeq_product_product_terminal. ff_u_bpcpeq_product_product = ff_q_bpcpeq_product_product_terminal * S ((S (m)) * ff_v_bpcpeq_product_product) + (z))) /\ forall ff_i_bpcpeq_product_product. (exists ff_lt_bpcpeq_product_product_bound. ff_lt_bpcpeq_product_product_bound + S ff_i_bpcpeq_product_product = m) -> exists ff_p_bpcpeq_product_product ff_r_bpcpeq_product_product ff_s_bpcpeq_product_product. ((((exists ff_h_bpcpeq_product_product_factor. ff_h_bpcpeq_product_product_factor + S (ff_p_bpcpeq_product_product) = S ((S (ff_i_bpcpeq_product_product)) * bpr_product_scale_bpcpeq_product)) /\ exists ff_q_bpcpeq_product_product_factor. bpr_product_code_bpcpeq_product = ff_q_bpcpeq_product_product_factor * S ((S (ff_i_bpcpeq_product_product)) * bpr_product_scale_bpcpeq_product) + (ff_p_bpcpeq_product_product))) /\ ((((exists ff_h_bpcpeq_product_product_partial. ff_h_bpcpeq_product_product_partial + S (ff_r_bpcpeq_product_product) = S ((S (ff_i_bpcpeq_product_product)) * ff_v_bpcpeq_product_product)) /\ exists ff_q_bpcpeq_product_product_partial. ff_u_bpcpeq_product_product = ff_q_bpcpeq_product_product_partial * S ((S (ff_i_bpcpeq_product_product)) * ff_v_bpcpeq_product_product) + (ff_r_bpcpeq_product_product))) /\ ((((exists ff_h_bpcpeq_product_product_successor. ff_h_bpcpeq_product_product_successor + S (ff_s_bpcpeq_product_product) = S ((S (S ff_i_bpcpeq_product_product)) * ff_v_bpcpeq_product_product)) /\ exists ff_q_bpcpeq_product_product_successor. ff_u_bpcpeq_product_product = ff_q_bpcpeq_product_product_successor * S ((S (S ff_i_bpcpeq_product_product)) * ff_v_bpcpeq_product_product) + (ff_s_bpcpeq_product_product))) /\ ff_s_bpcpeq_product_product = ff_r_bpcpeq_product_product * ff_p_bpcpeq_product_product)))))))) -> n = zProof neighborhood
Direct theorem prerequisites
BT002F multiple_antisymm BT00YY prime_contribution_product_divides BT0104 prime_contribution_reverse_dividesDirect theorem dependents
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
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 (3)
01Fix variables and assumptionsL1–6
02Establish hreverseL7–11
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution reverse divides.
03Establish hforwardL12–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime contribution product divides.
Original defined command ledger · 19 lines
- 0001
intro n - 0002
intro m - 0003
intro z - 0004
intro hn - 0005
intro hsupport - 0006
intro hproduct - 0007
have hreverse : Dvd(n,z)Exact native replay line
have hreverse : exists bpr_divides_quotient_bpcpeq_reverse. z = (n) * bpr_divides_quotient_bpcpeq_reverse - 0008
apply prime_contribution_reverse_divides - 0009
exact hn - 0010
exact hsupport - 0011
exact hproduct - 0012
have hforward : Dvd(z,n)Exact native replay line
have hforward : exists bpr_divides_quotient_bpcpeq_forward. n = (z) * bpr_divides_quotient_bpcpeq_forward - 0013
apply prime_contribution_product_divides - 0014
exact hproduct - 0015
specialize multiple_antisymm n - 0016
specialize multiple_antisymm z - 0017
apply multiple_antisymm - 0018
exact hreverse - 0019
exact hforward