BT00SK · Bertrand theorem

power_quotient_successor_pointwise_add

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

Successor prime-power quotients are the old quotients plus their valuation-threshold bits.

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. ∀ f. ∀ b. ∀ c. ∀ d. ∀ e. ∀ z. ∀ v. Prime(p) → PowerValuation(p,S n,f) → PowerQuotPrefix(p,n,b,c,S n) → PowerQuotPrefix(p,S n,d,e,S n) → (∀ x. Lt(x,S n) → ∃ y. BetaAt(z,v,x,y) ∧ (y = 1 ∧ Lt(x,f) ∨ y = 0 ∧ Lt(f,S x))) → ∀ x. ∀ y. ∀ m. ∀ k. Lt(x,S n) → BetaAt(b,c,x,y) → BetaAt(z,v,x,m) → BetaAt(d,e,x,k) → k = y + m

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

PD0002 Lt PD0004 Prime PD0013 BetaAt PD0046 PowerValuation PD0049 PowerQuotPrefix

12 occurrences

In local proof propositions

PD0002 Lt PD0003 Dvd PD0007 DivRem PD0020 Pow PD0044 PowerDivides

10 occurrences

Exact expanded native-PA statement
forall p n f b c d e z v. ((~(p = 1) /\ forall frm_prime_left_legendre_successor_prime frm_prime_right_legendre_successor_prime. p = frm_prime_left_legendre_successor_prime * frm_prime_right_legendre_successor_prime -> frm_prime_left_legendre_successor_prime = 1 \/ frm_prime_right_legendre_successor_prime = 1)) -> ((((exists blsr_le_gap_legendre_successor_pointwise_valuation_exponent_bound. blsr_le_gap_legendre_successor_pointwise_valuation_exponent_bound + (f) = (S n)) /\ (exists bpvi_result_legendre_successor_pointwise_valuation_selected. ((exists bpvi_b_legendre_successor_pointwise_valuation_selected_power bpvi_c_legendre_successor_pointwise_valuation_selected_power. ((forall bpvi_i_legendre_successor_pointwise_valuation_selected_power. (exists bpvi_repeat_gap_legendre_successor_pointwise_valuation_selected_power. bpvi_repeat_gap_legendre_successor_pointwise_valuation_selected_power + S bpvi_i_legendre_successor_pointwise_valuation_selected_power = f) -> (((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_repeat. bpvi_h_legendre_successor_pointwise_valuation_selected_power_repeat + S (p) = S ((S (bpvi_i_legendre_successor_pointwise_valuation_selected_power)) * bpvi_c_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_repeat. bpvi_b_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_repeat * S ((S (bpvi_i_legendre_successor_pointwise_valuation_selected_power)) * bpvi_c_legendre_successor_pointwise_valuation_selected_power) + (p)))) /\ (exists bpvi_u_legendre_successor_pointwise_valuation_selected_power bpvi_v_legendre_successor_pointwise_valuation_selected_power. ((((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_start. bpvi_h_legendre_successor_pointwise_valuation_selected_power_start + S (1) = S ((S (0)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_start. bpvi_u_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_start * S ((S (0)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power) + (1))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_terminal. bpvi_h_legendre_successor_pointwise_valuation_selected_power_terminal + S (bpvi_result_legendre_successor_pointwise_valuation_selected) = S ((S (f)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_terminal. bpvi_u_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_terminal * S ((S (f)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power) + (bpvi_result_legendre_successor_pointwise_valuation_selected))) /\ forall bpvi_j_legendre_successor_pointwise_valuation_selected_power. (exists bpvi_product_gap_legendre_successor_pointwise_valuation_selected_power. bpvi_product_gap_legendre_successor_pointwise_valuation_selected_power + S bpvi_j_legendre_successor_pointwise_valuation_selected_power = f) -> exists bpvi_factor_legendre_successor_pointwise_valuation_selected_power bpvi_partial_legendre_successor_pointwise_valuation_selected_power bpvi_successor_legendre_successor_pointwise_valuation_selected_power. ((((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_factor. bpvi_h_legendre_successor_pointwise_valuation_selected_power_factor + S (bpvi_factor_legendre_successor_pointwise_valuation_selected_power) = S ((S (bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_c_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_factor. bpvi_b_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_factor * S ((S (bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_c_legendre_successor_pointwise_valuation_selected_power) + (bpvi_factor_legendre_successor_pointwise_valuation_selected_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_partial. bpvi_h_legendre_successor_pointwise_valuation_selected_power_partial + S (bpvi_partial_legendre_successor_pointwise_valuation_selected_power) = S ((S (bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_partial. bpvi_u_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_partial * S ((S (bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power) + (bpvi_partial_legendre_successor_pointwise_valuation_selected_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_selected_power_successor. bpvi_h_legendre_successor_pointwise_valuation_selected_power_successor + S (bpvi_successor_legendre_successor_pointwise_valuation_selected_power) = S ((S (S bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_selected_power_successor. bpvi_u_legendre_successor_pointwise_valuation_selected_power = bpvi_q_legendre_successor_pointwise_valuation_selected_power_successor * S ((S (S bpvi_j_legendre_successor_pointwise_valuation_selected_power)) * bpvi_v_legendre_successor_pointwise_valuation_selected_power) + (bpvi_successor_legendre_successor_pointwise_valuation_selected_power))) /\ bpvi_successor_legendre_successor_pointwise_valuation_selected_power = bpvi_partial_legendre_successor_pointwise_valuation_selected_power * bpvi_factor_legendre_successor_pointwise_valuation_selected_power)))))))) /\ exists bpvi_divisor_factor_legendre_successor_pointwise_valuation_selected. S n = bpvi_result_legendre_successor_pointwise_valuation_selected * bpvi_divisor_factor_legendre_successor_pointwise_valuation_selected))) /\ forall blsr_candidate_legendre_successor_pointwise_valuation. (exists blsr_le_gap_legendre_successor_pointwise_valuation_candidate_bound. blsr_le_gap_legendre_successor_pointwise_valuation_candidate_bound + (blsr_candidate_legendre_successor_pointwise_valuation) = (S n)) -> (exists bpvi_result_legendre_successor_pointwise_valuation_candidate. ((exists bpvi_b_legendre_successor_pointwise_valuation_candidate_power bpvi_c_legendre_successor_pointwise_valuation_candidate_power. ((forall bpvi_i_legendre_successor_pointwise_valuation_candidate_power. (exists bpvi_repeat_gap_legendre_successor_pointwise_valuation_candidate_power. bpvi_repeat_gap_legendre_successor_pointwise_valuation_candidate_power + S bpvi_i_legendre_successor_pointwise_valuation_candidate_power = blsr_candidate_legendre_successor_pointwise_valuation) -> (((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_repeat. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_repeat + S (p) = S ((S (bpvi_i_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_c_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_repeat. bpvi_b_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_repeat * S ((S (bpvi_i_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_c_legendre_successor_pointwise_valuation_candidate_power) + (p)))) /\ (exists bpvi_u_legendre_successor_pointwise_valuation_candidate_power bpvi_v_legendre_successor_pointwise_valuation_candidate_power. ((((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_start. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_start + S (1) = S ((S (0)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_start. bpvi_u_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_start * S ((S (0)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power) + (1))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_terminal. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_terminal + S (bpvi_result_legendre_successor_pointwise_valuation_candidate) = S ((S (blsr_candidate_legendre_successor_pointwise_valuation)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_terminal. bpvi_u_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_terminal * S ((S (blsr_candidate_legendre_successor_pointwise_valuation)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power) + (bpvi_result_legendre_successor_pointwise_valuation_candidate))) /\ forall bpvi_j_legendre_successor_pointwise_valuation_candidate_power. (exists bpvi_product_gap_legendre_successor_pointwise_valuation_candidate_power. bpvi_product_gap_legendre_successor_pointwise_valuation_candidate_power + S bpvi_j_legendre_successor_pointwise_valuation_candidate_power = blsr_candidate_legendre_successor_pointwise_valuation) -> exists bpvi_factor_legendre_successor_pointwise_valuation_candidate_power bpvi_partial_legendre_successor_pointwise_valuation_candidate_power bpvi_successor_legendre_successor_pointwise_valuation_candidate_power. ((((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_factor. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_factor + S (bpvi_factor_legendre_successor_pointwise_valuation_candidate_power) = S ((S (bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_c_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_factor. bpvi_b_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_factor * S ((S (bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_c_legendre_successor_pointwise_valuation_candidate_power) + (bpvi_factor_legendre_successor_pointwise_valuation_candidate_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_partial. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_partial + S (bpvi_partial_legendre_successor_pointwise_valuation_candidate_power) = S ((S (bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_partial. bpvi_u_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_partial * S ((S (bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power) + (bpvi_partial_legendre_successor_pointwise_valuation_candidate_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_valuation_candidate_power_successor. bpvi_h_legendre_successor_pointwise_valuation_candidate_power_successor + S (bpvi_successor_legendre_successor_pointwise_valuation_candidate_power) = S ((S (S bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power)) /\ exists bpvi_q_legendre_successor_pointwise_valuation_candidate_power_successor. bpvi_u_legendre_successor_pointwise_valuation_candidate_power = bpvi_q_legendre_successor_pointwise_valuation_candidate_power_successor * S ((S (S bpvi_j_legendre_successor_pointwise_valuation_candidate_power)) * bpvi_v_legendre_successor_pointwise_valuation_candidate_power) + (bpvi_successor_legendre_successor_pointwise_valuation_candidate_power))) /\ bpvi_successor_legendre_successor_pointwise_valuation_candidate_power = bpvi_partial_legendre_successor_pointwise_valuation_candidate_power * bpvi_factor_legendre_successor_pointwise_valuation_candidate_power)))))))) /\ exists bpvi_divisor_factor_legendre_successor_pointwise_valuation_candidate. S n = bpvi_result_legendre_successor_pointwise_valuation_candidate * bpvi_divisor_factor_legendre_successor_pointwise_valuation_candidate)) -> (exists blsr_le_gap_legendre_successor_pointwise_valuation_maximal. blsr_le_gap_legendre_successor_pointwise_valuation_maximal + (blsr_candidate_legendre_successor_pointwise_valuation) = (f)))) -> (forall bls_index_legendre_successor_pointwise_old. (exists bls_gap_legendre_successor_pointwise_old_bound. bls_gap_legendre_successor_pointwise_old_bound + S (bls_index_legendre_successor_pointwise_old) = (S n)) -> exists bls_power_legendre_successor_pointwise_old bls_quotient_legendre_successor_pointwise_old bls_remainder_legendre_successor_pointwise_old. ((exists bpvi_b_bls_legendre_successor_pointwise_old_power bpvi_c_bls_legendre_successor_pointwise_old_power. ((forall bpvi_i_bls_legendre_successor_pointwise_old_power. (exists bpvi_repeat_gap_bls_legendre_successor_pointwise_old_power. bpvi_repeat_gap_bls_legendre_successor_pointwise_old_power + S bpvi_i_bls_legendre_successor_pointwise_old_power = S bls_index_legendre_successor_pointwise_old) -> (((exists bpvi_h_bls_legendre_successor_pointwise_old_power_repeat. bpvi_h_bls_legendre_successor_pointwise_old_power_repeat + S (p) = S ((S (bpvi_i_bls_legendre_successor_pointwise_old_power)) * bpvi_c_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_repeat. bpvi_b_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_repeat * S ((S (bpvi_i_bls_legendre_successor_pointwise_old_power)) * bpvi_c_bls_legendre_successor_pointwise_old_power) + (p)))) /\ (exists bpvi_u_bls_legendre_successor_pointwise_old_power bpvi_v_bls_legendre_successor_pointwise_old_power. ((((exists bpvi_h_bls_legendre_successor_pointwise_old_power_start. bpvi_h_bls_legendre_successor_pointwise_old_power_start + S (1) = S ((S (0)) * bpvi_v_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_start. bpvi_u_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_start * S ((S (0)) * bpvi_v_bls_legendre_successor_pointwise_old_power) + (1))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_old_power_terminal. bpvi_h_bls_legendre_successor_pointwise_old_power_terminal + S (bls_power_legendre_successor_pointwise_old) = S ((S (S bls_index_legendre_successor_pointwise_old)) * bpvi_v_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_terminal. bpvi_u_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_terminal * S ((S (S bls_index_legendre_successor_pointwise_old)) * bpvi_v_bls_legendre_successor_pointwise_old_power) + (bls_power_legendre_successor_pointwise_old))) /\ forall bpvi_j_bls_legendre_successor_pointwise_old_power. (exists bpvi_product_gap_bls_legendre_successor_pointwise_old_power. bpvi_product_gap_bls_legendre_successor_pointwise_old_power + S bpvi_j_bls_legendre_successor_pointwise_old_power = S bls_index_legendre_successor_pointwise_old) -> exists bpvi_factor_bls_legendre_successor_pointwise_old_power bpvi_partial_bls_legendre_successor_pointwise_old_power bpvi_successor_bls_legendre_successor_pointwise_old_power. ((((exists bpvi_h_bls_legendre_successor_pointwise_old_power_factor. bpvi_h_bls_legendre_successor_pointwise_old_power_factor + S (bpvi_factor_bls_legendre_successor_pointwise_old_power) = S ((S (bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_c_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_factor. bpvi_b_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_factor * S ((S (bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_c_bls_legendre_successor_pointwise_old_power) + (bpvi_factor_bls_legendre_successor_pointwise_old_power))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_old_power_partial. bpvi_h_bls_legendre_successor_pointwise_old_power_partial + S (bpvi_partial_bls_legendre_successor_pointwise_old_power) = S ((S (bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_v_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_partial. bpvi_u_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_partial * S ((S (bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_v_bls_legendre_successor_pointwise_old_power) + (bpvi_partial_bls_legendre_successor_pointwise_old_power))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_old_power_successor. bpvi_h_bls_legendre_successor_pointwise_old_power_successor + S (bpvi_successor_bls_legendre_successor_pointwise_old_power) = S ((S (S bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_v_bls_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_old_power_successor. bpvi_u_bls_legendre_successor_pointwise_old_power = bpvi_q_bls_legendre_successor_pointwise_old_power_successor * S ((S (S bpvi_j_bls_legendre_successor_pointwise_old_power)) * bpvi_v_bls_legendre_successor_pointwise_old_power) + (bpvi_successor_bls_legendre_successor_pointwise_old_power))) /\ bpvi_successor_bls_legendre_successor_pointwise_old_power = bpvi_partial_bls_legendre_successor_pointwise_old_power * bpvi_factor_bls_legendre_successor_pointwise_old_power)))))))) /\ ((((exists ff_h_bls_legendre_successor_pointwise_old_quotient_entry. ff_h_bls_legendre_successor_pointwise_old_quotient_entry + S (bls_quotient_legendre_successor_pointwise_old) = S ((S (bls_index_legendre_successor_pointwise_old)) * c)) /\ exists ff_q_bls_legendre_successor_pointwise_old_quotient_entry. b = ff_q_bls_legendre_successor_pointwise_old_quotient_entry * S ((S (bls_index_legendre_successor_pointwise_old)) * c) + (bls_quotient_legendre_successor_pointwise_old))) /\ ((n = bls_power_legendre_successor_pointwise_old * bls_quotient_legendre_successor_pointwise_old + bls_remainder_legendre_successor_pointwise_old /\ exists bls_remainder_gap_legendre_successor_pointwise_old_division. bls_remainder_gap_legendre_successor_pointwise_old_division + S (bls_remainder_legendre_successor_pointwise_old) = bls_power_legendre_successor_pointwise_old))))) -> (forall bls_index_legendre_successor_pointwise_new. (exists bls_gap_legendre_successor_pointwise_new_bound. bls_gap_legendre_successor_pointwise_new_bound + S (bls_index_legendre_successor_pointwise_new) = (S n)) -> exists bls_power_legendre_successor_pointwise_new bls_quotient_legendre_successor_pointwise_new bls_remainder_legendre_successor_pointwise_new. ((exists bpvi_b_bls_legendre_successor_pointwise_new_power bpvi_c_bls_legendre_successor_pointwise_new_power. ((forall bpvi_i_bls_legendre_successor_pointwise_new_power. (exists bpvi_repeat_gap_bls_legendre_successor_pointwise_new_power. bpvi_repeat_gap_bls_legendre_successor_pointwise_new_power + S bpvi_i_bls_legendre_successor_pointwise_new_power = S bls_index_legendre_successor_pointwise_new) -> (((exists bpvi_h_bls_legendre_successor_pointwise_new_power_repeat. bpvi_h_bls_legendre_successor_pointwise_new_power_repeat + S (p) = S ((S (bpvi_i_bls_legendre_successor_pointwise_new_power)) * bpvi_c_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_repeat. bpvi_b_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_repeat * S ((S (bpvi_i_bls_legendre_successor_pointwise_new_power)) * bpvi_c_bls_legendre_successor_pointwise_new_power) + (p)))) /\ (exists bpvi_u_bls_legendre_successor_pointwise_new_power bpvi_v_bls_legendre_successor_pointwise_new_power. ((((exists bpvi_h_bls_legendre_successor_pointwise_new_power_start. bpvi_h_bls_legendre_successor_pointwise_new_power_start + S (1) = S ((S (0)) * bpvi_v_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_start. bpvi_u_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_start * S ((S (0)) * bpvi_v_bls_legendre_successor_pointwise_new_power) + (1))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_new_power_terminal. bpvi_h_bls_legendre_successor_pointwise_new_power_terminal + S (bls_power_legendre_successor_pointwise_new) = S ((S (S bls_index_legendre_successor_pointwise_new)) * bpvi_v_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_terminal. bpvi_u_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_terminal * S ((S (S bls_index_legendre_successor_pointwise_new)) * bpvi_v_bls_legendre_successor_pointwise_new_power) + (bls_power_legendre_successor_pointwise_new))) /\ forall bpvi_j_bls_legendre_successor_pointwise_new_power. (exists bpvi_product_gap_bls_legendre_successor_pointwise_new_power. bpvi_product_gap_bls_legendre_successor_pointwise_new_power + S bpvi_j_bls_legendre_successor_pointwise_new_power = S bls_index_legendre_successor_pointwise_new) -> exists bpvi_factor_bls_legendre_successor_pointwise_new_power bpvi_partial_bls_legendre_successor_pointwise_new_power bpvi_successor_bls_legendre_successor_pointwise_new_power. ((((exists bpvi_h_bls_legendre_successor_pointwise_new_power_factor. bpvi_h_bls_legendre_successor_pointwise_new_power_factor + S (bpvi_factor_bls_legendre_successor_pointwise_new_power) = S ((S (bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_c_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_factor. bpvi_b_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_factor * S ((S (bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_c_bls_legendre_successor_pointwise_new_power) + (bpvi_factor_bls_legendre_successor_pointwise_new_power))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_new_power_partial. bpvi_h_bls_legendre_successor_pointwise_new_power_partial + S (bpvi_partial_bls_legendre_successor_pointwise_new_power) = S ((S (bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_v_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_partial. bpvi_u_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_partial * S ((S (bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_v_bls_legendre_successor_pointwise_new_power) + (bpvi_partial_bls_legendre_successor_pointwise_new_power))) /\ ((((exists bpvi_h_bls_legendre_successor_pointwise_new_power_successor. bpvi_h_bls_legendre_successor_pointwise_new_power_successor + S (bpvi_successor_bls_legendre_successor_pointwise_new_power) = S ((S (S bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_v_bls_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_bls_legendre_successor_pointwise_new_power_successor. bpvi_u_bls_legendre_successor_pointwise_new_power = bpvi_q_bls_legendre_successor_pointwise_new_power_successor * S ((S (S bpvi_j_bls_legendre_successor_pointwise_new_power)) * bpvi_v_bls_legendre_successor_pointwise_new_power) + (bpvi_successor_bls_legendre_successor_pointwise_new_power))) /\ bpvi_successor_bls_legendre_successor_pointwise_new_power = bpvi_partial_bls_legendre_successor_pointwise_new_power * bpvi_factor_bls_legendre_successor_pointwise_new_power)))))))) /\ ((((exists ff_h_bls_legendre_successor_pointwise_new_quotient_entry. ff_h_bls_legendre_successor_pointwise_new_quotient_entry + S (bls_quotient_legendre_successor_pointwise_new) = S ((S (bls_index_legendre_successor_pointwise_new)) * e)) /\ exists ff_q_bls_legendre_successor_pointwise_new_quotient_entry. d = ff_q_bls_legendre_successor_pointwise_new_quotient_entry * S ((S (bls_index_legendre_successor_pointwise_new)) * e) + (bls_quotient_legendre_successor_pointwise_new))) /\ ((S n = bls_power_legendre_successor_pointwise_new * bls_quotient_legendre_successor_pointwise_new + bls_remainder_legendre_successor_pointwise_new /\ exists bls_remainder_gap_legendre_successor_pointwise_new_division. bls_remainder_gap_legendre_successor_pointwise_new_division + S (bls_remainder_legendre_successor_pointwise_new) = bls_power_legendre_successor_pointwise_new))))) -> (forall eis_index_legendre_successor_pointwise_threshold. (exists eis_lt_gap_legendre_successor_pointwise_threshold_bound. eis_lt_gap_legendre_successor_pointwise_threshold_bound + S (eis_index_legendre_successor_pointwise_threshold) = S n) -> exists eis_bit_legendre_successor_pointwise_threshold. ((((exists ff_h_eis_legendre_successor_pointwise_threshold_decoded. ff_h_eis_legendre_successor_pointwise_threshold_decoded + S (eis_bit_legendre_successor_pointwise_threshold) = S ((S (eis_index_legendre_successor_pointwise_threshold)) * v)) /\ exists ff_q_eis_legendre_successor_pointwise_threshold_decoded. z = ff_q_eis_legendre_successor_pointwise_threshold_decoded * S ((S (eis_index_legendre_successor_pointwise_threshold)) * v) + (eis_bit_legendre_successor_pointwise_threshold))) /\ (((eis_bit_legendre_successor_pointwise_threshold = 1 /\ (exists eis_le_gap_legendre_successor_pointwise_threshold_choice_inside. eis_le_gap_legendre_successor_pointwise_threshold_choice_inside + (S eis_index_legendre_successor_pointwise_threshold) = f)) \/ (eis_bit_legendre_successor_pointwise_threshold = 0 /\ (exists eis_lt_gap_legendre_successor_pointwise_threshold_choice_outside. eis_lt_gap_legendre_successor_pointwise_threshold_choice_outside + S (f) = S eis_index_legendre_successor_pointwise_threshold)))))) -> forall i a bit s. (exists blsr_lt_gap_legendre_successor_pointwise_index. blsr_lt_gap_legendre_successor_pointwise_index + S (i) = (S n)) -> (((exists ff_h_legendre_successor_pointwise_old_entry. ff_h_legendre_successor_pointwise_old_entry + S (a) = S ((S (i)) * c)) /\ exists ff_q_legendre_successor_pointwise_old_entry. b = ff_q_legendre_successor_pointwise_old_entry * S ((S (i)) * c) + (a))) -> (((exists ff_h_legendre_successor_pointwise_bit_entry. ff_h_legendre_successor_pointwise_bit_entry + S (bit) = S ((S (i)) * v)) /\ exists ff_q_legendre_successor_pointwise_bit_entry. z = ff_q_legendre_successor_pointwise_bit_entry * S ((S (i)) * v) + (bit))) -> (((exists ff_h_legendre_successor_pointwise_new_entry. ff_h_legendre_successor_pointwise_new_entry + S (s) = S ((S (i)) * e)) /\ exists ff_q_legendre_successor_pointwise_new_entry. d = ff_q_legendre_successor_pointwise_new_entry * S ((S (i)) * e) + (s))) -> s = a + bit

Proof neighborhood

Direct theorem prerequisites

BT00SJ power_quotient_prefix_decoded_divrem BT00JB eisenstein_initial_segment_decoded_choice BT00SI valuation_threshold_bit_decides_power_divides BT0082 pow_functional BT00SH division_successor_quotient_by_bit BT000C succ_ne_zero

Direct theorem dependents

BT00SV prime_legendre_sum_succ

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

127 script commands · 30 reading checkpoints · 7 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)
power quotient prefix decoded divremeisenstein initial segment decoded choicevaluation threshold bit decides power dividespow functionaldivision successor quotient by bitsucc ne zero
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro f
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro d
  7. L7
    intro e
  8. L8
    intro z
  9. L9
    intro v
  10. L10
    intro hp
02Fix variables and assumptionsL11–20

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

  1. L11
    intro hvaluation
  2. L12
    intro holdprefix
  3. L13
    intro hnewprefix
  4. L14
    intro hthreshold
  5. L15
    intro i
  6. L16
    intro a
  7. L17
    intro bit
  8. L18
    intro s
  9. L19
    intro hi
  10. L20
    intro ha
03Fix variables and assumptionsL21–22

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

  1. L21
    intro hbit
  2. L22
    intro hs
04Establish holdL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power quotient prefix decoded divrem.

  1. L23
    have hold : ∃ D. ∃ r. Pow(p,S i,D) ∧ DivRem(n,D,a,r)Definitions: Pow(p,S i,D)DivRem(n,D,a,r)Original native command in the exact edition
  2. L24
    specialize power_quotient_prefix_decoded_divrem p
  3. L25
    specialize power_quotient_prefix_decoded_divrem n
  4. L26
    specialize power_quotient_prefix_decoded_divrem b
  5. L27
    specialize power_quotient_prefix_decoded_divrem c
  6. L28
    specialize power_quotient_prefix_decoded_divrem (S n)
  7. L29
    specialize power_quotient_prefix_decoded_divrem i
  8. L30
    specialize power_quotient_prefix_decoded_divrem a
  9. L31
    apply power_quotient_prefix_decoded_divrem
  10. L32
    exact holdprefix
05Use earlier factsL33–34

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

  1. L33
    exact hi
  2. L34
    exact ha
06Establish hnewL35–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power quotient prefix decoded divrem.

  1. L35
    have hnew : ∃ E. ∃ t. Pow(p,S i,E) ∧ DivRem(S n,E,s,t)Definitions: Pow(p,S i,E)DivRem(S n,E,s,t)Original native command in the exact edition
  2. L36
    specialize power_quotient_prefix_decoded_divrem p
  3. L37
    specialize power_quotient_prefix_decoded_divrem (S n)
  4. L38
    specialize power_quotient_prefix_decoded_divrem d
  5. L39
    specialize power_quotient_prefix_decoded_divrem e
  6. L40
    specialize power_quotient_prefix_decoded_divrem (S n)
  7. L41
    specialize power_quotient_prefix_decoded_divrem i
  8. L42
    specialize power_quotient_prefix_decoded_divrem s
  9. L43
    apply power_quotient_prefix_decoded_divrem
  10. L44
    exact hnewprefix
07Use earlier factsL45–46

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

  1. L45
    exact hi
  2. L46
    exact hs
08Separate the logical casesL47–52

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

  1. L47
    cases hold
  2. L48
    cases hold_witness
  3. L49
    cases hold_witness_witness
  4. L50
    cases hnew
  5. L51
    cases hnew_witness
  6. L52
    cases hnew_witness_witness
09Establish hpowerL53–62

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

  1. L53
    have hpower : x = x2
  2. L54
    specialize pow_functional p
  3. L55
    specialize pow_functional (S i)
  4. L56
    specialize pow_functional x
  5. L57
    specialize pow_functional x2
  6. L58
    apply pow_functional
  7. L59
    exact hold_witness_witness_left
  8. L60
    exact hnew_witness_witness_left
  9. L61
    rewrite <- hpower at hnew_witness_witness_right
  10. L62
    rewrite <- hpower at hnew_witness_witness_right
10Establish hchoiceL63–72

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein initial segment decoded choice.

  1. L63
    have hchoice : bit = 1 ∧ Lt(i,f) ∨ bit = 0 ∧ Lt(f,S i)Definitions: Lt(i,f)Lt(f,S i)Original native command in the exact edition
  2. L64
    specialize eisenstein_initial_segment_decoded_choice f
  3. L65
    specialize eisenstein_initial_segment_decoded_choice z
  4. L66
    specialize eisenstein_initial_segment_decoded_choice v
  5. L67
    specialize eisenstein_initial_segment_decoded_choice (S n)
  6. L68
    specialize eisenstein_initial_segment_decoded_choice i
  7. L69
    specialize eisenstein_initial_segment_decoded_choice bit
  8. L70
    apply eisenstein_initial_segment_decoded_choice
  9. L71
    exact hthreshold
  10. L72
    exact hi
11Use earlier factsL73–73

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

  1. L73
    exact hbit
12Establish hdecisionL74–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply valuation threshold bit decides power divides.

  1. L74
    have hdecision : bit = 1 ∧ PowerDivides(p,S i,S n) ∨ bit = 0 ∧ ¬PowerDivides(p,S i,S n)Definitions: PowerDivides(p,S i,S n)Original native command in the exact edition
  2. L75
    specialize valuation_threshold_bit_decides_power_divides p
  3. L76
    specialize valuation_threshold_bit_decides_power_divides (S n)
  4. L77
    specialize valuation_threshold_bit_decides_power_divides f
  5. L78
    specialize valuation_threshold_bit_decides_power_divides i
  6. L79
    specialize valuation_threshold_bit_decides_power_divides bit
  7. L80
    apply valuation_threshold_bit_decides_power_divides
  8. L81
    exact hp
  9. L82
    specialize succ_ne_zero n
  10. L83
    exact succ_ne_zero
13Use earlier factsL84–85

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

  1. L84
    exact hvaluation
  2. L85
    exact hchoice
14Establish hmultiple_bitL86–86

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

  1. L86
    have hmultiple_bit : bit = 1 ∧ Dvd(x,S n) ∨ bit = 0 ∧ ¬Dvd(x,S n)Definitions: Dvd(x,S n)Original native command in the exact edition
15Separate the logical casesL87–90

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

  1. L87
    cases hdecision
  2. L88
    cases hdecision_left
  3. L89
    left
  4. L90
    split
16Use earlier factsL91–91

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

  1. L91
    exact hdecision_left_left
17Separate the logical casesL92–94

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

  1. L92
    cases hdecision_left_right
  2. L93
    cases hdecision_left_right_witness
  3. L94
    cases hdecision_left_right_witness_right
18Establish hresultL95–102

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

  1. L95
    have hresult : x4 = x
  2. L96
    specialize pow_functional p
  3. L97
    specialize pow_functional (S i)
  4. L98
    specialize pow_functional x4
  5. L99
    specialize pow_functional x
  6. L100
    apply pow_functional
  7. L101
    exact hdecision_left_right_witness_left
  8. L102
    exact hold_witness_witness_left
19Separate the logical casesL103–103

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

  1. L103
    cases hdecision_left_right_witness_right
20Construct an explicit witnessL104–104

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

  1. L104
    exists x5
21Calculate and transport equalitiesL105–105

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

  1. L105
    rewrite <- hresult
22Use earlier factsL106–106

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

  1. L106
    exact hdecision_left_right_witness_right_witness
23Separate the logical casesL107–109

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

  1. L107
    cases hdecision_right
  2. L108
    right
  3. L109
    split
24Use earlier factsL110–110

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

  1. L110
    exact hdecision_right_left
25Fix variables and assumptionsL111–111

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

  1. L111
    intro hmultiple
26Use earlier factsL112–112

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

  1. L112
    apply hdecision_right_right
27Construct an explicit witnessL113–113

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

  1. L113
    exists x
28Separate the logical casesL114–114

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

  1. L114
    split
29Use earlier factsL115–124

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

  1. L115
    exact hold_witness_witness_left
  2. L116
    exact hmultiple
  3. L117
    specialize division_successor_quotient_by_bit x
  4. L118
    specialize division_successor_quotient_by_bit n
  5. L119
    specialize division_successor_quotient_by_bit a
  6. L120
    specialize division_successor_quotient_by_bit x1
  7. L121
    specialize division_successor_quotient_by_bit s
  8. L122
    specialize division_successor_quotient_by_bit x3
  9. L123
    specialize division_successor_quotient_by_bit bit
  10. L124
    apply division_successor_quotient_by_bit
30Use earlier factsL125–127

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

  1. L125
    exact hold_witness_witness_right
  2. L126
    exact hnew_witness_witness_right
  3. L127
    exact hmultiple_bit

Library-wide reading audit

Original defined command ledger · 127 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro f
  4. 0004intro b
  5. 0005intro c
  6. 0006intro d
  7. 0007intro e
  8. 0008intro z
  9. 0009intro v
  10. 0010intro hp
  11. 0011intro hvaluation
  12. 0012intro holdprefix
  13. 0013intro hnewprefix
  14. 0014intro hthreshold
  15. 0015intro i
  16. 0016intro a
  17. 0017intro bit
  18. 0018intro s
  19. 0019intro hi
  20. 0020intro ha
  21. 0021intro hbit
  22. 0022intro hs
  23. 0023have hold : ∃ D. ∃ r. Pow(p,S i,D) ∧ DivRem(n,D,a,r)
    Exact native replay linehave hold : exists D r. ((exists bpvi_b_legendre_successor_pointwise_old_power bpvi_c_legendre_successor_pointwise_old_power. ((forall bpvi_i_legendre_successor_pointwise_old_power. (exists bpvi_repeat_gap_legendre_successor_pointwise_old_power. bpvi_repeat_gap_legendre_successor_pointwise_old_power + S bpvi_i_legendre_successor_pointwise_old_power = S i) -> (((exists bpvi_h_legendre_successor_pointwise_old_power_repeat. bpvi_h_legendre_successor_pointwise_old_power_repeat + S (p) = S ((S (bpvi_i_legendre_successor_pointwise_old_power)) * bpvi_c_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_legendre_successor_pointwise_old_power_repeat. bpvi_b_legendre_successor_pointwise_old_power = bpvi_q_legendre_successor_pointwise_old_power_repeat * S ((S (bpvi_i_legendre_successor_pointwise_old_power)) * bpvi_c_legendre_successor_pointwise_old_power) + (p)))) /\ (exists bpvi_u_legendre_successor_pointwise_old_power bpvi_v_legendre_successor_pointwise_old_power. ((((exists bpvi_h_legendre_successor_pointwise_old_power_start. bpvi_h_legendre_successor_pointwise_old_power_start + S (1) = S ((S (0)) * bpvi_v_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_legendre_successor_pointwise_old_power_start. bpvi_u_legendre_successor_pointwise_old_power = bpvi_q_legendre_successor_pointwise_old_power_start * S ((S (0)) * bpvi_v_legendre_successor_pointwise_old_power) + (1))) /\ ((((exists bpvi_h_legendre_successor_pointwise_old_power_terminal. bpvi_h_legendre_successor_pointwise_old_power_terminal + S (D) = S ((S (S i)) * bpvi_v_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_legendre_successor_pointwise_old_power_terminal. bpvi_u_legendre_successor_pointwise_old_power = bpvi_q_legendre_successor_pointwise_old_power_terminal * S ((S (S i)) * bpvi_v_legendre_successor_pointwise_old_power) + (D))) /\ forall bpvi_j_legendre_successor_pointwise_old_power. (exists bpvi_product_gap_legendre_successor_pointwise_old_power. bpvi_product_gap_legendre_successor_pointwise_old_power + S bpvi_j_legendre_successor_pointwise_old_power = S i) -> exists bpvi_factor_legendre_successor_pointwise_old_power bpvi_partial_legendre_successor_pointwise_old_power bpvi_successor_legendre_successor_pointwise_old_power. ((((exists bpvi_h_legendre_successor_pointwise_old_power_factor. bpvi_h_legendre_successor_pointwise_old_power_factor + S (bpvi_factor_legendre_successor_pointwise_old_power) = S ((S (bpvi_j_legendre_successor_pointwise_old_power)) * bpvi_c_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_legendre_successor_pointwise_old_power_factor. bpvi_b_legendre_successor_pointwise_old_power = bpvi_q_legendre_successor_pointwise_old_power_factor * S ((S (bpvi_j_legendre_successor_pointwise_old_power)) * bpvi_c_legendre_successor_pointwise_old_power) + (bpvi_factor_legendre_successor_pointwise_old_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_old_power_partial. bpvi_h_legendre_successor_pointwise_old_power_partial + S (bpvi_partial_legendre_successor_pointwise_old_power) = S ((S (bpvi_j_legendre_successor_pointwise_old_power)) * bpvi_v_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_legendre_successor_pointwise_old_power_partial. bpvi_u_legendre_successor_pointwise_old_power = bpvi_q_legendre_successor_pointwise_old_power_partial * S ((S (bpvi_j_legendre_successor_pointwise_old_power)) * bpvi_v_legendre_successor_pointwise_old_power) + (bpvi_partial_legendre_successor_pointwise_old_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_old_power_successor. bpvi_h_legendre_successor_pointwise_old_power_successor + S (bpvi_successor_legendre_successor_pointwise_old_power) = S ((S (S bpvi_j_legendre_successor_pointwise_old_power)) * bpvi_v_legendre_successor_pointwise_old_power)) /\ exists bpvi_q_legendre_successor_pointwise_old_power_successor. bpvi_u_legendre_successor_pointwise_old_power = bpvi_q_legendre_successor_pointwise_old_power_successor * S ((S (S bpvi_j_legendre_successor_pointwise_old_power)) * bpvi_v_legendre_successor_pointwise_old_power) + (bpvi_successor_legendre_successor_pointwise_old_power))) /\ bpvi_successor_legendre_successor_pointwise_old_power = bpvi_partial_legendre_successor_pointwise_old_power * bpvi_factor_legendre_successor_pointwise_old_power)))))))) /\ (((n) = (D) * (a) + (r) /\ exists blsr_lt_gap_legendre_successor_pointwise_old_division_bound. blsr_lt_gap_legendre_successor_pointwise_old_division_bound + S (r) = (D))))
  24. 0024specialize power_quotient_prefix_decoded_divrem p
  25. 0025specialize power_quotient_prefix_decoded_divrem n
  26. 0026specialize power_quotient_prefix_decoded_divrem b
  27. 0027specialize power_quotient_prefix_decoded_divrem c
  28. 0028specialize power_quotient_prefix_decoded_divrem (S n)
  29. 0029specialize power_quotient_prefix_decoded_divrem i
  30. 0030specialize power_quotient_prefix_decoded_divrem a
  31. 0031apply power_quotient_prefix_decoded_divrem
  32. 0032exact holdprefix
  33. 0033exact hi
  34. 0034exact ha
  35. 0035have hnew : ∃ E. ∃ t. Pow(p,S i,E) ∧ DivRem(S n,E,s,t)
    Exact native replay linehave hnew : exists E t. ((exists bpvi_b_legendre_successor_pointwise_new_power bpvi_c_legendre_successor_pointwise_new_power. ((forall bpvi_i_legendre_successor_pointwise_new_power. (exists bpvi_repeat_gap_legendre_successor_pointwise_new_power. bpvi_repeat_gap_legendre_successor_pointwise_new_power + S bpvi_i_legendre_successor_pointwise_new_power = S i) -> (((exists bpvi_h_legendre_successor_pointwise_new_power_repeat. bpvi_h_legendre_successor_pointwise_new_power_repeat + S (p) = S ((S (bpvi_i_legendre_successor_pointwise_new_power)) * bpvi_c_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_legendre_successor_pointwise_new_power_repeat. bpvi_b_legendre_successor_pointwise_new_power = bpvi_q_legendre_successor_pointwise_new_power_repeat * S ((S (bpvi_i_legendre_successor_pointwise_new_power)) * bpvi_c_legendre_successor_pointwise_new_power) + (p)))) /\ (exists bpvi_u_legendre_successor_pointwise_new_power bpvi_v_legendre_successor_pointwise_new_power. ((((exists bpvi_h_legendre_successor_pointwise_new_power_start. bpvi_h_legendre_successor_pointwise_new_power_start + S (1) = S ((S (0)) * bpvi_v_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_legendre_successor_pointwise_new_power_start. bpvi_u_legendre_successor_pointwise_new_power = bpvi_q_legendre_successor_pointwise_new_power_start * S ((S (0)) * bpvi_v_legendre_successor_pointwise_new_power) + (1))) /\ ((((exists bpvi_h_legendre_successor_pointwise_new_power_terminal. bpvi_h_legendre_successor_pointwise_new_power_terminal + S (E) = S ((S (S i)) * bpvi_v_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_legendre_successor_pointwise_new_power_terminal. bpvi_u_legendre_successor_pointwise_new_power = bpvi_q_legendre_successor_pointwise_new_power_terminal * S ((S (S i)) * bpvi_v_legendre_successor_pointwise_new_power) + (E))) /\ forall bpvi_j_legendre_successor_pointwise_new_power. (exists bpvi_product_gap_legendre_successor_pointwise_new_power. bpvi_product_gap_legendre_successor_pointwise_new_power + S bpvi_j_legendre_successor_pointwise_new_power = S i) -> exists bpvi_factor_legendre_successor_pointwise_new_power bpvi_partial_legendre_successor_pointwise_new_power bpvi_successor_legendre_successor_pointwise_new_power. ((((exists bpvi_h_legendre_successor_pointwise_new_power_factor. bpvi_h_legendre_successor_pointwise_new_power_factor + S (bpvi_factor_legendre_successor_pointwise_new_power) = S ((S (bpvi_j_legendre_successor_pointwise_new_power)) * bpvi_c_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_legendre_successor_pointwise_new_power_factor. bpvi_b_legendre_successor_pointwise_new_power = bpvi_q_legendre_successor_pointwise_new_power_factor * S ((S (bpvi_j_legendre_successor_pointwise_new_power)) * bpvi_c_legendre_successor_pointwise_new_power) + (bpvi_factor_legendre_successor_pointwise_new_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_new_power_partial. bpvi_h_legendre_successor_pointwise_new_power_partial + S (bpvi_partial_legendre_successor_pointwise_new_power) = S ((S (bpvi_j_legendre_successor_pointwise_new_power)) * bpvi_v_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_legendre_successor_pointwise_new_power_partial. bpvi_u_legendre_successor_pointwise_new_power = bpvi_q_legendre_successor_pointwise_new_power_partial * S ((S (bpvi_j_legendre_successor_pointwise_new_power)) * bpvi_v_legendre_successor_pointwise_new_power) + (bpvi_partial_legendre_successor_pointwise_new_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_new_power_successor. bpvi_h_legendre_successor_pointwise_new_power_successor + S (bpvi_successor_legendre_successor_pointwise_new_power) = S ((S (S bpvi_j_legendre_successor_pointwise_new_power)) * bpvi_v_legendre_successor_pointwise_new_power)) /\ exists bpvi_q_legendre_successor_pointwise_new_power_successor. bpvi_u_legendre_successor_pointwise_new_power = bpvi_q_legendre_successor_pointwise_new_power_successor * S ((S (S bpvi_j_legendre_successor_pointwise_new_power)) * bpvi_v_legendre_successor_pointwise_new_power) + (bpvi_successor_legendre_successor_pointwise_new_power))) /\ bpvi_successor_legendre_successor_pointwise_new_power = bpvi_partial_legendre_successor_pointwise_new_power * bpvi_factor_legendre_successor_pointwise_new_power)))))))) /\ (((S n) = (E) * (s) + (t) /\ exists blsr_lt_gap_legendre_successor_pointwise_new_division_bound. blsr_lt_gap_legendre_successor_pointwise_new_division_bound + S (t) = (E))))
  36. 0036specialize power_quotient_prefix_decoded_divrem p
  37. 0037specialize power_quotient_prefix_decoded_divrem (S n)
  38. 0038specialize power_quotient_prefix_decoded_divrem d
  39. 0039specialize power_quotient_prefix_decoded_divrem e
  40. 0040specialize power_quotient_prefix_decoded_divrem (S n)
  41. 0041specialize power_quotient_prefix_decoded_divrem i
  42. 0042specialize power_quotient_prefix_decoded_divrem s
  43. 0043apply power_quotient_prefix_decoded_divrem
  44. 0044exact hnewprefix
  45. 0045exact hi
  46. 0046exact hs
  47. 0047cases hold
  48. 0048cases hold_witness
  49. 0049cases hold_witness_witness
  50. 0050cases hnew
  51. 0051cases hnew_witness
  52. 0052cases hnew_witness_witness
  53. 0053have hpower : x = x2
  54. 0054specialize pow_functional p
  55. 0055specialize pow_functional (S i)
  56. 0056specialize pow_functional x
  57. 0057specialize pow_functional x2
  58. 0058apply pow_functional
  59. 0059exact hold_witness_witness_left
  60. 0060exact hnew_witness_witness_left
  61. 0061rewrite <- hpower at hnew_witness_witness_right
  62. 0062rewrite <- hpower at hnew_witness_witness_right
  63. 0063have hchoice : bit = 1 ∧ Lt(i,f) ∨ bit = 0 ∧ Lt(f,S i)
    Exact native replay linehave hchoice : ((bit = 1 /\ (exists eis_le_gap_legendre_successor_pointwise_choice_inside. eis_le_gap_legendre_successor_pointwise_choice_inside + (S i) = f)) \/ (bit = 0 /\ (exists eis_lt_gap_legendre_successor_pointwise_choice_outside. eis_lt_gap_legendre_successor_pointwise_choice_outside + S (f) = S i)))
  64. 0064specialize eisenstein_initial_segment_decoded_choice f
  65. 0065specialize eisenstein_initial_segment_decoded_choice z
  66. 0066specialize eisenstein_initial_segment_decoded_choice v
  67. 0067specialize eisenstein_initial_segment_decoded_choice (S n)
  68. 0068specialize eisenstein_initial_segment_decoded_choice i
  69. 0069specialize eisenstein_initial_segment_decoded_choice bit
  70. 0070apply eisenstein_initial_segment_decoded_choice
  71. 0071exact hthreshold
  72. 0072exact hi
  73. 0073exact hbit
  74. 0074have hdecision : bit = 1 ∧ PowerDivides(p,S i,S n) ∨ bit = 0 ∧ ¬PowerDivides(p,S i,S n)
    Exact native replay linehave hdecision : ((bit = 1 /\ exists bpvi_result_legendre_successor_pointwise_decision_left. ((exists bpvi_b_legendre_successor_pointwise_decision_left_power bpvi_c_legendre_successor_pointwise_decision_left_power. ((forall bpvi_i_legendre_successor_pointwise_decision_left_power. (exists bpvi_repeat_gap_legendre_successor_pointwise_decision_left_power. bpvi_repeat_gap_legendre_successor_pointwise_decision_left_power + S bpvi_i_legendre_successor_pointwise_decision_left_power = S i) -> (((exists bpvi_h_legendre_successor_pointwise_decision_left_power_repeat. bpvi_h_legendre_successor_pointwise_decision_left_power_repeat + S (p) = S ((S (bpvi_i_legendre_successor_pointwise_decision_left_power)) * bpvi_c_legendre_successor_pointwise_decision_left_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_left_power_repeat. bpvi_b_legendre_successor_pointwise_decision_left_power = bpvi_q_legendre_successor_pointwise_decision_left_power_repeat * S ((S (bpvi_i_legendre_successor_pointwise_decision_left_power)) * bpvi_c_legendre_successor_pointwise_decision_left_power) + (p)))) /\ (exists bpvi_u_legendre_successor_pointwise_decision_left_power bpvi_v_legendre_successor_pointwise_decision_left_power. ((((exists bpvi_h_legendre_successor_pointwise_decision_left_power_start. bpvi_h_legendre_successor_pointwise_decision_left_power_start + S (1) = S ((S (0)) * bpvi_v_legendre_successor_pointwise_decision_left_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_left_power_start. bpvi_u_legendre_successor_pointwise_decision_left_power = bpvi_q_legendre_successor_pointwise_decision_left_power_start * S ((S (0)) * bpvi_v_legendre_successor_pointwise_decision_left_power) + (1))) /\ ((((exists bpvi_h_legendre_successor_pointwise_decision_left_power_terminal. bpvi_h_legendre_successor_pointwise_decision_left_power_terminal + S (bpvi_result_legendre_successor_pointwise_decision_left) = S ((S (S i)) * bpvi_v_legendre_successor_pointwise_decision_left_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_left_power_terminal. bpvi_u_legendre_successor_pointwise_decision_left_power = bpvi_q_legendre_successor_pointwise_decision_left_power_terminal * S ((S (S i)) * bpvi_v_legendre_successor_pointwise_decision_left_power) + (bpvi_result_legendre_successor_pointwise_decision_left))) /\ forall bpvi_j_legendre_successor_pointwise_decision_left_power. (exists bpvi_product_gap_legendre_successor_pointwise_decision_left_power. bpvi_product_gap_legendre_successor_pointwise_decision_left_power + S bpvi_j_legendre_successor_pointwise_decision_left_power = S i) -> exists bpvi_factor_legendre_successor_pointwise_decision_left_power bpvi_partial_legendre_successor_pointwise_decision_left_power bpvi_successor_legendre_successor_pointwise_decision_left_power. ((((exists bpvi_h_legendre_successor_pointwise_decision_left_power_factor. bpvi_h_legendre_successor_pointwise_decision_left_power_factor + S (bpvi_factor_legendre_successor_pointwise_decision_left_power) = S ((S (bpvi_j_legendre_successor_pointwise_decision_left_power)) * bpvi_c_legendre_successor_pointwise_decision_left_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_left_power_factor. bpvi_b_legendre_successor_pointwise_decision_left_power = bpvi_q_legendre_successor_pointwise_decision_left_power_factor * S ((S (bpvi_j_legendre_successor_pointwise_decision_left_power)) * bpvi_c_legendre_successor_pointwise_decision_left_power) + (bpvi_factor_legendre_successor_pointwise_decision_left_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_decision_left_power_partial. bpvi_h_legendre_successor_pointwise_decision_left_power_partial + S (bpvi_partial_legendre_successor_pointwise_decision_left_power) = S ((S (bpvi_j_legendre_successor_pointwise_decision_left_power)) * bpvi_v_legendre_successor_pointwise_decision_left_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_left_power_partial. bpvi_u_legendre_successor_pointwise_decision_left_power = bpvi_q_legendre_successor_pointwise_decision_left_power_partial * S ((S (bpvi_j_legendre_successor_pointwise_decision_left_power)) * bpvi_v_legendre_successor_pointwise_decision_left_power) + (bpvi_partial_legendre_successor_pointwise_decision_left_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_decision_left_power_successor. bpvi_h_legendre_successor_pointwise_decision_left_power_successor + S (bpvi_successor_legendre_successor_pointwise_decision_left_power) = S ((S (S bpvi_j_legendre_successor_pointwise_decision_left_power)) * bpvi_v_legendre_successor_pointwise_decision_left_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_left_power_successor. bpvi_u_legendre_successor_pointwise_decision_left_power = bpvi_q_legendre_successor_pointwise_decision_left_power_successor * S ((S (S bpvi_j_legendre_successor_pointwise_decision_left_power)) * bpvi_v_legendre_successor_pointwise_decision_left_power) + (bpvi_successor_legendre_successor_pointwise_decision_left_power))) /\ bpvi_successor_legendre_successor_pointwise_decision_left_power = bpvi_partial_legendre_successor_pointwise_decision_left_power * bpvi_factor_legendre_successor_pointwise_decision_left_power)))))))) /\ exists bpvi_divisor_factor_legendre_successor_pointwise_decision_left. S n = bpvi_result_legendre_successor_pointwise_decision_left * bpvi_divisor_factor_legendre_successor_pointwise_decision_left)) \/ (bit = 0 /\ ~(exists bpvi_result_legendre_successor_pointwise_decision_right. ((exists bpvi_b_legendre_successor_pointwise_decision_right_power bpvi_c_legendre_successor_pointwise_decision_right_power. ((forall bpvi_i_legendre_successor_pointwise_decision_right_power. (exists bpvi_repeat_gap_legendre_successor_pointwise_decision_right_power. bpvi_repeat_gap_legendre_successor_pointwise_decision_right_power + S bpvi_i_legendre_successor_pointwise_decision_right_power = S i) -> (((exists bpvi_h_legendre_successor_pointwise_decision_right_power_repeat. bpvi_h_legendre_successor_pointwise_decision_right_power_repeat + S (p) = S ((S (bpvi_i_legendre_successor_pointwise_decision_right_power)) * bpvi_c_legendre_successor_pointwise_decision_right_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_right_power_repeat. bpvi_b_legendre_successor_pointwise_decision_right_power = bpvi_q_legendre_successor_pointwise_decision_right_power_repeat * S ((S (bpvi_i_legendre_successor_pointwise_decision_right_power)) * bpvi_c_legendre_successor_pointwise_decision_right_power) + (p)))) /\ (exists bpvi_u_legendre_successor_pointwise_decision_right_power bpvi_v_legendre_successor_pointwise_decision_right_power. ((((exists bpvi_h_legendre_successor_pointwise_decision_right_power_start. bpvi_h_legendre_successor_pointwise_decision_right_power_start + S (1) = S ((S (0)) * bpvi_v_legendre_successor_pointwise_decision_right_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_right_power_start. bpvi_u_legendre_successor_pointwise_decision_right_power = bpvi_q_legendre_successor_pointwise_decision_right_power_start * S ((S (0)) * bpvi_v_legendre_successor_pointwise_decision_right_power) + (1))) /\ ((((exists bpvi_h_legendre_successor_pointwise_decision_right_power_terminal. bpvi_h_legendre_successor_pointwise_decision_right_power_terminal + S (bpvi_result_legendre_successor_pointwise_decision_right) = S ((S (S i)) * bpvi_v_legendre_successor_pointwise_decision_right_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_right_power_terminal. bpvi_u_legendre_successor_pointwise_decision_right_power = bpvi_q_legendre_successor_pointwise_decision_right_power_terminal * S ((S (S i)) * bpvi_v_legendre_successor_pointwise_decision_right_power) + (bpvi_result_legendre_successor_pointwise_decision_right))) /\ forall bpvi_j_legendre_successor_pointwise_decision_right_power. (exists bpvi_product_gap_legendre_successor_pointwise_decision_right_power. bpvi_product_gap_legendre_successor_pointwise_decision_right_power + S bpvi_j_legendre_successor_pointwise_decision_right_power = S i) -> exists bpvi_factor_legendre_successor_pointwise_decision_right_power bpvi_partial_legendre_successor_pointwise_decision_right_power bpvi_successor_legendre_successor_pointwise_decision_right_power. ((((exists bpvi_h_legendre_successor_pointwise_decision_right_power_factor. bpvi_h_legendre_successor_pointwise_decision_right_power_factor + S (bpvi_factor_legendre_successor_pointwise_decision_right_power) = S ((S (bpvi_j_legendre_successor_pointwise_decision_right_power)) * bpvi_c_legendre_successor_pointwise_decision_right_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_right_power_factor. bpvi_b_legendre_successor_pointwise_decision_right_power = bpvi_q_legendre_successor_pointwise_decision_right_power_factor * S ((S (bpvi_j_legendre_successor_pointwise_decision_right_power)) * bpvi_c_legendre_successor_pointwise_decision_right_power) + (bpvi_factor_legendre_successor_pointwise_decision_right_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_decision_right_power_partial. bpvi_h_legendre_successor_pointwise_decision_right_power_partial + S (bpvi_partial_legendre_successor_pointwise_decision_right_power) = S ((S (bpvi_j_legendre_successor_pointwise_decision_right_power)) * bpvi_v_legendre_successor_pointwise_decision_right_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_right_power_partial. bpvi_u_legendre_successor_pointwise_decision_right_power = bpvi_q_legendre_successor_pointwise_decision_right_power_partial * S ((S (bpvi_j_legendre_successor_pointwise_decision_right_power)) * bpvi_v_legendre_successor_pointwise_decision_right_power) + (bpvi_partial_legendre_successor_pointwise_decision_right_power))) /\ ((((exists bpvi_h_legendre_successor_pointwise_decision_right_power_successor. bpvi_h_legendre_successor_pointwise_decision_right_power_successor + S (bpvi_successor_legendre_successor_pointwise_decision_right_power) = S ((S (S bpvi_j_legendre_successor_pointwise_decision_right_power)) * bpvi_v_legendre_successor_pointwise_decision_right_power)) /\ exists bpvi_q_legendre_successor_pointwise_decision_right_power_successor. bpvi_u_legendre_successor_pointwise_decision_right_power = bpvi_q_legendre_successor_pointwise_decision_right_power_successor * S ((S (S bpvi_j_legendre_successor_pointwise_decision_right_power)) * bpvi_v_legendre_successor_pointwise_decision_right_power) + (bpvi_successor_legendre_successor_pointwise_decision_right_power))) /\ bpvi_successor_legendre_successor_pointwise_decision_right_power = bpvi_partial_legendre_successor_pointwise_decision_right_power * bpvi_factor_legendre_successor_pointwise_decision_right_power)))))))) /\ exists bpvi_divisor_factor_legendre_successor_pointwise_decision_right. S n = bpvi_result_legendre_successor_pointwise_decision_right * bpvi_divisor_factor_legendre_successor_pointwise_decision_right))))
  75. 0075specialize valuation_threshold_bit_decides_power_divides p
  76. 0076specialize valuation_threshold_bit_decides_power_divides (S n)
  77. 0077specialize valuation_threshold_bit_decides_power_divides f
  78. 0078specialize valuation_threshold_bit_decides_power_divides i
  79. 0079specialize valuation_threshold_bit_decides_power_divides bit
  80. 0080apply valuation_threshold_bit_decides_power_divides
  81. 0081exact hp
  82. 0082specialize succ_ne_zero n
  83. 0083exact succ_ne_zero
  84. 0084exact hvaluation
  85. 0085exact hchoice
  86. 0086have hmultiple_bit : bit = 1 ∧ Dvd(x,S n) ∨ bit = 0 ∧ ¬Dvd(x,S n)
    Exact native replay linehave hmultiple_bit : ((bit = 1 /\ exists k. S n = x * k) \/ (bit = 0 /\ ~(exists k. S n = x * k)))
  87. 0087cases hdecision
  88. 0088cases hdecision_left
  89. 0089left
  90. 0090split
  91. 0091exact hdecision_left_left
  92. 0092cases hdecision_left_right
  93. 0093cases hdecision_left_right_witness
  94. 0094cases hdecision_left_right_witness_right
  95. 0095have hresult : x4 = x
  96. 0096specialize pow_functional p
  97. 0097specialize pow_functional (S i)
  98. 0098specialize pow_functional x4
  99. 0099specialize pow_functional x
  100. 0100apply pow_functional
  101. 0101exact hdecision_left_right_witness_left
  102. 0102exact hold_witness_witness_left
  103. 0103cases hdecision_left_right_witness_right
  104. 0104exists x5
  105. 0105rewrite <- hresult
  106. 0106exact hdecision_left_right_witness_right_witness
  107. 0107cases hdecision_right
  108. 0108right
  109. 0109split
  110. 0110exact hdecision_right_left
  111. 0111intro hmultiple
  112. 0112apply hdecision_right_right
  113. 0113exists x
  114. 0114split
  115. 0115exact hold_witness_witness_left
  116. 0116exact hmultiple
  117. 0117specialize division_successor_quotient_by_bit x
  118. 0118specialize division_successor_quotient_by_bit n
  119. 0119specialize division_successor_quotient_by_bit a
  120. 0120specialize division_successor_quotient_by_bit x1
  121. 0121specialize division_successor_quotient_by_bit s
  122. 0122specialize division_successor_quotient_by_bit x3
  123. 0123specialize division_successor_quotient_by_bit bit
  124. 0124apply division_successor_quotient_by_bit
  125. 0125exact hold_witness_witness_right
  126. 0126exact hnew_witness_witness_right
  127. 0127exact hmultiple_bit