BT00T1 · Bertrand theorem

prime_factorial_valuation_eq_legendre_sum

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

At every prime, the factorial valuation exponent equals the finite Legendre sum.

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

∀ p. ∀ n. ∀ a. ∀ b. Prime(p) → FactorialValuation(p,n,a) → LegendreSum(p,n,b) → a = b

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

PD0004 Prime PD0048 FactorialValuation PD0050 LegendreSum

3 occurrences

In local proof propositions

PD0046 PowerValuation PD0048 FactorialValuation PD0050 LegendreSum

3 occurrences

Exact expanded native-PA statement
forall p n a b. ((~(p = 1) /\ forall frm_prime_left_blfg_equality_prime frm_prime_right_blfg_equality_prime. p = frm_prime_left_blfg_equality_prime * frm_prime_right_blfg_equality_prime -> frm_prime_left_blfg_equality_prime = 1 \/ frm_prime_right_blfg_equality_prime = 1)) -> (exists bfv_factorial_blfg_equality_factorial. ((exists ff_b_blfg_equality_factorial_factorial ff_c_blfg_equality_factorial_factorial. ((forall ff_i_blfg_equality_factorial_factorial_range. (exists ff_lt_blfg_equality_factorial_factorial_range_bound. ff_lt_blfg_equality_factorial_factorial_range_bound + S ff_i_blfg_equality_factorial_factorial_range = n) -> (((exists ff_h_blfg_equality_factorial_factorial_range_decoded. ff_h_blfg_equality_factorial_factorial_range_decoded + S (1 + ff_i_blfg_equality_factorial_factorial_range) = S ((S (ff_i_blfg_equality_factorial_factorial_range)) * ff_c_blfg_equality_factorial_factorial)) /\ exists ff_q_blfg_equality_factorial_factorial_range_decoded. ff_b_blfg_equality_factorial_factorial = ff_q_blfg_equality_factorial_factorial_range_decoded * S ((S (ff_i_blfg_equality_factorial_factorial_range)) * ff_c_blfg_equality_factorial_factorial) + (1 + ff_i_blfg_equality_factorial_factorial_range)))) /\ (exists ff_u_blfg_equality_factorial_factorial_product ff_v_blfg_equality_factorial_factorial_product. ((((exists ff_h_blfg_equality_factorial_factorial_product_start. ff_h_blfg_equality_factorial_factorial_product_start + S (1) = S ((S (0)) * ff_v_blfg_equality_factorial_factorial_product)) /\ exists ff_q_blfg_equality_factorial_factorial_product_start. ff_u_blfg_equality_factorial_factorial_product = ff_q_blfg_equality_factorial_factorial_product_start * S ((S (0)) * ff_v_blfg_equality_factorial_factorial_product) + (1))) /\ ((((exists ff_h_blfg_equality_factorial_factorial_product_terminal. ff_h_blfg_equality_factorial_factorial_product_terminal + S (bfv_factorial_blfg_equality_factorial) = S ((S (n)) * ff_v_blfg_equality_factorial_factorial_product)) /\ exists ff_q_blfg_equality_factorial_factorial_product_terminal. ff_u_blfg_equality_factorial_factorial_product = ff_q_blfg_equality_factorial_factorial_product_terminal * S ((S (n)) * ff_v_blfg_equality_factorial_factorial_product) + (bfv_factorial_blfg_equality_factorial))) /\ forall ff_i_blfg_equality_factorial_factorial_product. (exists ff_lt_blfg_equality_factorial_factorial_product_bound. ff_lt_blfg_equality_factorial_factorial_product_bound + S ff_i_blfg_equality_factorial_factorial_product = n) -> exists ff_p_blfg_equality_factorial_factorial_product ff_r_blfg_equality_factorial_factorial_product ff_s_blfg_equality_factorial_factorial_product. ((((exists ff_h_blfg_equality_factorial_factorial_product_factor. ff_h_blfg_equality_factorial_factorial_product_factor + S (ff_p_blfg_equality_factorial_factorial_product) = S ((S (ff_i_blfg_equality_factorial_factorial_product)) * ff_c_blfg_equality_factorial_factorial)) /\ exists ff_q_blfg_equality_factorial_factorial_product_factor. ff_b_blfg_equality_factorial_factorial = ff_q_blfg_equality_factorial_factorial_product_factor * S ((S (ff_i_blfg_equality_factorial_factorial_product)) * ff_c_blfg_equality_factorial_factorial) + (ff_p_blfg_equality_factorial_factorial_product))) /\ ((((exists ff_h_blfg_equality_factorial_factorial_product_partial. ff_h_blfg_equality_factorial_factorial_product_partial + S (ff_r_blfg_equality_factorial_factorial_product) = S ((S (ff_i_blfg_equality_factorial_factorial_product)) * ff_v_blfg_equality_factorial_factorial_product)) /\ exists ff_q_blfg_equality_factorial_factorial_product_partial. ff_u_blfg_equality_factorial_factorial_product = ff_q_blfg_equality_factorial_factorial_product_partial * S ((S (ff_i_blfg_equality_factorial_factorial_product)) * ff_v_blfg_equality_factorial_factorial_product) + (ff_r_blfg_equality_factorial_factorial_product))) /\ ((((exists ff_h_blfg_equality_factorial_factorial_product_successor. ff_h_blfg_equality_factorial_factorial_product_successor + S (ff_s_blfg_equality_factorial_factorial_product) = S ((S (S ff_i_blfg_equality_factorial_factorial_product)) * ff_v_blfg_equality_factorial_factorial_product)) /\ exists ff_q_blfg_equality_factorial_factorial_product_successor. ff_u_blfg_equality_factorial_factorial_product = ff_q_blfg_equality_factorial_factorial_product_successor * S ((S (S ff_i_blfg_equality_factorial_factorial_product)) * ff_v_blfg_equality_factorial_factorial_product) + (ff_s_blfg_equality_factorial_factorial_product))) /\ ff_s_blfg_equality_factorial_factorial_product = ff_r_blfg_equality_factorial_factorial_product * ff_p_blfg_equality_factorial_factorial_product)))))))) /\ (((exists bpv_gap_blfg_equality_factorial_valuation_exponent_bound. bpv_gap_blfg_equality_factorial_valuation_exponent_bound + a = bfv_factorial_blfg_equality_factorial) /\ (exists bpv_result_blfg_equality_factorial_valuation_selected. ((exists ff_b_blfg_equality_factorial_valuation_selected_power ff_c_blfg_equality_factorial_valuation_selected_power. ((forall ff_i_blfg_equality_factorial_valuation_selected_power_repeat. (exists ff_lt_blfg_equality_factorial_valuation_selected_power_repeat_bound. ff_lt_blfg_equality_factorial_valuation_selected_power_repeat_bound + S ff_i_blfg_equality_factorial_valuation_selected_power_repeat = a) -> (((exists ff_h_blfg_equality_factorial_valuation_selected_power_repeat_decoded. ff_h_blfg_equality_factorial_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_blfg_equality_factorial_valuation_selected_power_repeat)) * ff_c_blfg_equality_factorial_valuation_selected_power)) /\ exists ff_q_blfg_equality_factorial_valuation_selected_power_repeat_decoded. ff_b_blfg_equality_factorial_valuation_selected_power = ff_q_blfg_equality_factorial_valuation_selected_power_repeat_decoded * S ((S (ff_i_blfg_equality_factorial_valuation_selected_power_repeat)) * ff_c_blfg_equality_factorial_valuation_selected_power) + (p)))) /\ (exists ff_u_blfg_equality_factorial_valuation_selected_power_product ff_v_blfg_equality_factorial_valuation_selected_power_product. ((((exists ff_h_blfg_equality_factorial_valuation_selected_power_product_start. ff_h_blfg_equality_factorial_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_blfg_equality_factorial_valuation_selected_power_product)) /\ exists ff_q_blfg_equality_factorial_valuation_selected_power_product_start. ff_u_blfg_equality_factorial_valuation_selected_power_product = ff_q_blfg_equality_factorial_valuation_selected_power_product_start * S ((S (0)) * ff_v_blfg_equality_factorial_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_blfg_equality_factorial_valuation_selected_power_product_terminal. ff_h_blfg_equality_factorial_valuation_selected_power_product_terminal + S (bpv_result_blfg_equality_factorial_valuation_selected) = S ((S (a)) * ff_v_blfg_equality_factorial_valuation_selected_power_product)) /\ exists ff_q_blfg_equality_factorial_valuation_selected_power_product_terminal. ff_u_blfg_equality_factorial_valuation_selected_power_product = ff_q_blfg_equality_factorial_valuation_selected_power_product_terminal * S ((S (a)) * ff_v_blfg_equality_factorial_valuation_selected_power_product) + (bpv_result_blfg_equality_factorial_valuation_selected))) /\ forall ff_i_blfg_equality_factorial_valuation_selected_power_product. (exists ff_lt_blfg_equality_factorial_valuation_selected_power_product_bound. ff_lt_blfg_equality_factorial_valuation_selected_power_product_bound + S ff_i_blfg_equality_factorial_valuation_selected_power_product = a) -> exists ff_p_blfg_equality_factorial_valuation_selected_power_product ff_r_blfg_equality_factorial_valuation_selected_power_product ff_s_blfg_equality_factorial_valuation_selected_power_product. ((((exists ff_h_blfg_equality_factorial_valuation_selected_power_product_factor. ff_h_blfg_equality_factorial_valuation_selected_power_product_factor + S (ff_p_blfg_equality_factorial_valuation_selected_power_product) = S ((S (ff_i_blfg_equality_factorial_valuation_selected_power_product)) * ff_c_blfg_equality_factorial_valuation_selected_power)) /\ exists ff_q_blfg_equality_factorial_valuation_selected_power_product_factor. ff_b_blfg_equality_factorial_valuation_selected_power = ff_q_blfg_equality_factorial_valuation_selected_power_product_factor * S ((S (ff_i_blfg_equality_factorial_valuation_selected_power_product)) * ff_c_blfg_equality_factorial_valuation_selected_power) + (ff_p_blfg_equality_factorial_valuation_selected_power_product))) /\ ((((exists ff_h_blfg_equality_factorial_valuation_selected_power_product_partial. ff_h_blfg_equality_factorial_valuation_selected_power_product_partial + S (ff_r_blfg_equality_factorial_valuation_selected_power_product) = S ((S (ff_i_blfg_equality_factorial_valuation_selected_power_product)) * ff_v_blfg_equality_factorial_valuation_selected_power_product)) /\ exists ff_q_blfg_equality_factorial_valuation_selected_power_product_partial. ff_u_blfg_equality_factorial_valuation_selected_power_product = ff_q_blfg_equality_factorial_valuation_selected_power_product_partial * S ((S (ff_i_blfg_equality_factorial_valuation_selected_power_product)) * ff_v_blfg_equality_factorial_valuation_selected_power_product) + (ff_r_blfg_equality_factorial_valuation_selected_power_product))) /\ ((((exists ff_h_blfg_equality_factorial_valuation_selected_power_product_successor. ff_h_blfg_equality_factorial_valuation_selected_power_product_successor + S (ff_s_blfg_equality_factorial_valuation_selected_power_product) = S ((S (S ff_i_blfg_equality_factorial_valuation_selected_power_product)) * ff_v_blfg_equality_factorial_valuation_selected_power_product)) /\ exists ff_q_blfg_equality_factorial_valuation_selected_power_product_successor. ff_u_blfg_equality_factorial_valuation_selected_power_product = ff_q_blfg_equality_factorial_valuation_selected_power_product_successor * S ((S (S ff_i_blfg_equality_factorial_valuation_selected_power_product)) * ff_v_blfg_equality_factorial_valuation_selected_power_product) + (ff_s_blfg_equality_factorial_valuation_selected_power_product))) /\ ff_s_blfg_equality_factorial_valuation_selected_power_product = ff_r_blfg_equality_factorial_valuation_selected_power_product * ff_p_blfg_equality_factorial_valuation_selected_power_product)))))))) /\ (exists bpv_factor_blfg_equality_factorial_valuation_selected_divides. bfv_factorial_blfg_equality_factorial = bpv_result_blfg_equality_factorial_valuation_selected * bpv_factor_blfg_equality_factorial_valuation_selected_divides)))) /\ forall bpv_candidate_blfg_equality_factorial_valuation. (exists bpv_gap_blfg_equality_factorial_valuation_candidate_bound. bpv_gap_blfg_equality_factorial_valuation_candidate_bound + bpv_candidate_blfg_equality_factorial_valuation = bfv_factorial_blfg_equality_factorial) -> (exists bpv_result_blfg_equality_factorial_valuation_candidate. ((exists ff_b_blfg_equality_factorial_valuation_candidate_power ff_c_blfg_equality_factorial_valuation_candidate_power. ((forall ff_i_blfg_equality_factorial_valuation_candidate_power_repeat. (exists ff_lt_blfg_equality_factorial_valuation_candidate_power_repeat_bound. ff_lt_blfg_equality_factorial_valuation_candidate_power_repeat_bound + S ff_i_blfg_equality_factorial_valuation_candidate_power_repeat = bpv_candidate_blfg_equality_factorial_valuation) -> (((exists ff_h_blfg_equality_factorial_valuation_candidate_power_repeat_decoded. ff_h_blfg_equality_factorial_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_blfg_equality_factorial_valuation_candidate_power_repeat)) * ff_c_blfg_equality_factorial_valuation_candidate_power)) /\ exists ff_q_blfg_equality_factorial_valuation_candidate_power_repeat_decoded. ff_b_blfg_equality_factorial_valuation_candidate_power = ff_q_blfg_equality_factorial_valuation_candidate_power_repeat_decoded * S ((S (ff_i_blfg_equality_factorial_valuation_candidate_power_repeat)) * ff_c_blfg_equality_factorial_valuation_candidate_power) + (p)))) /\ (exists ff_u_blfg_equality_factorial_valuation_candidate_power_product ff_v_blfg_equality_factorial_valuation_candidate_power_product. ((((exists ff_h_blfg_equality_factorial_valuation_candidate_power_product_start. ff_h_blfg_equality_factorial_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_blfg_equality_factorial_valuation_candidate_power_product)) /\ exists ff_q_blfg_equality_factorial_valuation_candidate_power_product_start. ff_u_blfg_equality_factorial_valuation_candidate_power_product = ff_q_blfg_equality_factorial_valuation_candidate_power_product_start * S ((S (0)) * ff_v_blfg_equality_factorial_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_blfg_equality_factorial_valuation_candidate_power_product_terminal. ff_h_blfg_equality_factorial_valuation_candidate_power_product_terminal + S (bpv_result_blfg_equality_factorial_valuation_candidate) = S ((S (bpv_candidate_blfg_equality_factorial_valuation)) * ff_v_blfg_equality_factorial_valuation_candidate_power_product)) /\ exists ff_q_blfg_equality_factorial_valuation_candidate_power_product_terminal. ff_u_blfg_equality_factorial_valuation_candidate_power_product = ff_q_blfg_equality_factorial_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_blfg_equality_factorial_valuation)) * ff_v_blfg_equality_factorial_valuation_candidate_power_product) + (bpv_result_blfg_equality_factorial_valuation_candidate))) /\ forall ff_i_blfg_equality_factorial_valuation_candidate_power_product. (exists ff_lt_blfg_equality_factorial_valuation_candidate_power_product_bound. ff_lt_blfg_equality_factorial_valuation_candidate_power_product_bound + S ff_i_blfg_equality_factorial_valuation_candidate_power_product = bpv_candidate_blfg_equality_factorial_valuation) -> exists ff_p_blfg_equality_factorial_valuation_candidate_power_product ff_r_blfg_equality_factorial_valuation_candidate_power_product ff_s_blfg_equality_factorial_valuation_candidate_power_product. ((((exists ff_h_blfg_equality_factorial_valuation_candidate_power_product_factor. ff_h_blfg_equality_factorial_valuation_candidate_power_product_factor + S (ff_p_blfg_equality_factorial_valuation_candidate_power_product) = S ((S (ff_i_blfg_equality_factorial_valuation_candidate_power_product)) * ff_c_blfg_equality_factorial_valuation_candidate_power)) /\ exists ff_q_blfg_equality_factorial_valuation_candidate_power_product_factor. ff_b_blfg_equality_factorial_valuation_candidate_power = ff_q_blfg_equality_factorial_valuation_candidate_power_product_factor * S ((S (ff_i_blfg_equality_factorial_valuation_candidate_power_product)) * ff_c_blfg_equality_factorial_valuation_candidate_power) + (ff_p_blfg_equality_factorial_valuation_candidate_power_product))) /\ ((((exists ff_h_blfg_equality_factorial_valuation_candidate_power_product_partial. ff_h_blfg_equality_factorial_valuation_candidate_power_product_partial + S (ff_r_blfg_equality_factorial_valuation_candidate_power_product) = S ((S (ff_i_blfg_equality_factorial_valuation_candidate_power_product)) * ff_v_blfg_equality_factorial_valuation_candidate_power_product)) /\ exists ff_q_blfg_equality_factorial_valuation_candidate_power_product_partial. ff_u_blfg_equality_factorial_valuation_candidate_power_product = ff_q_blfg_equality_factorial_valuation_candidate_power_product_partial * S ((S (ff_i_blfg_equality_factorial_valuation_candidate_power_product)) * ff_v_blfg_equality_factorial_valuation_candidate_power_product) + (ff_r_blfg_equality_factorial_valuation_candidate_power_product))) /\ ((((exists ff_h_blfg_equality_factorial_valuation_candidate_power_product_successor. ff_h_blfg_equality_factorial_valuation_candidate_power_product_successor + S (ff_s_blfg_equality_factorial_valuation_candidate_power_product) = S ((S (S ff_i_blfg_equality_factorial_valuation_candidate_power_product)) * ff_v_blfg_equality_factorial_valuation_candidate_power_product)) /\ exists ff_q_blfg_equality_factorial_valuation_candidate_power_product_successor. ff_u_blfg_equality_factorial_valuation_candidate_power_product = ff_q_blfg_equality_factorial_valuation_candidate_power_product_successor * S ((S (S ff_i_blfg_equality_factorial_valuation_candidate_power_product)) * ff_v_blfg_equality_factorial_valuation_candidate_power_product) + (ff_s_blfg_equality_factorial_valuation_candidate_power_product))) /\ ff_s_blfg_equality_factorial_valuation_candidate_power_product = ff_r_blfg_equality_factorial_valuation_candidate_power_product * ff_p_blfg_equality_factorial_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_blfg_equality_factorial_valuation_candidate_divides. bfv_factorial_blfg_equality_factorial = bpv_result_blfg_equality_factorial_valuation_candidate * bpv_factor_blfg_equality_factorial_valuation_candidate_divides))) -> (exists bpv_gap_blfg_equality_factorial_valuation_maximal. bpv_gap_blfg_equality_factorial_valuation_maximal + bpv_candidate_blfg_equality_factorial_valuation = a)))) -> (exists bls_code_blfg_equality_legendre bls_scale_blfg_equality_legendre. ((forall bls_index_blfg_equality_legendre_prefix. (exists bls_gap_blfg_equality_legendre_prefix_bound. bls_gap_blfg_equality_legendre_prefix_bound + S (bls_index_blfg_equality_legendre_prefix) = (n)) -> exists bls_power_blfg_equality_legendre_prefix bls_quotient_blfg_equality_legendre_prefix bls_remainder_blfg_equality_legendre_prefix. ((exists bpvi_b_bls_blfg_equality_legendre_prefix_power bpvi_c_bls_blfg_equality_legendre_prefix_power. ((forall bpvi_i_bls_blfg_equality_legendre_prefix_power. (exists bpvi_repeat_gap_bls_blfg_equality_legendre_prefix_power. bpvi_repeat_gap_bls_blfg_equality_legendre_prefix_power + S bpvi_i_bls_blfg_equality_legendre_prefix_power = S bls_index_blfg_equality_legendre_prefix) -> (((exists bpvi_h_bls_blfg_equality_legendre_prefix_power_repeat. bpvi_h_bls_blfg_equality_legendre_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blfg_equality_legendre_prefix_power)) * bpvi_c_bls_blfg_equality_legendre_prefix_power)) /\ exists bpvi_q_bls_blfg_equality_legendre_prefix_power_repeat. bpvi_b_bls_blfg_equality_legendre_prefix_power = bpvi_q_bls_blfg_equality_legendre_prefix_power_repeat * S ((S (bpvi_i_bls_blfg_equality_legendre_prefix_power)) * bpvi_c_bls_blfg_equality_legendre_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blfg_equality_legendre_prefix_power bpvi_v_bls_blfg_equality_legendre_prefix_power. ((((exists bpvi_h_bls_blfg_equality_legendre_prefix_power_start. bpvi_h_bls_blfg_equality_legendre_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blfg_equality_legendre_prefix_power)) /\ exists bpvi_q_bls_blfg_equality_legendre_prefix_power_start. bpvi_u_bls_blfg_equality_legendre_prefix_power = bpvi_q_bls_blfg_equality_legendre_prefix_power_start * S ((S (0)) * bpvi_v_bls_blfg_equality_legendre_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blfg_equality_legendre_prefix_power_terminal. bpvi_h_bls_blfg_equality_legendre_prefix_power_terminal + S (bls_power_blfg_equality_legendre_prefix) = S ((S (S bls_index_blfg_equality_legendre_prefix)) * bpvi_v_bls_blfg_equality_legendre_prefix_power)) /\ exists bpvi_q_bls_blfg_equality_legendre_prefix_power_terminal. bpvi_u_bls_blfg_equality_legendre_prefix_power = bpvi_q_bls_blfg_equality_legendre_prefix_power_terminal * S ((S (S bls_index_blfg_equality_legendre_prefix)) * bpvi_v_bls_blfg_equality_legendre_prefix_power) + (bls_power_blfg_equality_legendre_prefix))) /\ forall bpvi_j_bls_blfg_equality_legendre_prefix_power. (exists bpvi_product_gap_bls_blfg_equality_legendre_prefix_power. bpvi_product_gap_bls_blfg_equality_legendre_prefix_power + S bpvi_j_bls_blfg_equality_legendre_prefix_power = S bls_index_blfg_equality_legendre_prefix) -> exists bpvi_factor_bls_blfg_equality_legendre_prefix_power bpvi_partial_bls_blfg_equality_legendre_prefix_power bpvi_successor_bls_blfg_equality_legendre_prefix_power. ((((exists bpvi_h_bls_blfg_equality_legendre_prefix_power_factor. bpvi_h_bls_blfg_equality_legendre_prefix_power_factor + S (bpvi_factor_bls_blfg_equality_legendre_prefix_power) = S ((S (bpvi_j_bls_blfg_equality_legendre_prefix_power)) * bpvi_c_bls_blfg_equality_legendre_prefix_power)) /\ exists bpvi_q_bls_blfg_equality_legendre_prefix_power_factor. bpvi_b_bls_blfg_equality_legendre_prefix_power = bpvi_q_bls_blfg_equality_legendre_prefix_power_factor * S ((S (bpvi_j_bls_blfg_equality_legendre_prefix_power)) * bpvi_c_bls_blfg_equality_legendre_prefix_power) + (bpvi_factor_bls_blfg_equality_legendre_prefix_power))) /\ ((((exists bpvi_h_bls_blfg_equality_legendre_prefix_power_partial. bpvi_h_bls_blfg_equality_legendre_prefix_power_partial + S (bpvi_partial_bls_blfg_equality_legendre_prefix_power) = S ((S (bpvi_j_bls_blfg_equality_legendre_prefix_power)) * bpvi_v_bls_blfg_equality_legendre_prefix_power)) /\ exists bpvi_q_bls_blfg_equality_legendre_prefix_power_partial. bpvi_u_bls_blfg_equality_legendre_prefix_power = bpvi_q_bls_blfg_equality_legendre_prefix_power_partial * S ((S (bpvi_j_bls_blfg_equality_legendre_prefix_power)) * bpvi_v_bls_blfg_equality_legendre_prefix_power) + (bpvi_partial_bls_blfg_equality_legendre_prefix_power))) /\ ((((exists bpvi_h_bls_blfg_equality_legendre_prefix_power_successor. bpvi_h_bls_blfg_equality_legendre_prefix_power_successor + S (bpvi_successor_bls_blfg_equality_legendre_prefix_power) = S ((S (S bpvi_j_bls_blfg_equality_legendre_prefix_power)) * bpvi_v_bls_blfg_equality_legendre_prefix_power)) /\ exists bpvi_q_bls_blfg_equality_legendre_prefix_power_successor. bpvi_u_bls_blfg_equality_legendre_prefix_power = bpvi_q_bls_blfg_equality_legendre_prefix_power_successor * S ((S (S bpvi_j_bls_blfg_equality_legendre_prefix_power)) * bpvi_v_bls_blfg_equality_legendre_prefix_power) + (bpvi_successor_bls_blfg_equality_legendre_prefix_power))) /\ bpvi_successor_bls_blfg_equality_legendre_prefix_power = bpvi_partial_bls_blfg_equality_legendre_prefix_power * bpvi_factor_bls_blfg_equality_legendre_prefix_power)))))))) /\ ((((exists ff_h_bls_blfg_equality_legendre_prefix_quotient_entry. ff_h_bls_blfg_equality_legendre_prefix_quotient_entry + S (bls_quotient_blfg_equality_legendre_prefix) = S ((S (bls_index_blfg_equality_legendre_prefix)) * bls_scale_blfg_equality_legendre)) /\ exists ff_q_bls_blfg_equality_legendre_prefix_quotient_entry. bls_code_blfg_equality_legendre = ff_q_bls_blfg_equality_legendre_prefix_quotient_entry * S ((S (bls_index_blfg_equality_legendre_prefix)) * bls_scale_blfg_equality_legendre) + (bls_quotient_blfg_equality_legendre_prefix))) /\ ((n = bls_power_blfg_equality_legendre_prefix * bls_quotient_blfg_equality_legendre_prefix + bls_remainder_blfg_equality_legendre_prefix /\ exists bls_remainder_gap_blfg_equality_legendre_prefix_division. bls_remainder_gap_blfg_equality_legendre_prefix_division + S (bls_remainder_blfg_equality_legendre_prefix) = bls_power_blfg_equality_legendre_prefix))))) /\ (exists ff_u_bls_blfg_equality_legendre_sum ff_v_bls_blfg_equality_legendre_sum. ((((exists ff_h_bls_blfg_equality_legendre_sum_start. ff_h_bls_blfg_equality_legendre_sum_start + S (0) = S ((S (0)) * ff_v_bls_blfg_equality_legendre_sum)) /\ exists ff_q_bls_blfg_equality_legendre_sum_start. ff_u_bls_blfg_equality_legendre_sum = ff_q_bls_blfg_equality_legendre_sum_start * S ((S (0)) * ff_v_bls_blfg_equality_legendre_sum) + (0))) /\ ((((exists ff_h_bls_blfg_equality_legendre_sum_terminal. ff_h_bls_blfg_equality_legendre_sum_terminal + S (b) = S ((S (n)) * ff_v_bls_blfg_equality_legendre_sum)) /\ exists ff_q_bls_blfg_equality_legendre_sum_terminal. ff_u_bls_blfg_equality_legendre_sum = ff_q_bls_blfg_equality_legendre_sum_terminal * S ((S (n)) * ff_v_bls_blfg_equality_legendre_sum) + (b))) /\ forall ff_i_bls_blfg_equality_legendre_sum. (exists ff_lt_bls_blfg_equality_legendre_sum_bound. ff_lt_bls_blfg_equality_legendre_sum_bound + S ff_i_bls_blfg_equality_legendre_sum = n) -> exists ff_a_bls_blfg_equality_legendre_sum ff_r_bls_blfg_equality_legendre_sum ff_s_bls_blfg_equality_legendre_sum. ((((exists ff_h_bls_blfg_equality_legendre_sum_summand. ff_h_bls_blfg_equality_legendre_sum_summand + S (ff_a_bls_blfg_equality_legendre_sum) = S ((S (ff_i_bls_blfg_equality_legendre_sum)) * bls_scale_blfg_equality_legendre)) /\ exists ff_q_bls_blfg_equality_legendre_sum_summand. bls_code_blfg_equality_legendre = ff_q_bls_blfg_equality_legendre_sum_summand * S ((S (ff_i_bls_blfg_equality_legendre_sum)) * bls_scale_blfg_equality_legendre) + (ff_a_bls_blfg_equality_legendre_sum))) /\ ((((exists ff_h_bls_blfg_equality_legendre_sum_partial. ff_h_bls_blfg_equality_legendre_sum_partial + S (ff_r_bls_blfg_equality_legendre_sum) = S ((S (ff_i_bls_blfg_equality_legendre_sum)) * ff_v_bls_blfg_equality_legendre_sum)) /\ exists ff_q_bls_blfg_equality_legendre_sum_partial. ff_u_bls_blfg_equality_legendre_sum = ff_q_bls_blfg_equality_legendre_sum_partial * S ((S (ff_i_bls_blfg_equality_legendre_sum)) * ff_v_bls_blfg_equality_legendre_sum) + (ff_r_bls_blfg_equality_legendre_sum))) /\ ((((exists ff_h_bls_blfg_equality_legendre_sum_successor. ff_h_bls_blfg_equality_legendre_sum_successor + S (ff_s_bls_blfg_equality_legendre_sum) = S ((S (S ff_i_bls_blfg_equality_legendre_sum)) * ff_v_bls_blfg_equality_legendre_sum)) /\ exists ff_q_bls_blfg_equality_legendre_sum_successor. ff_u_bls_blfg_equality_legendre_sum = ff_q_bls_blfg_equality_legendre_sum_successor * S ((S (S ff_i_bls_blfg_equality_legendre_sum)) * ff_v_bls_blfg_equality_legendre_sum) + (ff_s_bls_blfg_equality_legendre_sum))) /\ ff_s_bls_blfg_equality_legendre_sum = ff_r_bls_blfg_equality_legendre_sum + ff_a_bls_blfg_equality_legendre_sum)))))))) -> a = b

