BT0103 · Bertrand theorem

prime_contribution_cofactor_eq_one

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

A supported contribution cofactor is the multiplicative unit.

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. ∀ q. ¬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 = z · q → q = 1

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

PD0003 Dvd PD0004 Prime

2 occurrences

Exact expanded native-PA statement
forall n m z q. ~(n = 0) -> (forall bpr_support_prime_bpcceo_support. ((~(bpr_support_prime_bpcceo_support = 1) /\ forall bpr_left_bpcceo_support_prime bpr_right_bpcceo_support_prime. bpr_support_prime_bpcceo_support = bpr_left_bpcceo_support_prime * bpr_right_bpcceo_support_prime -> bpr_left_bpcceo_support_prime = 1 \/ bpr_right_bpcceo_support_prime = 1)) -> (exists bpr_divides_quotient_bpcceo_support_divides. n = (bpr_support_prime_bpcceo_support) * bpr_divides_quotient_bpcceo_support_divides) -> (exists bpr_le_gap_bpcceo_support_bound. bpr_le_gap_bpcceo_support_bound + (bpr_support_prime_bpcceo_support) = (m))) -> (exists bpr_product_code_bpcceo_product bpr_product_scale_bpcceo_product. ((forall bpr_prefix_index_bpcceo_product_prefix. (exists bpr_gap_bpcceo_product_prefix_bound. bpr_gap_bpcceo_product_prefix_bound + S (bpr_prefix_index_bpcceo_product_prefix) = m) -> exists bpr_prefix_value_bpcceo_product_prefix. ((((exists bpr_height_bpcceo_product_prefix_decoded. bpr_height_bpcceo_product_prefix_decoded + S (bpr_prefix_value_bpcceo_product_prefix) = S ((S (bpr_prefix_index_bpcceo_product_prefix)) * bpr_product_scale_bpcceo_product)) /\ exists bpr_quotient_bpcceo_product_prefix_decoded. bpr_product_code_bpcceo_product = bpr_quotient_bpcceo_product_prefix_decoded * S ((S (bpr_prefix_index_bpcceo_product_prefix)) * bpr_product_scale_bpcceo_product) + (bpr_prefix_value_bpcceo_product_prefix))) /\ (((((~(S (bpr_prefix_index_bpcceo_product_prefix) = 1) /\ forall bpr_left_bpcceo_product_prefix_choice_prime bpr_right_bpcceo_product_prefix_choice_prime. S (bpr_prefix_index_bpcceo_product_prefix) = bpr_left_bpcceo_product_prefix_choice_prime * bpr_right_bpcceo_product_prefix_choice_prime -> bpr_left_bpcceo_product_prefix_choice_prime = 1 \/ bpr_right_bpcceo_product_prefix_choice_prime = 1)) /\ exists bpr_choice_exponent_bpcceo_product_prefix_choice. ((((exists bpr_le_gap_bpcceo_product_prefix_choice_valuation_selected_bound. bpr_le_gap_bpcceo_product_prefix_choice_valuation_selected_bound + (bpr_choice_exponent_bpcceo_product_prefix_choice) = (n)) /\ (exists bpr_power_value_bpcceo_product_prefix_choice_valuation_selected. ((exists bpr_power_code_bpcceo_product_prefix_choice_valuation_selected_power bpr_power_scale_bpcceo_product_prefix_choice_valuation_selected_power. ((forall bpr_power_index_bpcceo_product_prefix_choice_valuation_selected_power. (exists bpr_gap_bpcceo_product_prefix_choice_valuation_selected_power_repeat_bound. bpr_gap_bpcceo_product_prefix_choice_valuation_selected_power_repeat_bound + S (bpr_power_index_bpcceo_product_prefix_choice_valuation_selected_power) = bpr_choice_exponent_bpcceo_product_prefix_choice) -> (((exists bpr_height_bpcceo_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_height_bpcceo_product_prefix_choice_valuation_selected_power_repeat_entry + S (S (bpr_prefix_index_bpcceo_product_prefix)) = S ((S (bpr_power_index_bpcceo_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcceo_product_prefix_choice_valuation_selected_power)) /\ exists bpr_quotient_bpcceo_product_prefix_choice_valuation_selected_power_repeat_entry. bpr_power_code_bpcceo_product_prefix_choice_valuation_selected_power = bpr_quotient_bpcceo_product_prefix_choice_valuation_selected_power_repeat_entry * S ((S (bpr_power_index_bpcceo_product_prefix_choice_valuation_selected_power)) * bpr_power_scale_bpcceo_product_prefix_choice_valuation_selected_power) + (S (bpr_prefix_index_bpcceo_product_prefix))))) /\ (exists ff_u_bpcceo_product_prefix_choice_valuation_selected_power_product ff_v_bpcceo_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcceo_product_prefix_choice_valuation_selected_power_product_start. ff_h_bpcceo_product_prefix_choice_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bpcceo_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_valuation_selected_power_product_start. ff_u_bpcceo_product_prefix_choice_valuation_selected_power_product = ff_q_bpcceo_product_prefix_choice_valuation_selected_power_product_start * S ((S (0)) * ff_v_bpcceo_product_prefix_choice_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bpcceo_product_prefix_choice_valuation_selected_power_product_terminal. ff_h_bpcceo_product_prefix_choice_valuation_selected_power_product_terminal + S (bpr_power_value_bpcceo_product_prefix_choice_valuation_selected) = S ((S (bpr_choice_exponent_bpcceo_product_prefix_choice)) * ff_v_bpcceo_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_valuation_selected_power_product_terminal. ff_u_bpcceo_product_prefix_choice_valuation_selected_power_product = ff_q_bpcceo_product_prefix_choice_valuation_selected_power_product_terminal * S ((S (bpr_choice_exponent_bpcceo_product_prefix_choice)) * ff_v_bpcceo_product_prefix_choice_valuation_selected_power_product) + (bpr_power_value_bpcceo_product_prefix_choice_valuation_selected))) /\ forall ff_i_bpcceo_product_prefix_choice_valuation_selected_power_product. (exists ff_lt_bpcceo_product_prefix_choice_valuation_selected_power_product_bound. ff_lt_bpcceo_product_prefix_choice_valuation_selected_power_product_bound + S ff_i_bpcceo_product_prefix_choice_valuation_selected_power_product = bpr_choice_exponent_bpcceo_product_prefix_choice) -> exists ff_p_bpcceo_product_prefix_choice_valuation_selected_power_product ff_r_bpcceo_product_prefix_choice_valuation_selected_power_product ff_s_bpcceo_product_prefix_choice_valuation_selected_power_product. ((((exists ff_h_bpcceo_product_prefix_choice_valuation_selected_power_product_factor. ff_h_bpcceo_product_prefix_choice_valuation_selected_power_product_factor + S (ff_p_bpcceo_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcceo_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcceo_product_prefix_choice_valuation_selected_power)) /\ exists ff_q_bpcceo_product_prefix_choice_valuation_selected_power_product_factor. bpr_power_code_bpcceo_product_prefix_choice_valuation_selected_power = ff_q_bpcceo_product_prefix_choice_valuation_selected_power_product_factor * S ((S (ff_i_bpcceo_product_prefix_choice_valuation_selected_power_product)) * bpr_power_scale_bpcceo_product_prefix_choice_valuation_selected_power) + (ff_p_bpcceo_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcceo_product_prefix_choice_valuation_selected_power_product_partial. ff_h_bpcceo_product_prefix_choice_valuation_selected_power_product_partial + S (ff_r_bpcceo_product_prefix_choice_valuation_selected_power_product) = S ((S (ff_i_bpcceo_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcceo_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_valuation_selected_power_product_partial. ff_u_bpcceo_product_prefix_choice_valuation_selected_power_product = ff_q_bpcceo_product_prefix_choice_valuation_selected_power_product_partial * S ((S (ff_i_bpcceo_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcceo_product_prefix_choice_valuation_selected_power_product) + (ff_r_bpcceo_product_prefix_choice_valuation_selected_power_product))) /\ ((((exists ff_h_bpcceo_product_prefix_choice_valuation_selected_power_product_successor. ff_h_bpcceo_product_prefix_choice_valuation_selected_power_product_successor + S (ff_s_bpcceo_product_prefix_choice_valuation_selected_power_product) = S ((S (S ff_i_bpcceo_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcceo_product_prefix_choice_valuation_selected_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_valuation_selected_power_product_successor. ff_u_bpcceo_product_prefix_choice_valuation_selected_power_product = ff_q_bpcceo_product_prefix_choice_valuation_selected_power_product_successor * S ((S (S ff_i_bpcceo_product_prefix_choice_valuation_selected_power_product)) * ff_v_bpcceo_product_prefix_choice_valuation_selected_power_product) + (ff_s_bpcceo_product_prefix_choice_valuation_selected_power_product))) /\ ff_s_bpcceo_product_prefix_choice_valuation_selected_power_product = ff_r_bpcceo_product_prefix_choice_valuation_selected_power_product * ff_p_bpcceo_product_prefix_choice_valuation_selected_power_product)))))))) /\ (exists bpr_divides_quotient_bpcceo_product_prefix_choice_valuation_selected_divides. n = (bpr_power_value_bpcceo_product_prefix_choice_valuation_selected) * bpr_divides_quotient_bpcceo_product_prefix_choice_valuation_selected_divides)))) /\ forall bpr_valuation_candidate_bpcceo_product_prefix_choice_valuation. (exists bpr_le_gap_bpcceo_product_prefix_choice_valuation_candidate_bound. bpr_le_gap_bpcceo_product_prefix_choice_valuation_candidate_bound + (bpr_valuation_candidate_bpcceo_product_prefix_choice_valuation) = (n)) -> (exists bpr_power_value_bpcceo_product_prefix_choice_valuation_candidate. ((exists bpr_power_code_bpcceo_product_prefix_choice_valuation_candidate_power bpr_power_scale_bpcceo_product_prefix_choice_valuation_candidate_power. ((forall bpr_power_index_bpcceo_product_prefix_choice_valuation_candidate_power. (exists bpr_gap_bpcceo_product_prefix_choice_valuation_candidate_power_repeat_bound. bpr_gap_bpcceo_product_prefix_choice_valuation_candidate_power_repeat_bound + S (bpr_power_index_bpcceo_product_prefix_choice_valuation_candidate_power) = bpr_valuation_candidate_bpcceo_product_prefix_choice_valuation) -> (((exists bpr_height_bpcceo_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_height_bpcceo_product_prefix_choice_valuation_candidate_power_repeat_entry + S (S (bpr_prefix_index_bpcceo_product_prefix)) = S ((S (bpr_power_index_bpcceo_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcceo_product_prefix_choice_valuation_candidate_power)) /\ exists bpr_quotient_bpcceo_product_prefix_choice_valuation_candidate_power_repeat_entry. bpr_power_code_bpcceo_product_prefix_choice_valuation_candidate_power = bpr_quotient_bpcceo_product_prefix_choice_valuation_candidate_power_repeat_entry * S ((S (bpr_power_index_bpcceo_product_prefix_choice_valuation_candidate_power)) * bpr_power_scale_bpcceo_product_prefix_choice_valuation_candidate_power) + (S (bpr_prefix_index_bpcceo_product_prefix))))) /\ (exists ff_u_bpcceo_product_prefix_choice_valuation_candidate_power_product ff_v_bpcceo_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcceo_product_prefix_choice_valuation_candidate_power_product_start. ff_h_bpcceo_product_prefix_choice_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bpcceo_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_valuation_candidate_power_product_start. ff_u_bpcceo_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcceo_product_prefix_choice_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bpcceo_product_prefix_choice_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bpcceo_product_prefix_choice_valuation_candidate_power_product_terminal. ff_h_bpcceo_product_prefix_choice_valuation_candidate_power_product_terminal + S (bpr_power_value_bpcceo_product_prefix_choice_valuation_candidate) = S ((S (bpr_valuation_candidate_bpcceo_product_prefix_choice_valuation)) * ff_v_bpcceo_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_valuation_candidate_power_product_terminal. ff_u_bpcceo_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcceo_product_prefix_choice_valuation_candidate_power_product_terminal * S ((S (bpr_valuation_candidate_bpcceo_product_prefix_choice_valuation)) * ff_v_bpcceo_product_prefix_choice_valuation_candidate_power_product) + (bpr_power_value_bpcceo_product_prefix_choice_valuation_candidate))) /\ forall ff_i_bpcceo_product_prefix_choice_valuation_candidate_power_product. (exists ff_lt_bpcceo_product_prefix_choice_valuation_candidate_power_product_bound. ff_lt_bpcceo_product_prefix_choice_valuation_candidate_power_product_bound + S ff_i_bpcceo_product_prefix_choice_valuation_candidate_power_product = bpr_valuation_candidate_bpcceo_product_prefix_choice_valuation) -> exists ff_p_bpcceo_product_prefix_choice_valuation_candidate_power_product ff_r_bpcceo_product_prefix_choice_valuation_candidate_power_product ff_s_bpcceo_product_prefix_choice_valuation_candidate_power_product. ((((exists ff_h_bpcceo_product_prefix_choice_valuation_candidate_power_product_factor. ff_h_bpcceo_product_prefix_choice_valuation_candidate_power_product_factor + S (ff_p_bpcceo_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcceo_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcceo_product_prefix_choice_valuation_candidate_power)) /\ exists ff_q_bpcceo_product_prefix_choice_valuation_candidate_power_product_factor. bpr_power_code_bpcceo_product_prefix_choice_valuation_candidate_power = ff_q_bpcceo_product_prefix_choice_valuation_candidate_power_product_factor * S ((S (ff_i_bpcceo_product_prefix_choice_valuation_candidate_power_product)) * bpr_power_scale_bpcceo_product_prefix_choice_valuation_candidate_power) + (ff_p_bpcceo_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcceo_product_prefix_choice_valuation_candidate_power_product_partial. ff_h_bpcceo_product_prefix_choice_valuation_candidate_power_product_partial + S (ff_r_bpcceo_product_prefix_choice_valuation_candidate_power_product) = S ((S (ff_i_bpcceo_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcceo_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_valuation_candidate_power_product_partial. ff_u_bpcceo_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcceo_product_prefix_choice_valuation_candidate_power_product_partial * S ((S (ff_i_bpcceo_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcceo_product_prefix_choice_valuation_candidate_power_product) + (ff_r_bpcceo_product_prefix_choice_valuation_candidate_power_product))) /\ ((((exists ff_h_bpcceo_product_prefix_choice_valuation_candidate_power_product_successor. ff_h_bpcceo_product_prefix_choice_valuation_candidate_power_product_successor + S (ff_s_bpcceo_product_prefix_choice_valuation_candidate_power_product) = S ((S (S ff_i_bpcceo_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcceo_product_prefix_choice_valuation_candidate_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_valuation_candidate_power_product_successor. ff_u_bpcceo_product_prefix_choice_valuation_candidate_power_product = ff_q_bpcceo_product_prefix_choice_valuation_candidate_power_product_successor * S ((S (S ff_i_bpcceo_product_prefix_choice_valuation_candidate_power_product)) * ff_v_bpcceo_product_prefix_choice_valuation_candidate_power_product) + (ff_s_bpcceo_product_prefix_choice_valuation_candidate_power_product))) /\ ff_s_bpcceo_product_prefix_choice_valuation_candidate_power_product = ff_r_bpcceo_product_prefix_choice_valuation_candidate_power_product * ff_p_bpcceo_product_prefix_choice_valuation_candidate_power_product)))))))) /\ (exists bpr_divides_quotient_bpcceo_product_prefix_choice_valuation_candidate_divides. n = (bpr_power_value_bpcceo_product_prefix_choice_valuation_candidate) * bpr_divides_quotient_bpcceo_product_prefix_choice_valuation_candidate_divides))) -> (exists bpr_le_gap_bpcceo_product_prefix_choice_valuation_candidate_below. bpr_le_gap_bpcceo_product_prefix_choice_valuation_candidate_below + (bpr_valuation_candidate_bpcceo_product_prefix_choice_valuation) = (bpr_choice_exponent_bpcceo_product_prefix_choice))) /\ (exists bpr_power_code_bpcceo_product_prefix_choice_power bpr_power_scale_bpcceo_product_prefix_choice_power. ((forall bpr_power_index_bpcceo_product_prefix_choice_power. (exists bpr_gap_bpcceo_product_prefix_choice_power_repeat_bound. bpr_gap_bpcceo_product_prefix_choice_power_repeat_bound + S (bpr_power_index_bpcceo_product_prefix_choice_power) = bpr_choice_exponent_bpcceo_product_prefix_choice) -> (((exists bpr_height_bpcceo_product_prefix_choice_power_repeat_entry. bpr_height_bpcceo_product_prefix_choice_power_repeat_entry + S (S (bpr_prefix_index_bpcceo_product_prefix)) = S ((S (bpr_power_index_bpcceo_product_prefix_choice_power)) * bpr_power_scale_bpcceo_product_prefix_choice_power)) /\ exists bpr_quotient_bpcceo_product_prefix_choice_power_repeat_entry. bpr_power_code_bpcceo_product_prefix_choice_power = bpr_quotient_bpcceo_product_prefix_choice_power_repeat_entry * S ((S (bpr_power_index_bpcceo_product_prefix_choice_power)) * bpr_power_scale_bpcceo_product_prefix_choice_power) + (S (bpr_prefix_index_bpcceo_product_prefix))))) /\ (exists ff_u_bpcceo_product_prefix_choice_power_product ff_v_bpcceo_product_prefix_choice_power_product. ((((exists ff_h_bpcceo_product_prefix_choice_power_product_start. ff_h_bpcceo_product_prefix_choice_power_product_start + S (1) = S ((S (0)) * ff_v_bpcceo_product_prefix_choice_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_power_product_start. ff_u_bpcceo_product_prefix_choice_power_product = ff_q_bpcceo_product_prefix_choice_power_product_start * S ((S (0)) * ff_v_bpcceo_product_prefix_choice_power_product) + (1))) /\ ((((exists ff_h_bpcceo_product_prefix_choice_power_product_terminal. ff_h_bpcceo_product_prefix_choice_power_product_terminal + S (bpr_prefix_value_bpcceo_product_prefix) = S ((S (bpr_choice_exponent_bpcceo_product_prefix_choice)) * ff_v_bpcceo_product_prefix_choice_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_power_product_terminal. ff_u_bpcceo_product_prefix_choice_power_product = ff_q_bpcceo_product_prefix_choice_power_product_terminal * S ((S (bpr_choice_exponent_bpcceo_product_prefix_choice)) * ff_v_bpcceo_product_prefix_choice_power_product) + (bpr_prefix_value_bpcceo_product_prefix))) /\ forall ff_i_bpcceo_product_prefix_choice_power_product. (exists ff_lt_bpcceo_product_prefix_choice_power_product_bound. ff_lt_bpcceo_product_prefix_choice_power_product_bound + S ff_i_bpcceo_product_prefix_choice_power_product = bpr_choice_exponent_bpcceo_product_prefix_choice) -> exists ff_p_bpcceo_product_prefix_choice_power_product ff_r_bpcceo_product_prefix_choice_power_product ff_s_bpcceo_product_prefix_choice_power_product. ((((exists ff_h_bpcceo_product_prefix_choice_power_product_factor. ff_h_bpcceo_product_prefix_choice_power_product_factor + S (ff_p_bpcceo_product_prefix_choice_power_product) = S ((S (ff_i_bpcceo_product_prefix_choice_power_product)) * bpr_power_scale_bpcceo_product_prefix_choice_power)) /\ exists ff_q_bpcceo_product_prefix_choice_power_product_factor. bpr_power_code_bpcceo_product_prefix_choice_power = ff_q_bpcceo_product_prefix_choice_power_product_factor * S ((S (ff_i_bpcceo_product_prefix_choice_power_product)) * bpr_power_scale_bpcceo_product_prefix_choice_power) + (ff_p_bpcceo_product_prefix_choice_power_product))) /\ ((((exists ff_h_bpcceo_product_prefix_choice_power_product_partial. ff_h_bpcceo_product_prefix_choice_power_product_partial + S (ff_r_bpcceo_product_prefix_choice_power_product) = S ((S (ff_i_bpcceo_product_prefix_choice_power_product)) * ff_v_bpcceo_product_prefix_choice_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_power_product_partial. ff_u_bpcceo_product_prefix_choice_power_product = ff_q_bpcceo_product_prefix_choice_power_product_partial * S ((S (ff_i_bpcceo_product_prefix_choice_power_product)) * ff_v_bpcceo_product_prefix_choice_power_product) + (ff_r_bpcceo_product_prefix_choice_power_product))) /\ ((((exists ff_h_bpcceo_product_prefix_choice_power_product_successor. ff_h_bpcceo_product_prefix_choice_power_product_successor + S (ff_s_bpcceo_product_prefix_choice_power_product) = S ((S (S ff_i_bpcceo_product_prefix_choice_power_product)) * ff_v_bpcceo_product_prefix_choice_power_product)) /\ exists ff_q_bpcceo_product_prefix_choice_power_product_successor. ff_u_bpcceo_product_prefix_choice_power_product = ff_q_bpcceo_product_prefix_choice_power_product_successor * S ((S (S ff_i_bpcceo_product_prefix_choice_power_product)) * ff_v_bpcceo_product_prefix_choice_power_product) + (ff_s_bpcceo_product_prefix_choice_power_product))) /\ ff_s_bpcceo_product_prefix_choice_power_product = ff_r_bpcceo_product_prefix_choice_power_product * ff_p_bpcceo_product_prefix_choice_power_product)))))))))) \/ (~((~(S (bpr_prefix_index_bpcceo_product_prefix) = 1) /\ forall bpr_left_bpcceo_product_prefix_choice_prime bpr_right_bpcceo_product_prefix_choice_prime. S (bpr_prefix_index_bpcceo_product_prefix) = bpr_left_bpcceo_product_prefix_choice_prime * bpr_right_bpcceo_product_prefix_choice_prime -> bpr_left_bpcceo_product_prefix_choice_prime = 1 \/ bpr_right_bpcceo_product_prefix_choice_prime = 1)) /\ bpr_prefix_value_bpcceo_product_prefix = 1))))) /\ (exists ff_u_bpcceo_product_product ff_v_bpcceo_product_product. ((((exists ff_h_bpcceo_product_product_start. ff_h_bpcceo_product_product_start + S (1) = S ((S (0)) * ff_v_bpcceo_product_product)) /\ exists ff_q_bpcceo_product_product_start. ff_u_bpcceo_product_product = ff_q_bpcceo_product_product_start * S ((S (0)) * ff_v_bpcceo_product_product) + (1))) /\ ((((exists ff_h_bpcceo_product_product_terminal. ff_h_bpcceo_product_product_terminal + S (z) = S ((S (m)) * ff_v_bpcceo_product_product)) /\ exists ff_q_bpcceo_product_product_terminal. ff_u_bpcceo_product_product = ff_q_bpcceo_product_product_terminal * S ((S (m)) * ff_v_bpcceo_product_product) + (z))) /\ forall ff_i_bpcceo_product_product. (exists ff_lt_bpcceo_product_product_bound. ff_lt_bpcceo_product_product_bound + S ff_i_bpcceo_product_product = m) -> exists ff_p_bpcceo_product_product ff_r_bpcceo_product_product ff_s_bpcceo_product_product. ((((exists ff_h_bpcceo_product_product_factor. ff_h_bpcceo_product_product_factor + S (ff_p_bpcceo_product_product) = S ((S (ff_i_bpcceo_product_product)) * bpr_product_scale_bpcceo_product)) /\ exists ff_q_bpcceo_product_product_factor. bpr_product_code_bpcceo_product = ff_q_bpcceo_product_product_factor * S ((S (ff_i_bpcceo_product_product)) * bpr_product_scale_bpcceo_product) + (ff_p_bpcceo_product_product))) /\ ((((exists ff_h_bpcceo_product_product_partial. ff_h_bpcceo_product_product_partial + S (ff_r_bpcceo_product_product) = S ((S (ff_i_bpcceo_product_product)) * ff_v_bpcceo_product_product)) /\ exists ff_q_bpcceo_product_product_partial. ff_u_bpcceo_product_product = ff_q_bpcceo_product_product_partial * S ((S (ff_i_bpcceo_product_product)) * ff_v_bpcceo_product_product) + (ff_r_bpcceo_product_product))) /\ ((((exists ff_h_bpcceo_product_product_successor. ff_h_bpcceo_product_product_successor + S (ff_s_bpcceo_product_product) = S ((S (S ff_i_bpcceo_product_product)) * ff_v_bpcceo_product_product)) /\ exists ff_q_bpcceo_product_product_successor. ff_u_bpcceo_product_product = ff_q_bpcceo_product_product_successor * S ((S (S ff_i_bpcceo_product_product)) * ff_v_bpcceo_product_product) + (ff_s_bpcceo_product_product))) /\ ff_s_bpcceo_product_product = ff_r_bpcceo_product_product * ff_p_bpcceo_product_product)))))))) -> n = z * q -> q = 1

Proof neighborhood

Direct theorem prerequisites

BT003A eq_decidable BT003L prime_divisor_exists BT0102 prime_contribution_cofactor_prime_contradiction

Direct theorem dependents

BT0104 prime_contribution_reverse_divides

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

41 script commands · 9 reading checkpoints · 3 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 (3)
eq decidableprime divisor existsprime contribution cofactor prime contradiction
01Fix variables and assumptionsL1–8

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 hn
  6. L6
    intro hsupport
  7. L7
    intro hproduct
  8. L8
    intro hfactor
02Establish hcasesL9–12

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

  1. L9
    have hcases : q = 1 \/ ~(q = 1)
  2. L10
    specialize eq_decidable q
  3. L11
    specialize eq_decidable 1
  4. L12
    exact eq_decidable
03Separate the logical casesL13–13

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

  1. L13
    cases hcases
04Use earlier factsL14–14

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

  1. L14
    exact hcases_left
05Establish hq0L15–21

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

  1. L15
    have hq0 : ~(q = 0)
  2. L16
    intro hqzero
  3. L17
    apply hn
  4. L18
    trans z * q
  5. L19
    exact hfactor
  6. L20
    rewrite hqzero
  7. L21
    apply PA5
06Establish hprimeL22–26

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

  1. L22
    have hprime : ∃ p. Prime(p) ∧ Dvd(p,q)Definitions: Prime(p)Dvd(p,q)Original native command in the exact edition
  2. L23
    specialize prime_divisor_exists q
  3. L24
    apply prime_divisor_exists
  4. L25
    exact hq0
  5. L26
    exact hcases_right
07Separate the logical casesL27–29

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

  1. L27
    cases hprime
  2. L28
    cases hprime_witness
  3. L29
    exfalso
08Use earlier factsL30–39

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

  1. L30
    specialize prime_contribution_cofactor_prime_contradiction n
  2. L31
    specialize prime_contribution_cofactor_prime_contradiction m
  3. L32
    specialize prime_contribution_cofactor_prime_contradiction z
  4. L33
    specialize prime_contribution_cofactor_prime_contradiction q
  5. L34
    specialize prime_contribution_cofactor_prime_contradiction x
  6. L35
    apply prime_contribution_cofactor_prime_contradiction
  7. L36
    exact hn
  8. L37
    exact hsupport
  9. L38
    exact hproduct
  10. L39
    exact hfactor
09Use earlier factsL40–41

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

  1. L40
    exact hprime_witness_left
  2. L41
    exact hprime_witness_right

Library-wide reading audit

Original defined command ledger · 41 lines
  1. 0001intro n
  2. 0002intro m
  3. 0003intro z
  4. 0004intro q
  5. 0005intro hn
  6. 0006intro hsupport
  7. 0007intro hproduct
  8. 0008intro hfactor
  9. 0009have hcases : q = 1 \/ ~(q = 1)
  10. 0010specialize eq_decidable q
  11. 0011specialize eq_decidable 1
  12. 0012exact eq_decidable
  13. 0013cases hcases
  14. 0014exact hcases_left
  15. 0015have hq0 : ~(q = 0)
  16. 0016intro hqzero
  17. 0017apply hn
  18. 0018trans z * q
  19. 0019exact hfactor
  20. 0020rewrite hqzero
  21. 0021apply PA5
  22. 0022have hprime : ∃ p. Prime(p) ∧ Dvd(p,q)
    Exact native replay linehave hprime : exists p. ((~(p = 1) /\ forall bpr_left_bpcceo_prime bpr_right_bpcceo_prime. p = bpr_left_bpcceo_prime * bpr_right_bpcceo_prime -> bpr_left_bpcceo_prime = 1 \/ bpr_right_bpcceo_prime = 1)) /\ (exists bpr_divides_quotient_bpcceo_divides. q = (p) * bpr_divides_quotient_bpcceo_divides)
  23. 0023specialize prime_divisor_exists q
  24. 0024apply prime_divisor_exists
  25. 0025exact hq0
  26. 0026exact hcases_right
  27. 0027cases hprime
  28. 0028cases hprime_witness
  29. 0029exfalso
  30. 0030specialize prime_contribution_cofactor_prime_contradiction n
  31. 0031specialize prime_contribution_cofactor_prime_contradiction m
  32. 0032specialize prime_contribution_cofactor_prime_contradiction z
  33. 0033specialize prime_contribution_cofactor_prime_contradiction q
  34. 0034specialize prime_contribution_cofactor_prime_contradiction x
  35. 0035apply prime_contribution_cofactor_prime_contradiction
  36. 0036exact hn
  37. 0037exact hsupport
  38. 0038exact hproduct
  39. 0039exact hfactor
  40. 0040exact hprime_witness_left
  41. 0041exact hprime_witness_right