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.
Exact expanded PA statement
forall p n e g. ((~(p = 1) /\ forall frm_prime_left_b5cvlsepe_prime frm_prime_right_b5cvlsepe_prime. p = frm_prime_left_b5cvlsepe_prime * frm_prime_right_b5cvlsepe_prime -> frm_prime_left_b5cvlsepe_prime = 1 \/ frm_prime_right_b5cvlsepe_prime = 1)) -> (exists bls_code_b5cvlsepe_legendre bls_scale_b5cvlsepe_legendre. ((forall bls_index_b5cvlsepe_legendre_prefix. (exists bls_gap_b5cvlsepe_legendre_prefix_bound. bls_gap_b5cvlsepe_legendre_prefix_bound + S (bls_index_b5cvlsepe_legendre_prefix) = (n)) -> exists bls_power_b5cvlsepe_legendre_prefix bls_quotient_b5cvlsepe_legendre_prefix bls_remainder_b5cvlsepe_legendre_prefix. ((exists bpvi_b_bls_b5cvlsepe_legendre_prefix_power bpvi_c_bls_b5cvlsepe_legendre_prefix_power. ((forall bpvi_i_bls_b5cvlsepe_legendre_prefix_power. (exists bpvi_repeat_gap_bls_b5cvlsepe_legendre_prefix_power. bpvi_repeat_gap_bls_b5cvlsepe_legendre_prefix_power + S bpvi_i_bls_b5cvlsepe_legendre_prefix_power = S bls_index_b5cvlsepe_legendre_prefix) -> (((exists bpvi_h_bls_b5cvlsepe_legendre_prefix_power_repeat. bpvi_h_bls_b5cvlsepe_legendre_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_b5cvlsepe_legendre_prefix_power)) * bpvi_c_bls_b5cvlsepe_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_legendre_prefix_power_repeat. bpvi_b_bls_b5cvlsepe_legendre_prefix_power = bpvi_q_bls_b5cvlsepe_legendre_prefix_power_repeat * S ((S (bpvi_i_bls_b5cvlsepe_legendre_prefix_power)) * bpvi_c_bls_b5cvlsepe_legendre_prefix_power) + (p)))) /\ (exists bpvi_u_bls_b5cvlsepe_legendre_prefix_power bpvi_v_bls_b5cvlsepe_legendre_prefix_power. ((((exists bpvi_h_bls_b5cvlsepe_legendre_prefix_power_start. bpvi_h_bls_b5cvlsepe_legendre_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5cvlsepe_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_legendre_prefix_power_start. bpvi_u_bls_b5cvlsepe_legendre_prefix_power = bpvi_q_bls_b5cvlsepe_legendre_prefix_power_start * S ((S (0)) * bpvi_v_bls_b5cvlsepe_legendre_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_b5cvlsepe_legendre_prefix_power_terminal. bpvi_h_bls_b5cvlsepe_legendre_prefix_power_terminal + S (bls_power_b5cvlsepe_legendre_prefix) = S ((S (S bls_index_b5cvlsepe_legendre_prefix)) * bpvi_v_bls_b5cvlsepe_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_legendre_prefix_power_terminal. bpvi_u_bls_b5cvlsepe_legendre_prefix_power = bpvi_q_bls_b5cvlsepe_legendre_prefix_power_terminal * S ((S (S bls_index_b5cvlsepe_legendre_prefix)) * bpvi_v_bls_b5cvlsepe_legendre_prefix_power) + (bls_power_b5cvlsepe_legendre_prefix))) /\ forall bpvi_j_bls_b5cvlsepe_legendre_prefix_power. (exists bpvi_product_gap_bls_b5cvlsepe_legendre_prefix_power. bpvi_product_gap_bls_b5cvlsepe_legendre_prefix_power + S bpvi_j_bls_b5cvlsepe_legendre_prefix_power = S bls_index_b5cvlsepe_legendre_prefix) -> exists bpvi_factor_bls_b5cvlsepe_legendre_prefix_power bpvi_partial_bls_b5cvlsepe_legendre_prefix_power bpvi_successor_bls_b5cvlsepe_legendre_prefix_power. ((((exists bpvi_h_bls_b5cvlsepe_legendre_prefix_power_factor. bpvi_h_bls_b5cvlsepe_legendre_prefix_power_factor + S (bpvi_factor_bls_b5cvlsepe_legendre_prefix_power) = S ((S (bpvi_j_bls_b5cvlsepe_legendre_prefix_power)) * bpvi_c_bls_b5cvlsepe_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_legendre_prefix_power_factor. bpvi_b_bls_b5cvlsepe_legendre_prefix_power = bpvi_q_bls_b5cvlsepe_legendre_prefix_power_factor * S ((S (bpvi_j_bls_b5cvlsepe_legendre_prefix_power)) * bpvi_c_bls_b5cvlsepe_legendre_prefix_power) + (bpvi_factor_bls_b5cvlsepe_legendre_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvlsepe_legendre_prefix_power_partial. bpvi_h_bls_b5cvlsepe_legendre_prefix_power_partial + S (bpvi_partial_bls_b5cvlsepe_legendre_prefix_power) = S ((S (bpvi_j_bls_b5cvlsepe_legendre_prefix_power)) * bpvi_v_bls_b5cvlsepe_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_legendre_prefix_power_partial. bpvi_u_bls_b5cvlsepe_legendre_prefix_power = bpvi_q_bls_b5cvlsepe_legendre_prefix_power_partial * S ((S (bpvi_j_bls_b5cvlsepe_legendre_prefix_power)) * bpvi_v_bls_b5cvlsepe_legendre_prefix_power) + (bpvi_partial_bls_b5cvlsepe_legendre_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvlsepe_legendre_prefix_power_successor. bpvi_h_bls_b5cvlsepe_legendre_prefix_power_successor + S (bpvi_successor_bls_b5cvlsepe_legendre_prefix_power) = S ((S (S bpvi_j_bls_b5cvlsepe_legendre_prefix_power)) * bpvi_v_bls_b5cvlsepe_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_legendre_prefix_power_successor. bpvi_u_bls_b5cvlsepe_legendre_prefix_power = bpvi_q_bls_b5cvlsepe_legendre_prefix_power_successor * S ((S (S bpvi_j_bls_b5cvlsepe_legendre_prefix_power)) * bpvi_v_bls_b5cvlsepe_legendre_prefix_power) + (bpvi_successor_bls_b5cvlsepe_legendre_prefix_power))) /\ bpvi_successor_bls_b5cvlsepe_legendre_prefix_power = bpvi_partial_bls_b5cvlsepe_legendre_prefix_power * bpvi_factor_bls_b5cvlsepe_legendre_prefix_power)))))))) /\ ((((exists ff_h_bls_b5cvlsepe_legendre_prefix_quotient_entry. ff_h_bls_b5cvlsepe_legendre_prefix_quotient_entry + S (bls_quotient_b5cvlsepe_legendre_prefix) = S ((S (bls_index_b5cvlsepe_legendre_prefix)) * bls_scale_b5cvlsepe_legendre)) /\ exists ff_q_bls_b5cvlsepe_legendre_prefix_quotient_entry. bls_code_b5cvlsepe_legendre = ff_q_bls_b5cvlsepe_legendre_prefix_quotient_entry * S ((S (bls_index_b5cvlsepe_legendre_prefix)) * bls_scale_b5cvlsepe_legendre) + (bls_quotient_b5cvlsepe_legendre_prefix))) /\ ((n = bls_power_b5cvlsepe_legendre_prefix * bls_quotient_b5cvlsepe_legendre_prefix + bls_remainder_b5cvlsepe_legendre_prefix /\ exists bls_remainder_gap_b5cvlsepe_legendre_prefix_division. bls_remainder_gap_b5cvlsepe_legendre_prefix_division + S (bls_remainder_b5cvlsepe_legendre_prefix) = bls_power_b5cvlsepe_legendre_prefix))))) /\ (exists ff_u_bls_b5cvlsepe_legendre_sum ff_v_bls_b5cvlsepe_legendre_sum. ((((exists ff_h_bls_b5cvlsepe_legendre_sum_start. ff_h_bls_b5cvlsepe_legendre_sum_start + S (0) = S ((S (0)) * ff_v_bls_b5cvlsepe_legendre_sum)) /\ exists ff_q_bls_b5cvlsepe_legendre_sum_start. ff_u_bls_b5cvlsepe_legendre_sum = ff_q_bls_b5cvlsepe_legendre_sum_start * S ((S (0)) * ff_v_bls_b5cvlsepe_legendre_sum) + (0))) /\ ((((exists ff_h_bls_b5cvlsepe_legendre_sum_terminal. ff_h_bls_b5cvlsepe_legendre_sum_terminal + S (e) = S ((S (n)) * ff_v_bls_b5cvlsepe_legendre_sum)) /\ exists ff_q_bls_b5cvlsepe_legendre_sum_terminal. ff_u_bls_b5cvlsepe_legendre_sum = ff_q_bls_b5cvlsepe_legendre_sum_terminal * S ((S (n)) * ff_v_bls_b5cvlsepe_legendre_sum) + (e))) /\ forall ff_i_bls_b5cvlsepe_legendre_sum. (exists ff_lt_bls_b5cvlsepe_legendre_sum_bound. ff_lt_bls_b5cvlsepe_legendre_sum_bound + S ff_i_bls_b5cvlsepe_legendre_sum = n) -> exists ff_a_bls_b5cvlsepe_legendre_sum ff_r_bls_b5cvlsepe_legendre_sum ff_s_bls_b5cvlsepe_legendre_sum. ((((exists ff_h_bls_b5cvlsepe_legendre_sum_summand. ff_h_bls_b5cvlsepe_legendre_sum_summand + S (ff_a_bls_b5cvlsepe_legendre_sum) = S ((S (ff_i_bls_b5cvlsepe_legendre_sum)) * bls_scale_b5cvlsepe_legendre)) /\ exists ff_q_bls_b5cvlsepe_legendre_sum_summand. bls_code_b5cvlsepe_legendre = ff_q_bls_b5cvlsepe_legendre_sum_summand * S ((S (ff_i_bls_b5cvlsepe_legendre_sum)) * bls_scale_b5cvlsepe_legendre) + (ff_a_bls_b5cvlsepe_legendre_sum))) /\ ((((exists ff_h_bls_b5cvlsepe_legendre_sum_partial. ff_h_bls_b5cvlsepe_legendre_sum_partial + S (ff_r_bls_b5cvlsepe_legendre_sum) = S ((S (ff_i_bls_b5cvlsepe_legendre_sum)) * ff_v_bls_b5cvlsepe_legendre_sum)) /\ exists ff_q_bls_b5cvlsepe_legendre_sum_partial. ff_u_bls_b5cvlsepe_legendre_sum = ff_q_bls_b5cvlsepe_legendre_sum_partial * S ((S (ff_i_bls_b5cvlsepe_legendre_sum)) * ff_v_bls_b5cvlsepe_legendre_sum) + (ff_r_bls_b5cvlsepe_legendre_sum))) /\ ((((exists ff_h_bls_b5cvlsepe_legendre_sum_successor. ff_h_bls_b5cvlsepe_legendre_sum_successor + S (ff_s_bls_b5cvlsepe_legendre_sum) = S ((S (S ff_i_bls_b5cvlsepe_legendre_sum)) * ff_v_bls_b5cvlsepe_legendre_sum)) /\ exists ff_q_bls_b5cvlsepe_legendre_sum_successor. ff_u_bls_b5cvlsepe_legendre_sum = ff_q_bls_b5cvlsepe_legendre_sum_successor * S ((S (S ff_i_bls_b5cvlsepe_legendre_sum)) * ff_v_bls_b5cvlsepe_legendre_sum) + (ff_s_bls_b5cvlsepe_legendre_sum))) /\ ff_s_bls_b5cvlsepe_legendre_sum = ff_r_bls_b5cvlsepe_legendre_sum + ff_a_bls_b5cvlsepe_legendre_sum)))))))) -> exists b c. ((forall bls_index_b5cvlsepe_prefix. (exists bls_gap_b5cvlsepe_prefix_bound. bls_gap_b5cvlsepe_prefix_bound + S (bls_index_b5cvlsepe_prefix) = (n + g)) -> exists bls_power_b5cvlsepe_prefix bls_quotient_b5cvlsepe_prefix bls_remainder_b5cvlsepe_prefix. ((exists bpvi_b_bls_b5cvlsepe_prefix_power bpvi_c_bls_b5cvlsepe_prefix_power. ((forall bpvi_i_bls_b5cvlsepe_prefix_power. (exists bpvi_repeat_gap_bls_b5cvlsepe_prefix_power. bpvi_repeat_gap_bls_b5cvlsepe_prefix_power + S bpvi_i_bls_b5cvlsepe_prefix_power = S bls_index_b5cvlsepe_prefix) -> (((exists bpvi_h_bls_b5cvlsepe_prefix_power_repeat. bpvi_h_bls_b5cvlsepe_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_b5cvlsepe_prefix_power)) * bpvi_c_bls_b5cvlsepe_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_prefix_power_repeat. bpvi_b_bls_b5cvlsepe_prefix_power = bpvi_q_bls_b5cvlsepe_prefix_power_repeat * S ((S (bpvi_i_bls_b5cvlsepe_prefix_power)) * bpvi_c_bls_b5cvlsepe_prefix_power) + (p)))) /\ (exists bpvi_u_bls_b5cvlsepe_prefix_power bpvi_v_bls_b5cvlsepe_prefix_power. ((((exists bpvi_h_bls_b5cvlsepe_prefix_power_start. bpvi_h_bls_b5cvlsepe_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5cvlsepe_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_prefix_power_start. bpvi_u_bls_b5cvlsepe_prefix_power = bpvi_q_bls_b5cvlsepe_prefix_power_start * S ((S (0)) * bpvi_v_bls_b5cvlsepe_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_b5cvlsepe_prefix_power_terminal. bpvi_h_bls_b5cvlsepe_prefix_power_terminal + S (bls_power_b5cvlsepe_prefix) = S ((S (S bls_index_b5cvlsepe_prefix)) * bpvi_v_bls_b5cvlsepe_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_prefix_power_terminal. bpvi_u_bls_b5cvlsepe_prefix_power = bpvi_q_bls_b5cvlsepe_prefix_power_terminal * S ((S (S bls_index_b5cvlsepe_prefix)) * bpvi_v_bls_b5cvlsepe_prefix_power) + (bls_power_b5cvlsepe_prefix))) /\ forall bpvi_j_bls_b5cvlsepe_prefix_power. (exists bpvi_product_gap_bls_b5cvlsepe_prefix_power. bpvi_product_gap_bls_b5cvlsepe_prefix_power + S bpvi_j_bls_b5cvlsepe_prefix_power = S bls_index_b5cvlsepe_prefix) -> exists bpvi_factor_bls_b5cvlsepe_prefix_power bpvi_partial_bls_b5cvlsepe_prefix_power bpvi_successor_bls_b5cvlsepe_prefix_power. ((((exists bpvi_h_bls_b5cvlsepe_prefix_power_factor. bpvi_h_bls_b5cvlsepe_prefix_power_factor + S (bpvi_factor_bls_b5cvlsepe_prefix_power) = S ((S (bpvi_j_bls_b5cvlsepe_prefix_power)) * bpvi_c_bls_b5cvlsepe_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_prefix_power_factor. bpvi_b_bls_b5cvlsepe_prefix_power = bpvi_q_bls_b5cvlsepe_prefix_power_factor * S ((S (bpvi_j_bls_b5cvlsepe_prefix_power)) * bpvi_c_bls_b5cvlsepe_prefix_power) + (bpvi_factor_bls_b5cvlsepe_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvlsepe_prefix_power_partial. bpvi_h_bls_b5cvlsepe_prefix_power_partial + S (bpvi_partial_bls_b5cvlsepe_prefix_power) = S ((S (bpvi_j_bls_b5cvlsepe_prefix_power)) * bpvi_v_bls_b5cvlsepe_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_prefix_power_partial. bpvi_u_bls_b5cvlsepe_prefix_power = bpvi_q_bls_b5cvlsepe_prefix_power_partial * S ((S (bpvi_j_bls_b5cvlsepe_prefix_power)) * bpvi_v_bls_b5cvlsepe_prefix_power) + (bpvi_partial_bls_b5cvlsepe_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvlsepe_prefix_power_successor. bpvi_h_bls_b5cvlsepe_prefix_power_successor + S (bpvi_successor_bls_b5cvlsepe_prefix_power) = S ((S (S bpvi_j_bls_b5cvlsepe_prefix_power)) * bpvi_v_bls_b5cvlsepe_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_prefix_power_successor. bpvi_u_bls_b5cvlsepe_prefix_power = bpvi_q_bls_b5cvlsepe_prefix_power_successor * S ((S (S bpvi_j_bls_b5cvlsepe_prefix_power)) * bpvi_v_bls_b5cvlsepe_prefix_power) + (bpvi_successor_bls_b5cvlsepe_prefix_power))) /\ bpvi_successor_bls_b5cvlsepe_prefix_power = bpvi_partial_bls_b5cvlsepe_prefix_power * bpvi_factor_bls_b5cvlsepe_prefix_power)))))))) /\ ((((exists ff_h_bls_b5cvlsepe_prefix_quotient_entry. ff_h_bls_b5cvlsepe_prefix_quotient_entry + S (bls_quotient_b5cvlsepe_prefix) = S ((S (bls_index_b5cvlsepe_prefix)) * c)) /\ exists ff_q_bls_b5cvlsepe_prefix_quotient_entry. b = ff_q_bls_b5cvlsepe_prefix_quotient_entry * S ((S (bls_index_b5cvlsepe_prefix)) * c) + (bls_quotient_b5cvlsepe_prefix))) /\ ((n = bls_power_b5cvlsepe_prefix * bls_quotient_b5cvlsepe_prefix + bls_remainder_b5cvlsepe_prefix /\ exists bls_remainder_gap_b5cvlsepe_prefix_division. bls_remainder_gap_b5cvlsepe_prefix_division + S (bls_remainder_b5cvlsepe_prefix) = bls_power_b5cvlsepe_prefix))))) /\ (exists fs_u_b5cvlsepe_sum fs_v_b5cvlsepe_sum. ((((exists fs_h_b5cvlsepe_sum_body_start. fs_h_b5cvlsepe_sum_body_start + S (0) = S ((S (0)) * fs_v_b5cvlsepe_sum)) /\ exists fs_q_b5cvlsepe_sum_body_start. fs_u_b5cvlsepe_sum = fs_q_b5cvlsepe_sum_body_start * S ((S (0)) * fs_v_b5cvlsepe_sum) + (0))) /\ ((((exists fs_h_b5cvlsepe_sum_body_terminal. fs_h_b5cvlsepe_sum_body_terminal + S (e) = S ((S (n + g)) * fs_v_b5cvlsepe_sum)) /\ exists fs_q_b5cvlsepe_sum_body_terminal. fs_u_b5cvlsepe_sum = fs_q_b5cvlsepe_sum_body_terminal * S ((S (n + g)) * fs_v_b5cvlsepe_sum) + (e))) /\ forall fs_i_b5cvlsepe_sum_body_steps. (exists fs_lt_b5cvlsepe_sum_body_steps_bound. fs_lt_b5cvlsepe_sum_body_steps_bound + S fs_i_b5cvlsepe_sum_body_steps = n + g) -> exists fs_a_b5cvlsepe_sum_body_steps fs_r_b5cvlsepe_sum_body_steps fs_s_b5cvlsepe_sum_body_steps. ((((exists fs_h_b5cvlsepe_sum_body_steps_summand. fs_h_b5cvlsepe_sum_body_steps_summand + S (fs_a_b5cvlsepe_sum_body_steps) = S ((S (fs_i_b5cvlsepe_sum_body_steps)) * c)) /\ exists fs_q_b5cvlsepe_sum_body_steps_summand. b = fs_q_b5cvlsepe_sum_body_steps_summand * S ((S (fs_i_b5cvlsepe_sum_body_steps)) * c) + (fs_a_b5cvlsepe_sum_body_steps))) /\ ((((exists fs_h_b5cvlsepe_sum_body_steps_partial. fs_h_b5cvlsepe_sum_body_steps_partial + S (fs_r_b5cvlsepe_sum_body_steps) = S ((S (fs_i_b5cvlsepe_sum_body_steps)) * fs_v_b5cvlsepe_sum)) /\ exists fs_q_b5cvlsepe_sum_body_steps_partial. fs_u_b5cvlsepe_sum = fs_q_b5cvlsepe_sum_body_steps_partial * S ((S (fs_i_b5cvlsepe_sum_body_steps)) * fs_v_b5cvlsepe_sum) + (fs_r_b5cvlsepe_sum_body_steps))) /\ ((((exists fs_h_b5cvlsepe_sum_body_steps_successor. fs_h_b5cvlsepe_sum_body_steps_successor + S (fs_s_b5cvlsepe_sum_body_steps) = S ((S (S fs_i_b5cvlsepe_sum_body_steps)) * fs_v_b5cvlsepe_sum)) /\ exists fs_q_b5cvlsepe_sum_body_steps_successor. fs_u_b5cvlsepe_sum = fs_q_b5cvlsepe_sum_body_steps_successor * S ((S (S fs_i_b5cvlsepe_sum_body_steps)) * fs_v_b5cvlsepe_sum) + (fs_s_b5cvlsepe_sum_body_steps))) /\ fs_s_b5cvlsepe_sum_body_steps = fs_r_b5cvlsepe_sum_body_steps + fs_a_b5cvlsepe_sum_body_steps)))))))Structural proof guide
A Legendre sum admits an arbitrarily long zero-extended quotient code.
Direct prerequisites: prime_power_quotient_prefix_exists, beta_sum_exists, power_quotient_prefix_sum_extend_zero. The authored body proceeds by case analysis (3), intermediate claims (3), equality transport (2).
Proof neighborhood
Direct dependencies
BT00S0 prime_power_quotient_prefix_exists BT008A beta_sum_exists BT00XQ power_quotient_prefix_sum_extend_zeroDirect dependents
Formal native tactic body
Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (3)
01Fix variables and assumptionsL1–6
02Establish hprefixL7–12
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime power quotient prefix exists.
03Separate the logical casesL13–14
04Establish hsumL15–19
05Separate the logical casesL20–20
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L20
cases hsum
06Establish htotalL21–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply power quotient prefix sum extend zero.
- L21
have htotal : x2 = e - L22
specialize power_quotient_prefix_sum_extend_zero p - L23
specialize power_quotient_prefix_sum_extend_zero n - L24
specialize power_quotient_prefix_sum_extend_zero x - L25
specialize power_quotient_prefix_sum_extend_zero x1 - L26
specialize power_quotient_prefix_sum_extend_zero g - L27
specialize power_quotient_prefix_sum_extend_zero x2 - L28
specialize power_quotient_prefix_sum_extend_zero e - L29
apply power_quotient_prefix_sum_extend_zero - L30
exact hp
07Use earlier factsL31–33
08Construct an explicit witnessL34–35
09Separate the logical casesL36–36
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L36
split
10Use earlier factsL37–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L37
exact hprefix_witness_witness
11Calculate and transport equalitiesL38–39
12Use earlier factsL40–40
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L40
exact hsum_witness
Original exact command ledger · 40 lines
- 0001
intro p - 0002
intro n - 0003
intro e - 0004
intro g - 0005
intro hp - 0006
intro hlegendre - 0007
have hprefix : exists b c. forall bls_index_b5cvlsepe_generated_prefix. (exists bls_gap_b5cvlsepe_generated_prefix_bound. bls_gap_b5cvlsepe_generated_prefix_bound + S (bls_index_b5cvlsepe_generated_prefix) = (n + g)) -> exists bls_power_b5cvlsepe_generated_prefix bls_quotient_b5cvlsepe_generated_prefix bls_remainder_b5cvlsepe_generated_prefix. ((exists bpvi_b_bls_b5cvlsepe_generated_prefix_power bpvi_c_bls_b5cvlsepe_generated_prefix_power. ((forall bpvi_i_bls_b5cvlsepe_generated_prefix_power. (exists bpvi_repeat_gap_bls_b5cvlsepe_generated_prefix_power. bpvi_repeat_gap_bls_b5cvlsepe_generated_prefix_power + S bpvi_i_bls_b5cvlsepe_generated_prefix_power = S bls_index_b5cvlsepe_generated_prefix) -> (((exists bpvi_h_bls_b5cvlsepe_generated_prefix_power_repeat. bpvi_h_bls_b5cvlsepe_generated_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_b5cvlsepe_generated_prefix_power)) * bpvi_c_bls_b5cvlsepe_generated_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_generated_prefix_power_repeat. bpvi_b_bls_b5cvlsepe_generated_prefix_power = bpvi_q_bls_b5cvlsepe_generated_prefix_power_repeat * S ((S (bpvi_i_bls_b5cvlsepe_generated_prefix_power)) * bpvi_c_bls_b5cvlsepe_generated_prefix_power) + (p)))) /\ (exists bpvi_u_bls_b5cvlsepe_generated_prefix_power bpvi_v_bls_b5cvlsepe_generated_prefix_power. ((((exists bpvi_h_bls_b5cvlsepe_generated_prefix_power_start. bpvi_h_bls_b5cvlsepe_generated_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5cvlsepe_generated_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_generated_prefix_power_start. bpvi_u_bls_b5cvlsepe_generated_prefix_power = bpvi_q_bls_b5cvlsepe_generated_prefix_power_start * S ((S (0)) * bpvi_v_bls_b5cvlsepe_generated_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_b5cvlsepe_generated_prefix_power_terminal. bpvi_h_bls_b5cvlsepe_generated_prefix_power_terminal + S (bls_power_b5cvlsepe_generated_prefix) = S ((S (S bls_index_b5cvlsepe_generated_prefix)) * bpvi_v_bls_b5cvlsepe_generated_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_generated_prefix_power_terminal. bpvi_u_bls_b5cvlsepe_generated_prefix_power = bpvi_q_bls_b5cvlsepe_generated_prefix_power_terminal * S ((S (S bls_index_b5cvlsepe_generated_prefix)) * bpvi_v_bls_b5cvlsepe_generated_prefix_power) + (bls_power_b5cvlsepe_generated_prefix))) /\ forall bpvi_j_bls_b5cvlsepe_generated_prefix_power. (exists bpvi_product_gap_bls_b5cvlsepe_generated_prefix_power. bpvi_product_gap_bls_b5cvlsepe_generated_prefix_power + S bpvi_j_bls_b5cvlsepe_generated_prefix_power = S bls_index_b5cvlsepe_generated_prefix) -> exists bpvi_factor_bls_b5cvlsepe_generated_prefix_power bpvi_partial_bls_b5cvlsepe_generated_prefix_power bpvi_successor_bls_b5cvlsepe_generated_prefix_power. ((((exists bpvi_h_bls_b5cvlsepe_generated_prefix_power_factor. bpvi_h_bls_b5cvlsepe_generated_prefix_power_factor + S (bpvi_factor_bls_b5cvlsepe_generated_prefix_power) = S ((S (bpvi_j_bls_b5cvlsepe_generated_prefix_power)) * bpvi_c_bls_b5cvlsepe_generated_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_generated_prefix_power_factor. bpvi_b_bls_b5cvlsepe_generated_prefix_power = bpvi_q_bls_b5cvlsepe_generated_prefix_power_factor * S ((S (bpvi_j_bls_b5cvlsepe_generated_prefix_power)) * bpvi_c_bls_b5cvlsepe_generated_prefix_power) + (bpvi_factor_bls_b5cvlsepe_generated_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvlsepe_generated_prefix_power_partial. bpvi_h_bls_b5cvlsepe_generated_prefix_power_partial + S (bpvi_partial_bls_b5cvlsepe_generated_prefix_power) = S ((S (bpvi_j_bls_b5cvlsepe_generated_prefix_power)) * bpvi_v_bls_b5cvlsepe_generated_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_generated_prefix_power_partial. bpvi_u_bls_b5cvlsepe_generated_prefix_power = bpvi_q_bls_b5cvlsepe_generated_prefix_power_partial * S ((S (bpvi_j_bls_b5cvlsepe_generated_prefix_power)) * bpvi_v_bls_b5cvlsepe_generated_prefix_power) + (bpvi_partial_bls_b5cvlsepe_generated_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvlsepe_generated_prefix_power_successor. bpvi_h_bls_b5cvlsepe_generated_prefix_power_successor + S (bpvi_successor_bls_b5cvlsepe_generated_prefix_power) = S ((S (S bpvi_j_bls_b5cvlsepe_generated_prefix_power)) * bpvi_v_bls_b5cvlsepe_generated_prefix_power)) /\ exists bpvi_q_bls_b5cvlsepe_generated_prefix_power_successor. bpvi_u_bls_b5cvlsepe_generated_prefix_power = bpvi_q_bls_b5cvlsepe_generated_prefix_power_successor * S ((S (S bpvi_j_bls_b5cvlsepe_generated_prefix_power)) * bpvi_v_bls_b5cvlsepe_generated_prefix_power) + (bpvi_successor_bls_b5cvlsepe_generated_prefix_power))) /\ bpvi_successor_bls_b5cvlsepe_generated_prefix_power = bpvi_partial_bls_b5cvlsepe_generated_prefix_power * bpvi_factor_bls_b5cvlsepe_generated_prefix_power)))))))) /\ ((((exists ff_h_bls_b5cvlsepe_generated_prefix_quotient_entry. ff_h_bls_b5cvlsepe_generated_prefix_quotient_entry + S (bls_quotient_b5cvlsepe_generated_prefix) = S ((S (bls_index_b5cvlsepe_generated_prefix)) * c)) /\ exists ff_q_bls_b5cvlsepe_generated_prefix_quotient_entry. b = ff_q_bls_b5cvlsepe_generated_prefix_quotient_entry * S ((S (bls_index_b5cvlsepe_generated_prefix)) * c) + (bls_quotient_b5cvlsepe_generated_prefix))) /\ ((n = bls_power_b5cvlsepe_generated_prefix * bls_quotient_b5cvlsepe_generated_prefix + bls_remainder_b5cvlsepe_generated_prefix /\ exists bls_remainder_gap_b5cvlsepe_generated_prefix_division. bls_remainder_gap_b5cvlsepe_generated_prefix_division + S (bls_remainder_b5cvlsepe_generated_prefix) = bls_power_b5cvlsepe_generated_prefix)))) - 0008
specialize prime_power_quotient_prefix_exists p - 0009
specialize prime_power_quotient_prefix_exists n - 0010
specialize prime_power_quotient_prefix_exists (n + g) - 0011
apply prime_power_quotient_prefix_exists - 0012
exact hp - 0013
cases hprefix - 0014
cases hprefix_witness - 0015
have hsum : exists t. exists fs_u_b5cvlsepe_generated_sum fs_v_b5cvlsepe_generated_sum. ((((exists fs_h_b5cvlsepe_generated_sum_body_start. fs_h_b5cvlsepe_generated_sum_body_start + S (0) = S ((S (0)) * fs_v_b5cvlsepe_generated_sum)) /\ exists fs_q_b5cvlsepe_generated_sum_body_start. fs_u_b5cvlsepe_generated_sum = fs_q_b5cvlsepe_generated_sum_body_start * S ((S (0)) * fs_v_b5cvlsepe_generated_sum) + (0))) /\ ((((exists fs_h_b5cvlsepe_generated_sum_body_terminal. fs_h_b5cvlsepe_generated_sum_body_terminal + S (t) = S ((S (n + g)) * fs_v_b5cvlsepe_generated_sum)) /\ exists fs_q_b5cvlsepe_generated_sum_body_terminal. fs_u_b5cvlsepe_generated_sum = fs_q_b5cvlsepe_generated_sum_body_terminal * S ((S (n + g)) * fs_v_b5cvlsepe_generated_sum) + (t))) /\ forall fs_i_b5cvlsepe_generated_sum_body_steps. (exists fs_lt_b5cvlsepe_generated_sum_body_steps_bound. fs_lt_b5cvlsepe_generated_sum_body_steps_bound + S fs_i_b5cvlsepe_generated_sum_body_steps = n + g) -> exists fs_a_b5cvlsepe_generated_sum_body_steps fs_r_b5cvlsepe_generated_sum_body_steps fs_s_b5cvlsepe_generated_sum_body_steps. ((((exists fs_h_b5cvlsepe_generated_sum_body_steps_summand. fs_h_b5cvlsepe_generated_sum_body_steps_summand + S (fs_a_b5cvlsepe_generated_sum_body_steps) = S ((S (fs_i_b5cvlsepe_generated_sum_body_steps)) * x1)) /\ exists fs_q_b5cvlsepe_generated_sum_body_steps_summand. x = fs_q_b5cvlsepe_generated_sum_body_steps_summand * S ((S (fs_i_b5cvlsepe_generated_sum_body_steps)) * x1) + (fs_a_b5cvlsepe_generated_sum_body_steps))) /\ ((((exists fs_h_b5cvlsepe_generated_sum_body_steps_partial. fs_h_b5cvlsepe_generated_sum_body_steps_partial + S (fs_r_b5cvlsepe_generated_sum_body_steps) = S ((S (fs_i_b5cvlsepe_generated_sum_body_steps)) * fs_v_b5cvlsepe_generated_sum)) /\ exists fs_q_b5cvlsepe_generated_sum_body_steps_partial. fs_u_b5cvlsepe_generated_sum = fs_q_b5cvlsepe_generated_sum_body_steps_partial * S ((S (fs_i_b5cvlsepe_generated_sum_body_steps)) * fs_v_b5cvlsepe_generated_sum) + (fs_r_b5cvlsepe_generated_sum_body_steps))) /\ ((((exists fs_h_b5cvlsepe_generated_sum_body_steps_successor. fs_h_b5cvlsepe_generated_sum_body_steps_successor + S (fs_s_b5cvlsepe_generated_sum_body_steps) = S ((S (S fs_i_b5cvlsepe_generated_sum_body_steps)) * fs_v_b5cvlsepe_generated_sum)) /\ exists fs_q_b5cvlsepe_generated_sum_body_steps_successor. fs_u_b5cvlsepe_generated_sum = fs_q_b5cvlsepe_generated_sum_body_steps_successor * S ((S (S fs_i_b5cvlsepe_generated_sum_body_steps)) * fs_v_b5cvlsepe_generated_sum) + (fs_s_b5cvlsepe_generated_sum_body_steps))) /\ fs_s_b5cvlsepe_generated_sum_body_steps = fs_r_b5cvlsepe_generated_sum_body_steps + fs_a_b5cvlsepe_generated_sum_body_steps))))) - 0016
specialize beta_sum_exists x - 0017
specialize beta_sum_exists x1 - 0018
specialize beta_sum_exists (n + g) - 0019
exact beta_sum_exists - 0020
cases hsum - 0021
have htotal : x2 = e - 0022
specialize power_quotient_prefix_sum_extend_zero p - 0023
specialize power_quotient_prefix_sum_extend_zero n - 0024
specialize power_quotient_prefix_sum_extend_zero x - 0025
specialize power_quotient_prefix_sum_extend_zero x1 - 0026
specialize power_quotient_prefix_sum_extend_zero g - 0027
specialize power_quotient_prefix_sum_extend_zero x2 - 0028
specialize power_quotient_prefix_sum_extend_zero e - 0029
apply power_quotient_prefix_sum_extend_zero - 0030
exact hp - 0031
exact hprefix_witness_witness - 0032
exact hsum_witness - 0033
exact hlegendre - 0034
exists x - 0035
exists x1 - 0036
split - 0037
exact hprefix_witness_witness - 0038
rewrite <- htotal - 0039
rewrite <- htotal - 0040
exact hsum_witness