Proof neighborhood

Direct theorem prerequisites

BT00RO prime_factorial_valuation_zero BT00S4 legendre_sum_zero BT00RM factorial_valuation_exists BT00S2 prime_legendre_sum_exists BT00Q7 power_valuation_exists BT00T0 factorial_legendre_successor_agreement

Direct theorem dependents

BT00XN central_binom_legendre_valuation_balance

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

69 script commands · 15 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.

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 (6)
prime factorial valuation zerolegendre sum zerofactorial valuation existsprime legendre sum existspower valuation existsfactorial legendre successor agreement
01Fix variables and assumptionsL1–1

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

  1. L1
    intro p
02Induction on nL2–7

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction n
  2. L3
    intro a
  3. L4
    intro b
  4. L5
    intro hp
  5. L6
    intro hfactorial
  6. L7
    intro hlegendre
03Establish haL8–15

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

  1. L8
    have ha : a = 0
  2. L9
    specialize prime_factorial_valuation_zero p
  3. L10
    specialize prime_factorial_valuation_zero 0
  4. L11
    specialize prime_factorial_valuation_zero a
  5. L12
    apply prime_factorial_valuation_zero
  6. L13
    refl
  7. L14
    exact hp
  8. L15
    exact hfactorial
04Establish hbL16–25

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

  1. L16
    have hb : b = 0
  2. L17
    specialize legendre_sum_zero p
  3. L18
    specialize legendre_sum_zero 0
  4. L19
    specialize legendre_sum_zero b
  5. L20
    apply legendre_sum_zero
  6. L21
    refl
  7. L22
    exact hlegendre
  8. L23
    trans 0
  9. L24
    exact ha
  10. L25
    symm
