BT00ST · Bertrand theorem

legendre_sum_zero_extended_prefix

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

An old Legendre sum has a successor-length quotient code ending in zero.

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. ∀ e. Prime(p) → LegendreSum(p,n,e) → ∃ x. ∃ y. PowerQuotPrefix(p,n,x,y,S n) ∧ Sum(x,y,S n,e)

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

PD0004 Prime PD0015 Sum PD0049 PowerQuotPrefix PD0050 LegendreSum

4 occurrences

In local proof propositions

PD0013 BetaAt PD0015 Sum PD0049 PowerQuotPrefix PD0050 LegendreSum

6 occurrences

Exact expanded native-PA statement
forall p n e. ((~(p = 1) /\ forall frm_prime_left_blrr_tail_prime frm_prime_right_blrr_tail_prime. p = frm_prime_left_blrr_tail_prime * frm_prime_right_blrr_tail_prime -> frm_prime_left_blrr_tail_prime = 1 \/ frm_prime_right_blrr_tail_prime = 1)) -> (exists bls_code_blrr_extend_old bls_scale_blrr_extend_old. ((forall bls_index_blrr_extend_old_prefix. (exists bls_gap_blrr_extend_old_prefix_bound. bls_gap_blrr_extend_old_prefix_bound + S (bls_index_blrr_extend_old_prefix) = (n)) -> exists bls_power_blrr_extend_old_prefix bls_quotient_blrr_extend_old_prefix bls_remainder_blrr_extend_old_prefix. ((exists bpvi_b_bls_blrr_extend_old_prefix_power bpvi_c_bls_blrr_extend_old_prefix_power. ((forall bpvi_i_bls_blrr_extend_old_prefix_power. (exists bpvi_repeat_gap_bls_blrr_extend_old_prefix_power. bpvi_repeat_gap_bls_blrr_extend_old_prefix_power + S bpvi_i_bls_blrr_extend_old_prefix_power = S bls_index_blrr_extend_old_prefix) -> (((exists bpvi_h_bls_blrr_extend_old_prefix_power_repeat. bpvi_h_bls_blrr_extend_old_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_extend_old_prefix_power)) * bpvi_c_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_repeat. bpvi_b_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_repeat * S ((S (bpvi_i_bls_blrr_extend_old_prefix_power)) * bpvi_c_bls_blrr_extend_old_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blrr_extend_old_prefix_power bpvi_v_bls_blrr_extend_old_prefix_power. ((((exists bpvi_h_bls_blrr_extend_old_prefix_power_start. bpvi_h_bls_blrr_extend_old_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_start. bpvi_u_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_start * S ((S (0)) * bpvi_v_bls_blrr_extend_old_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_extend_old_prefix_power_terminal. bpvi_h_bls_blrr_extend_old_prefix_power_terminal + S (bls_power_blrr_extend_old_prefix) = S ((S (S bls_index_blrr_extend_old_prefix)) * bpvi_v_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_terminal. bpvi_u_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_terminal * S ((S (S bls_index_blrr_extend_old_prefix)) * bpvi_v_bls_blrr_extend_old_prefix_power) + (bls_power_blrr_extend_old_prefix))) /\ forall bpvi_j_bls_blrr_extend_old_prefix_power. (exists bpvi_product_gap_bls_blrr_extend_old_prefix_power. bpvi_product_gap_bls_blrr_extend_old_prefix_power + S bpvi_j_bls_blrr_extend_old_prefix_power = S bls_index_blrr_extend_old_prefix) -> exists bpvi_factor_bls_blrr_extend_old_prefix_power bpvi_partial_bls_blrr_extend_old_prefix_power bpvi_successor_bls_blrr_extend_old_prefix_power. ((((exists bpvi_h_bls_blrr_extend_old_prefix_power_factor. bpvi_h_bls_blrr_extend_old_prefix_power_factor + S (bpvi_factor_bls_blrr_extend_old_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_c_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_factor. bpvi_b_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_factor * S ((S (bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_c_bls_blrr_extend_old_prefix_power) + (bpvi_factor_bls_blrr_extend_old_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_old_prefix_power_partial. bpvi_h_bls_blrr_extend_old_prefix_power_partial + S (bpvi_partial_bls_blrr_extend_old_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_v_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_partial. bpvi_u_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_partial * S ((S (bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_v_bls_blrr_extend_old_prefix_power) + (bpvi_partial_bls_blrr_extend_old_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_old_prefix_power_successor. bpvi_h_bls_blrr_extend_old_prefix_power_successor + S (bpvi_successor_bls_blrr_extend_old_prefix_power) = S ((S (S bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_v_bls_blrr_extend_old_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_old_prefix_power_successor. bpvi_u_bls_blrr_extend_old_prefix_power = bpvi_q_bls_blrr_extend_old_prefix_power_successor * S ((S (S bpvi_j_bls_blrr_extend_old_prefix_power)) * bpvi_v_bls_blrr_extend_old_prefix_power) + (bpvi_successor_bls_blrr_extend_old_prefix_power))) /\ bpvi_successor_bls_blrr_extend_old_prefix_power = bpvi_partial_bls_blrr_extend_old_prefix_power * bpvi_factor_bls_blrr_extend_old_prefix_power)))))))) /\ ((((exists ff_h_bls_blrr_extend_old_prefix_quotient_entry. ff_h_bls_blrr_extend_old_prefix_quotient_entry + S (bls_quotient_blrr_extend_old_prefix) = S ((S (bls_index_blrr_extend_old_prefix)) * bls_scale_blrr_extend_old)) /\ exists ff_q_bls_blrr_extend_old_prefix_quotient_entry. bls_code_blrr_extend_old = ff_q_bls_blrr_extend_old_prefix_quotient_entry * S ((S (bls_index_blrr_extend_old_prefix)) * bls_scale_blrr_extend_old) + (bls_quotient_blrr_extend_old_prefix))) /\ ((n = bls_power_blrr_extend_old_prefix * bls_quotient_blrr_extend_old_prefix + bls_remainder_blrr_extend_old_prefix /\ exists bls_remainder_gap_blrr_extend_old_prefix_division. bls_remainder_gap_blrr_extend_old_prefix_division + S (bls_remainder_blrr_extend_old_prefix) = bls_power_blrr_extend_old_prefix))))) /\ (exists ff_u_bls_blrr_extend_old_sum ff_v_bls_blrr_extend_old_sum. ((((exists ff_h_bls_blrr_extend_old_sum_start. ff_h_bls_blrr_extend_old_sum_start + S (0) = S ((S (0)) * ff_v_bls_blrr_extend_old_sum)) /\ exists ff_q_bls_blrr_extend_old_sum_start. ff_u_bls_blrr_extend_old_sum = ff_q_bls_blrr_extend_old_sum_start * S ((S (0)) * ff_v_bls_blrr_extend_old_sum) + (0))) /\ ((((exists ff_h_bls_blrr_extend_old_sum_terminal. ff_h_bls_blrr_extend_old_sum_terminal + S (e) = S ((S (n)) * ff_v_bls_blrr_extend_old_sum)) /\ exists ff_q_bls_blrr_extend_old_sum_terminal. ff_u_bls_blrr_extend_old_sum = ff_q_bls_blrr_extend_old_sum_terminal * S ((S (n)) * ff_v_bls_blrr_extend_old_sum) + (e))) /\ forall ff_i_bls_blrr_extend_old_sum. (exists ff_lt_bls_blrr_extend_old_sum_bound. ff_lt_bls_blrr_extend_old_sum_bound + S ff_i_bls_blrr_extend_old_sum = n) -> exists ff_a_bls_blrr_extend_old_sum ff_r_bls_blrr_extend_old_sum ff_s_bls_blrr_extend_old_sum. ((((exists ff_h_bls_blrr_extend_old_sum_summand. ff_h_bls_blrr_extend_old_sum_summand + S (ff_a_bls_blrr_extend_old_sum) = S ((S (ff_i_bls_blrr_extend_old_sum)) * bls_scale_blrr_extend_old)) /\ exists ff_q_bls_blrr_extend_old_sum_summand. bls_code_blrr_extend_old = ff_q_bls_blrr_extend_old_sum_summand * S ((S (ff_i_bls_blrr_extend_old_sum)) * bls_scale_blrr_extend_old) + (ff_a_bls_blrr_extend_old_sum))) /\ ((((exists ff_h_bls_blrr_extend_old_sum_partial. ff_h_bls_blrr_extend_old_sum_partial + S (ff_r_bls_blrr_extend_old_sum) = S ((S (ff_i_bls_blrr_extend_old_sum)) * ff_v_bls_blrr_extend_old_sum)) /\ exists ff_q_bls_blrr_extend_old_sum_partial. ff_u_bls_blrr_extend_old_sum = ff_q_bls_blrr_extend_old_sum_partial * S ((S (ff_i_bls_blrr_extend_old_sum)) * ff_v_bls_blrr_extend_old_sum) + (ff_r_bls_blrr_extend_old_sum))) /\ ((((exists ff_h_bls_blrr_extend_old_sum_successor. ff_h_bls_blrr_extend_old_sum_successor + S (ff_s_bls_blrr_extend_old_sum) = S ((S (S ff_i_bls_blrr_extend_old_sum)) * ff_v_bls_blrr_extend_old_sum)) /\ exists ff_q_bls_blrr_extend_old_sum_successor. ff_u_bls_blrr_extend_old_sum = ff_q_bls_blrr_extend_old_sum_successor * S ((S (S ff_i_bls_blrr_extend_old_sum)) * ff_v_bls_blrr_extend_old_sum) + (ff_s_bls_blrr_extend_old_sum))) /\ ff_s_bls_blrr_extend_old_sum = ff_r_bls_blrr_extend_old_sum + ff_a_bls_blrr_extend_old_sum)))))))) -> (exists b c. ((forall bls_index_blrr_extend_prefix. (exists bls_gap_blrr_extend_prefix_bound. bls_gap_blrr_extend_prefix_bound + S (bls_index_blrr_extend_prefix) = (S n)) -> exists bls_power_blrr_extend_prefix bls_quotient_blrr_extend_prefix bls_remainder_blrr_extend_prefix. ((exists bpvi_b_bls_blrr_extend_prefix_power bpvi_c_bls_blrr_extend_prefix_power. ((forall bpvi_i_bls_blrr_extend_prefix_power. (exists bpvi_repeat_gap_bls_blrr_extend_prefix_power. bpvi_repeat_gap_bls_blrr_extend_prefix_power + S bpvi_i_bls_blrr_extend_prefix_power = S bls_index_blrr_extend_prefix) -> (((exists bpvi_h_bls_blrr_extend_prefix_power_repeat. bpvi_h_bls_blrr_extend_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_repeat. bpvi_b_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_repeat * S ((S (bpvi_i_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blrr_extend_prefix_power bpvi_v_bls_blrr_extend_prefix_power. ((((exists bpvi_h_bls_blrr_extend_prefix_power_start. bpvi_h_bls_blrr_extend_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_start. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_start * S ((S (0)) * bpvi_v_bls_blrr_extend_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_terminal. bpvi_h_bls_blrr_extend_prefix_power_terminal + S (bls_power_blrr_extend_prefix) = S ((S (S bls_index_blrr_extend_prefix)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_terminal. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_terminal * S ((S (S bls_index_blrr_extend_prefix)) * bpvi_v_bls_blrr_extend_prefix_power) + (bls_power_blrr_extend_prefix))) /\ forall bpvi_j_bls_blrr_extend_prefix_power. (exists bpvi_product_gap_bls_blrr_extend_prefix_power. bpvi_product_gap_bls_blrr_extend_prefix_power + S bpvi_j_bls_blrr_extend_prefix_power = S bls_index_blrr_extend_prefix) -> exists bpvi_factor_bls_blrr_extend_prefix_power bpvi_partial_bls_blrr_extend_prefix_power bpvi_successor_bls_blrr_extend_prefix_power. ((((exists bpvi_h_bls_blrr_extend_prefix_power_factor. bpvi_h_bls_blrr_extend_prefix_power_factor + S (bpvi_factor_bls_blrr_extend_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_factor. bpvi_b_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_factor * S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power) + (bpvi_factor_bls_blrr_extend_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_partial. bpvi_h_bls_blrr_extend_prefix_power_partial + S (bpvi_partial_bls_blrr_extend_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_partial. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_partial * S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power) + (bpvi_partial_bls_blrr_extend_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_successor. bpvi_h_bls_blrr_extend_prefix_power_successor + S (bpvi_successor_bls_blrr_extend_prefix_power) = S ((S (S bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_successor. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_successor * S ((S (S bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power) + (bpvi_successor_bls_blrr_extend_prefix_power))) /\ bpvi_successor_bls_blrr_extend_prefix_power = bpvi_partial_bls_blrr_extend_prefix_power * bpvi_factor_bls_blrr_extend_prefix_power)))))))) /\ ((((exists ff_h_bls_blrr_extend_prefix_quotient_entry. ff_h_bls_blrr_extend_prefix_quotient_entry + S (bls_quotient_blrr_extend_prefix) = S ((S (bls_index_blrr_extend_prefix)) * c)) /\ exists ff_q_bls_blrr_extend_prefix_quotient_entry. b = ff_q_bls_blrr_extend_prefix_quotient_entry * S ((S (bls_index_blrr_extend_prefix)) * c) + (bls_quotient_blrr_extend_prefix))) /\ ((n = bls_power_blrr_extend_prefix * bls_quotient_blrr_extend_prefix + bls_remainder_blrr_extend_prefix /\ exists bls_remainder_gap_blrr_extend_prefix_division. bls_remainder_gap_blrr_extend_prefix_division + S (bls_remainder_blrr_extend_prefix) = bls_power_blrr_extend_prefix))))) /\ (exists fs_u_blrr_extend_sum fs_v_blrr_extend_sum. ((((exists fs_h_blrr_extend_sum_body_start. fs_h_blrr_extend_sum_body_start + S (0) = S ((S (0)) * fs_v_blrr_extend_sum)) /\ exists fs_q_blrr_extend_sum_body_start. fs_u_blrr_extend_sum = fs_q_blrr_extend_sum_body_start * S ((S (0)) * fs_v_blrr_extend_sum) + (0))) /\ ((((exists fs_h_blrr_extend_sum_body_terminal. fs_h_blrr_extend_sum_body_terminal + S (e) = S ((S (S n)) * fs_v_blrr_extend_sum)) /\ exists fs_q_blrr_extend_sum_body_terminal. fs_u_blrr_extend_sum = fs_q_blrr_extend_sum_body_terminal * S ((S (S n)) * fs_v_blrr_extend_sum) + (e))) /\ forall fs_i_blrr_extend_sum_body_steps. (exists fs_lt_blrr_extend_sum_body_steps_bound. fs_lt_blrr_extend_sum_body_steps_bound + S fs_i_blrr_extend_sum_body_steps = S n) -> exists fs_a_blrr_extend_sum_body_steps fs_r_blrr_extend_sum_body_steps fs_s_blrr_extend_sum_body_steps. ((((exists fs_h_blrr_extend_sum_body_steps_summand. fs_h_blrr_extend_sum_body_steps_summand + S (fs_a_blrr_extend_sum_body_steps) = S ((S (fs_i_blrr_extend_sum_body_steps)) * c)) /\ exists fs_q_blrr_extend_sum_body_steps_summand. b = fs_q_blrr_extend_sum_body_steps_summand * S ((S (fs_i_blrr_extend_sum_body_steps)) * c) + (fs_a_blrr_extend_sum_body_steps))) /\ ((((exists fs_h_blrr_extend_sum_body_steps_partial. fs_h_blrr_extend_sum_body_steps_partial + S (fs_r_blrr_extend_sum_body_steps) = S ((S (fs_i_blrr_extend_sum_body_steps)) * fs_v_blrr_extend_sum)) /\ exists fs_q_blrr_extend_sum_body_steps_partial. fs_u_blrr_extend_sum = fs_q_blrr_extend_sum_body_steps_partial * S ((S (fs_i_blrr_extend_sum_body_steps)) * fs_v_blrr_extend_sum) + (fs_r_blrr_extend_sum_body_steps))) /\ ((((exists fs_h_blrr_extend_sum_body_steps_successor. fs_h_blrr_extend_sum_body_steps_successor + S (fs_s_blrr_extend_sum_body_steps) = S ((S (S fs_i_blrr_extend_sum_body_steps)) * fs_v_blrr_extend_sum)) /\ exists fs_q_blrr_extend_sum_body_steps_successor. fs_u_blrr_extend_sum = fs_q_blrr_extend_sum_body_steps_successor * S ((S (S fs_i_blrr_extend_sum_body_steps)) * fs_v_blrr_extend_sum) + (fs_s_blrr_extend_sum_body_steps))) /\ fs_s_blrr_extend_sum_body_steps = fs_r_blrr_extend_sum_body_steps + fs_a_blrr_extend_sum_body_steps))))))))

Proof neighborhood

Direct theorem prerequisites

BT00S0 prime_power_quotient_prefix_exists BT00SS prime_power_quotient_prefix_last_zero BT008A beta_sum_exists BT00SR beta_sum_succ_last_zero BT0018 le_succ BT00S3 legendre_sum_functional

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

65 script commands · 18 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)
prime power quotient prefix existsprime power quotient prefix last zerobeta sum existsbeta sum succ last zerole succlegendre sum functional
01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro e
  4. L4
    intro hp
  5. L5
    intro hlegendre
02Establish hprefixL6–11

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

  1. L6
    have hprefix : ∃ b. ∃ c. PowerQuotPrefix(p,n,b,c,S n)Definitions: PowerQuotPrefix(p,n,b,c,S n)Original native command in the exact edition
  2. L7
    specialize prime_power_quotient_prefix_exists p
  3. L8
    specialize prime_power_quotient_prefix_exists n
  4. L9
    specialize prime_power_quotient_prefix_exists (S n)
  5. L10
    apply prime_power_quotient_prefix_exists
  6. L11
    exact hp
03Separate the logical casesL12–13

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

  1. L12
    cases hprefix
  2. L13
    cases hprefix_witness
04Establish hzeroL14–21

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

  1. L14
    have hzero : BetaAt(x,x1,n,0)Definitions: BetaAt(x,x1,n,0)Original native command in the exact edition
  2. L15
    specialize prime_power_quotient_prefix_last_zero p
  3. L16
    specialize prime_power_quotient_prefix_last_zero n
  4. L17
    specialize prime_power_quotient_prefix_last_zero x
  5. L18
    specialize prime_power_quotient_prefix_last_zero x1
  6. L19
    apply prime_power_quotient_prefix_last_zero
  7. L20
    exact hp
  8. L21
    exact hprefix_witness_witness
05Establish hsuccessor_sumL22–26

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

  1. L22
    have hsuccessor_sum : ∃ q. Sum(x,x1,S n,q)Definitions: Sum(x,x1,S n,q)Original native command in the exact edition
  2. L23
    specialize beta_sum_exists x
  3. L24
    specialize beta_sum_exists x1
  4. L25
    specialize beta_sum_exists (S n)
  5. L26
    exact beta_sum_exists
06Separate the logical casesL27–27

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

  1. L27
    cases hsuccessor_sum
07Establish hpredecessor_sumL28–35

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

  1. L28
    have hpredecessor_sum : Sum(x,x1,n,x2)Definitions: Sum(x,x1,n,x2)Original native command in the exact edition
  2. L29
    specialize beta_sum_succ_last_zero x
  3. L30
    specialize beta_sum_succ_last_zero x1
  4. L31
    specialize beta_sum_succ_last_zero n
  5. L32
    specialize beta_sum_succ_last_zero x2
  6. L33
    apply beta_sum_succ_last_zero
  7. L34
    exact hsuccessor_sum_witness
  8. L35
    exact hzero
08Establish hrestrictedL36–44

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

  1. L36
    have hrestricted : PowerQuotPrefix(p,n,x,x1,n)Definitions: PowerQuotPrefix(p,n,x,x1,n)Original native command in the exact edition
  2. L37
    intro i
  3. L38
    intro hi
  4. L39
    specialize hprefix_witness_witness i
  5. L40
    apply hprefix_witness_witness
  6. L41
    specialize le_succ (S i)
  7. L42
    specialize le_succ n
  8. L43
    apply le_succ
  9. L44
    exact hi
09Establish hcompetingL45–45

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

  1. L45
    have hcompeting : LegendreSum(p,n,x2)Definitions: LegendreSum(p,n,x2)Original native command in the exact edition
10Construct an explicit witnessL46–47

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

  1. L46
    exists x
  2. L47
    exists x1
11Separate the logical casesL48–48

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

  1. L48
    split
12Use earlier factsL49–50

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

  1. L49
    exact hrestricted
  2. L50
    exact hpredecessor_sum
13Establish heqL51–58

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

  1. L51
    have heq : e = x2
  2. L52
    specialize legendre_sum_functional p
  3. L53
    specialize legendre_sum_functional n
  4. L54
    specialize legendre_sum_functional e
  5. L55
    specialize legendre_sum_functional x2
  6. L56
    apply legendre_sum_functional
  7. L57
    exact hlegendre
  8. L58
    exact hcompeting
14Construct an explicit witnessL59–60

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

  1. L59
    exists x
  2. L60
    exists x1
15Separate the logical casesL61–61

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

  1. L61
    split
16Use earlier factsL62–62

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

  1. L62
    exact hprefix_witness_witness
17Calculate and transport equalitiesL63–64

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

  1. L63
    rewrite heq
  2. L64
    rewrite heq
18Use earlier factsL65–65

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

  1. L65
    exact hsuccessor_sum_witness

Library-wide reading audit

Original defined command ledger · 65 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro e
  4. 0004intro hp
  5. 0005intro hlegendre
  6. 0006have hprefix : ∃ b. ∃ c. PowerQuotPrefix(p,n,b,c,S n)
    Exact native replay linehave hprefix : exists b c. (forall bls_index_blrr_extend_prefix. (exists bls_gap_blrr_extend_prefix_bound. bls_gap_blrr_extend_prefix_bound + S (bls_index_blrr_extend_prefix) = (S n)) -> exists bls_power_blrr_extend_prefix bls_quotient_blrr_extend_prefix bls_remainder_blrr_extend_prefix. ((exists bpvi_b_bls_blrr_extend_prefix_power bpvi_c_bls_blrr_extend_prefix_power. ((forall bpvi_i_bls_blrr_extend_prefix_power. (exists bpvi_repeat_gap_bls_blrr_extend_prefix_power. bpvi_repeat_gap_bls_blrr_extend_prefix_power + S bpvi_i_bls_blrr_extend_prefix_power = S bls_index_blrr_extend_prefix) -> (((exists bpvi_h_bls_blrr_extend_prefix_power_repeat. bpvi_h_bls_blrr_extend_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_repeat. bpvi_b_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_repeat * S ((S (bpvi_i_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blrr_extend_prefix_power bpvi_v_bls_blrr_extend_prefix_power. ((((exists bpvi_h_bls_blrr_extend_prefix_power_start. bpvi_h_bls_blrr_extend_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_start. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_start * S ((S (0)) * bpvi_v_bls_blrr_extend_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_terminal. bpvi_h_bls_blrr_extend_prefix_power_terminal + S (bls_power_blrr_extend_prefix) = S ((S (S bls_index_blrr_extend_prefix)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_terminal. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_terminal * S ((S (S bls_index_blrr_extend_prefix)) * bpvi_v_bls_blrr_extend_prefix_power) + (bls_power_blrr_extend_prefix))) /\ forall bpvi_j_bls_blrr_extend_prefix_power. (exists bpvi_product_gap_bls_blrr_extend_prefix_power. bpvi_product_gap_bls_blrr_extend_prefix_power + S bpvi_j_bls_blrr_extend_prefix_power = S bls_index_blrr_extend_prefix) -> exists bpvi_factor_bls_blrr_extend_prefix_power bpvi_partial_bls_blrr_extend_prefix_power bpvi_successor_bls_blrr_extend_prefix_power. ((((exists bpvi_h_bls_blrr_extend_prefix_power_factor. bpvi_h_bls_blrr_extend_prefix_power_factor + S (bpvi_factor_bls_blrr_extend_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_factor. bpvi_b_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_factor * S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_c_bls_blrr_extend_prefix_power) + (bpvi_factor_bls_blrr_extend_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_partial. bpvi_h_bls_blrr_extend_prefix_power_partial + S (bpvi_partial_bls_blrr_extend_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_partial. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_partial * S ((S (bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power) + (bpvi_partial_bls_blrr_extend_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_prefix_power_successor. bpvi_h_bls_blrr_extend_prefix_power_successor + S (bpvi_successor_bls_blrr_extend_prefix_power) = S ((S (S bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_prefix_power_successor. bpvi_u_bls_blrr_extend_prefix_power = bpvi_q_bls_blrr_extend_prefix_power_successor * S ((S (S bpvi_j_bls_blrr_extend_prefix_power)) * bpvi_v_bls_blrr_extend_prefix_power) + (bpvi_successor_bls_blrr_extend_prefix_power))) /\ bpvi_successor_bls_blrr_extend_prefix_power = bpvi_partial_bls_blrr_extend_prefix_power * bpvi_factor_bls_blrr_extend_prefix_power)))))))) /\ ((((exists ff_h_bls_blrr_extend_prefix_quotient_entry. ff_h_bls_blrr_extend_prefix_quotient_entry + S (bls_quotient_blrr_extend_prefix) = S ((S (bls_index_blrr_extend_prefix)) * c)) /\ exists ff_q_bls_blrr_extend_prefix_quotient_entry. b = ff_q_bls_blrr_extend_prefix_quotient_entry * S ((S (bls_index_blrr_extend_prefix)) * c) + (bls_quotient_blrr_extend_prefix))) /\ ((n = bls_power_blrr_extend_prefix * bls_quotient_blrr_extend_prefix + bls_remainder_blrr_extend_prefix /\ exists bls_remainder_gap_blrr_extend_prefix_division. bls_remainder_gap_blrr_extend_prefix_division + S (bls_remainder_blrr_extend_prefix) = bls_power_blrr_extend_prefix)))))
  7. 0007specialize prime_power_quotient_prefix_exists p
  8. 0008specialize prime_power_quotient_prefix_exists n
  9. 0009specialize prime_power_quotient_prefix_exists (S n)
  10. 0010apply prime_power_quotient_prefix_exists
  11. 0011exact hp
  12. 0012cases hprefix
  13. 0013cases hprefix_witness
  14. 0014have hzero : BetaAt(x,x1,n,0)
    Exact native replay linehave hzero : ((exists fs_h_blrr_extend_last_zero. fs_h_blrr_extend_last_zero + S (0) = S ((S (n)) * x1)) /\ exists fs_q_blrr_extend_last_zero. x = fs_q_blrr_extend_last_zero * S ((S (n)) * x1) + (0))
  15. 0015specialize prime_power_quotient_prefix_last_zero p
  16. 0016specialize prime_power_quotient_prefix_last_zero n
  17. 0017specialize prime_power_quotient_prefix_last_zero x
  18. 0018specialize prime_power_quotient_prefix_last_zero x1
  19. 0019apply prime_power_quotient_prefix_last_zero
  20. 0020exact hp
  21. 0021exact hprefix_witness_witness
  22. 0022have hsuccessor_sum : ∃ q. Sum(x,x1,S n,q)
    Exact native replay linehave hsuccessor_sum : exists q. exists fs_u_blrr_extend_sum_exists fs_v_blrr_extend_sum_exists. ((((exists fs_h_blrr_extend_sum_exists_body_start. fs_h_blrr_extend_sum_exists_body_start + S (0) = S ((S (0)) * fs_v_blrr_extend_sum_exists)) /\ exists fs_q_blrr_extend_sum_exists_body_start. fs_u_blrr_extend_sum_exists = fs_q_blrr_extend_sum_exists_body_start * S ((S (0)) * fs_v_blrr_extend_sum_exists) + (0))) /\ ((((exists fs_h_blrr_extend_sum_exists_body_terminal. fs_h_blrr_extend_sum_exists_body_terminal + S (q) = S ((S (S n)) * fs_v_blrr_extend_sum_exists)) /\ exists fs_q_blrr_extend_sum_exists_body_terminal. fs_u_blrr_extend_sum_exists = fs_q_blrr_extend_sum_exists_body_terminal * S ((S (S n)) * fs_v_blrr_extend_sum_exists) + (q))) /\ forall fs_i_blrr_extend_sum_exists_body_steps. (exists fs_lt_blrr_extend_sum_exists_body_steps_bound. fs_lt_blrr_extend_sum_exists_body_steps_bound + S fs_i_blrr_extend_sum_exists_body_steps = S n) -> exists fs_a_blrr_extend_sum_exists_body_steps fs_r_blrr_extend_sum_exists_body_steps fs_s_blrr_extend_sum_exists_body_steps. ((((exists fs_h_blrr_extend_sum_exists_body_steps_summand. fs_h_blrr_extend_sum_exists_body_steps_summand + S (fs_a_blrr_extend_sum_exists_body_steps) = S ((S (fs_i_blrr_extend_sum_exists_body_steps)) * x1)) /\ exists fs_q_blrr_extend_sum_exists_body_steps_summand. x = fs_q_blrr_extend_sum_exists_body_steps_summand * S ((S (fs_i_blrr_extend_sum_exists_body_steps)) * x1) + (fs_a_blrr_extend_sum_exists_body_steps))) /\ ((((exists fs_h_blrr_extend_sum_exists_body_steps_partial. fs_h_blrr_extend_sum_exists_body_steps_partial + S (fs_r_blrr_extend_sum_exists_body_steps) = S ((S (fs_i_blrr_extend_sum_exists_body_steps)) * fs_v_blrr_extend_sum_exists)) /\ exists fs_q_blrr_extend_sum_exists_body_steps_partial. fs_u_blrr_extend_sum_exists = fs_q_blrr_extend_sum_exists_body_steps_partial * S ((S (fs_i_blrr_extend_sum_exists_body_steps)) * fs_v_blrr_extend_sum_exists) + (fs_r_blrr_extend_sum_exists_body_steps))) /\ ((((exists fs_h_blrr_extend_sum_exists_body_steps_successor. fs_h_blrr_extend_sum_exists_body_steps_successor + S (fs_s_blrr_extend_sum_exists_body_steps) = S ((S (S fs_i_blrr_extend_sum_exists_body_steps)) * fs_v_blrr_extend_sum_exists)) /\ exists fs_q_blrr_extend_sum_exists_body_steps_successor. fs_u_blrr_extend_sum_exists = fs_q_blrr_extend_sum_exists_body_steps_successor * S ((S (S fs_i_blrr_extend_sum_exists_body_steps)) * fs_v_blrr_extend_sum_exists) + (fs_s_blrr_extend_sum_exists_body_steps))) /\ fs_s_blrr_extend_sum_exists_body_steps = fs_r_blrr_extend_sum_exists_body_steps + fs_a_blrr_extend_sum_exists_body_steps)))))
  23. 0023specialize beta_sum_exists x
  24. 0024specialize beta_sum_exists x1
  25. 0025specialize beta_sum_exists (S n)
  26. 0026exact beta_sum_exists
  27. 0027cases hsuccessor_sum
  28. 0028have hpredecessor_sum : Sum(x,x1,n,x2)
    Exact native replay linehave hpredecessor_sum : exists ff_u_blrr_extend_predecessor_sum ff_v_blrr_extend_predecessor_sum. ((((exists ff_h_blrr_extend_predecessor_sum_start. ff_h_blrr_extend_predecessor_sum_start + S (0) = S ((S (0)) * ff_v_blrr_extend_predecessor_sum)) /\ exists ff_q_blrr_extend_predecessor_sum_start. ff_u_blrr_extend_predecessor_sum = ff_q_blrr_extend_predecessor_sum_start * S ((S (0)) * ff_v_blrr_extend_predecessor_sum) + (0))) /\ ((((exists ff_h_blrr_extend_predecessor_sum_terminal. ff_h_blrr_extend_predecessor_sum_terminal + S (x2) = S ((S (n)) * ff_v_blrr_extend_predecessor_sum)) /\ exists ff_q_blrr_extend_predecessor_sum_terminal. ff_u_blrr_extend_predecessor_sum = ff_q_blrr_extend_predecessor_sum_terminal * S ((S (n)) * ff_v_blrr_extend_predecessor_sum) + (x2))) /\ forall ff_i_blrr_extend_predecessor_sum. (exists ff_lt_blrr_extend_predecessor_sum_bound. ff_lt_blrr_extend_predecessor_sum_bound + S ff_i_blrr_extend_predecessor_sum = n) -> exists ff_a_blrr_extend_predecessor_sum ff_r_blrr_extend_predecessor_sum ff_s_blrr_extend_predecessor_sum. ((((exists ff_h_blrr_extend_predecessor_sum_summand. ff_h_blrr_extend_predecessor_sum_summand + S (ff_a_blrr_extend_predecessor_sum) = S ((S (ff_i_blrr_extend_predecessor_sum)) * x1)) /\ exists ff_q_blrr_extend_predecessor_sum_summand. x = ff_q_blrr_extend_predecessor_sum_summand * S ((S (ff_i_blrr_extend_predecessor_sum)) * x1) + (ff_a_blrr_extend_predecessor_sum))) /\ ((((exists ff_h_blrr_extend_predecessor_sum_partial. ff_h_blrr_extend_predecessor_sum_partial + S (ff_r_blrr_extend_predecessor_sum) = S ((S (ff_i_blrr_extend_predecessor_sum)) * ff_v_blrr_extend_predecessor_sum)) /\ exists ff_q_blrr_extend_predecessor_sum_partial. ff_u_blrr_extend_predecessor_sum = ff_q_blrr_extend_predecessor_sum_partial * S ((S (ff_i_blrr_extend_predecessor_sum)) * ff_v_blrr_extend_predecessor_sum) + (ff_r_blrr_extend_predecessor_sum))) /\ ((((exists ff_h_blrr_extend_predecessor_sum_successor. ff_h_blrr_extend_predecessor_sum_successor + S (ff_s_blrr_extend_predecessor_sum) = S ((S (S ff_i_blrr_extend_predecessor_sum)) * ff_v_blrr_extend_predecessor_sum)) /\ exists ff_q_blrr_extend_predecessor_sum_successor. ff_u_blrr_extend_predecessor_sum = ff_q_blrr_extend_predecessor_sum_successor * S ((S (S ff_i_blrr_extend_predecessor_sum)) * ff_v_blrr_extend_predecessor_sum) + (ff_s_blrr_extend_predecessor_sum))) /\ ff_s_blrr_extend_predecessor_sum = ff_r_blrr_extend_predecessor_sum + ff_a_blrr_extend_predecessor_sum)))))
  29. 0029specialize beta_sum_succ_last_zero x
  30. 0030specialize beta_sum_succ_last_zero x1
  31. 0031specialize beta_sum_succ_last_zero n
  32. 0032specialize beta_sum_succ_last_zero x2
  33. 0033apply beta_sum_succ_last_zero
  34. 0034exact hsuccessor_sum_witness
  35. 0035exact hzero
  36. 0036have hrestricted : PowerQuotPrefix(p,n,x,x1,n)
    Exact native replay linehave hrestricted : forall bls_index_blrr_extend_restricted. (exists bls_gap_blrr_extend_restricted_bound. bls_gap_blrr_extend_restricted_bound + S (bls_index_blrr_extend_restricted) = (n)) -> exists bls_power_blrr_extend_restricted bls_quotient_blrr_extend_restricted bls_remainder_blrr_extend_restricted. ((exists bpvi_b_bls_blrr_extend_restricted_power bpvi_c_bls_blrr_extend_restricted_power. ((forall bpvi_i_bls_blrr_extend_restricted_power. (exists bpvi_repeat_gap_bls_blrr_extend_restricted_power. bpvi_repeat_gap_bls_blrr_extend_restricted_power + S bpvi_i_bls_blrr_extend_restricted_power = S bls_index_blrr_extend_restricted) -> (((exists bpvi_h_bls_blrr_extend_restricted_power_repeat. bpvi_h_bls_blrr_extend_restricted_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_extend_restricted_power)) * bpvi_c_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_repeat. bpvi_b_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_repeat * S ((S (bpvi_i_bls_blrr_extend_restricted_power)) * bpvi_c_bls_blrr_extend_restricted_power) + (p)))) /\ (exists bpvi_u_bls_blrr_extend_restricted_power bpvi_v_bls_blrr_extend_restricted_power. ((((exists bpvi_h_bls_blrr_extend_restricted_power_start. bpvi_h_bls_blrr_extend_restricted_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_start. bpvi_u_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_start * S ((S (0)) * bpvi_v_bls_blrr_extend_restricted_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_extend_restricted_power_terminal. bpvi_h_bls_blrr_extend_restricted_power_terminal + S (bls_power_blrr_extend_restricted) = S ((S (S bls_index_blrr_extend_restricted)) * bpvi_v_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_terminal. bpvi_u_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_terminal * S ((S (S bls_index_blrr_extend_restricted)) * bpvi_v_bls_blrr_extend_restricted_power) + (bls_power_blrr_extend_restricted))) /\ forall bpvi_j_bls_blrr_extend_restricted_power. (exists bpvi_product_gap_bls_blrr_extend_restricted_power. bpvi_product_gap_bls_blrr_extend_restricted_power + S bpvi_j_bls_blrr_extend_restricted_power = S bls_index_blrr_extend_restricted) -> exists bpvi_factor_bls_blrr_extend_restricted_power bpvi_partial_bls_blrr_extend_restricted_power bpvi_successor_bls_blrr_extend_restricted_power. ((((exists bpvi_h_bls_blrr_extend_restricted_power_factor. bpvi_h_bls_blrr_extend_restricted_power_factor + S (bpvi_factor_bls_blrr_extend_restricted_power) = S ((S (bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_c_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_factor. bpvi_b_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_factor * S ((S (bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_c_bls_blrr_extend_restricted_power) + (bpvi_factor_bls_blrr_extend_restricted_power))) /\ ((((exists bpvi_h_bls_blrr_extend_restricted_power_partial. bpvi_h_bls_blrr_extend_restricted_power_partial + S (bpvi_partial_bls_blrr_extend_restricted_power) = S ((S (bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_v_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_partial. bpvi_u_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_partial * S ((S (bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_v_bls_blrr_extend_restricted_power) + (bpvi_partial_bls_blrr_extend_restricted_power))) /\ ((((exists bpvi_h_bls_blrr_extend_restricted_power_successor. bpvi_h_bls_blrr_extend_restricted_power_successor + S (bpvi_successor_bls_blrr_extend_restricted_power) = S ((S (S bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_v_bls_blrr_extend_restricted_power)) /\ exists bpvi_q_bls_blrr_extend_restricted_power_successor. bpvi_u_bls_blrr_extend_restricted_power = bpvi_q_bls_blrr_extend_restricted_power_successor * S ((S (S bpvi_j_bls_blrr_extend_restricted_power)) * bpvi_v_bls_blrr_extend_restricted_power) + (bpvi_successor_bls_blrr_extend_restricted_power))) /\ bpvi_successor_bls_blrr_extend_restricted_power = bpvi_partial_bls_blrr_extend_restricted_power * bpvi_factor_bls_blrr_extend_restricted_power)))))))) /\ ((((exists ff_h_bls_blrr_extend_restricted_quotient_entry. ff_h_bls_blrr_extend_restricted_quotient_entry + S (bls_quotient_blrr_extend_restricted) = S ((S (bls_index_blrr_extend_restricted)) * x1)) /\ exists ff_q_bls_blrr_extend_restricted_quotient_entry. x = ff_q_bls_blrr_extend_restricted_quotient_entry * S ((S (bls_index_blrr_extend_restricted)) * x1) + (bls_quotient_blrr_extend_restricted))) /\ ((n = bls_power_blrr_extend_restricted * bls_quotient_blrr_extend_restricted + bls_remainder_blrr_extend_restricted /\ exists bls_remainder_gap_blrr_extend_restricted_division. bls_remainder_gap_blrr_extend_restricted_division + S (bls_remainder_blrr_extend_restricted) = bls_power_blrr_extend_restricted))))
  37. 0037intro i
  38. 0038intro hi
  39. 0039specialize hprefix_witness_witness i
  40. 0040apply hprefix_witness_witness
  41. 0041specialize le_succ (S i)
  42. 0042specialize le_succ n
  43. 0043apply le_succ
  44. 0044exact hi
  45. 0045have hcompeting : LegendreSum(p,n,x2)
    Exact native replay linehave hcompeting : exists bls_code_blrr_extend_competing bls_scale_blrr_extend_competing. ((forall bls_index_blrr_extend_competing_prefix. (exists bls_gap_blrr_extend_competing_prefix_bound. bls_gap_blrr_extend_competing_prefix_bound + S (bls_index_blrr_extend_competing_prefix) = (n)) -> exists bls_power_blrr_extend_competing_prefix bls_quotient_blrr_extend_competing_prefix bls_remainder_blrr_extend_competing_prefix. ((exists bpvi_b_bls_blrr_extend_competing_prefix_power bpvi_c_bls_blrr_extend_competing_prefix_power. ((forall bpvi_i_bls_blrr_extend_competing_prefix_power. (exists bpvi_repeat_gap_bls_blrr_extend_competing_prefix_power. bpvi_repeat_gap_bls_blrr_extend_competing_prefix_power + S bpvi_i_bls_blrr_extend_competing_prefix_power = S bls_index_blrr_extend_competing_prefix) -> (((exists bpvi_h_bls_blrr_extend_competing_prefix_power_repeat. bpvi_h_bls_blrr_extend_competing_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_extend_competing_prefix_power)) * bpvi_c_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_repeat. bpvi_b_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_repeat * S ((S (bpvi_i_bls_blrr_extend_competing_prefix_power)) * bpvi_c_bls_blrr_extend_competing_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blrr_extend_competing_prefix_power bpvi_v_bls_blrr_extend_competing_prefix_power. ((((exists bpvi_h_bls_blrr_extend_competing_prefix_power_start. bpvi_h_bls_blrr_extend_competing_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_start. bpvi_u_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_start * S ((S (0)) * bpvi_v_bls_blrr_extend_competing_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_extend_competing_prefix_power_terminal. bpvi_h_bls_blrr_extend_competing_prefix_power_terminal + S (bls_power_blrr_extend_competing_prefix) = S ((S (S bls_index_blrr_extend_competing_prefix)) * bpvi_v_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_terminal. bpvi_u_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_terminal * S ((S (S bls_index_blrr_extend_competing_prefix)) * bpvi_v_bls_blrr_extend_competing_prefix_power) + (bls_power_blrr_extend_competing_prefix))) /\ forall bpvi_j_bls_blrr_extend_competing_prefix_power. (exists bpvi_product_gap_bls_blrr_extend_competing_prefix_power. bpvi_product_gap_bls_blrr_extend_competing_prefix_power + S bpvi_j_bls_blrr_extend_competing_prefix_power = S bls_index_blrr_extend_competing_prefix) -> exists bpvi_factor_bls_blrr_extend_competing_prefix_power bpvi_partial_bls_blrr_extend_competing_prefix_power bpvi_successor_bls_blrr_extend_competing_prefix_power. ((((exists bpvi_h_bls_blrr_extend_competing_prefix_power_factor. bpvi_h_bls_blrr_extend_competing_prefix_power_factor + S (bpvi_factor_bls_blrr_extend_competing_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_c_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_factor. bpvi_b_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_factor * S ((S (bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_c_bls_blrr_extend_competing_prefix_power) + (bpvi_factor_bls_blrr_extend_competing_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_competing_prefix_power_partial. bpvi_h_bls_blrr_extend_competing_prefix_power_partial + S (bpvi_partial_bls_blrr_extend_competing_prefix_power) = S ((S (bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_v_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_partial. bpvi_u_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_partial * S ((S (bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_v_bls_blrr_extend_competing_prefix_power) + (bpvi_partial_bls_blrr_extend_competing_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_extend_competing_prefix_power_successor. bpvi_h_bls_blrr_extend_competing_prefix_power_successor + S (bpvi_successor_bls_blrr_extend_competing_prefix_power) = S ((S (S bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_v_bls_blrr_extend_competing_prefix_power)) /\ exists bpvi_q_bls_blrr_extend_competing_prefix_power_successor. bpvi_u_bls_blrr_extend_competing_prefix_power = bpvi_q_bls_blrr_extend_competing_prefix_power_successor * S ((S (S bpvi_j_bls_blrr_extend_competing_prefix_power)) * bpvi_v_bls_blrr_extend_competing_prefix_power) + (bpvi_successor_bls_blrr_extend_competing_prefix_power))) /\ bpvi_successor_bls_blrr_extend_competing_prefix_power = bpvi_partial_bls_blrr_extend_competing_prefix_power * bpvi_factor_bls_blrr_extend_competing_prefix_power)))))))) /\ ((((exists ff_h_bls_blrr_extend_competing_prefix_quotient_entry. ff_h_bls_blrr_extend_competing_prefix_quotient_entry + S (bls_quotient_blrr_extend_competing_prefix) = S ((S (bls_index_blrr_extend_competing_prefix)) * bls_scale_blrr_extend_competing)) /\ exists ff_q_bls_blrr_extend_competing_prefix_quotient_entry. bls_code_blrr_extend_competing = ff_q_bls_blrr_extend_competing_prefix_quotient_entry * S ((S (bls_index_blrr_extend_competing_prefix)) * bls_scale_blrr_extend_competing) + (bls_quotient_blrr_extend_competing_prefix))) /\ ((n = bls_power_blrr_extend_competing_prefix * bls_quotient_blrr_extend_competing_prefix + bls_remainder_blrr_extend_competing_prefix /\ exists bls_remainder_gap_blrr_extend_competing_prefix_division. bls_remainder_gap_blrr_extend_competing_prefix_division + S (bls_remainder_blrr_extend_competing_prefix) = bls_power_blrr_extend_competing_prefix))))) /\ (exists ff_u_bls_blrr_extend_competing_sum ff_v_bls_blrr_extend_competing_sum. ((((exists ff_h_bls_blrr_extend_competing_sum_start. ff_h_bls_blrr_extend_competing_sum_start + S (0) = S ((S (0)) * ff_v_bls_blrr_extend_competing_sum)) /\ exists ff_q_bls_blrr_extend_competing_sum_start. ff_u_bls_blrr_extend_competing_sum = ff_q_bls_blrr_extend_competing_sum_start * S ((S (0)) * ff_v_bls_blrr_extend_competing_sum) + (0))) /\ ((((exists ff_h_bls_blrr_extend_competing_sum_terminal. ff_h_bls_blrr_extend_competing_sum_terminal + S (x2) = S ((S (n)) * ff_v_bls_blrr_extend_competing_sum)) /\ exists ff_q_bls_blrr_extend_competing_sum_terminal. ff_u_bls_blrr_extend_competing_sum = ff_q_bls_blrr_extend_competing_sum_terminal * S ((S (n)) * ff_v_bls_blrr_extend_competing_sum) + (x2))) /\ forall ff_i_bls_blrr_extend_competing_sum. (exists ff_lt_bls_blrr_extend_competing_sum_bound. ff_lt_bls_blrr_extend_competing_sum_bound + S ff_i_bls_blrr_extend_competing_sum = n) -> exists ff_a_bls_blrr_extend_competing_sum ff_r_bls_blrr_extend_competing_sum ff_s_bls_blrr_extend_competing_sum. ((((exists ff_h_bls_blrr_extend_competing_sum_summand. ff_h_bls_blrr_extend_competing_sum_summand + S (ff_a_bls_blrr_extend_competing_sum) = S ((S (ff_i_bls_blrr_extend_competing_sum)) * bls_scale_blrr_extend_competing)) /\ exists ff_q_bls_blrr_extend_competing_sum_summand. bls_code_blrr_extend_competing = ff_q_bls_blrr_extend_competing_sum_summand * S ((S (ff_i_bls_blrr_extend_competing_sum)) * bls_scale_blrr_extend_competing) + (ff_a_bls_blrr_extend_competing_sum))) /\ ((((exists ff_h_bls_blrr_extend_competing_sum_partial. ff_h_bls_blrr_extend_competing_sum_partial + S (ff_r_bls_blrr_extend_competing_sum) = S ((S (ff_i_bls_blrr_extend_competing_sum)) * ff_v_bls_blrr_extend_competing_sum)) /\ exists ff_q_bls_blrr_extend_competing_sum_partial. ff_u_bls_blrr_extend_competing_sum = ff_q_bls_blrr_extend_competing_sum_partial * S ((S (ff_i_bls_blrr_extend_competing_sum)) * ff_v_bls_blrr_extend_competing_sum) + (ff_r_bls_blrr_extend_competing_sum))) /\ ((((exists ff_h_bls_blrr_extend_competing_sum_successor. ff_h_bls_blrr_extend_competing_sum_successor + S (ff_s_bls_blrr_extend_competing_sum) = S ((S (S ff_i_bls_blrr_extend_competing_sum)) * ff_v_bls_blrr_extend_competing_sum)) /\ exists ff_q_bls_blrr_extend_competing_sum_successor. ff_u_bls_blrr_extend_competing_sum = ff_q_bls_blrr_extend_competing_sum_successor * S ((S (S ff_i_bls_blrr_extend_competing_sum)) * ff_v_bls_blrr_extend_competing_sum) + (ff_s_bls_blrr_extend_competing_sum))) /\ ff_s_bls_blrr_extend_competing_sum = ff_r_bls_blrr_extend_competing_sum + ff_a_bls_blrr_extend_competing_sum)))))))
  46. 0046exists x
  47. 0047exists x1
  48. 0048split
  49. 0049exact hrestricted
  50. 0050exact hpredecessor_sum
  51. 0051have heq : e = x2
  52. 0052specialize legendre_sum_functional p
  53. 0053specialize legendre_sum_functional n
  54. 0054specialize legendre_sum_functional e
  55. 0055specialize legendre_sum_functional x2
  56. 0056apply legendre_sum_functional
  57. 0057exact hlegendre
  58. 0058exact hcompeting
  59. 0059exists x
  60. 0060exists x1
  61. 0061split
  62. 0062exact hprefix_witness_witness
  63. 0063rewrite heq
  64. 0064rewrite heq
  65. 0065exact hsuccessor_sum_witness