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. ∀ sn. ∀ e. ∀ f. ∀ g. sn = S n → Prime(p) → FactorialValuation(p,n,e) → PowerValuation(p,sn,f) → FactorialValuation(p,sn,g) → g = e + fEvery 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
4 occurrences
In local proof propositions
1 occurrences
Exact expanded native-PA statement
forall p n sn e f g. sn = S n -> ((~(p = 1) /\ forall frm_prime_left_bfv_prime frm_prime_right_bfv_prime. p = frm_prime_left_bfv_prime * frm_prime_right_bfv_prime -> frm_prime_left_bfv_prime = 1 \/ frm_prime_right_bfv_prime = 1)) -> (exists bfv_factorial_bfv_successor_predecessor. ((exists ff_b_bfv_successor_predecessor_factorial ff_c_bfv_successor_predecessor_factorial. ((forall ff_i_bfv_successor_predecessor_factorial_range. (exists ff_lt_bfv_successor_predecessor_factorial_range_bound. ff_lt_bfv_successor_predecessor_factorial_range_bound + S ff_i_bfv_successor_predecessor_factorial_range = n) -> (((exists ff_h_bfv_successor_predecessor_factorial_range_decoded. ff_h_bfv_successor_predecessor_factorial_range_decoded + S (1 + ff_i_bfv_successor_predecessor_factorial_range) = S ((S (ff_i_bfv_successor_predecessor_factorial_range)) * ff_c_bfv_successor_predecessor_factorial)) /\ exists ff_q_bfv_successor_predecessor_factorial_range_decoded. ff_b_bfv_successor_predecessor_factorial = ff_q_bfv_successor_predecessor_factorial_range_decoded * S ((S (ff_i_bfv_successor_predecessor_factorial_range)) * ff_c_bfv_successor_predecessor_factorial) + (1 + ff_i_bfv_successor_predecessor_factorial_range)))) /\ (exists ff_u_bfv_successor_predecessor_factorial_product ff_v_bfv_successor_predecessor_factorial_product. ((((exists ff_h_bfv_successor_predecessor_factorial_product_start. ff_h_bfv_successor_predecessor_factorial_product_start + S (1) = S ((S (0)) * ff_v_bfv_successor_predecessor_factorial_product)) /\ exists ff_q_bfv_successor_predecessor_factorial_product_start. ff_u_bfv_successor_predecessor_factorial_product = ff_q_bfv_successor_predecessor_factorial_product_start * S ((S (0)) * ff_v_bfv_successor_predecessor_factorial_product) + (1))) /\ ((((exists ff_h_bfv_successor_predecessor_factorial_product_terminal. ff_h_bfv_successor_predecessor_factorial_product_terminal + S (bfv_factorial_bfv_successor_predecessor) = S ((S (n)) * ff_v_bfv_successor_predecessor_factorial_product)) /\ exists ff_q_bfv_successor_predecessor_factorial_product_terminal. ff_u_bfv_successor_predecessor_factorial_product = ff_q_bfv_successor_predecessor_factorial_product_terminal * S ((S (n)) * ff_v_bfv_successor_predecessor_factorial_product) + (bfv_factorial_bfv_successor_predecessor))) /\ forall ff_i_bfv_successor_predecessor_factorial_product. (exists ff_lt_bfv_successor_predecessor_factorial_product_bound. ff_lt_bfv_successor_predecessor_factorial_product_bound + S ff_i_bfv_successor_predecessor_factorial_product = n) -> exists ff_p_bfv_successor_predecessor_factorial_product ff_r_bfv_successor_predecessor_factorial_product ff_s_bfv_successor_predecessor_factorial_product. ((((exists ff_h_bfv_successor_predecessor_factorial_product_factor. ff_h_bfv_successor_predecessor_factorial_product_factor + S (ff_p_bfv_successor_predecessor_factorial_product) = S ((S (ff_i_bfv_successor_predecessor_factorial_product)) * ff_c_bfv_successor_predecessor_factorial)) /\ exists ff_q_bfv_successor_predecessor_factorial_product_factor. ff_b_bfv_successor_predecessor_factorial = ff_q_bfv_successor_predecessor_factorial_product_factor * S ((S (ff_i_bfv_successor_predecessor_factorial_product)) * ff_c_bfv_successor_predecessor_factorial) + (ff_p_bfv_successor_predecessor_factorial_product))) /\ ((((exists ff_h_bfv_successor_predecessor_factorial_product_partial. ff_h_bfv_successor_predecessor_factorial_product_partial + S (ff_r_bfv_successor_predecessor_factorial_product) = S ((S (ff_i_bfv_successor_predecessor_factorial_product)) * ff_v_bfv_successor_predecessor_factorial_product)) /\ exists ff_q_bfv_successor_predecessor_factorial_product_partial. ff_u_bfv_successor_predecessor_factorial_product = ff_q_bfv_successor_predecessor_factorial_product_partial * S ((S (ff_i_bfv_successor_predecessor_factorial_product)) * ff_v_bfv_successor_predecessor_factorial_product) + (ff_r_bfv_successor_predecessor_factorial_product))) /\ ((((exists ff_h_bfv_successor_predecessor_factorial_product_successor. ff_h_bfv_successor_predecessor_factorial_product_successor + S (ff_s_bfv_successor_predecessor_factorial_product) = S ((S (S ff_i_bfv_successor_predecessor_factorial_product)) * ff_v_bfv_successor_predecessor_factorial_product)) /\ exists ff_q_bfv_successor_predecessor_factorial_product_successor. ff_u_bfv_successor_predecessor_factorial_product = ff_q_bfv_successor_predecessor_factorial_product_successor * S ((S (S ff_i_bfv_successor_predecessor_factorial_product)) * ff_v_bfv_successor_predecessor_factorial_product) + (ff_s_bfv_successor_predecessor_factorial_product))) /\ ff_s_bfv_successor_predecessor_factorial_product = ff_r_bfv_successor_predecessor_factorial_product * ff_p_bfv_successor_predecessor_factorial_product)))))))) /\ (((exists bpv_gap_bfv_successor_predecessor_valuation_exponent_bound. bpv_gap_bfv_successor_predecessor_valuation_exponent_bound + e = bfv_factorial_bfv_successor_predecessor) /\ (exists bpv_result_bfv_successor_predecessor_valuation_selected. ((exists ff_b_bfv_successor_predecessor_valuation_selected_power ff_c_bfv_successor_predecessor_valuation_selected_power. ((forall ff_i_bfv_successor_predecessor_valuation_selected_power_repeat. (exists ff_lt_bfv_successor_predecessor_valuation_selected_power_repeat_bound. ff_lt_bfv_successor_predecessor_valuation_selected_power_repeat_bound + S ff_i_bfv_successor_predecessor_valuation_selected_power_repeat = e) -> (((exists ff_h_bfv_successor_predecessor_valuation_selected_power_repeat_decoded. ff_h_bfv_successor_predecessor_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_successor_predecessor_valuation_selected_power_repeat)) * ff_c_bfv_successor_predecessor_valuation_selected_power)) /\ exists ff_q_bfv_successor_predecessor_valuation_selected_power_repeat_decoded. ff_b_bfv_successor_predecessor_valuation_selected_power = ff_q_bfv_successor_predecessor_valuation_selected_power_repeat_decoded * S ((S (ff_i_bfv_successor_predecessor_valuation_selected_power_repeat)) * ff_c_bfv_successor_predecessor_valuation_selected_power) + (p)))) /\ (exists ff_u_bfv_successor_predecessor_valuation_selected_power_product ff_v_bfv_successor_predecessor_valuation_selected_power_product. ((((exists ff_h_bfv_successor_predecessor_valuation_selected_power_product_start. ff_h_bfv_successor_predecessor_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_successor_predecessor_valuation_selected_power_product)) /\ exists ff_q_bfv_successor_predecessor_valuation_selected_power_product_start. ff_u_bfv_successor_predecessor_valuation_selected_power_product = ff_q_bfv_successor_predecessor_valuation_selected_power_product_start * S ((S (0)) * ff_v_bfv_successor_predecessor_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bfv_successor_predecessor_valuation_selected_power_product_terminal. ff_h_bfv_successor_predecessor_valuation_selected_power_product_terminal + S (bpv_result_bfv_successor_predecessor_valuation_selected) = S ((S (e)) * ff_v_bfv_successor_predecessor_valuation_selected_power_product)) /\ exists ff_q_bfv_successor_predecessor_valuation_selected_power_product_terminal. ff_u_bfv_successor_predecessor_valuation_selected_power_product = ff_q_bfv_successor_predecessor_valuation_selected_power_product_terminal * S ((S (e)) * ff_v_bfv_successor_predecessor_valuation_selected_power_product) + (bpv_result_bfv_successor_predecessor_valuation_selected))) /\ forall ff_i_bfv_successor_predecessor_valuation_selected_power_product. (exists ff_lt_bfv_successor_predecessor_valuation_selected_power_product_bound. ff_lt_bfv_successor_predecessor_valuation_selected_power_product_bound + S ff_i_bfv_successor_predecessor_valuation_selected_power_product = e) -> exists ff_p_bfv_successor_predecessor_valuation_selected_power_product ff_r_bfv_successor_predecessor_valuation_selected_power_product ff_s_bfv_successor_predecessor_valuation_selected_power_product. ((((exists ff_h_bfv_successor_predecessor_valuation_selected_power_product_factor. ff_h_bfv_successor_predecessor_valuation_selected_power_product_factor + S (ff_p_bfv_successor_predecessor_valuation_selected_power_product) = S ((S (ff_i_bfv_successor_predecessor_valuation_selected_power_product)) * ff_c_bfv_successor_predecessor_valuation_selected_power)) /\ exists ff_q_bfv_successor_predecessor_valuation_selected_power_product_factor. ff_b_bfv_successor_predecessor_valuation_selected_power = ff_q_bfv_successor_predecessor_valuation_selected_power_product_factor * S ((S (ff_i_bfv_successor_predecessor_valuation_selected_power_product)) * ff_c_bfv_successor_predecessor_valuation_selected_power) + (ff_p_bfv_successor_predecessor_valuation_selected_power_product))) /\ ((((exists ff_h_bfv_successor_predecessor_valuation_selected_power_product_partial. ff_h_bfv_successor_predecessor_valuation_selected_power_product_partial + S (ff_r_bfv_successor_predecessor_valuation_selected_power_product) = S ((S (ff_i_bfv_successor_predecessor_valuation_selected_power_product)) * ff_v_bfv_successor_predecessor_valuation_selected_power_product)) /\ exists ff_q_bfv_successor_predecessor_valuation_selected_power_product_partial. ff_u_bfv_successor_predecessor_valuation_selected_power_product = ff_q_bfv_successor_predecessor_valuation_selected_power_product_partial * S ((S (ff_i_bfv_successor_predecessor_valuation_selected_power_product)) * ff_v_bfv_successor_predecessor_valuation_selected_power_product) + (ff_r_bfv_successor_predecessor_valuation_selected_power_product))) /\ ((((exists ff_h_bfv_successor_predecessor_valuation_selected_power_product_successor. ff_h_bfv_successor_predecessor_valuation_selected_power_product_successor + S (ff_s_bfv_successor_predecessor_valuation_selected_power_product) = S ((S (S ff_i_bfv_successor_predecessor_valuation_selected_power_product)) * ff_v_bfv_successor_predecessor_valuation_selected_power_product)) /\ exists ff_q_bfv_successor_predecessor_valuation_selected_power_product_successor. ff_u_bfv_successor_predecessor_valuation_selected_power_product = ff_q_bfv_successor_predecessor_valuation_selected_power_product_successor * S ((S (S ff_i_bfv_successor_predecessor_valuation_selected_power_product)) * ff_v_bfv_successor_predecessor_valuation_selected_power_product) + (ff_s_bfv_successor_predecessor_valuation_selected_power_product))) /\ ff_s_bfv_successor_predecessor_valuation_selected_power_product = ff_r_bfv_successor_predecessor_valuation_selected_power_product * ff_p_bfv_successor_predecessor_valuation_selected_power_product)))))))) /\ (exists bpv_factor_bfv_successor_predecessor_valuation_selected_divides. bfv_factorial_bfv_successor_predecessor = bpv_result_bfv_successor_predecessor_valuation_selected * bpv_factor_bfv_successor_predecessor_valuation_selected_divides)))) /\ forall bpv_candidate_bfv_successor_predecessor_valuation. (exists bpv_gap_bfv_successor_predecessor_valuation_candidate_bound. bpv_gap_bfv_successor_predecessor_valuation_candidate_bound + bpv_candidate_bfv_successor_predecessor_valuation = bfv_factorial_bfv_successor_predecessor) -> (exists bpv_result_bfv_successor_predecessor_valuation_candidate. ((exists ff_b_bfv_successor_predecessor_valuation_candidate_power ff_c_bfv_successor_predecessor_valuation_candidate_power. ((forall ff_i_bfv_successor_predecessor_valuation_candidate_power_repeat. (exists ff_lt_bfv_successor_predecessor_valuation_candidate_power_repeat_bound. ff_lt_bfv_successor_predecessor_valuation_candidate_power_repeat_bound + S ff_i_bfv_successor_predecessor_valuation_candidate_power_repeat = bpv_candidate_bfv_successor_predecessor_valuation) -> (((exists ff_h_bfv_successor_predecessor_valuation_candidate_power_repeat_decoded. ff_h_bfv_successor_predecessor_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_successor_predecessor_valuation_candidate_power_repeat)) * ff_c_bfv_successor_predecessor_valuation_candidate_power)) /\ exists ff_q_bfv_successor_predecessor_valuation_candidate_power_repeat_decoded. ff_b_bfv_successor_predecessor_valuation_candidate_power = ff_q_bfv_successor_predecessor_valuation_candidate_power_repeat_decoded * S ((S (ff_i_bfv_successor_predecessor_valuation_candidate_power_repeat)) * ff_c_bfv_successor_predecessor_valuation_candidate_power) + (p)))) /\ (exists ff_u_bfv_successor_predecessor_valuation_candidate_power_product ff_v_bfv_successor_predecessor_valuation_candidate_power_product. ((((exists ff_h_bfv_successor_predecessor_valuation_candidate_power_product_start. ff_h_bfv_successor_predecessor_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_successor_predecessor_valuation_candidate_power_product)) /\ exists ff_q_bfv_successor_predecessor_valuation_candidate_power_product_start. ff_u_bfv_successor_predecessor_valuation_candidate_power_product = ff_q_bfv_successor_predecessor_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bfv_successor_predecessor_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bfv_successor_predecessor_valuation_candidate_power_product_terminal. ff_h_bfv_successor_predecessor_valuation_candidate_power_product_terminal + S (bpv_result_bfv_successor_predecessor_valuation_candidate) = S ((S (bpv_candidate_bfv_successor_predecessor_valuation)) * ff_v_bfv_successor_predecessor_valuation_candidate_power_product)) /\ exists ff_q_bfv_successor_predecessor_valuation_candidate_power_product_terminal. ff_u_bfv_successor_predecessor_valuation_candidate_power_product = ff_q_bfv_successor_predecessor_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_bfv_successor_predecessor_valuation)) * ff_v_bfv_successor_predecessor_valuation_candidate_power_product) + (bpv_result_bfv_successor_predecessor_valuation_candidate))) /\ forall ff_i_bfv_successor_predecessor_valuation_candidate_power_product. (exists ff_lt_bfv_successor_predecessor_valuation_candidate_power_product_bound. ff_lt_bfv_successor_predecessor_valuation_candidate_power_product_bound + S ff_i_bfv_successor_predecessor_valuation_candidate_power_product = bpv_candidate_bfv_successor_predecessor_valuation) -> exists ff_p_bfv_successor_predecessor_valuation_candidate_power_product ff_r_bfv_successor_predecessor_valuation_candidate_power_product ff_s_bfv_successor_predecessor_valuation_candidate_power_product. ((((exists ff_h_bfv_successor_predecessor_valuation_candidate_power_product_factor. ff_h_bfv_successor_predecessor_valuation_candidate_power_product_factor + S (ff_p_bfv_successor_predecessor_valuation_candidate_power_product) = S ((S (ff_i_bfv_successor_predecessor_valuation_candidate_power_product)) * ff_c_bfv_successor_predecessor_valuation_candidate_power)) /\ exists ff_q_bfv_successor_predecessor_valuation_candidate_power_product_factor. ff_b_bfv_successor_predecessor_valuation_candidate_power = ff_q_bfv_successor_predecessor_valuation_candidate_power_product_factor * S ((S (ff_i_bfv_successor_predecessor_valuation_candidate_power_product)) * ff_c_bfv_successor_predecessor_valuation_candidate_power) + (ff_p_bfv_successor_predecessor_valuation_candidate_power_product))) /\ ((((exists ff_h_bfv_successor_predecessor_valuation_candidate_power_product_partial. ff_h_bfv_successor_predecessor_valuation_candidate_power_product_partial + S (ff_r_bfv_successor_predecessor_valuation_candidate_power_product) = S ((S (ff_i_bfv_successor_predecessor_valuation_candidate_power_product)) * ff_v_bfv_successor_predecessor_valuation_candidate_power_product)) /\ exists ff_q_bfv_successor_predecessor_valuation_candidate_power_product_partial. ff_u_bfv_successor_predecessor_valuation_candidate_power_product = ff_q_bfv_successor_predecessor_valuation_candidate_power_product_partial * S ((S (ff_i_bfv_successor_predecessor_valuation_candidate_power_product)) * ff_v_bfv_successor_predecessor_valuation_candidate_power_product) + (ff_r_bfv_successor_predecessor_valuation_candidate_power_product))) /\ ((((exists ff_h_bfv_successor_predecessor_valuation_candidate_power_product_successor. ff_h_bfv_successor_predecessor_valuation_candidate_power_product_successor + S (ff_s_bfv_successor_predecessor_valuation_candidate_power_product) = S ((S (S ff_i_bfv_successor_predecessor_valuation_candidate_power_product)) * ff_v_bfv_successor_predecessor_valuation_candidate_power_product)) /\ exists ff_q_bfv_successor_predecessor_valuation_candidate_power_product_successor. ff_u_bfv_successor_predecessor_valuation_candidate_power_product = ff_q_bfv_successor_predecessor_valuation_candidate_power_product_successor * S ((S (S ff_i_bfv_successor_predecessor_valuation_candidate_power_product)) * ff_v_bfv_successor_predecessor_valuation_candidate_power_product) + (ff_s_bfv_successor_predecessor_valuation_candidate_power_product))) /\ ff_s_bfv_successor_predecessor_valuation_candidate_power_product = ff_r_bfv_successor_predecessor_valuation_candidate_power_product * ff_p_bfv_successor_predecessor_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_bfv_successor_predecessor_valuation_candidate_divides. bfv_factorial_bfv_successor_predecessor = bpv_result_bfv_successor_predecessor_valuation_candidate * bpv_factor_bfv_successor_predecessor_valuation_candidate_divides))) -> (exists bpv_gap_bfv_successor_predecessor_valuation_maximal. bpv_gap_bfv_successor_predecessor_valuation_maximal + bpv_candidate_bfv_successor_predecessor_valuation = e)))) -> (((exists bpv_gap_bfv_successor_factor_exponent_bound. bpv_gap_bfv_successor_factor_exponent_bound + f = sn) /\ (exists bpv_result_bfv_successor_factor_selected. ((exists ff_b_bfv_successor_factor_selected_power ff_c_bfv_successor_factor_selected_power. ((forall ff_i_bfv_successor_factor_selected_power_repeat. (exists ff_lt_bfv_successor_factor_selected_power_repeat_bound. ff_lt_bfv_successor_factor_selected_power_repeat_bound + S ff_i_bfv_successor_factor_selected_power_repeat = f) -> (((exists ff_h_bfv_successor_factor_selected_power_repeat_decoded. ff_h_bfv_successor_factor_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_successor_factor_selected_power_repeat)) * ff_c_bfv_successor_factor_selected_power)) /\ exists ff_q_bfv_successor_factor_selected_power_repeat_decoded. ff_b_bfv_successor_factor_selected_power = ff_q_bfv_successor_factor_selected_power_repeat_decoded * S ((S (ff_i_bfv_successor_factor_selected_power_repeat)) * ff_c_bfv_successor_factor_selected_power) + (p)))) /\ (exists ff_u_bfv_successor_factor_selected_power_product ff_v_bfv_successor_factor_selected_power_product. ((((exists ff_h_bfv_successor_factor_selected_power_product_start. ff_h_bfv_successor_factor_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_successor_factor_selected_power_product)) /\ exists ff_q_bfv_successor_factor_selected_power_product_start. ff_u_bfv_successor_factor_selected_power_product = ff_q_bfv_successor_factor_selected_power_product_start * S ((S (0)) * ff_v_bfv_successor_factor_selected_power_product) + (1))) /\ ((((exists ff_h_bfv_successor_factor_selected_power_product_terminal. ff_h_bfv_successor_factor_selected_power_product_terminal + S (bpv_result_bfv_successor_factor_selected) = S ((S (f)) * ff_v_bfv_successor_factor_selected_power_product)) /\ exists ff_q_bfv_successor_factor_selected_power_product_terminal. ff_u_bfv_successor_factor_selected_power_product = ff_q_bfv_successor_factor_selected_power_product_terminal * S ((S (f)) * ff_v_bfv_successor_factor_selected_power_product) + (bpv_result_bfv_successor_factor_selected))) /\ forall ff_i_bfv_successor_factor_selected_power_product. (exists ff_lt_bfv_successor_factor_selected_power_product_bound. ff_lt_bfv_successor_factor_selected_power_product_bound + S ff_i_bfv_successor_factor_selected_power_product = f) -> exists ff_p_bfv_successor_factor_selected_power_product ff_r_bfv_successor_factor_selected_power_product ff_s_bfv_successor_factor_selected_power_product. ((((exists ff_h_bfv_successor_factor_selected_power_product_factor. ff_h_bfv_successor_factor_selected_power_product_factor + S (ff_p_bfv_successor_factor_selected_power_product) = S ((S (ff_i_bfv_successor_factor_selected_power_product)) * ff_c_bfv_successor_factor_selected_power)) /\ exists ff_q_bfv_successor_factor_selected_power_product_factor. ff_b_bfv_successor_factor_selected_power = ff_q_bfv_successor_factor_selected_power_product_factor * S ((S (ff_i_bfv_successor_factor_selected_power_product)) * ff_c_bfv_successor_factor_selected_power) + (ff_p_bfv_successor_factor_selected_power_product))) /\ ((((exists ff_h_bfv_successor_factor_selected_power_product_partial. ff_h_bfv_successor_factor_selected_power_product_partial + S (ff_r_bfv_successor_factor_selected_power_product) = S ((S (ff_i_bfv_successor_factor_selected_power_product)) * ff_v_bfv_successor_factor_selected_power_product)) /\ exists ff_q_bfv_successor_factor_selected_power_product_partial. ff_u_bfv_successor_factor_selected_power_product = ff_q_bfv_successor_factor_selected_power_product_partial * S ((S (ff_i_bfv_successor_factor_selected_power_product)) * ff_v_bfv_successor_factor_selected_power_product) + (ff_r_bfv_successor_factor_selected_power_product))) /\ ((((exists ff_h_bfv_successor_factor_selected_power_product_successor. ff_h_bfv_successor_factor_selected_power_product_successor + S (ff_s_bfv_successor_factor_selected_power_product) = S ((S (S ff_i_bfv_successor_factor_selected_power_product)) * ff_v_bfv_successor_factor_selected_power_product)) /\ exists ff_q_bfv_successor_factor_selected_power_product_successor. ff_u_bfv_successor_factor_selected_power_product = ff_q_bfv_successor_factor_selected_power_product_successor * S ((S (S ff_i_bfv_successor_factor_selected_power_product)) * ff_v_bfv_successor_factor_selected_power_product) + (ff_s_bfv_successor_factor_selected_power_product))) /\ ff_s_bfv_successor_factor_selected_power_product = ff_r_bfv_successor_factor_selected_power_product * ff_p_bfv_successor_factor_selected_power_product)))))))) /\ (exists bpv_factor_bfv_successor_factor_selected_divides. sn = bpv_result_bfv_successor_factor_selected * bpv_factor_bfv_successor_factor_selected_divides)))) /\ forall bpv_candidate_bfv_successor_factor. (exists bpv_gap_bfv_successor_factor_candidate_bound. bpv_gap_bfv_successor_factor_candidate_bound + bpv_candidate_bfv_successor_factor = sn) -> (exists bpv_result_bfv_successor_factor_candidate. ((exists ff_b_bfv_successor_factor_candidate_power ff_c_bfv_successor_factor_candidate_power. ((forall ff_i_bfv_successor_factor_candidate_power_repeat. (exists ff_lt_bfv_successor_factor_candidate_power_repeat_bound. ff_lt_bfv_successor_factor_candidate_power_repeat_bound + S ff_i_bfv_successor_factor_candidate_power_repeat = bpv_candidate_bfv_successor_factor) -> (((exists ff_h_bfv_successor_factor_candidate_power_repeat_decoded. ff_h_bfv_successor_factor_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_successor_factor_candidate_power_repeat)) * ff_c_bfv_successor_factor_candidate_power)) /\ exists ff_q_bfv_successor_factor_candidate_power_repeat_decoded. ff_b_bfv_successor_factor_candidate_power = ff_q_bfv_successor_factor_candidate_power_repeat_decoded * S ((S (ff_i_bfv_successor_factor_candidate_power_repeat)) * ff_c_bfv_successor_factor_candidate_power) + (p)))) /\ (exists ff_u_bfv_successor_factor_candidate_power_product ff_v_bfv_successor_factor_candidate_power_product. ((((exists ff_h_bfv_successor_factor_candidate_power_product_start. ff_h_bfv_successor_factor_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_successor_factor_candidate_power_product)) /\ exists ff_q_bfv_successor_factor_candidate_power_product_start. ff_u_bfv_successor_factor_candidate_power_product = ff_q_bfv_successor_factor_candidate_power_product_start * S ((S (0)) * ff_v_bfv_successor_factor_candidate_power_product) + (1))) /\ ((((exists ff_h_bfv_successor_factor_candidate_power_product_terminal. ff_h_bfv_successor_factor_candidate_power_product_terminal + S (bpv_result_bfv_successor_factor_candidate) = S ((S (bpv_candidate_bfv_successor_factor)) * ff_v_bfv_successor_factor_candidate_power_product)) /\ exists ff_q_bfv_successor_factor_candidate_power_product_terminal. ff_u_bfv_successor_factor_candidate_power_product = ff_q_bfv_successor_factor_candidate_power_product_terminal * S ((S (bpv_candidate_bfv_successor_factor)) * ff_v_bfv_successor_factor_candidate_power_product) + (bpv_result_bfv_successor_factor_candidate))) /\ forall ff_i_bfv_successor_factor_candidate_power_product. (exists ff_lt_bfv_successor_factor_candidate_power_product_bound. ff_lt_bfv_successor_factor_candidate_power_product_bound + S ff_i_bfv_successor_factor_candidate_power_product = bpv_candidate_bfv_successor_factor) -> exists ff_p_bfv_successor_factor_candidate_power_product ff_r_bfv_successor_factor_candidate_power_product ff_s_bfv_successor_factor_candidate_power_product. ((((exists ff_h_bfv_successor_factor_candidate_power_product_factor. ff_h_bfv_successor_factor_candidate_power_product_factor + S (ff_p_bfv_successor_factor_candidate_power_product) = S ((S (ff_i_bfv_successor_factor_candidate_power_product)) * ff_c_bfv_successor_factor_candidate_power)) /\ exists ff_q_bfv_successor_factor_candidate_power_product_factor. ff_b_bfv_successor_factor_candidate_power = ff_q_bfv_successor_factor_candidate_power_product_factor * S ((S (ff_i_bfv_successor_factor_candidate_power_product)) * ff_c_bfv_successor_factor_candidate_power) + (ff_p_bfv_successor_factor_candidate_power_product))) /\ ((((exists ff_h_bfv_successor_factor_candidate_power_product_partial. ff_h_bfv_successor_factor_candidate_power_product_partial + S (ff_r_bfv_successor_factor_candidate_power_product) = S ((S (ff_i_bfv_successor_factor_candidate_power_product)) * ff_v_bfv_successor_factor_candidate_power_product)) /\ exists ff_q_bfv_successor_factor_candidate_power_product_partial. ff_u_bfv_successor_factor_candidate_power_product = ff_q_bfv_successor_factor_candidate_power_product_partial * S ((S (ff_i_bfv_successor_factor_candidate_power_product)) * ff_v_bfv_successor_factor_candidate_power_product) + (ff_r_bfv_successor_factor_candidate_power_product))) /\ ((((exists ff_h_bfv_successor_factor_candidate_power_product_successor. ff_h_bfv_successor_factor_candidate_power_product_successor + S (ff_s_bfv_successor_factor_candidate_power_product) = S ((S (S ff_i_bfv_successor_factor_candidate_power_product)) * ff_v_bfv_successor_factor_candidate_power_product)) /\ exists ff_q_bfv_successor_factor_candidate_power_product_successor. ff_u_bfv_successor_factor_candidate_power_product = ff_q_bfv_successor_factor_candidate_power_product_successor * S ((S (S ff_i_bfv_successor_factor_candidate_power_product)) * ff_v_bfv_successor_factor_candidate_power_product) + (ff_s_bfv_successor_factor_candidate_power_product))) /\ ff_s_bfv_successor_factor_candidate_power_product = ff_r_bfv_successor_factor_candidate_power_product * ff_p_bfv_successor_factor_candidate_power_product)))))))) /\ (exists bpv_factor_bfv_successor_factor_candidate_divides. sn = bpv_result_bfv_successor_factor_candidate * bpv_factor_bfv_successor_factor_candidate_divides))) -> (exists bpv_gap_bfv_successor_factor_maximal. bpv_gap_bfv_successor_factor_maximal + bpv_candidate_bfv_successor_factor = f)) -> (exists bfv_factorial_bfv_successor_value. ((exists ff_b_bfv_successor_value_factorial ff_c_bfv_successor_value_factorial. ((forall ff_i_bfv_successor_value_factorial_range. (exists ff_lt_bfv_successor_value_factorial_range_bound. ff_lt_bfv_successor_value_factorial_range_bound + S ff_i_bfv_successor_value_factorial_range = sn) -> (((exists ff_h_bfv_successor_value_factorial_range_decoded. ff_h_bfv_successor_value_factorial_range_decoded + S (1 + ff_i_bfv_successor_value_factorial_range) = S ((S (ff_i_bfv_successor_value_factorial_range)) * ff_c_bfv_successor_value_factorial)) /\ exists ff_q_bfv_successor_value_factorial_range_decoded. ff_b_bfv_successor_value_factorial = ff_q_bfv_successor_value_factorial_range_decoded * S ((S (ff_i_bfv_successor_value_factorial_range)) * ff_c_bfv_successor_value_factorial) + (1 + ff_i_bfv_successor_value_factorial_range)))) /\ (exists ff_u_bfv_successor_value_factorial_product ff_v_bfv_successor_value_factorial_product. ((((exists ff_h_bfv_successor_value_factorial_product_start. ff_h_bfv_successor_value_factorial_product_start + S (1) = S ((S (0)) * ff_v_bfv_successor_value_factorial_product)) /\ exists ff_q_bfv_successor_value_factorial_product_start. ff_u_bfv_successor_value_factorial_product = ff_q_bfv_successor_value_factorial_product_start * S ((S (0)) * ff_v_bfv_successor_value_factorial_product) + (1))) /\ ((((exists ff_h_bfv_successor_value_factorial_product_terminal. ff_h_bfv_successor_value_factorial_product_terminal + S (bfv_factorial_bfv_successor_value) = S ((S (sn)) * ff_v_bfv_successor_value_factorial_product)) /\ exists ff_q_bfv_successor_value_factorial_product_terminal. ff_u_bfv_successor_value_factorial_product = ff_q_bfv_successor_value_factorial_product_terminal * S ((S (sn)) * ff_v_bfv_successor_value_factorial_product) + (bfv_factorial_bfv_successor_value))) /\ forall ff_i_bfv_successor_value_factorial_product. (exists ff_lt_bfv_successor_value_factorial_product_bound. ff_lt_bfv_successor_value_factorial_product_bound + S ff_i_bfv_successor_value_factorial_product = sn) -> exists ff_p_bfv_successor_value_factorial_product ff_r_bfv_successor_value_factorial_product ff_s_bfv_successor_value_factorial_product. ((((exists ff_h_bfv_successor_value_factorial_product_factor. ff_h_bfv_successor_value_factorial_product_factor + S (ff_p_bfv_successor_value_factorial_product) = S ((S (ff_i_bfv_successor_value_factorial_product)) * ff_c_bfv_successor_value_factorial)) /\ exists ff_q_bfv_successor_value_factorial_product_factor. ff_b_bfv_successor_value_factorial = ff_q_bfv_successor_value_factorial_product_factor * S ((S (ff_i_bfv_successor_value_factorial_product)) * ff_c_bfv_successor_value_factorial) + (ff_p_bfv_successor_value_factorial_product))) /\ ((((exists ff_h_bfv_successor_value_factorial_product_partial. ff_h_bfv_successor_value_factorial_product_partial + S (ff_r_bfv_successor_value_factorial_product) = S ((S (ff_i_bfv_successor_value_factorial_product)) * ff_v_bfv_successor_value_factorial_product)) /\ exists ff_q_bfv_successor_value_factorial_product_partial. ff_u_bfv_successor_value_factorial_product = ff_q_bfv_successor_value_factorial_product_partial * S ((S (ff_i_bfv_successor_value_factorial_product)) * ff_v_bfv_successor_value_factorial_product) + (ff_r_bfv_successor_value_factorial_product))) /\ ((((exists ff_h_bfv_successor_value_factorial_product_successor. ff_h_bfv_successor_value_factorial_product_successor + S (ff_s_bfv_successor_value_factorial_product) = S ((S (S ff_i_bfv_successor_value_factorial_product)) * ff_v_bfv_successor_value_factorial_product)) /\ exists ff_q_bfv_successor_value_factorial_product_successor. ff_u_bfv_successor_value_factorial_product = ff_q_bfv_successor_value_factorial_product_successor * S ((S (S ff_i_bfv_successor_value_factorial_product)) * ff_v_bfv_successor_value_factorial_product) + (ff_s_bfv_successor_value_factorial_product))) /\ ff_s_bfv_successor_value_factorial_product = ff_r_bfv_successor_value_factorial_product * ff_p_bfv_successor_value_factorial_product)))))))) /\ (((exists bpv_gap_bfv_successor_value_valuation_exponent_bound. bpv_gap_bfv_successor_value_valuation_exponent_bound + g = bfv_factorial_bfv_successor_value) /\ (exists bpv_result_bfv_successor_value_valuation_selected. ((exists ff_b_bfv_successor_value_valuation_selected_power ff_c_bfv_successor_value_valuation_selected_power. ((forall ff_i_bfv_successor_value_valuation_selected_power_repeat. (exists ff_lt_bfv_successor_value_valuation_selected_power_repeat_bound. ff_lt_bfv_successor_value_valuation_selected_power_repeat_bound + S ff_i_bfv_successor_value_valuation_selected_power_repeat = g) -> (((exists ff_h_bfv_successor_value_valuation_selected_power_repeat_decoded. ff_h_bfv_successor_value_valuation_selected_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_successor_value_valuation_selected_power_repeat)) * ff_c_bfv_successor_value_valuation_selected_power)) /\ exists ff_q_bfv_successor_value_valuation_selected_power_repeat_decoded. ff_b_bfv_successor_value_valuation_selected_power = ff_q_bfv_successor_value_valuation_selected_power_repeat_decoded * S ((S (ff_i_bfv_successor_value_valuation_selected_power_repeat)) * ff_c_bfv_successor_value_valuation_selected_power) + (p)))) /\ (exists ff_u_bfv_successor_value_valuation_selected_power_product ff_v_bfv_successor_value_valuation_selected_power_product. ((((exists ff_h_bfv_successor_value_valuation_selected_power_product_start. ff_h_bfv_successor_value_valuation_selected_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_successor_value_valuation_selected_power_product)) /\ exists ff_q_bfv_successor_value_valuation_selected_power_product_start. ff_u_bfv_successor_value_valuation_selected_power_product = ff_q_bfv_successor_value_valuation_selected_power_product_start * S ((S (0)) * ff_v_bfv_successor_value_valuation_selected_power_product) + (1))) /\ ((((exists ff_h_bfv_successor_value_valuation_selected_power_product_terminal. ff_h_bfv_successor_value_valuation_selected_power_product_terminal + S (bpv_result_bfv_successor_value_valuation_selected) = S ((S (g)) * ff_v_bfv_successor_value_valuation_selected_power_product)) /\ exists ff_q_bfv_successor_value_valuation_selected_power_product_terminal. ff_u_bfv_successor_value_valuation_selected_power_product = ff_q_bfv_successor_value_valuation_selected_power_product_terminal * S ((S (g)) * ff_v_bfv_successor_value_valuation_selected_power_product) + (bpv_result_bfv_successor_value_valuation_selected))) /\ forall ff_i_bfv_successor_value_valuation_selected_power_product. (exists ff_lt_bfv_successor_value_valuation_selected_power_product_bound. ff_lt_bfv_successor_value_valuation_selected_power_product_bound + S ff_i_bfv_successor_value_valuation_selected_power_product = g) -> exists ff_p_bfv_successor_value_valuation_selected_power_product ff_r_bfv_successor_value_valuation_selected_power_product ff_s_bfv_successor_value_valuation_selected_power_product. ((((exists ff_h_bfv_successor_value_valuation_selected_power_product_factor. ff_h_bfv_successor_value_valuation_selected_power_product_factor + S (ff_p_bfv_successor_value_valuation_selected_power_product) = S ((S (ff_i_bfv_successor_value_valuation_selected_power_product)) * ff_c_bfv_successor_value_valuation_selected_power)) /\ exists ff_q_bfv_successor_value_valuation_selected_power_product_factor. ff_b_bfv_successor_value_valuation_selected_power = ff_q_bfv_successor_value_valuation_selected_power_product_factor * S ((S (ff_i_bfv_successor_value_valuation_selected_power_product)) * ff_c_bfv_successor_value_valuation_selected_power) + (ff_p_bfv_successor_value_valuation_selected_power_product))) /\ ((((exists ff_h_bfv_successor_value_valuation_selected_power_product_partial. ff_h_bfv_successor_value_valuation_selected_power_product_partial + S (ff_r_bfv_successor_value_valuation_selected_power_product) = S ((S (ff_i_bfv_successor_value_valuation_selected_power_product)) * ff_v_bfv_successor_value_valuation_selected_power_product)) /\ exists ff_q_bfv_successor_value_valuation_selected_power_product_partial. ff_u_bfv_successor_value_valuation_selected_power_product = ff_q_bfv_successor_value_valuation_selected_power_product_partial * S ((S (ff_i_bfv_successor_value_valuation_selected_power_product)) * ff_v_bfv_successor_value_valuation_selected_power_product) + (ff_r_bfv_successor_value_valuation_selected_power_product))) /\ ((((exists ff_h_bfv_successor_value_valuation_selected_power_product_successor. ff_h_bfv_successor_value_valuation_selected_power_product_successor + S (ff_s_bfv_successor_value_valuation_selected_power_product) = S ((S (S ff_i_bfv_successor_value_valuation_selected_power_product)) * ff_v_bfv_successor_value_valuation_selected_power_product)) /\ exists ff_q_bfv_successor_value_valuation_selected_power_product_successor. ff_u_bfv_successor_value_valuation_selected_power_product = ff_q_bfv_successor_value_valuation_selected_power_product_successor * S ((S (S ff_i_bfv_successor_value_valuation_selected_power_product)) * ff_v_bfv_successor_value_valuation_selected_power_product) + (ff_s_bfv_successor_value_valuation_selected_power_product))) /\ ff_s_bfv_successor_value_valuation_selected_power_product = ff_r_bfv_successor_value_valuation_selected_power_product * ff_p_bfv_successor_value_valuation_selected_power_product)))))))) /\ (exists bpv_factor_bfv_successor_value_valuation_selected_divides. bfv_factorial_bfv_successor_value = bpv_result_bfv_successor_value_valuation_selected * bpv_factor_bfv_successor_value_valuation_selected_divides)))) /\ forall bpv_candidate_bfv_successor_value_valuation. (exists bpv_gap_bfv_successor_value_valuation_candidate_bound. bpv_gap_bfv_successor_value_valuation_candidate_bound + bpv_candidate_bfv_successor_value_valuation = bfv_factorial_bfv_successor_value) -> (exists bpv_result_bfv_successor_value_valuation_candidate. ((exists ff_b_bfv_successor_value_valuation_candidate_power ff_c_bfv_successor_value_valuation_candidate_power. ((forall ff_i_bfv_successor_value_valuation_candidate_power_repeat. (exists ff_lt_bfv_successor_value_valuation_candidate_power_repeat_bound. ff_lt_bfv_successor_value_valuation_candidate_power_repeat_bound + S ff_i_bfv_successor_value_valuation_candidate_power_repeat = bpv_candidate_bfv_successor_value_valuation) -> (((exists ff_h_bfv_successor_value_valuation_candidate_power_repeat_decoded. ff_h_bfv_successor_value_valuation_candidate_power_repeat_decoded + S (p) = S ((S (ff_i_bfv_successor_value_valuation_candidate_power_repeat)) * ff_c_bfv_successor_value_valuation_candidate_power)) /\ exists ff_q_bfv_successor_value_valuation_candidate_power_repeat_decoded. ff_b_bfv_successor_value_valuation_candidate_power = ff_q_bfv_successor_value_valuation_candidate_power_repeat_decoded * S ((S (ff_i_bfv_successor_value_valuation_candidate_power_repeat)) * ff_c_bfv_successor_value_valuation_candidate_power) + (p)))) /\ (exists ff_u_bfv_successor_value_valuation_candidate_power_product ff_v_bfv_successor_value_valuation_candidate_power_product. ((((exists ff_h_bfv_successor_value_valuation_candidate_power_product_start. ff_h_bfv_successor_value_valuation_candidate_power_product_start + S (1) = S ((S (0)) * ff_v_bfv_successor_value_valuation_candidate_power_product)) /\ exists ff_q_bfv_successor_value_valuation_candidate_power_product_start. ff_u_bfv_successor_value_valuation_candidate_power_product = ff_q_bfv_successor_value_valuation_candidate_power_product_start * S ((S (0)) * ff_v_bfv_successor_value_valuation_candidate_power_product) + (1))) /\ ((((exists ff_h_bfv_successor_value_valuation_candidate_power_product_terminal. ff_h_bfv_successor_value_valuation_candidate_power_product_terminal + S (bpv_result_bfv_successor_value_valuation_candidate) = S ((S (bpv_candidate_bfv_successor_value_valuation)) * ff_v_bfv_successor_value_valuation_candidate_power_product)) /\ exists ff_q_bfv_successor_value_valuation_candidate_power_product_terminal. ff_u_bfv_successor_value_valuation_candidate_power_product = ff_q_bfv_successor_value_valuation_candidate_power_product_terminal * S ((S (bpv_candidate_bfv_successor_value_valuation)) * ff_v_bfv_successor_value_valuation_candidate_power_product) + (bpv_result_bfv_successor_value_valuation_candidate))) /\ forall ff_i_bfv_successor_value_valuation_candidate_power_product. (exists ff_lt_bfv_successor_value_valuation_candidate_power_product_bound. ff_lt_bfv_successor_value_valuation_candidate_power_product_bound + S ff_i_bfv_successor_value_valuation_candidate_power_product = bpv_candidate_bfv_successor_value_valuation) -> exists ff_p_bfv_successor_value_valuation_candidate_power_product ff_r_bfv_successor_value_valuation_candidate_power_product ff_s_bfv_successor_value_valuation_candidate_power_product. ((((exists ff_h_bfv_successor_value_valuation_candidate_power_product_factor. ff_h_bfv_successor_value_valuation_candidate_power_product_factor + S (ff_p_bfv_successor_value_valuation_candidate_power_product) = S ((S (ff_i_bfv_successor_value_valuation_candidate_power_product)) * ff_c_bfv_successor_value_valuation_candidate_power)) /\ exists ff_q_bfv_successor_value_valuation_candidate_power_product_factor. ff_b_bfv_successor_value_valuation_candidate_power = ff_q_bfv_successor_value_valuation_candidate_power_product_factor * S ((S (ff_i_bfv_successor_value_valuation_candidate_power_product)) * ff_c_bfv_successor_value_valuation_candidate_power) + (ff_p_bfv_successor_value_valuation_candidate_power_product))) /\ ((((exists ff_h_bfv_successor_value_valuation_candidate_power_product_partial. ff_h_bfv_successor_value_valuation_candidate_power_product_partial + S (ff_r_bfv_successor_value_valuation_candidate_power_product) = S ((S (ff_i_bfv_successor_value_valuation_candidate_power_product)) * ff_v_bfv_successor_value_valuation_candidate_power_product)) /\ exists ff_q_bfv_successor_value_valuation_candidate_power_product_partial. ff_u_bfv_successor_value_valuation_candidate_power_product = ff_q_bfv_successor_value_valuation_candidate_power_product_partial * S ((S (ff_i_bfv_successor_value_valuation_candidate_power_product)) * ff_v_bfv_successor_value_valuation_candidate_power_product) + (ff_r_bfv_successor_value_valuation_candidate_power_product))) /\ ((((exists ff_h_bfv_successor_value_valuation_candidate_power_product_successor. ff_h_bfv_successor_value_valuation_candidate_power_product_successor + S (ff_s_bfv_successor_value_valuation_candidate_power_product) = S ((S (S ff_i_bfv_successor_value_valuation_candidate_power_product)) * ff_v_bfv_successor_value_valuation_candidate_power_product)) /\ exists ff_q_bfv_successor_value_valuation_candidate_power_product_successor. ff_u_bfv_successor_value_valuation_candidate_power_product = ff_q_bfv_successor_value_valuation_candidate_power_product_successor * S ((S (S ff_i_bfv_successor_value_valuation_candidate_power_product)) * ff_v_bfv_successor_value_valuation_candidate_power_product) + (ff_s_bfv_successor_value_valuation_candidate_power_product))) /\ ff_s_bfv_successor_value_valuation_candidate_power_product = ff_r_bfv_successor_value_valuation_candidate_power_product * ff_p_bfv_successor_value_valuation_candidate_power_product)))))))) /\ (exists bpv_factor_bfv_successor_value_valuation_candidate_divides. bfv_factorial_bfv_successor_value = bpv_result_bfv_successor_value_valuation_candidate * bpv_factor_bfv_successor_value_valuation_candidate_divides))) -> (exists bpv_gap_bfv_successor_value_valuation_maximal. bpv_gap_bfv_successor_value_valuation_maximal + bpv_candidate_bfv_successor_value_valuation = g)))) -> g = e + fProof neighborhood
Direct theorem prerequisites
BT0092 factorial_succ_decompose BT0090 factorial_functional BT00RK factorial_nonzero BT000C succ_ne_zero BT00QT prime_power_valuation_mulDirect theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (5)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–11
Work with arbitrary variables or the premises of the current implication.
- L11
intro hsuccessor
03Separate the logical casesL12–15
04Establish hdecompositionL16–22
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factorial succ decompose.
- L16
have hdecomposition : ∃ R. Factorial(n,R) ∧ x1 = R · S nDefinitions: Factorial(n,R)Original native command in the exact edition - L17
specialize factorial_succ_decompose n - L18
specialize factorial_succ_decompose sn - L19
specialize factorial_succ_decompose x1 - L20
apply factorial_succ_decompose - L21
exact hsn - L22
exact hsuccessor_witness_left
05Separate the logical casesL23–24
06Establish hpredecessor_valueL25–31
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factorial functional.
07Establish hproductL32–38
08Establish hpredecessor_nonzeroL39–45
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factorial nonzero.
09Establish hfactor_nonzeroL46–55
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply succ ne zero.
10Calculate and transport equalitiesL56–57
11Use earlier factsL58–67
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L58
specialize prime_power_valuation_mul p - L59
specialize prime_power_valuation_mul x - L60
specialize prime_power_valuation_mul sn - L61
specialize prime_power_valuation_mul e - L62
specialize prime_power_valuation_mul f - L63
specialize prime_power_valuation_mul g - L64
apply prime_power_valuation_mul - L65
exact hp - L66
exact hpredecessor_nonzero - L67
exact hfactor_nonzero
Original defined command ledger · 70 lines
- 0001
intro p - 0002
intro n - 0003
intro sn - 0004
intro e - 0005
intro f - 0006
intro g - 0007
intro hsn - 0008
intro hp - 0009
intro hpredecessor - 0010
intro hfactor - 0011
intro hsuccessor - 0012
cases hpredecessor - 0013
cases hpredecessor_witness - 0014
cases hsuccessor - 0015
cases hsuccessor_witness - 0016
have hdecomposition : ∃ R. Factorial(n,R) ∧ x1 = R · S nExact native replay line
have hdecomposition : exists R. (exists ff_b_bfv_successor_decomposition ff_c_bfv_successor_decomposition. ((forall ff_i_bfv_successor_decomposition_range. (exists ff_lt_bfv_successor_decomposition_range_bound. ff_lt_bfv_successor_decomposition_range_bound + S ff_i_bfv_successor_decomposition_range = n) -> (((exists ff_h_bfv_successor_decomposition_range_decoded. ff_h_bfv_successor_decomposition_range_decoded + S (1 + ff_i_bfv_successor_decomposition_range) = S ((S (ff_i_bfv_successor_decomposition_range)) * ff_c_bfv_successor_decomposition)) /\ exists ff_q_bfv_successor_decomposition_range_decoded. ff_b_bfv_successor_decomposition = ff_q_bfv_successor_decomposition_range_decoded * S ((S (ff_i_bfv_successor_decomposition_range)) * ff_c_bfv_successor_decomposition) + (1 + ff_i_bfv_successor_decomposition_range)))) /\ (exists ff_u_bfv_successor_decomposition_product ff_v_bfv_successor_decomposition_product. ((((exists ff_h_bfv_successor_decomposition_product_start. ff_h_bfv_successor_decomposition_product_start + S (1) = S ((S (0)) * ff_v_bfv_successor_decomposition_product)) /\ exists ff_q_bfv_successor_decomposition_product_start. ff_u_bfv_successor_decomposition_product = ff_q_bfv_successor_decomposition_product_start * S ((S (0)) * ff_v_bfv_successor_decomposition_product) + (1))) /\ ((((exists ff_h_bfv_successor_decomposition_product_terminal. ff_h_bfv_successor_decomposition_product_terminal + S (R) = S ((S (n)) * ff_v_bfv_successor_decomposition_product)) /\ exists ff_q_bfv_successor_decomposition_product_terminal. ff_u_bfv_successor_decomposition_product = ff_q_bfv_successor_decomposition_product_terminal * S ((S (n)) * ff_v_bfv_successor_decomposition_product) + (R))) /\ forall ff_i_bfv_successor_decomposition_product. (exists ff_lt_bfv_successor_decomposition_product_bound. ff_lt_bfv_successor_decomposition_product_bound + S ff_i_bfv_successor_decomposition_product = n) -> exists ff_p_bfv_successor_decomposition_product ff_r_bfv_successor_decomposition_product ff_s_bfv_successor_decomposition_product. ((((exists ff_h_bfv_successor_decomposition_product_factor. ff_h_bfv_successor_decomposition_product_factor + S (ff_p_bfv_successor_decomposition_product) = S ((S (ff_i_bfv_successor_decomposition_product)) * ff_c_bfv_successor_decomposition)) /\ exists ff_q_bfv_successor_decomposition_product_factor. ff_b_bfv_successor_decomposition = ff_q_bfv_successor_decomposition_product_factor * S ((S (ff_i_bfv_successor_decomposition_product)) * ff_c_bfv_successor_decomposition) + (ff_p_bfv_successor_decomposition_product))) /\ ((((exists ff_h_bfv_successor_decomposition_product_partial. ff_h_bfv_successor_decomposition_product_partial + S (ff_r_bfv_successor_decomposition_product) = S ((S (ff_i_bfv_successor_decomposition_product)) * ff_v_bfv_successor_decomposition_product)) /\ exists ff_q_bfv_successor_decomposition_product_partial. ff_u_bfv_successor_decomposition_product = ff_q_bfv_successor_decomposition_product_partial * S ((S (ff_i_bfv_successor_decomposition_product)) * ff_v_bfv_successor_decomposition_product) + (ff_r_bfv_successor_decomposition_product))) /\ ((((exists ff_h_bfv_successor_decomposition_product_successor. ff_h_bfv_successor_decomposition_product_successor + S (ff_s_bfv_successor_decomposition_product) = S ((S (S ff_i_bfv_successor_decomposition_product)) * ff_v_bfv_successor_decomposition_product)) /\ exists ff_q_bfv_successor_decomposition_product_successor. ff_u_bfv_successor_decomposition_product = ff_q_bfv_successor_decomposition_product_successor * S ((S (S ff_i_bfv_successor_decomposition_product)) * ff_v_bfv_successor_decomposition_product) + (ff_s_bfv_successor_decomposition_product))) /\ ff_s_bfv_successor_decomposition_product = ff_r_bfv_successor_decomposition_product * ff_p_bfv_successor_decomposition_product)))))))) /\ x1 = R * S n - 0017
specialize factorial_succ_decompose n - 0018
specialize factorial_succ_decompose sn - 0019
specialize factorial_succ_decompose x1 - 0020
apply factorial_succ_decompose - 0021
exact hsn - 0022
exact hsuccessor_witness_left - 0023
cases hdecomposition - 0024
cases hdecomposition_witness - 0025
have hpredecessor_value : x2 = x - 0026
specialize factorial_functional n - 0027
specialize factorial_functional x2 - 0028
specialize factorial_functional x - 0029
apply factorial_functional - 0030
exact hdecomposition_witness_left - 0031
exact hpredecessor_witness_left - 0032
have hproduct : x1 = x * sn - 0033
trans x2 * S n - 0034
exact hdecomposition_witness_right - 0035
congr - 0036
exact hpredecessor_value - 0037
symm - 0038
exact hsn - 0039
have hpredecessor_nonzero : ~(x = 0) - 0040
intro hpredecessor_zero - 0041
specialize factorial_nonzero n - 0042
specialize factorial_nonzero x - 0043
apply factorial_nonzero - 0044
exact hpredecessor_witness_left - 0045
exact hpredecessor_zero - 0046
have hfactor_nonzero : ~(sn = 0) - 0047
intro hzero - 0048
specialize succ_ne_zero n - 0049
apply succ_ne_zero - 0050
trans sn - 0051
symm - 0052
exact hsn - 0053
exact hzero - 0054
rewrite hproduct at hsuccessor_witness_right - 0055
rewrite hproduct at hsuccessor_witness_right - 0056
rewrite hproduct at hsuccessor_witness_right - 0057
rewrite hproduct at hsuccessor_witness_right - 0058
specialize prime_power_valuation_mul p - 0059
specialize prime_power_valuation_mul x - 0060
specialize prime_power_valuation_mul sn - 0061
specialize prime_power_valuation_mul e - 0062
specialize prime_power_valuation_mul f - 0063
specialize prime_power_valuation_mul g - 0064
apply prime_power_valuation_mul - 0065
exact hp - 0066
exact hpredecessor_nonzero - 0067
exact hfactor_nonzero - 0068
exact hpredecessor_witness_right - 0069
exact hfactor - 0070
exact hsuccessor_witness_right