05Use earlier factsL26–26

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

  1. L26
    exact hb
06Fix variables and assumptionsL27–31

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

  1. L27
    intro a
  2. L28
    intro b
  3. L29
    intro hp
  4. L30
    intro hfactorial
  5. L31
    intro hlegendre
07Establish hfactorial_oldL32–35

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

  1. L32
    have hfactorial_old : ∃ e. FactorialValuation(p,n,e)Definitions: FactorialValuation(p,n,e)Original native command in the exact edition
  2. L33
    specialize factorial_valuation_exists p
  3. L34
    specialize factorial_valuation_exists n
  4. L35
    exact factorial_valuation_exists
08Separate the logical casesL36–36

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

  1. L36
    cases hfactorial_old
09Establish hlegendre_oldL37–41

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

  1. L37
    have hlegendre_old : ∃ s. LegendreSum(p,n,s)Definitions: LegendreSum(p,n,s)Original native command in the exact edition
  2. L38
    specialize prime_legendre_sum_exists p
  3. L39
    specialize prime_legendre_sum_exists n
  4. L40
    apply prime_legendre_sum_exists
  5. L41
    exact hp
10Separate the logical casesL42–42

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

  1. L42
    cases hlegendre_old
11Establish hcontributionL43–46

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

  1. L43
    have hcontribution : ∃ f. PowerValuation(p,S n,f)Definitions: PowerValuation(p,S n,f)Original native command in the exact edition
  2. L44
    specialize power_valuation_exists p
  3. L45
    specialize power_valuation_exists (S n)
  4. L46
    exact power_valuation_exists
12Separate the logical casesL47–47

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

  1. L47
    cases hcontribution
13Establish hpredecessor_agreementL48–57

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

  1. L48
    have hpredecessor_agreement : x = x1
  2. L49
    specialize IH x
  3. L50
    specialize IH x1
  4. L51
    apply IH
  5. L52
    exact hp
  6. L53
    exact hfactorial_old_witness
  7. L54
    exact hlegendre_old_witness
  8. L55
    specialize factorial_legendre_successor_agreement p
  9. L56
    specialize factorial_legendre_successor_agreement n
  10. L57
    specialize factorial_legendre_successor_agreement x
14Use earlier factsL58–67

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

  1. L58
    specialize factorial_legendre_successor_agreement a
  2. L59
    specialize factorial_legendre_successor_agreement x1
  3. L60
    specialize factorial_legendre_successor_agreement b
  4. L61
    specialize factorial_legendre_successor_agreement x2
  5. L62
    apply factorial_legendre_successor_agreement
  6. L63
    exact hp
  7. L64
    exact hfactorial_old_witness
  8. L65
    exact hfactorial
  9. L66
    exact hcontribution_witness
  10. L67
    exact hlegendre_old_witness
15Use earlier factsL68–69

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

  1. L68
    exact hlegendre
  2. L69
    exact hpredecessor_agreement

Library-wide reading audit

Original defined command ledger · 69 lines
  1. 0001intro p
  2. 0002induction n
  3. 0003intro a
  4. 0004intro b
  5. 0005intro hp
  6. 0006intro hfactorial
  7. 0007intro hlegendre
  8. 0008have ha : a = 0
  9. 0009specialize prime_factorial_valuation_zero p
  10. 0010specialize prime_factorial_valuation_zero 0
  11. 0011specialize prime_factorial_valuation_zero a
  12. 0012apply prime_factorial_valuation_zero
  13. 0013refl
  14. 0014exact hp
  15. 0015exact hfactorial
  16. 0016have hb : b = 0
  17. 0017specialize legendre_sum_zero p
  18. 0018specialize legendre_sum_zero 0
  19. 0019specialize legendre_sum_zero b
  20. 0020apply legendre_sum_zero
  21. 0021refl
  22. 0022exact hlegendre
  23. 0023trans 0
  24. 0024exact ha
  25. 0025symm
  26. 0026exact hb
  27. 0027intro a
  28. 0028intro b
  29. 0029intro hp
  30. 0030intro hfactorial
  31. 0031intro hlegendre
  32. 0032have hfactorial_old : ∃ e. FactorialValuation(p,n,e)
    Exact native replay linehave hfactorial_old : exists e. exists bfv_factorial_blfg_induction_factorial_old. ((exists ff_b_blfg_induction_factorial_old_factorial ff_c_blfg_induction_factorial_old_factorial. ((forall ff_i_blfg_induction_factorial_old_factorial_range. (exists ff_lt_blfg_induction_factorial_old_factorial_range_bound. ff_lt_blfg_induction_factorial_old_factorial_range_bound + S ff_i_blfg_induction_factorial_old_factorial_range = n) -> (((exists ff_h_blfg_induction_factorial_old_factorial_range_decoded. ff_h_blfg_induction_factorial_old_factorial_range_decoded + S (1 + ff_i_blfg_induction_factorial_old_factorial_range) = S ((S (ff_i_blfg_induction_factorial_old_factorial_range)) * ff_c_blfg_induction_factorial_old_factorial)) /\ exists ff_q_blfg_induction_factorial_old_factorial_range_decoded. ff_b_blfg_induction_factorial_old_factorial = ff_q_blfg_induction_factorial_old_factorial_range_decoded * S ((S (ff_i_blfg_induction_factorial_old_factorial_range)) * ff_c_blfg_induction_factorial_old_factorial) + (1 + ff_i_blfg_induction_factorial_old_factorial_range)))) /\ (exists ff_u_blfg_induction_factorial_old_factorial_product ff_v_blfg_induction_factorial_old_factorial_product. ((((exists ff_h_blfg_induction_factorial_old_factorial_product_start. ff_h_blfg_induction_factorial_old_factorial_product_start + S (1) = S ((S (0)) * ff_v_blfg_induction_factorial_old_factorial_product)) /\ exists ff_q_blfg_induction_factorial_old_factorial_product_start. ff_u_blfg_induction_factorial_old_factorial_product = ff_q_blfg_induction_factorial_old_factorial_product_start * S ((S (0)) * ff_v_blfg_induction_factorial_old_factorial_product) + (1))) /\ ((((exists ff_h_blfg_induction_factorial_old_factorial_product_terminal. ff_h_blfg_induction_factorial_old_factorial_product_terminal + S (bfv_factorial_blfg_induction_factorial_old) = S ((S (n)) * ff_v_blfg_induction_factorial_old_factorial_product)) /\ exists ff_q_blfg_induction_factorial_old_factorial_product_terminal. ff_u_blfg_induction_factorial_old_factorial_product = ff_q_blfg_induction_factorial_old_factorial_product_terminal * S ((S (n)) * ff_v_blfg_induction_factorial_old_factorial_product) + (bfv_factorial_blfg_induction_factorial_old))) /\ forall ff_i_blfg_induction_factorial_old_factorial_product. (exists ff_lt_blfg_induction_factorial_old_factorial_product_bound. ff_lt_blfg_induction_factorial_old_factorial_product_bound + S ff_i_blfg_induction_factorial_old_factorial_product = n) -> exists ff_p_blfg_induction_factorial_old_factorial_product ff_r_blfg_induction_factorial_old_factorial_product ff_s_blfg_induction_factorial_old_factorial_product. ((((exists ff_h_blfg_induction_factorial_old_factorial_product_factor. ff_h_blfg_induction_factorial_old_factorial_product_factor + S (ff_p_blfg_induction_factorial_old_factorial_product) = S ((S (ff_i_blfg_induction_factorial_old_factorial_product)) * ff_c_blfg_induction_factorial_old_factorial)) /\ exists ff_q_blfg_induction_factorial_old_factorial_product_factor. ff_b_blfg_induction_factorial_old_factorial = ff_q_blfg_induction_factorial_old_factorial_product_factor * S ((S (ff_i_blfg_induction_factorial_old_factorial_product)) * ff_c_blfg_induction_factorial_old_factorial) + (ff_p_blfg_induction_factorial_old_factorial_product))) /\ ((((exists ff_h_blfg_induction_factorial_old_factorial_product_partial. ff_h_blfg_induction_factorial_old_factorial_product_partial + S (ff_r_blfg_induction_factorial_old_factorial_product) = S ((S (ff_i_blfg_induction_factorial_old_factorial_product)) * ff_v_blfg_induction_factorial_old_factorial_product)) /\ exists ff_q_blfg_induction_factorial_old_factorial_product_partial. ff_u_blfg_induction_factorial_old_factorial_product = ff_q_blfg_induction_factorial_old_factorial_product_partial * S ((S (ff_i_blfg_induction_factorial_old_factorial_product)) * ff_v_blfg_induction_factorial_old_factorial_product) + (ff_r_blfg_induction_factorial_old_factorial_product))) /\ ((((exists ff_h_blfg_induction_factorial_old_factorial_product_successor. ff_h_blfg_induction_factorial_old_factorial_product_successor + S (ff_s_blfg_induction_factorial_old_factorial_product) = S ((S (S ff_i_blfg_induction_factorial_old_factorial_product)) * ff_v_blfg_induction_factorial_old_factorial_product)) /\ exists ff_q_blfg_induction_factorial_old_factorial_product_successor. ff_u_blfg_induction_factorial_old_factorial_product = ff_q_blfg_induction_factorial_old_factorial_product_successor * S ((S (S ff_i_blfg_induction_factorial_old_factorial_product)) * ff_v_blfg_induction_factorial_old_factorial_product) + (ff_s_blfg_induction_factorial_old_factorial_product))) /\ ff_s_blfg_induction_factorial_old_factorial_product = ff_r_blfg_induction_factorial_old_factorial_product * ff_p_blfg_induction_factorial_old_factorial_product)))))))) /\ (((exists bpv_gap_blfg_induction_factorial_old_valuation_exponent_bound. bpv_gap_blfg_induction_factorial_old_valuation_exponent_bound + e = bfv_factorial_blfg_induction_factorial_old) /\ (exists bpv_result_blfg_induction_factorial_old_valuation_selected. ((exists ff_b_blfg_induction_factorial_old_valuation_selected_power ff_c_blfg_induction_factorial_old_valuation_selected_power. ((forall ff_i_blfg_induction_factorial_old_valuation_selected_power_repeat. (exists ff_lt_blfg_induction_factorial_old_valuation_selected_power_repeat_bound. ff_lt_blfg_induction_factorial_old_valuation_selected_power_repeat_bound + S ff_i_blfg_induction_factorial_old_valuation_selected_power_repeat = e) -> (((exists ff_h_blfg_induction_factorial_old_valuation_selected_power_repeat_decoded. ff_h_blfg_induction_factorial_old_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_blfg_induction_factorial_old_valuation_selected_power_repeat)) * ff_c_blfg_induction_factorial_old_valuation_selected_power)) /\ exists ff_q_blfg_induction_factorial_old_valuation_selected_power_repeat_decoded. ff_b_blfg_induction_factorial_old_valuation_selected_power = ff_q_blfg_induction_factorial_old_valuation_selected_power_repeat_decoded * S ((S (ff_i_blfg_induction_factorial_old_valuation_selected_power_repeat)) * ff_c_blfg_induction_factorial_old_valuation_selected_power) + (p)))) /\ (exists ff_u_blfg_induction_factorial_old_valuation_selected_power_product ff_v_blfg_induction_factorial_old_valuation_selected_power_product. ((((exists ff_h_blfg_induction_factorial_old_valuation_selected_power_product_start. ff_h_blfg_induction_factorial_old_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_blfg_induction_factorial_old_valuation_selected_power_product)) /\ exists ff_q_blfg_induction_factorial_old_valuation_selected_power_product_start. ff_u_blfg_induction_factorial_old_valuation_selected_power_product = ff_q_blfg_induction_factorial_old_valuation_selected_power_product_start * S ((S (0)) * ff_v_blfg_induction_factorial_old_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_blfg_induction_factorial_old_valuation_selected_power_product_terminal. ff_h_blfg_induction_factorial_old_valuation_selected_power_product_terminal + S (bpv_result_blfg_induction_factorial_old_valuation_selected) = S ((S (e)) * ff_v_blfg_induction_factorial_old_valuation_selected_power_product)) /\ exists ff_q_blfg_induction_factorial_old_valuation_selected_power_product_terminal. ff_u_blfg_induction_factorial_old_valuation_selected_power_product = ff_q_blfg_induction_factorial_old_valuation_selected_power_product_terminal * S ((S (e)) * ff_v_blfg_induction_factorial_old_valuation_selected_power_product) + (bpv_result_blfg_induction_factorial_old_valuation_selected))) /\ forall ff_i_blfg_induction_factorial_old_valuation_selected_power_product. (exists ff_lt_blfg_induction_factorial_old_valuation_selected_power_product_bound. ff_lt_blfg_induction_factorial_old_valuation_selected_power_product_bound + S ff_i_blfg_induction_factorial_old_valuation_selected_power_product = e) -> exists ff_p_blfg_induction_factorial_old_valuation_selected_power_product ff_r_blfg_induction_factorial_old_valuation_selected_power_product ff_s_blfg_induction_factorial_old_valuation_selected_power_product. ((((exists ff_h_blfg_induction_factorial_old_valuation_selected_power_product_factor. ff_h_blfg_induction_factorial_old_valuation_selected_power_product_factor + S (ff_p_blfg_induction_factorial_old_valuation_selected_power_product) = S ((S (ff_i_blfg_induction_factorial_old_valuation_selected_power_product)) * ff_c_blfg_induction_factorial_old_valuation_selected_power)) /\ exists ff_q_blfg_induction_factorial_old_valuation_selected_power_product_factor. ff_b_blfg_induction_factorial_old_valuation_selected_power = ff_q_blfg_induction_factorial_old_valuation_selected_power_product_factor * S ((S (ff_i_blfg_induction_factorial_old_valuation_selected_power_product)) * ff_c_blfg_induction_factorial_old_valuation_selected_power) + (ff_p_blfg_induction_factorial_old_valuation_selected_power_product))) /\ ((((exists ff_h_blfg_induction_factorial_old_valuation_selected_power_product_partial. ff_h_blfg_induction_factorial_old_valuation_selected_power_product_partial + S (ff_r_blfg_induction_factorial_old_valuation_selected_power_product) = S ((S (ff_i_blfg_induction_factorial_old_valuation_selected_power_product)) * ff_v_blfg_induction_factorial_old_valuation_selected_power_product)) /\ exists ff_q_blfg_induction_factorial_old_valuation_selected_power_product_partial. ff_u_blfg_induction_factorial_old_valuation_selected_power_product = ff_q_blfg_induction_factorial_old_valuation_selected_power_product_partial * S ((S (ff_i_blfg_induction_factorial_old_valuation_selected_power_product)) * ff_v_blfg_induction_factorial_old_valuation_selected_power_product) + (ff_r_blfg_induction_factorial_old_valuation_selected_power_product))) /\ ((((exists ff_h_blfg_induction_factorial_old_valuation_selected_power_product_successor. ff_h_blfg_induction_factorial_old_valuation_selected_power_product_successor + S (ff_s_blfg_induction_factorial_old_valuation_selected_power_product) = S ((S (S ff_i_blfg_induction_factorial_old_valuation_selected_power_product)) * ff_v_blfg_induction_factorial_old_valuation_selected_power_product)) /\ exists ff_q_blfg_induction_factorial_old_valuation_selected_power_product_successor. ff_u_blfg_induction_factorial_old_valuation_selected_power_product = ff_q_blfg_induction_factorial_old_valuation_selected_power_product_successor * S ((S (S ff_i_blfg_induction_factorial_old_valuation_selected_power_product)) * ff_v_blfg_induction_factorial_old_valuation_selected_power_product) + (ff_s_blfg_induction_factorial_old_valuation_selected_power_product))) /\ ff_s_blfg_induction_factorial_old_valuation_selected_power_product = ff_r_blfg_induction_factorial_old_valuation_selected_power_product * ff_p_blfg_induction_factorial_old_valuation_selected_power_product)))))))) /\ (exists bpv_factor_blfg_induction_factorial_old_valuation_selected_divides. bfv_factorial_blfg_induction_factorial_old = bpv_result_blfg_induction_factorial_old_valuation_selected * bpv_factor_blfg_induction_factorial_old_valuation_selected_divides)))) /\ forall bpv_candidate_blfg_induction_factorial_old_valuation. (exists bpv_gap_blfg_induction_factorial_old_valuation_candidate_bound. bpv_gap_blfg_induction_factorial_old_valuation_candidate_bound + bpv_candidate_blfg_induction_factorial_old_valuation = bfv_factorial_blfg_induction_factorial_old) -> (exists bpv_result_blfg_induction_factorial_old_valuation_candidate. ((exists ff_b_blfg_induction_factorial_old_valuation_candidate_power ff_c_blfg_induction_factorial_old_valuation_candidate_power. ((forall ff_i_blfg_induction_factorial_old_valuation_candidate_power_repeat. (exists ff_lt_blfg_induction_factorial_old_valuation_candidate_power_repeat_bound. ff_lt_blfg_induction_factorial_old_valuation_candidate_power_repeat_bound + S ff_i_blfg_induction_factorial_old_valuation_candidate_power_repeat = bpv_candidate_blfg_induction_factorial_old_valuation) -> (((exists ff_h_blfg_induction_factorial_old_valuation_candidate_power_repeat_decoded. ff_h_blfg_induction_factorial_old_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_blfg_induction_factorial_old_valuation_candidate_power_repeat)) * ff_c_blfg_induction_factorial_old_valuation_candidate_power)) /\ exists ff_q_blfg_induction_factorial_old_valuation_candidate_power_repeat_decoded. ff_b_blfg_induction_factorial_old_valuation_candidate_power = ff_q_blfg_induction_factorial_old_valuation_candidate_power_repeat_decoded * S ((S (ff_i_blfg_induction_factorial_old_valuation_candidate_power_repeat)) * ff_c_blfg_induction_factorial_old_valuation_candidate_power) + (p)))) /\ (exists ff_u_blfg_induction_factorial_old_valuation_candidate_power_product ff_v_blfg_induction_factorial_old_valuation_candidate_power_product. ((((exists ff_h_blfg_induction_factorial_old_valuation_candidate_power_product_start. ff_h_blfg_induction_factorial_old_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_blfg_induction_factorial_old_valuation_candidate_power_product)) /\ exists ff_q_blfg_induction_factorial_old_valuation_candidate_power_product_start. ff_u_blfg_induction_factorial_old_valuation_candidate_power_product = ff_q_blfg_induction_factorial_old_valuation_candidate_power_product_start * S ((S (0)) * ff_v_blfg_induction_factorial_old_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_blfg_induction_factorial_old_valuation_candidate_power_product_terminal. ff_h_blfg_induction_factorial_old_valuation_candidate_power_product_terminal + S (bpv_result_blfg_induction_factorial_old_valuation_candidate) = S ((S (bpv_candidate_blfg_induction_factorial_old_valuation)) * ff_v_blfg_induction_factorial_old_valuation_candidate_power_product)) /\ exists ff_q_blfg_induction_factorial_old_valuation_candidate_power_product_terminal. ff_u_blfg_induction_factorial_old_valuation_candidate_power_product = ff_q_blfg_induction_factorial_old_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_blfg_induction_factorial_old_valuation)) * ff_v_blfg_induction_factorial_old_valuation_candidate_power_product) + (bpv_result_blfg_induction_factorial_old_valuation_candidate))) /\ forall ff_i_blfg_induction_factorial_old_valuation_candidate_power_product. (exists ff_lt_blfg_induction_factorial_old_valuation_candidate_power_product_bound. ff_lt_blfg_induction_factorial_old_valuation_candidate_power_product_bound + S ff_i_blfg_induction_factorial_old_valuation_candidate_power_product = bpv_candidate_blfg_induction_factorial_old_valuation) -> exists ff_p_blfg_induction_factorial_old_valuation_candidate_power_product ff_r_blfg_induction_factorial_old_valuation_candidate_power_product ff_s_blfg_induction_factorial_old_valuation_candidate_power_product. ((((exists ff_h_blfg_induction_factorial_old_valuation_candidate_power_product_factor. ff_h_blfg_induction_factorial_old_valuation_candidate_power_product_factor + S (ff_p_blfg_induction_factorial_old_valuation_candidate_power_product) = S ((S (ff_i_blfg_induction_factorial_old_valuation_candidate_power_product)) * ff_c_blfg_induction_factorial_old_valuation_candidate_power)) /\ exists ff_q_blfg_induction_factorial_old_valuation_candidate_power_product_factor. ff_b_blfg_induction_factorial_old_valuation_candidate_power = ff_q_blfg_induction_factorial_old_valuation_candidate_power_product_factor * S ((S (ff_i_blfg_induction_factorial_old_valuation_candidate_power_product)) * ff_c_blfg_induction_factorial_old_valuation_candidate_power) + (ff_p_blfg_induction_factorial_old_valuation_candidate_power_product))) /\ ((((exists ff_h_blfg_induction_factorial_old_valuation_candidate_power_product_partial. ff_h_blfg_induction_factorial_old_valuation_candidate_power_product_partial + S (ff_r_blfg_induction_factorial_old_valuation_candidate_power_product) = S ((S (ff_i_blfg_induction_factorial_old_valuation_candidate_power_product)) * ff_v_blfg_induction_factorial_old_valuation_candidate_power_product)) /\ exists ff_q_blfg_induction_factorial_old_valuation_candidate_power_product_partial. ff_u_blfg_induction_factorial_old_valuation_candidate_power_product = ff_q_blfg_induction_factorial_old_valuation_candidate_power_product_partial * S ((S (ff_i_blfg_induction_factorial_old_valuation_candidate_power_product)) * ff_v_blfg_induction_factorial_old_valuation_candidate_power_product) + (ff_r_blfg_induction_factorial_old_valuation_candidate_power_product))) /\ ((((exists ff_h_blfg_induction_factorial_old_valuation_candidate_power_product_successor. ff_h_blfg_induction_factorial_old_valuation_candidate_power_product_successor + S (ff_s_blfg_induction_factorial_old_valuation_candidate_power_product) = S ((S (S ff_i_blfg_induction_factorial_old_valuation_candidate_power_product)) * ff_v_blfg_induction_factorial_old_valuation_candidate_power_product)) /\ exists ff_q_blfg_induction_factorial_old_valuation_candidate_power_product_successor. ff_u_blfg_induction_factorial_old_valuation_candidate_power_product = ff_q_blfg_induction_factorial_old_valuation_candidate_power_product_successor * S ((S (S ff_i_blfg_induction_factorial_old_valuation_candidate_power_product)) * ff_v_blfg_induction_factorial_old_valuation_candidate_power_product) + (ff_s_blfg_induction_factorial_old_valuation_candidate_power_product))) /\ ff_s_blfg_induction_factorial_old_valuation_candidate_power_product = ff_r_blfg_induction_factorial_old_valuation_candidate_power_product * ff_p_blfg_induction_factorial_old_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_blfg_induction_factorial_old_valuation_candidate_divides. bfv_factorial_blfg_induction_factorial_old = bpv_result_blfg_induction_factorial_old_valuation_candidate * bpv_factor_blfg_induction_factorial_old_valuation_candidate_divides))) -> (exists bpv_gap_blfg_induction_factorial_old_valuation_maximal. bpv_gap_blfg_induction_factorial_old_valuation_maximal + bpv_candidate_blfg_induction_factorial_old_valuation = e)))
  33. 0033specialize factorial_valuation_exists p
  34. 0034specialize factorial_valuation_exists n
  35. 0035exact factorial_valuation_exists
  36. 0036cases hfactorial_old
  37. 0037have hlegendre_old : ∃ s. LegendreSum(p,n,s)
    Exact native replay linehave hlegendre_old : exists s. exists bls_code_blfg_induction_legendre_old bls_scale_blfg_induction_legendre_old. ((forall bls_index_blfg_induction_legendre_old_prefix. (exists bls_gap_blfg_induction_legendre_old_prefix_bound. bls_gap_blfg_induction_legendre_old_prefix_bound + S (bls_index_blfg_induction_legendre_old_prefix) = (n)) -> exists bls_power_blfg_induction_legendre_old_prefix bls_quotient_blfg_induction_legendre_old_prefix bls_remainder_blfg_induction_legendre_old_prefix. ((exists bpvi_b_bls_blfg_induction_legendre_old_prefix_power bpvi_c_bls_blfg_induction_legendre_old_prefix_power. ((forall bpvi_i_bls_blfg_induction_legendre_old_prefix_power. (exists bpvi_repeat_gap_bls_blfg_induction_legendre_old_prefix_power. bpvi_repeat_gap_bls_blfg_induction_legendre_old_prefix_power + S bpvi_i_bls_blfg_induction_legendre_old_prefix_power = S bls_index_blfg_induction_legendre_old_prefix) -> (((exists bpvi_h_bls_blfg_induction_legendre_old_prefix_power_repeat. bpvi_h_bls_blfg_induction_legendre_old_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blfg_induction_legendre_old_prefix_power)) * bpvi_c_bls_blfg_induction_legendre_old_prefix_power)) /\ exists bpvi_q_bls_blfg_induction_legendre_old_prefix_power_repeat. bpvi_b_bls_blfg_induction_legendre_old_prefix_power = bpvi_q_bls_blfg_induction_legendre_old_prefix_power_repeat * S ((S (bpvi_i_bls_blfg_induction_legendre_old_prefix_power)) * bpvi_c_bls_blfg_induction_legendre_old_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blfg_induction_legendre_old_prefix_power bpvi_v_bls_blfg_induction_legendre_old_prefix_power. ((((exists bpvi_h_bls_blfg_induction_legendre_old_prefix_power_start. bpvi_h_bls_blfg_induction_legendre_old_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blfg_induction_legendre_old_prefix_power)) /\ exists bpvi_q_bls_blfg_induction_legendre_old_prefix_power_start. bpvi_u_bls_blfg_induction_legendre_old_prefix_power = bpvi_q_bls_blfg_induction_legendre_old_prefix_power_start * S ((S (0)) * bpvi_v_bls_blfg_induction_legendre_old_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blfg_induction_legendre_old_prefix_power_terminal. bpvi_h_bls_blfg_induction_legendre_old_prefix_power_terminal + S (bls_power_blfg_induction_legendre_old_prefix) = S ((S (S bls_index_blfg_induction_legendre_old_prefix)) * bpvi_v_bls_blfg_induction_legendre_old_prefix_power)) /\ exists bpvi_q_bls_blfg_induction_legendre_old_prefix_power_terminal. bpvi_u_bls_blfg_induction_legendre_old_prefix_power = bpvi_q_bls_blfg_induction_legendre_old_prefix_power_terminal * S ((S (S bls_index_blfg_induction_legendre_old_prefix)) * bpvi_v_bls_blfg_induction_legendre_old_prefix_power) + (bls_power_blfg_induction_legendre_old_prefix))) /\ forall bpvi_j_bls_blfg_induction_legendre_old_prefix_power. (exists bpvi_product_gap_bls_blfg_induction_legendre_old_prefix_power. bpvi_product_gap_bls_blfg_induction_legendre_old_prefix_power + S bpvi_j_bls_blfg_induction_legendre_old_prefix_power = S bls_index_blfg_induction_legendre_old_prefix) -> exists bpvi_factor_bls_blfg_induction_legendre_old_prefix_power bpvi_partial_bls_blfg_induction_legendre_old_prefix_power bpvi_successor_bls_blfg_induction_legendre_old_prefix_power. ((((exists bpvi_h_bls_blfg_induction_legendre_old_prefix_power_factor. bpvi_h_bls_blfg_induction_legendre_old_prefix_power_factor + S (bpvi_factor_bls_blfg_induction_legendre_old_prefix_power) = S ((S (bpvi_j_bls_blfg_induction_legendre_old_prefix_power)) * bpvi_c_bls_blfg_induction_legendre_old_prefix_power)) /\ exists bpvi_q_bls_blfg_induction_legendre_old_prefix_power_factor. bpvi_b_bls_blfg_induction_legendre_old_prefix_power = bpvi_q_bls_blfg_induction_legendre_old_prefix_power_factor * S ((S (bpvi_j_bls_blfg_induction_legendre_old_prefix_power)) * bpvi_c_bls_blfg_induction_legendre_old_prefix_power) + (bpvi_factor_bls_blfg_induction_legendre_old_prefix_power))) /\ ((((exists bpvi_h_bls_blfg_induction_legendre_old_prefix_power_partial. bpvi_h_bls_blfg_induction_legendre_old_prefix_power_partial + S (bpvi_partial_bls_blfg_induction_legendre_old_prefix_power) = S ((S (bpvi_j_bls_blfg_induction_legendre_old_prefix_power)) * bpvi_v_bls_blfg_induction_legendre_old_prefix_power)) /\ exists bpvi_q_bls_blfg_induction_legendre_old_prefix_power_partial. bpvi_u_bls_blfg_induction_legendre_old_prefix_power = bpvi_q_bls_blfg_induction_legendre_old_prefix_power_partial * S ((S (bpvi_j_bls_blfg_induction_legendre_old_prefix_power)) * bpvi_v_bls_blfg_induction_legendre_old_prefix_power) + (bpvi_partial_bls_blfg_induction_legendre_old_prefix_power))) /\ ((((exists bpvi_h_bls_blfg_induction_legendre_old_prefix_power_successor. bpvi_h_bls_blfg_induction_legendre_old_prefix_power_successor + S (bpvi_successor_bls_blfg_induction_legendre_old_prefix_power) = S ((S (S bpvi_j_bls_blfg_induction_legendre_old_prefix_power)) * bpvi_v_bls_blfg_induction_legendre_old_prefix_power)) /\ exists bpvi_q_bls_blfg_induction_legendre_old_prefix_power_successor. bpvi_u_bls_blfg_induction_legendre_old_prefix_power = bpvi_q_bls_blfg_induction_legendre_old_prefix_power_successor * S ((S (S bpvi_j_bls_blfg_induction_legendre_old_prefix_power)) * bpvi_v_bls_blfg_induction_legendre_old_prefix_power) + (bpvi_successor_bls_blfg_induction_legendre_old_prefix_power))) /\ bpvi_successor_bls_blfg_induction_legendre_old_prefix_power = bpvi_partial_bls_blfg_induction_legendre_old_prefix_power * bpvi_factor_bls_blfg_induction_legendre_old_prefix_power)))))))) /\ ((((exists ff_h_bls_blfg_induction_legendre_old_prefix_quotient_entry. ff_h_bls_blfg_induction_legendre_old_prefix_quotient_entry + S (bls_quotient_blfg_induction_legendre_old_prefix) = S ((S (bls_index_blfg_induction_legendre_old_prefix)) * bls_scale_blfg_induction_legendre_old)) /\ exists ff_q_bls_blfg_induction_legendre_old_prefix_quotient_entry. bls_code_blfg_induction_legendre_old = ff_q_bls_blfg_induction_legendre_old_prefix_quotient_entry * S ((S (bls_index_blfg_induction_legendre_old_prefix)) * bls_scale_blfg_induction_legendre_old) + (bls_quotient_blfg_induction_legendre_old_prefix))) /\ ((n = bls_power_blfg_induction_legendre_old_prefix * bls_quotient_blfg_induction_legendre_old_prefix + bls_remainder_blfg_induction_legendre_old_prefix /\ exists bls_remainder_gap_blfg_induction_legendre_old_prefix_division. bls_remainder_gap_blfg_induction_legendre_old_prefix_division + S (bls_remainder_blfg_induction_legendre_old_prefix) = bls_power_blfg_induction_legendre_old_prefix))))) /\ (exists ff_u_bls_blfg_induction_legendre_old_sum ff_v_bls_blfg_induction_legendre_old_sum. ((((exists ff_h_bls_blfg_induction_legendre_old_sum_start. ff_h_bls_blfg_induction_legendre_old_sum_start + S (0) = S ((S (0)) * ff_v_bls_blfg_induction_legendre_old_sum)) /\ exists ff_q_bls_blfg_induction_legendre_old_sum_start. ff_u_bls_blfg_induction_legendre_old_sum = ff_q_bls_blfg_induction_legendre_old_sum_start * S ((S (0)) * ff_v_bls_blfg_induction_legendre_old_sum) + (0))) /\ ((((exists ff_h_bls_blfg_induction_legendre_old_sum_terminal. ff_h_bls_blfg_induction_legendre_old_sum_terminal + S (s) = S ((S (n)) * ff_v_bls_blfg_induction_legendre_old_sum)) /\ exists ff_q_bls_blfg_induction_legendre_old_sum_terminal. ff_u_bls_blfg_induction_legendre_old_sum = ff_q_bls_blfg_induction_legendre_old_sum_terminal * S ((S (n)) * ff_v_bls_blfg_induction_legendre_old_sum) + (s))) /\ forall ff_i_bls_blfg_induction_legendre_old_sum. (exists ff_lt_bls_blfg_induction_legendre_old_sum_bound. ff_lt_bls_blfg_induction_legendre_old_sum_bound + S ff_i_bls_blfg_induction_legendre_old_sum = n) -> exists ff_a_bls_blfg_induction_legendre_old_sum ff_r_bls_blfg_induction_legendre_old_sum ff_s_bls_blfg_induction_legendre_old_sum. ((((exists ff_h_bls_blfg_induction_legendre_old_sum_summand. ff_h_bls_blfg_induction_legendre_old_sum_summand + S (ff_a_bls_blfg_induction_legendre_old_sum) = S ((S (ff_i_bls_blfg_induction_legendre_old_sum)) * bls_scale_blfg_induction_legendre_old)) /\ exists ff_q_bls_blfg_induction_legendre_old_sum_summand. bls_code_blfg_induction_legendre_old = ff_q_bls_blfg_induction_legendre_old_sum_summand * S ((S (ff_i_bls_blfg_induction_legendre_old_sum)) * bls_scale_blfg_induction_legendre_old) + (ff_a_bls_blfg_induction_legendre_old_sum))) /\ ((((exists ff_h_bls_blfg_induction_legendre_old_sum_partial. ff_h_bls_blfg_induction_legendre_old_sum_partial + S (ff_r_bls_blfg_induction_legendre_old_sum) = S ((S (ff_i_bls_blfg_induction_legendre_old_sum)) * ff_v_bls_blfg_induction_legendre_old_sum)) /\ exists ff_q_bls_blfg_induction_legendre_old_sum_partial. ff_u_bls_blfg_induction_legendre_old_sum = ff_q_bls_blfg_induction_legendre_old_sum_partial * S ((S (ff_i_bls_blfg_induction_legendre_old_sum)) * ff_v_bls_blfg_induction_legendre_old_sum) + (ff_r_bls_blfg_induction_legendre_old_sum))) /\ ((((exists ff_h_bls_blfg_induction_legendre_old_sum_successor. ff_h_bls_blfg_induction_legendre_old_sum_successor + S (ff_s_bls_blfg_induction_legendre_old_sum) = S ((S (S ff_i_bls_blfg_induction_legendre_old_sum)) * ff_v_bls_blfg_induction_legendre_old_sum)) /\ exists ff_q_bls_blfg_induction_legendre_old_sum_successor. ff_u_bls_blfg_induction_legendre_old_sum = ff_q_bls_blfg_induction_legendre_old_sum_successor * S ((S (S ff_i_bls_blfg_induction_legendre_old_sum)) * ff_v_bls_blfg_induction_legendre_old_sum) + (ff_s_bls_blfg_induction_legendre_old_sum))) /\ ff_s_bls_blfg_induction_legendre_old_sum = ff_r_bls_blfg_induction_legendre_old_sum + ff_a_bls_blfg_induction_legendre_old_sum)))))))
  38. 0038specialize prime_legendre_sum_exists p
  39. 0039specialize prime_legendre_sum_exists n
  40. 0040apply prime_legendre_sum_exists
  41. 0041exact hp
  42. 0042cases hlegendre_old
  43. 0043have hcontribution : ∃ f. PowerValuation(p,S n,f)
    Exact native replay linehave hcontribution : exists f. (((exists blsr_le_gap_blfg_induction_contribution_exponent_bound. blsr_le_gap_blfg_induction_contribution_exponent_bound + (f) = (S n)) /\ (exists bpvi_result_blfg_induction_contribution_selected. ((exists bpvi_b_blfg_induction_contribution_selected_power bpvi_c_blfg_induction_contribution_selected_power. ((forall bpvi_i_blfg_induction_contribution_selected_power. (exists bpvi_repeat_gap_blfg_induction_contribution_selected_power. bpvi_repeat_gap_blfg_induction_contribution_selected_power + S bpvi_i_blfg_induction_contribution_selected_power = f) -> (((exists bpvi_h_blfg_induction_contribution_selected_power_repeat. bpvi_h_blfg_induction_contribution_selected_power_repeat + S (p) = S ((S (bpvi_i_blfg_induction_contribution_selected_power)) * bpvi_c_blfg_induction_contribution_selected_power)) /\ exists bpvi_q_blfg_induction_contribution_selected_power_repeat. bpvi_b_blfg_induction_contribution_selected_power = bpvi_q_blfg_induction_contribution_selected_power_repeat * S ((S (bpvi_i_blfg_induction_contribution_selected_power)) * bpvi_c_blfg_induction_contribution_selected_power) + (p)))) /\ (exists bpvi_u_blfg_induction_contribution_selected_power bpvi_v_blfg_induction_contribution_selected_power. ((((exists bpvi_h_blfg_induction_contribution_selected_power_start. bpvi_h_blfg_induction_contribution_selected_power_start + S (1) = S ((S (0)) * bpvi_v_blfg_induction_contribution_selected_power)) /\ exists bpvi_q_blfg_induction_contribution_selected_power_start. bpvi_u_blfg_induction_contribution_selected_power = bpvi_q_blfg_induction_contribution_selected_power_start * S ((S (0)) * bpvi_v_blfg_induction_contribution_selected_power) + (1))) /\ ((((exists bpvi_h_blfg_induction_contribution_selected_power_terminal. bpvi_h_blfg_induction_contribution_selected_power_terminal + S (bpvi_result_blfg_induction_contribution_selected) = S ((S (f)) * bpvi_v_blfg_induction_contribution_selected_power)) /\ exists bpvi_q_blfg_induction_contribution_selected_power_terminal. bpvi_u_blfg_induction_contribution_selected_power = bpvi_q_blfg_induction_contribution_selected_power_terminal * S ((S (f)) * bpvi_v_blfg_induction_contribution_selected_power) + (bpvi_result_blfg_induction_contribution_selected))) /\ forall bpvi_j_blfg_induction_contribution_selected_power. (exists bpvi_product_gap_blfg_induction_contribution_selected_power. bpvi_product_gap_blfg_induction_contribution_selected_power + S bpvi_j_blfg_induction_contribution_selected_power = f) -> exists bpvi_factor_blfg_induction_contribution_selected_power bpvi_partial_blfg_induction_contribution_selected_power bpvi_successor_blfg_induction_contribution_selected_power. ((((exists bpvi_h_blfg_induction_contribution_selected_power_factor. bpvi_h_blfg_induction_contribution_selected_power_factor + S (bpvi_factor_blfg_induction_contribution_selected_power) = S ((S (bpvi_j_blfg_induction_contribution_selected_power)) * bpvi_c_blfg_induction_contribution_selected_power)) /\ exists bpvi_q_blfg_induction_contribution_selected_power_factor. bpvi_b_blfg_induction_contribution_selected_power = bpvi_q_blfg_induction_contribution_selected_power_factor * S ((S (bpvi_j_blfg_induction_contribution_selected_power)) * bpvi_c_blfg_induction_contribution_selected_power) + (bpvi_factor_blfg_induction_contribution_selected_power))) /\ ((((exists bpvi_h_blfg_induction_contribution_selected_power_partial. bpvi_h_blfg_induction_contribution_selected_power_partial + S (bpvi_partial_blfg_induction_contribution_selected_power) = S ((S (bpvi_j_blfg_induction_contribution_selected_power)) * bpvi_v_blfg_induction_contribution_selected_power)) /\ exists bpvi_q_blfg_induction_contribution_selected_power_partial. bpvi_u_blfg_induction_contribution_selected_power = bpvi_q_blfg_induction_contribution_selected_power_partial * S ((S (bpvi_j_blfg_induction_contribution_selected_power)) * bpvi_v_blfg_induction_contribution_selected_power) + (bpvi_partial_blfg_induction_contribution_selected_power))) /\ ((((exists bpvi_h_blfg_induction_contribution_selected_power_successor. bpvi_h_blfg_induction_contribution_selected_power_successor + S (bpvi_successor_blfg_induction_contribution_selected_power) = S ((S (S bpvi_j_blfg_induction_contribution_selected_power)) * bpvi_v_blfg_induction_contribution_selected_power)) /\ exists bpvi_q_blfg_induction_contribution_selected_power_successor. bpvi_u_blfg_induction_contribution_selected_power = bpvi_q_blfg_induction_contribution_selected_power_successor * S ((S (S bpvi_j_blfg_induction_contribution_selected_power)) * bpvi_v_blfg_induction_contribution_selected_power) + (bpvi_successor_blfg_induction_contribution_selected_power))) /\ bpvi_successor_blfg_induction_contribution_selected_power = bpvi_partial_blfg_induction_contribution_selected_power * bpvi_factor_blfg_induction_contribution_selected_power)))))))) /\ exists bpvi_divisor_factor_blfg_induction_contribution_selected. S n = bpvi_result_blfg_induction_contribution_selected * bpvi_divisor_factor_blfg_induction_contribution_selected))) /\ forall blsr_candidate_blfg_induction_contribution. (exists blsr_le_gap_blfg_induction_contribution_candidate_bound. blsr_le_gap_blfg_induction_contribution_candidate_bound + (blsr_candidate_blfg_induction_contribution) = (S n)) -> (exists bpvi_result_blfg_induction_contribution_candidate. ((exists bpvi_b_blfg_induction_contribution_candidate_power bpvi_c_blfg_induction_contribution_candidate_power. ((forall bpvi_i_blfg_induction_contribution_candidate_power. (exists bpvi_repeat_gap_blfg_induction_contribution_candidate_power. bpvi_repeat_gap_blfg_induction_contribution_candidate_power + S bpvi_i_blfg_induction_contribution_candidate_power = blsr_candidate_blfg_induction_contribution) -> (((exists bpvi_h_blfg_induction_contribution_candidate_power_repeat. bpvi_h_blfg_induction_contribution_candidate_power_repeat + S (p) = S ((S (bpvi_i_blfg_induction_contribution_candidate_power)) * bpvi_c_blfg_induction_contribution_candidate_power)) /\ exists bpvi_q_blfg_induction_contribution_candidate_power_repeat. bpvi_b_blfg_induction_contribution_candidate_power = bpvi_q_blfg_induction_contribution_candidate_power_repeat * S ((S (bpvi_i_blfg_induction_contribution_candidate_power)) * bpvi_c_blfg_induction_contribution_candidate_power) + (p)))) /\ (exists bpvi_u_blfg_induction_contribution_candidate_power bpvi_v_blfg_induction_contribution_candidate_power. ((((exists bpvi_h_blfg_induction_contribution_candidate_power_start. bpvi_h_blfg_induction_contribution_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_blfg_induction_contribution_candidate_power)) /\ exists bpvi_q_blfg_induction_contribution_candidate_power_start. bpvi_u_blfg_induction_contribution_candidate_power = bpvi_q_blfg_induction_contribution_candidate_power_start * S ((S (0)) * bpvi_v_blfg_induction_contribution_candidate_power) + (1))) /\ ((((exists bpvi_h_blfg_induction_contribution_candidate_power_terminal. bpvi_h_blfg_induction_contribution_candidate_power_terminal + S (bpvi_result_blfg_induction_contribution_candidate) = S ((S (blsr_candidate_blfg_induction_contribution)) * bpvi_v_blfg_induction_contribution_candidate_power)) /\ exists bpvi_q_blfg_induction_contribution_candidate_power_terminal. bpvi_u_blfg_induction_contribution_candidate_power = bpvi_q_blfg_induction_contribution_candidate_power_terminal * S ((S (blsr_candidate_blfg_induction_contribution)) * bpvi_v_blfg_induction_contribution_candidate_power) + (bpvi_result_blfg_induction_contribution_candidate))) /\ forall bpvi_j_blfg_induction_contribution_candidate_power. (exists bpvi_product_gap_blfg_induction_contribution_candidate_power. bpvi_product_gap_blfg_induction_contribution_candidate_power + S bpvi_j_blfg_induction_contribution_candidate_power = blsr_candidate_blfg_induction_contribution) -> exists bpvi_factor_blfg_induction_contribution_candidate_power bpvi_partial_blfg_induction_contribution_candidate_power bpvi_successor_blfg_induction_contribution_candidate_power. ((((exists bpvi_h_blfg_induction_contribution_candidate_power_factor. bpvi_h_blfg_induction_contribution_candidate_power_factor + S (bpvi_factor_blfg_induction_contribution_candidate_power) = S ((S (bpvi_j_blfg_induction_contribution_candidate_power)) * bpvi_c_blfg_induction_contribution_candidate_power)) /\ exists bpvi_q_blfg_induction_contribution_candidate_power_factor. bpvi_b_blfg_induction_contribution_candidate_power = bpvi_q_blfg_induction_contribution_candidate_power_factor * S ((S (bpvi_j_blfg_induction_contribution_candidate_power)) * bpvi_c_blfg_induction_contribution_candidate_power) + (bpvi_factor_blfg_induction_contribution_candidate_power))) /\ ((((exists bpvi_h_blfg_induction_contribution_candidate_power_partial. bpvi_h_blfg_induction_contribution_candidate_power_partial + S (bpvi_partial_blfg_induction_contribution_candidate_power) = S ((S (bpvi_j_blfg_induction_contribution_candidate_power)) * bpvi_v_blfg_induction_contribution_candidate_power)) /\ exists bpvi_q_blfg_induction_contribution_candidate_power_partial. bpvi_u_blfg_induction_contribution_candidate_power = bpvi_q_blfg_induction_contribution_candidate_power_partial * S ((S (bpvi_j_blfg_induction_contribution_candidate_power)) * bpvi_v_blfg_induction_contribution_candidate_power) + (bpvi_partial_blfg_induction_contribution_candidate_power))) /\ ((((exists bpvi_h_blfg_induction_contribution_candidate_power_successor. bpvi_h_blfg_induction_contribution_candidate_power_successor + S (bpvi_successor_blfg_induction_contribution_candidate_power) = S ((S (S bpvi_j_blfg_induction_contribution_candidate_power)) * bpvi_v_blfg_induction_contribution_candidate_power)) /\ exists bpvi_q_blfg_induction_contribution_candidate_power_successor. bpvi_u_blfg_induction_contribution_candidate_power = bpvi_q_blfg_induction_contribution_candidate_power_successor * S ((S (S bpvi_j_blfg_induction_contribution_candidate_power)) * bpvi_v_blfg_induction_contribution_candidate_power) + (bpvi_successor_blfg_induction_contribution_candidate_power))) /\ bpvi_successor_blfg_induction_contribution_candidate_power = bpvi_partial_blfg_induction_contribution_candidate_power * bpvi_factor_blfg_induction_contribution_candidate_power)))))))) /\ exists bpvi_divisor_factor_blfg_induction_contribution_candidate. S n = bpvi_result_blfg_induction_contribution_candidate * bpvi_divisor_factor_blfg_induction_contribution_candidate)) -> (exists blsr_le_gap_blfg_induction_contribution_maximal. blsr_le_gap_blfg_induction_contribution_maximal + (blsr_candidate_blfg_induction_contribution) = (f)))
  44. 0044specialize power_valuation_exists p
  45. 0045specialize power_valuation_exists (S n)
  46. 0046exact power_valuation_exists
  47. 0047cases hcontribution
  48. 0048have hpredecessor_agreement : x = x1
  49. 0049specialize IH x
  50. 0050specialize IH x1
  51. 0051apply IH
  52. 0052exact hp
  53. 0053exact hfactorial_old_witness
  54. 0054exact hlegendre_old_witness
  55. 0055specialize factorial_legendre_successor_agreement p
  56. 0056specialize factorial_legendre_successor_agreement n
  57. 0057specialize factorial_legendre_successor_agreement x
  58. 0058specialize factorial_legendre_successor_agreement a
  59. 0059specialize factorial_legendre_successor_agreement x1
  60. 0060specialize factorial_legendre_successor_agreement b
  61. 0061specialize factorial_legendre_successor_agreement x2
  62. 0062apply factorial_legendre_successor_agreement
  63. 0063exact hp
  64. 0064exact hfactorial_old_witness
  65. 0065exact hfactorial
  66. 0066exact hcontribution_witness
  67. 0067exact hlegendre_old_witness
  68. 0068exact hlegendre
  69. 0069exact hpredecessor_agreement