BT00XQ · Bertrand theorem

power_quotient_prefix_sum_extend_zero

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

Zero quotient tails preserve the finite Legendre sum.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ p. ∀ n. ∀ b. ∀ c. ∀ g. ∀ t. ∀ e. Prime(p) → PowerQuotPrefix(p,n,b,c,n + g) → Sum(b,c,n + g,t) → LegendreSum(p,n,e) → t = 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

PD0001 Le PD0002 Lt PD0013 BetaAt PD0015 Sum PD0049 PowerQuotPrefix PD0050 LegendreSum

6 occurrences

Exact expanded native-PA statement
forall p n b c g t e. ((~(p = 1) /\ forall frm_prime_left_b5cvpsez_prime frm_prime_right_b5cvpsez_prime. p = frm_prime_left_b5cvpsez_prime * frm_prime_right_b5cvpsez_prime -> frm_prime_left_b5cvpsez_prime = 1 \/ frm_prime_right_b5cvpsez_prime = 1)) -> (forall bls_index_b5cvpsez_prefix. (exists bls_gap_b5cvpsez_prefix_bound. bls_gap_b5cvpsez_prefix_bound + S (bls_index_b5cvpsez_prefix) = (n + g)) -> exists bls_power_b5cvpsez_prefix bls_quotient_b5cvpsez_prefix bls_remainder_b5cvpsez_prefix. ((exists bpvi_b_bls_b5cvpsez_prefix_power bpvi_c_bls_b5cvpsez_prefix_power. ((forall bpvi_i_bls_b5cvpsez_prefix_power. (exists bpvi_repeat_gap_bls_b5cvpsez_prefix_power. bpvi_repeat_gap_bls_b5cvpsez_prefix_power + S bpvi_i_bls_b5cvpsez_prefix_power = S bls_index_b5cvpsez_prefix) -> (((exists bpvi_h_bls_b5cvpsez_prefix_power_repeat. bpvi_h_bls_b5cvpsez_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_b5cvpsez_prefix_power)) * bpvi_c_bls_b5cvpsez_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_prefix_power_repeat. bpvi_b_bls_b5cvpsez_prefix_power = bpvi_q_bls_b5cvpsez_prefix_power_repeat * S ((S (bpvi_i_bls_b5cvpsez_prefix_power)) * bpvi_c_bls_b5cvpsez_prefix_power) + (p)))) /\ (exists bpvi_u_bls_b5cvpsez_prefix_power bpvi_v_bls_b5cvpsez_prefix_power. ((((exists bpvi_h_bls_b5cvpsez_prefix_power_start. bpvi_h_bls_b5cvpsez_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5cvpsez_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_prefix_power_start. bpvi_u_bls_b5cvpsez_prefix_power = bpvi_q_bls_b5cvpsez_prefix_power_start * S ((S (0)) * bpvi_v_bls_b5cvpsez_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_b5cvpsez_prefix_power_terminal. bpvi_h_bls_b5cvpsez_prefix_power_terminal + S (bls_power_b5cvpsez_prefix) = S ((S (S bls_index_b5cvpsez_prefix)) * bpvi_v_bls_b5cvpsez_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_prefix_power_terminal. bpvi_u_bls_b5cvpsez_prefix_power = bpvi_q_bls_b5cvpsez_prefix_power_terminal * S ((S (S bls_index_b5cvpsez_prefix)) * bpvi_v_bls_b5cvpsez_prefix_power) + (bls_power_b5cvpsez_prefix))) /\ forall bpvi_j_bls_b5cvpsez_prefix_power. (exists bpvi_product_gap_bls_b5cvpsez_prefix_power. bpvi_product_gap_bls_b5cvpsez_prefix_power + S bpvi_j_bls_b5cvpsez_prefix_power = S bls_index_b5cvpsez_prefix) -> exists bpvi_factor_bls_b5cvpsez_prefix_power bpvi_partial_bls_b5cvpsez_prefix_power bpvi_successor_bls_b5cvpsez_prefix_power. ((((exists bpvi_h_bls_b5cvpsez_prefix_power_factor. bpvi_h_bls_b5cvpsez_prefix_power_factor + S (bpvi_factor_bls_b5cvpsez_prefix_power) = S ((S (bpvi_j_bls_b5cvpsez_prefix_power)) * bpvi_c_bls_b5cvpsez_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_prefix_power_factor. bpvi_b_bls_b5cvpsez_prefix_power = bpvi_q_bls_b5cvpsez_prefix_power_factor * S ((S (bpvi_j_bls_b5cvpsez_prefix_power)) * bpvi_c_bls_b5cvpsez_prefix_power) + (bpvi_factor_bls_b5cvpsez_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_prefix_power_partial. bpvi_h_bls_b5cvpsez_prefix_power_partial + S (bpvi_partial_bls_b5cvpsez_prefix_power) = S ((S (bpvi_j_bls_b5cvpsez_prefix_power)) * bpvi_v_bls_b5cvpsez_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_prefix_power_partial. bpvi_u_bls_b5cvpsez_prefix_power = bpvi_q_bls_b5cvpsez_prefix_power_partial * S ((S (bpvi_j_bls_b5cvpsez_prefix_power)) * bpvi_v_bls_b5cvpsez_prefix_power) + (bpvi_partial_bls_b5cvpsez_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_prefix_power_successor. bpvi_h_bls_b5cvpsez_prefix_power_successor + S (bpvi_successor_bls_b5cvpsez_prefix_power) = S ((S (S bpvi_j_bls_b5cvpsez_prefix_power)) * bpvi_v_bls_b5cvpsez_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_prefix_power_successor. bpvi_u_bls_b5cvpsez_prefix_power = bpvi_q_bls_b5cvpsez_prefix_power_successor * S ((S (S bpvi_j_bls_b5cvpsez_prefix_power)) * bpvi_v_bls_b5cvpsez_prefix_power) + (bpvi_successor_bls_b5cvpsez_prefix_power))) /\ bpvi_successor_bls_b5cvpsez_prefix_power = bpvi_partial_bls_b5cvpsez_prefix_power * bpvi_factor_bls_b5cvpsez_prefix_power)))))))) /\ ((((exists ff_h_bls_b5cvpsez_prefix_quotient_entry. ff_h_bls_b5cvpsez_prefix_quotient_entry + S (bls_quotient_b5cvpsez_prefix) = S ((S (bls_index_b5cvpsez_prefix)) * c)) /\ exists ff_q_bls_b5cvpsez_prefix_quotient_entry. b = ff_q_bls_b5cvpsez_prefix_quotient_entry * S ((S (bls_index_b5cvpsez_prefix)) * c) + (bls_quotient_b5cvpsez_prefix))) /\ ((n = bls_power_b5cvpsez_prefix * bls_quotient_b5cvpsez_prefix + bls_remainder_b5cvpsez_prefix /\ exists bls_remainder_gap_b5cvpsez_prefix_division. bls_remainder_gap_b5cvpsez_prefix_division + S (bls_remainder_b5cvpsez_prefix) = bls_power_b5cvpsez_prefix))))) -> (exists fs_u_b5cvpsez_sum fs_v_b5cvpsez_sum. ((((exists fs_h_b5cvpsez_sum_body_start. fs_h_b5cvpsez_sum_body_start + S (0) = S ((S (0)) * fs_v_b5cvpsez_sum)) /\ exists fs_q_b5cvpsez_sum_body_start. fs_u_b5cvpsez_sum = fs_q_b5cvpsez_sum_body_start * S ((S (0)) * fs_v_b5cvpsez_sum) + (0))) /\ ((((exists fs_h_b5cvpsez_sum_body_terminal. fs_h_b5cvpsez_sum_body_terminal + S (t) = S ((S (n + g)) * fs_v_b5cvpsez_sum)) /\ exists fs_q_b5cvpsez_sum_body_terminal. fs_u_b5cvpsez_sum = fs_q_b5cvpsez_sum_body_terminal * S ((S (n + g)) * fs_v_b5cvpsez_sum) + (t))) /\ forall fs_i_b5cvpsez_sum_body_steps. (exists fs_lt_b5cvpsez_sum_body_steps_bound. fs_lt_b5cvpsez_sum_body_steps_bound + S fs_i_b5cvpsez_sum_body_steps = n + g) -> exists fs_a_b5cvpsez_sum_body_steps fs_r_b5cvpsez_sum_body_steps fs_s_b5cvpsez_sum_body_steps. ((((exists fs_h_b5cvpsez_sum_body_steps_summand. fs_h_b5cvpsez_sum_body_steps_summand + S (fs_a_b5cvpsez_sum_body_steps) = S ((S (fs_i_b5cvpsez_sum_body_steps)) * c)) /\ exists fs_q_b5cvpsez_sum_body_steps_summand. b = fs_q_b5cvpsez_sum_body_steps_summand * S ((S (fs_i_b5cvpsez_sum_body_steps)) * c) + (fs_a_b5cvpsez_sum_body_steps))) /\ ((((exists fs_h_b5cvpsez_sum_body_steps_partial. fs_h_b5cvpsez_sum_body_steps_partial + S (fs_r_b5cvpsez_sum_body_steps) = S ((S (fs_i_b5cvpsez_sum_body_steps)) * fs_v_b5cvpsez_sum)) /\ exists fs_q_b5cvpsez_sum_body_steps_partial. fs_u_b5cvpsez_sum = fs_q_b5cvpsez_sum_body_steps_partial * S ((S (fs_i_b5cvpsez_sum_body_steps)) * fs_v_b5cvpsez_sum) + (fs_r_b5cvpsez_sum_body_steps))) /\ ((((exists fs_h_b5cvpsez_sum_body_steps_successor. fs_h_b5cvpsez_sum_body_steps_successor + S (fs_s_b5cvpsez_sum_body_steps) = S ((S (S fs_i_b5cvpsez_sum_body_steps)) * fs_v_b5cvpsez_sum)) /\ exists fs_q_b5cvpsez_sum_body_steps_successor. fs_u_b5cvpsez_sum = fs_q_b5cvpsez_sum_body_steps_successor * S ((S (S fs_i_b5cvpsez_sum_body_steps)) * fs_v_b5cvpsez_sum) + (fs_s_b5cvpsez_sum_body_steps))) /\ fs_s_b5cvpsez_sum_body_steps = fs_r_b5cvpsez_sum_body_steps + fs_a_b5cvpsez_sum_body_steps)))))) -> (exists bls_code_b5cvpsez_legendre bls_scale_b5cvpsez_legendre. ((forall bls_index_b5cvpsez_legendre_prefix. (exists bls_gap_b5cvpsez_legendre_prefix_bound. bls_gap_b5cvpsez_legendre_prefix_bound + S (bls_index_b5cvpsez_legendre_prefix) = (n)) -> exists bls_power_b5cvpsez_legendre_prefix bls_quotient_b5cvpsez_legendre_prefix bls_remainder_b5cvpsez_legendre_prefix. ((exists bpvi_b_bls_b5cvpsez_legendre_prefix_power bpvi_c_bls_b5cvpsez_legendre_prefix_power. ((forall bpvi_i_bls_b5cvpsez_legendre_prefix_power. (exists bpvi_repeat_gap_bls_b5cvpsez_legendre_prefix_power. bpvi_repeat_gap_bls_b5cvpsez_legendre_prefix_power + S bpvi_i_bls_b5cvpsez_legendre_prefix_power = S bls_index_b5cvpsez_legendre_prefix) -> (((exists bpvi_h_bls_b5cvpsez_legendre_prefix_power_repeat. bpvi_h_bls_b5cvpsez_legendre_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_b5cvpsez_legendre_prefix_power)) * bpvi_c_bls_b5cvpsez_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_legendre_prefix_power_repeat. bpvi_b_bls_b5cvpsez_legendre_prefix_power = bpvi_q_bls_b5cvpsez_legendre_prefix_power_repeat * S ((S (bpvi_i_bls_b5cvpsez_legendre_prefix_power)) * bpvi_c_bls_b5cvpsez_legendre_prefix_power) + (p)))) /\ (exists bpvi_u_bls_b5cvpsez_legendre_prefix_power bpvi_v_bls_b5cvpsez_legendre_prefix_power. ((((exists bpvi_h_bls_b5cvpsez_legendre_prefix_power_start. bpvi_h_bls_b5cvpsez_legendre_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5cvpsez_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_legendre_prefix_power_start. bpvi_u_bls_b5cvpsez_legendre_prefix_power = bpvi_q_bls_b5cvpsez_legendre_prefix_power_start * S ((S (0)) * bpvi_v_bls_b5cvpsez_legendre_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_b5cvpsez_legendre_prefix_power_terminal. bpvi_h_bls_b5cvpsez_legendre_prefix_power_terminal + S (bls_power_b5cvpsez_legendre_prefix) = S ((S (S bls_index_b5cvpsez_legendre_prefix)) * bpvi_v_bls_b5cvpsez_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_legendre_prefix_power_terminal. bpvi_u_bls_b5cvpsez_legendre_prefix_power = bpvi_q_bls_b5cvpsez_legendre_prefix_power_terminal * S ((S (S bls_index_b5cvpsez_legendre_prefix)) * bpvi_v_bls_b5cvpsez_legendre_prefix_power) + (bls_power_b5cvpsez_legendre_prefix))) /\ forall bpvi_j_bls_b5cvpsez_legendre_prefix_power. (exists bpvi_product_gap_bls_b5cvpsez_legendre_prefix_power. bpvi_product_gap_bls_b5cvpsez_legendre_prefix_power + S bpvi_j_bls_b5cvpsez_legendre_prefix_power = S bls_index_b5cvpsez_legendre_prefix) -> exists bpvi_factor_bls_b5cvpsez_legendre_prefix_power bpvi_partial_bls_b5cvpsez_legendre_prefix_power bpvi_successor_bls_b5cvpsez_legendre_prefix_power. ((((exists bpvi_h_bls_b5cvpsez_legendre_prefix_power_factor. bpvi_h_bls_b5cvpsez_legendre_prefix_power_factor + S (bpvi_factor_bls_b5cvpsez_legendre_prefix_power) = S ((S (bpvi_j_bls_b5cvpsez_legendre_prefix_power)) * bpvi_c_bls_b5cvpsez_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_legendre_prefix_power_factor. bpvi_b_bls_b5cvpsez_legendre_prefix_power = bpvi_q_bls_b5cvpsez_legendre_prefix_power_factor * S ((S (bpvi_j_bls_b5cvpsez_legendre_prefix_power)) * bpvi_c_bls_b5cvpsez_legendre_prefix_power) + (bpvi_factor_bls_b5cvpsez_legendre_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_legendre_prefix_power_partial. bpvi_h_bls_b5cvpsez_legendre_prefix_power_partial + S (bpvi_partial_bls_b5cvpsez_legendre_prefix_power) = S ((S (bpvi_j_bls_b5cvpsez_legendre_prefix_power)) * bpvi_v_bls_b5cvpsez_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_legendre_prefix_power_partial. bpvi_u_bls_b5cvpsez_legendre_prefix_power = bpvi_q_bls_b5cvpsez_legendre_prefix_power_partial * S ((S (bpvi_j_bls_b5cvpsez_legendre_prefix_power)) * bpvi_v_bls_b5cvpsez_legendre_prefix_power) + (bpvi_partial_bls_b5cvpsez_legendre_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_legendre_prefix_power_successor. bpvi_h_bls_b5cvpsez_legendre_prefix_power_successor + S (bpvi_successor_bls_b5cvpsez_legendre_prefix_power) = S ((S (S bpvi_j_bls_b5cvpsez_legendre_prefix_power)) * bpvi_v_bls_b5cvpsez_legendre_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_legendre_prefix_power_successor. bpvi_u_bls_b5cvpsez_legendre_prefix_power = bpvi_q_bls_b5cvpsez_legendre_prefix_power_successor * S ((S (S bpvi_j_bls_b5cvpsez_legendre_prefix_power)) * bpvi_v_bls_b5cvpsez_legendre_prefix_power) + (bpvi_successor_bls_b5cvpsez_legendre_prefix_power))) /\ bpvi_successor_bls_b5cvpsez_legendre_prefix_power = bpvi_partial_bls_b5cvpsez_legendre_prefix_power * bpvi_factor_bls_b5cvpsez_legendre_prefix_power)))))))) /\ ((((exists ff_h_bls_b5cvpsez_legendre_prefix_quotient_entry. ff_h_bls_b5cvpsez_legendre_prefix_quotient_entry + S (bls_quotient_b5cvpsez_legendre_prefix) = S ((S (bls_index_b5cvpsez_legendre_prefix)) * bls_scale_b5cvpsez_legendre)) /\ exists ff_q_bls_b5cvpsez_legendre_prefix_quotient_entry. bls_code_b5cvpsez_legendre = ff_q_bls_b5cvpsez_legendre_prefix_quotient_entry * S ((S (bls_index_b5cvpsez_legendre_prefix)) * bls_scale_b5cvpsez_legendre) + (bls_quotient_b5cvpsez_legendre_prefix))) /\ ((n = bls_power_b5cvpsez_legendre_prefix * bls_quotient_b5cvpsez_legendre_prefix + bls_remainder_b5cvpsez_legendre_prefix /\ exists bls_remainder_gap_b5cvpsez_legendre_prefix_division. bls_remainder_gap_b5cvpsez_legendre_prefix_division + S (bls_remainder_b5cvpsez_legendre_prefix) = bls_power_b5cvpsez_legendre_prefix))))) /\ (exists ff_u_bls_b5cvpsez_legendre_sum ff_v_bls_b5cvpsez_legendre_sum. ((((exists ff_h_bls_b5cvpsez_legendre_sum_start. ff_h_bls_b5cvpsez_legendre_sum_start + S (0) = S ((S (0)) * ff_v_bls_b5cvpsez_legendre_sum)) /\ exists ff_q_bls_b5cvpsez_legendre_sum_start. ff_u_bls_b5cvpsez_legendre_sum = ff_q_bls_b5cvpsez_legendre_sum_start * S ((S (0)) * ff_v_bls_b5cvpsez_legendre_sum) + (0))) /\ ((((exists ff_h_bls_b5cvpsez_legendre_sum_terminal. ff_h_bls_b5cvpsez_legendre_sum_terminal + S (e) = S ((S (n)) * ff_v_bls_b5cvpsez_legendre_sum)) /\ exists ff_q_bls_b5cvpsez_legendre_sum_terminal. ff_u_bls_b5cvpsez_legendre_sum = ff_q_bls_b5cvpsez_legendre_sum_terminal * S ((S (n)) * ff_v_bls_b5cvpsez_legendre_sum) + (e))) /\ forall ff_i_bls_b5cvpsez_legendre_sum. (exists ff_lt_bls_b5cvpsez_legendre_sum_bound. ff_lt_bls_b5cvpsez_legendre_sum_bound + S ff_i_bls_b5cvpsez_legendre_sum = n) -> exists ff_a_bls_b5cvpsez_legendre_sum ff_r_bls_b5cvpsez_legendre_sum ff_s_bls_b5cvpsez_legendre_sum. ((((exists ff_h_bls_b5cvpsez_legendre_sum_summand. ff_h_bls_b5cvpsez_legendre_sum_summand + S (ff_a_bls_b5cvpsez_legendre_sum) = S ((S (ff_i_bls_b5cvpsez_legendre_sum)) * bls_scale_b5cvpsez_legendre)) /\ exists ff_q_bls_b5cvpsez_legendre_sum_summand. bls_code_b5cvpsez_legendre = ff_q_bls_b5cvpsez_legendre_sum_summand * S ((S (ff_i_bls_b5cvpsez_legendre_sum)) * bls_scale_b5cvpsez_legendre) + (ff_a_bls_b5cvpsez_legendre_sum))) /\ ((((exists ff_h_bls_b5cvpsez_legendre_sum_partial. ff_h_bls_b5cvpsez_legendre_sum_partial + S (ff_r_bls_b5cvpsez_legendre_sum) = S ((S (ff_i_bls_b5cvpsez_legendre_sum)) * ff_v_bls_b5cvpsez_legendre_sum)) /\ exists ff_q_bls_b5cvpsez_legendre_sum_partial. ff_u_bls_b5cvpsez_legendre_sum = ff_q_bls_b5cvpsez_legendre_sum_partial * S ((S (ff_i_bls_b5cvpsez_legendre_sum)) * ff_v_bls_b5cvpsez_legendre_sum) + (ff_r_bls_b5cvpsez_legendre_sum))) /\ ((((exists ff_h_bls_b5cvpsez_legendre_sum_successor. ff_h_bls_b5cvpsez_legendre_sum_successor + S (ff_s_bls_b5cvpsez_legendre_sum) = S ((S (S ff_i_bls_b5cvpsez_legendre_sum)) * ff_v_bls_b5cvpsez_legendre_sum)) /\ exists ff_q_bls_b5cvpsez_legendre_sum_successor. ff_u_bls_b5cvpsez_legendre_sum = ff_q_bls_b5cvpsez_legendre_sum_successor * S ((S (S ff_i_bls_b5cvpsez_legendre_sum)) * ff_v_bls_b5cvpsez_legendre_sum) + (ff_s_bls_b5cvpsez_legendre_sum))) /\ ff_s_bls_b5cvpsez_legendre_sum = ff_r_bls_b5cvpsez_legendre_sum + ff_a_bls_b5cvpsez_legendre_sum)))))))) -> t = e

Proof neighborhood

Direct theorem prerequisites

BT00S3 legendre_sum_functional BT0018 le_succ BT0002 add_comm BT0000 zero_add BT00SR beta_sum_succ_last_zero BT00XP power_quotient_prefix_tail_entry_zero

Direct theorem dependents

BT00XR legendre_sum_extended_prefix_exists

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

86 script commands · 22 reading checkpoints · 8 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)
legendre sum functionalle succadd commzero addbeta sum succ last zeropower quotient prefix tail entry zero
01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
02Induction on gL5–11

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

  1. L5
    induction g
  2. L6
    intro t
  3. L7
    intro e
  4. L8
    intro hp
  5. L9
    intro hprefix
  6. L10
    intro hsum
  7. L11
    intro hlegendre
03Establish hbase_lengthL12–17

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

  1. L12
    have hbase_length : n + 0 = n
  2. L13
    apply PA3
  3. L14
    rewrite hbase_length at hprefix
  4. L15
    rewrite hbase_length at hsum
  5. L16
    rewrite hbase_length at hsum
  6. L17
    rewrite hbase_length at hsum
04Establish hcompetingL18–18

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

  1. L18
    have hcompeting : LegendreSum(p,n,t)Definitions: LegendreSum(p,n,t)Original native command in the exact edition
05Construct an explicit witnessL19–20

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

  1. L19
    exists b
  2. L20
    exists c
06Separate the logical casesL21–21

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

  1. L21
    split
07Use earlier factsL22–30

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

  1. L22
    exact hprefix
  2. L23
    exact hsum
  3. L24
    specialize legendre_sum_functional p
  4. L25
    specialize legendre_sum_functional n
  5. L26
    specialize legendre_sum_functional t
  6. L27
    specialize legendre_sum_functional e
  7. L28
    apply legendre_sum_functional
  8. L29
    exact hcompeting
  9. L30
    exact hlegendre
08Fix variables and assumptionsL31–36

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

  1. L31
    intro t
  2. L32
    intro e
  3. L33
    intro hp
  4. L34
    intro hprefix
  5. L35
    intro hsum
  6. L36
    intro hlegendre
09Establish hstep_lengthL37–38

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

  1. L37
    have hstep_length : n + S g = S (n + g)
  2. L38
    apply PA4
10Establish hrestrictedL39–48

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

  1. L39
    have hrestricted : PowerQuotPrefix(p,n,b,c,n + g)Definitions: PowerQuotPrefix(p,n,b,c,n + g)Original native command in the exact edition
  2. L40
    intro i
  3. L41
    intro hi
  4. L42
    specialize hprefix i
  5. L43
    apply hprefix
  6. L44
    rewrite hstep_length
  7. L45
    specialize le_succ (S i)
  8. L46
    specialize le_succ (n + g)
  9. L47
    apply le_succ
  10. L48
    exact hi
11Establish htail_startL49–49

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

  1. L49
    have htail_start : Le(n,n + g)Definitions: Le(n,n + g)Original native command in the exact edition
12Construct an explicit witnessL50–50

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

  1. L50
    exists g
13Use earlier factsL51–51

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

  1. L51
    apply add_comm
14Establish htail_boundL52–52

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

  1. L52
    have htail_bound : Lt(n + g,n + S g)Definitions: Lt(n + g,n + S g)Original native command in the exact edition
15Construct an explicit witnessL53–53

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

  1. L53
    exists 0
16Calculate and transport equalitiesL54–54

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

  1. L54
    rewrite hstep_length
17Use earlier factsL55–56

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

  1. L55
    specialize zero_add (S (n + g))
  2. L56
    exact zero_add
18Establish hzeroL57–66

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

  1. L57
    have hzero : BetaAt(b,c,n + g,0)Definitions: BetaAt(b,c,n + g,0)Original native command in the exact edition
  2. L58
    specialize power_quotient_prefix_tail_entry_zero p
  3. L59
    specialize power_quotient_prefix_tail_entry_zero n
  4. L60
    specialize power_quotient_prefix_tail_entry_zero b
  5. L61
    specialize power_quotient_prefix_tail_entry_zero c
  6. L62
    specialize power_quotient_prefix_tail_entry_zero (n + S g)
  7. L63
    specialize power_quotient_prefix_tail_entry_zero (n + g)
  8. L64
    apply power_quotient_prefix_tail_entry_zero
  9. L65
    exact hp
  10. L66
    exact hprefix
19Use earlier factsL67–68

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

  1. L67
    exact htail_start
  2. L68
    exact htail_bound
20Calculate and transport equalitiesL69–71

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

  1. L69
    rewrite hstep_length at hsum
  2. L70
    rewrite hstep_length at hsum
  3. L71
    rewrite hstep_length at hsum
21Establish hprefix_sumL72–81

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

  1. L72
    have hprefix_sum : Sum(b,c,n + g,t)Definitions: Sum(b,c,n + g,t)Original native command in the exact edition
  2. L73
    specialize beta_sum_succ_last_zero b
  3. L74
    specialize beta_sum_succ_last_zero c
  4. L75
    specialize beta_sum_succ_last_zero (n + g)
  5. L76
    specialize beta_sum_succ_last_zero t
  6. L77
    apply beta_sum_succ_last_zero
  7. L78
    exact hsum
  8. L79
    exact hzero
  9. L80
    specialize IH t
  10. L81
    specialize IH e
22Use earlier factsL82–86

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

  1. L82
    apply IH
  2. L83
    exact hp
  3. L84
    exact hrestricted
  4. L85
    exact hprefix_sum
  5. L86
    exact hlegendre

Library-wide reading audit

Original defined command ledger · 86 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005induction g
  6. 0006intro t
  7. 0007intro e
  8. 0008intro hp
  9. 0009intro hprefix
  10. 0010intro hsum
  11. 0011intro hlegendre
  12. 0012have hbase_length : n + 0 = n
  13. 0013apply PA3
  14. 0014rewrite hbase_length at hprefix
  15. 0015rewrite hbase_length at hsum
  16. 0016rewrite hbase_length at hsum
  17. 0017rewrite hbase_length at hsum
  18. 0018have hcompeting : LegendreSum(p,n,t)
    Exact native replay linehave hcompeting : exists bls_code_b5cvpsez_base bls_scale_b5cvpsez_base. ((forall bls_index_b5cvpsez_base_prefix. (exists bls_gap_b5cvpsez_base_prefix_bound. bls_gap_b5cvpsez_base_prefix_bound + S (bls_index_b5cvpsez_base_prefix) = (n)) -> exists bls_power_b5cvpsez_base_prefix bls_quotient_b5cvpsez_base_prefix bls_remainder_b5cvpsez_base_prefix. ((exists bpvi_b_bls_b5cvpsez_base_prefix_power bpvi_c_bls_b5cvpsez_base_prefix_power. ((forall bpvi_i_bls_b5cvpsez_base_prefix_power. (exists bpvi_repeat_gap_bls_b5cvpsez_base_prefix_power. bpvi_repeat_gap_bls_b5cvpsez_base_prefix_power + S bpvi_i_bls_b5cvpsez_base_prefix_power = S bls_index_b5cvpsez_base_prefix) -> (((exists bpvi_h_bls_b5cvpsez_base_prefix_power_repeat. bpvi_h_bls_b5cvpsez_base_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_b5cvpsez_base_prefix_power)) * bpvi_c_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_repeat. bpvi_b_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_repeat * S ((S (bpvi_i_bls_b5cvpsez_base_prefix_power)) * bpvi_c_bls_b5cvpsez_base_prefix_power) + (p)))) /\ (exists bpvi_u_bls_b5cvpsez_base_prefix_power bpvi_v_bls_b5cvpsez_base_prefix_power. ((((exists bpvi_h_bls_b5cvpsez_base_prefix_power_start. bpvi_h_bls_b5cvpsez_base_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_start. bpvi_u_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_start * S ((S (0)) * bpvi_v_bls_b5cvpsez_base_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_b5cvpsez_base_prefix_power_terminal. bpvi_h_bls_b5cvpsez_base_prefix_power_terminal + S (bls_power_b5cvpsez_base_prefix) = S ((S (S bls_index_b5cvpsez_base_prefix)) * bpvi_v_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_terminal. bpvi_u_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_terminal * S ((S (S bls_index_b5cvpsez_base_prefix)) * bpvi_v_bls_b5cvpsez_base_prefix_power) + (bls_power_b5cvpsez_base_prefix))) /\ forall bpvi_j_bls_b5cvpsez_base_prefix_power. (exists bpvi_product_gap_bls_b5cvpsez_base_prefix_power. bpvi_product_gap_bls_b5cvpsez_base_prefix_power + S bpvi_j_bls_b5cvpsez_base_prefix_power = S bls_index_b5cvpsez_base_prefix) -> exists bpvi_factor_bls_b5cvpsez_base_prefix_power bpvi_partial_bls_b5cvpsez_base_prefix_power bpvi_successor_bls_b5cvpsez_base_prefix_power. ((((exists bpvi_h_bls_b5cvpsez_base_prefix_power_factor. bpvi_h_bls_b5cvpsez_base_prefix_power_factor + S (bpvi_factor_bls_b5cvpsez_base_prefix_power) = S ((S (bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_c_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_factor. bpvi_b_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_factor * S ((S (bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_c_bls_b5cvpsez_base_prefix_power) + (bpvi_factor_bls_b5cvpsez_base_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_base_prefix_power_partial. bpvi_h_bls_b5cvpsez_base_prefix_power_partial + S (bpvi_partial_bls_b5cvpsez_base_prefix_power) = S ((S (bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_v_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_partial. bpvi_u_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_partial * S ((S (bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_v_bls_b5cvpsez_base_prefix_power) + (bpvi_partial_bls_b5cvpsez_base_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_base_prefix_power_successor. bpvi_h_bls_b5cvpsez_base_prefix_power_successor + S (bpvi_successor_bls_b5cvpsez_base_prefix_power) = S ((S (S bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_v_bls_b5cvpsez_base_prefix_power)) /\ exists bpvi_q_bls_b5cvpsez_base_prefix_power_successor. bpvi_u_bls_b5cvpsez_base_prefix_power = bpvi_q_bls_b5cvpsez_base_prefix_power_successor * S ((S (S bpvi_j_bls_b5cvpsez_base_prefix_power)) * bpvi_v_bls_b5cvpsez_base_prefix_power) + (bpvi_successor_bls_b5cvpsez_base_prefix_power))) /\ bpvi_successor_bls_b5cvpsez_base_prefix_power = bpvi_partial_bls_b5cvpsez_base_prefix_power * bpvi_factor_bls_b5cvpsez_base_prefix_power)))))))) /\ ((((exists ff_h_bls_b5cvpsez_base_prefix_quotient_entry. ff_h_bls_b5cvpsez_base_prefix_quotient_entry + S (bls_quotient_b5cvpsez_base_prefix) = S ((S (bls_index_b5cvpsez_base_prefix)) * bls_scale_b5cvpsez_base)) /\ exists ff_q_bls_b5cvpsez_base_prefix_quotient_entry. bls_code_b5cvpsez_base = ff_q_bls_b5cvpsez_base_prefix_quotient_entry * S ((S (bls_index_b5cvpsez_base_prefix)) * bls_scale_b5cvpsez_base) + (bls_quotient_b5cvpsez_base_prefix))) /\ ((n = bls_power_b5cvpsez_base_prefix * bls_quotient_b5cvpsez_base_prefix + bls_remainder_b5cvpsez_base_prefix /\ exists bls_remainder_gap_b5cvpsez_base_prefix_division. bls_remainder_gap_b5cvpsez_base_prefix_division + S (bls_remainder_b5cvpsez_base_prefix) = bls_power_b5cvpsez_base_prefix))))) /\ (exists ff_u_bls_b5cvpsez_base_sum ff_v_bls_b5cvpsez_base_sum. ((((exists ff_h_bls_b5cvpsez_base_sum_start. ff_h_bls_b5cvpsez_base_sum_start + S (0) = S ((S (0)) * ff_v_bls_b5cvpsez_base_sum)) /\ exists ff_q_bls_b5cvpsez_base_sum_start. ff_u_bls_b5cvpsez_base_sum = ff_q_bls_b5cvpsez_base_sum_start * S ((S (0)) * ff_v_bls_b5cvpsez_base_sum) + (0))) /\ ((((exists ff_h_bls_b5cvpsez_base_sum_terminal. ff_h_bls_b5cvpsez_base_sum_terminal + S (t) = S ((S (n)) * ff_v_bls_b5cvpsez_base_sum)) /\ exists ff_q_bls_b5cvpsez_base_sum_terminal. ff_u_bls_b5cvpsez_base_sum = ff_q_bls_b5cvpsez_base_sum_terminal * S ((S (n)) * ff_v_bls_b5cvpsez_base_sum) + (t))) /\ forall ff_i_bls_b5cvpsez_base_sum. (exists ff_lt_bls_b5cvpsez_base_sum_bound. ff_lt_bls_b5cvpsez_base_sum_bound + S ff_i_bls_b5cvpsez_base_sum = n) -> exists ff_a_bls_b5cvpsez_base_sum ff_r_bls_b5cvpsez_base_sum ff_s_bls_b5cvpsez_base_sum. ((((exists ff_h_bls_b5cvpsez_base_sum_summand. ff_h_bls_b5cvpsez_base_sum_summand + S (ff_a_bls_b5cvpsez_base_sum) = S ((S (ff_i_bls_b5cvpsez_base_sum)) * bls_scale_b5cvpsez_base)) /\ exists ff_q_bls_b5cvpsez_base_sum_summand. bls_code_b5cvpsez_base = ff_q_bls_b5cvpsez_base_sum_summand * S ((S (ff_i_bls_b5cvpsez_base_sum)) * bls_scale_b5cvpsez_base) + (ff_a_bls_b5cvpsez_base_sum))) /\ ((((exists ff_h_bls_b5cvpsez_base_sum_partial. ff_h_bls_b5cvpsez_base_sum_partial + S (ff_r_bls_b5cvpsez_base_sum) = S ((S (ff_i_bls_b5cvpsez_base_sum)) * ff_v_bls_b5cvpsez_base_sum)) /\ exists ff_q_bls_b5cvpsez_base_sum_partial. ff_u_bls_b5cvpsez_base_sum = ff_q_bls_b5cvpsez_base_sum_partial * S ((S (ff_i_bls_b5cvpsez_base_sum)) * ff_v_bls_b5cvpsez_base_sum) + (ff_r_bls_b5cvpsez_base_sum))) /\ ((((exists ff_h_bls_b5cvpsez_base_sum_successor. ff_h_bls_b5cvpsez_base_sum_successor + S (ff_s_bls_b5cvpsez_base_sum) = S ((S (S ff_i_bls_b5cvpsez_base_sum)) * ff_v_bls_b5cvpsez_base_sum)) /\ exists ff_q_bls_b5cvpsez_base_sum_successor. ff_u_bls_b5cvpsez_base_sum = ff_q_bls_b5cvpsez_base_sum_successor * S ((S (S ff_i_bls_b5cvpsez_base_sum)) * ff_v_bls_b5cvpsez_base_sum) + (ff_s_bls_b5cvpsez_base_sum))) /\ ff_s_bls_b5cvpsez_base_sum = ff_r_bls_b5cvpsez_base_sum + ff_a_bls_b5cvpsez_base_sum)))))))
  19. 0019exists b
  20. 0020exists c
  21. 0021split
  22. 0022exact hprefix
  23. 0023exact hsum
  24. 0024specialize legendre_sum_functional p
  25. 0025specialize legendre_sum_functional n
  26. 0026specialize legendre_sum_functional t
  27. 0027specialize legendre_sum_functional e
  28. 0028apply legendre_sum_functional
  29. 0029exact hcompeting
  30. 0030exact hlegendre
  31. 0031intro t
  32. 0032intro e
  33. 0033intro hp
  34. 0034intro hprefix
  35. 0035intro hsum
  36. 0036intro hlegendre
  37. 0037have hstep_length : n + S g = S (n + g)
  38. 0038apply PA4
  39. 0039have hrestricted : PowerQuotPrefix(p,n,b,c,n + g)
    Exact native replay linehave hrestricted : forall bls_index_b5cvpsez_restricted. (exists bls_gap_b5cvpsez_restricted_bound. bls_gap_b5cvpsez_restricted_bound + S (bls_index_b5cvpsez_restricted) = (n + g)) -> exists bls_power_b5cvpsez_restricted bls_quotient_b5cvpsez_restricted bls_remainder_b5cvpsez_restricted. ((exists bpvi_b_bls_b5cvpsez_restricted_power bpvi_c_bls_b5cvpsez_restricted_power. ((forall bpvi_i_bls_b5cvpsez_restricted_power. (exists bpvi_repeat_gap_bls_b5cvpsez_restricted_power. bpvi_repeat_gap_bls_b5cvpsez_restricted_power + S bpvi_i_bls_b5cvpsez_restricted_power = S bls_index_b5cvpsez_restricted) -> (((exists bpvi_h_bls_b5cvpsez_restricted_power_repeat. bpvi_h_bls_b5cvpsez_restricted_power_repeat + S (p) = S ((S (bpvi_i_bls_b5cvpsez_restricted_power)) * bpvi_c_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_repeat. bpvi_b_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_repeat * S ((S (bpvi_i_bls_b5cvpsez_restricted_power)) * bpvi_c_bls_b5cvpsez_restricted_power) + (p)))) /\ (exists bpvi_u_bls_b5cvpsez_restricted_power bpvi_v_bls_b5cvpsez_restricted_power. ((((exists bpvi_h_bls_b5cvpsez_restricted_power_start. bpvi_h_bls_b5cvpsez_restricted_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_start. bpvi_u_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_start * S ((S (0)) * bpvi_v_bls_b5cvpsez_restricted_power) + (1))) /\ ((((exists bpvi_h_bls_b5cvpsez_restricted_power_terminal. bpvi_h_bls_b5cvpsez_restricted_power_terminal + S (bls_power_b5cvpsez_restricted) = S ((S (S bls_index_b5cvpsez_restricted)) * bpvi_v_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_terminal. bpvi_u_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_terminal * S ((S (S bls_index_b5cvpsez_restricted)) * bpvi_v_bls_b5cvpsez_restricted_power) + (bls_power_b5cvpsez_restricted))) /\ forall bpvi_j_bls_b5cvpsez_restricted_power. (exists bpvi_product_gap_bls_b5cvpsez_restricted_power. bpvi_product_gap_bls_b5cvpsez_restricted_power + S bpvi_j_bls_b5cvpsez_restricted_power = S bls_index_b5cvpsez_restricted) -> exists bpvi_factor_bls_b5cvpsez_restricted_power bpvi_partial_bls_b5cvpsez_restricted_power bpvi_successor_bls_b5cvpsez_restricted_power. ((((exists bpvi_h_bls_b5cvpsez_restricted_power_factor. bpvi_h_bls_b5cvpsez_restricted_power_factor + S (bpvi_factor_bls_b5cvpsez_restricted_power) = S ((S (bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_c_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_factor. bpvi_b_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_factor * S ((S (bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_c_bls_b5cvpsez_restricted_power) + (bpvi_factor_bls_b5cvpsez_restricted_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_restricted_power_partial. bpvi_h_bls_b5cvpsez_restricted_power_partial + S (bpvi_partial_bls_b5cvpsez_restricted_power) = S ((S (bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_v_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_partial. bpvi_u_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_partial * S ((S (bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_v_bls_b5cvpsez_restricted_power) + (bpvi_partial_bls_b5cvpsez_restricted_power))) /\ ((((exists bpvi_h_bls_b5cvpsez_restricted_power_successor. bpvi_h_bls_b5cvpsez_restricted_power_successor + S (bpvi_successor_bls_b5cvpsez_restricted_power) = S ((S (S bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_v_bls_b5cvpsez_restricted_power)) /\ exists bpvi_q_bls_b5cvpsez_restricted_power_successor. bpvi_u_bls_b5cvpsez_restricted_power = bpvi_q_bls_b5cvpsez_restricted_power_successor * S ((S (S bpvi_j_bls_b5cvpsez_restricted_power)) * bpvi_v_bls_b5cvpsez_restricted_power) + (bpvi_successor_bls_b5cvpsez_restricted_power))) /\ bpvi_successor_bls_b5cvpsez_restricted_power = bpvi_partial_bls_b5cvpsez_restricted_power * bpvi_factor_bls_b5cvpsez_restricted_power)))))))) /\ ((((exists ff_h_bls_b5cvpsez_restricted_quotient_entry. ff_h_bls_b5cvpsez_restricted_quotient_entry + S (bls_quotient_b5cvpsez_restricted) = S ((S (bls_index_b5cvpsez_restricted)) * c)) /\ exists ff_q_bls_b5cvpsez_restricted_quotient_entry. b = ff_q_bls_b5cvpsez_restricted_quotient_entry * S ((S (bls_index_b5cvpsez_restricted)) * c) + (bls_quotient_b5cvpsez_restricted))) /\ ((n = bls_power_b5cvpsez_restricted * bls_quotient_b5cvpsez_restricted + bls_remainder_b5cvpsez_restricted /\ exists bls_remainder_gap_b5cvpsez_restricted_division. bls_remainder_gap_b5cvpsez_restricted_division + S (bls_remainder_b5cvpsez_restricted) = bls_power_b5cvpsez_restricted))))
  40. 0040intro i
  41. 0041intro hi
  42. 0042specialize hprefix i
  43. 0043apply hprefix
  44. 0044rewrite hstep_length
  45. 0045specialize le_succ (S i)
  46. 0046specialize le_succ (n + g)
  47. 0047apply le_succ
  48. 0048exact hi
  49. 0049have htail_start : Le(n,n + g)
    Exact native replay linehave htail_start : exists k. k + n = n + g
  50. 0050exists g
  51. 0051apply add_comm
  52. 0052have htail_bound : Lt(n + g,n + S g)
    Exact native replay linehave htail_bound : exists k. k + S (n + g) = n + S g
  53. 0053exists 0
  54. 0054rewrite hstep_length
  55. 0055specialize zero_add (S (n + g))
  56. 0056exact zero_add
  57. 0057have hzero : BetaAt(b,c,n + g,0)
    Exact native replay linehave hzero : ((exists fs_h_b5cvpsez_zero. fs_h_b5cvpsez_zero + S (0) = S ((S (n + g)) * c)) /\ exists fs_q_b5cvpsez_zero. b = fs_q_b5cvpsez_zero * S ((S (n + g)) * c) + (0))
  58. 0058specialize power_quotient_prefix_tail_entry_zero p
  59. 0059specialize power_quotient_prefix_tail_entry_zero n
  60. 0060specialize power_quotient_prefix_tail_entry_zero b
  61. 0061specialize power_quotient_prefix_tail_entry_zero c
  62. 0062specialize power_quotient_prefix_tail_entry_zero (n + S g)
  63. 0063specialize power_quotient_prefix_tail_entry_zero (n + g)
  64. 0064apply power_quotient_prefix_tail_entry_zero
  65. 0065exact hp
  66. 0066exact hprefix
  67. 0067exact htail_start
  68. 0068exact htail_bound
  69. 0069rewrite hstep_length at hsum
  70. 0070rewrite hstep_length at hsum
  71. 0071rewrite hstep_length at hsum
  72. 0072have hprefix_sum : Sum(b,c,n + g,t)
    Exact native replay linehave hprefix_sum : exists fs_u_b5cvpsez_prefix_sum fs_v_b5cvpsez_prefix_sum. ((((exists fs_h_b5cvpsez_prefix_sum_body_start. fs_h_b5cvpsez_prefix_sum_body_start + S (0) = S ((S (0)) * fs_v_b5cvpsez_prefix_sum)) /\ exists fs_q_b5cvpsez_prefix_sum_body_start. fs_u_b5cvpsez_prefix_sum = fs_q_b5cvpsez_prefix_sum_body_start * S ((S (0)) * fs_v_b5cvpsez_prefix_sum) + (0))) /\ ((((exists fs_h_b5cvpsez_prefix_sum_body_terminal. fs_h_b5cvpsez_prefix_sum_body_terminal + S (t) = S ((S (n + g)) * fs_v_b5cvpsez_prefix_sum)) /\ exists fs_q_b5cvpsez_prefix_sum_body_terminal. fs_u_b5cvpsez_prefix_sum = fs_q_b5cvpsez_prefix_sum_body_terminal * S ((S (n + g)) * fs_v_b5cvpsez_prefix_sum) + (t))) /\ forall fs_i_b5cvpsez_prefix_sum_body_steps. (exists fs_lt_b5cvpsez_prefix_sum_body_steps_bound. fs_lt_b5cvpsez_prefix_sum_body_steps_bound + S fs_i_b5cvpsez_prefix_sum_body_steps = n + g) -> exists fs_a_b5cvpsez_prefix_sum_body_steps fs_r_b5cvpsez_prefix_sum_body_steps fs_s_b5cvpsez_prefix_sum_body_steps. ((((exists fs_h_b5cvpsez_prefix_sum_body_steps_summand. fs_h_b5cvpsez_prefix_sum_body_steps_summand + S (fs_a_b5cvpsez_prefix_sum_body_steps) = S ((S (fs_i_b5cvpsez_prefix_sum_body_steps)) * c)) /\ exists fs_q_b5cvpsez_prefix_sum_body_steps_summand. b = fs_q_b5cvpsez_prefix_sum_body_steps_summand * S ((S (fs_i_b5cvpsez_prefix_sum_body_steps)) * c) + (fs_a_b5cvpsez_prefix_sum_body_steps))) /\ ((((exists fs_h_b5cvpsez_prefix_sum_body_steps_partial. fs_h_b5cvpsez_prefix_sum_body_steps_partial + S (fs_r_b5cvpsez_prefix_sum_body_steps) = S ((S (fs_i_b5cvpsez_prefix_sum_body_steps)) * fs_v_b5cvpsez_prefix_sum)) /\ exists fs_q_b5cvpsez_prefix_sum_body_steps_partial. fs_u_b5cvpsez_prefix_sum = fs_q_b5cvpsez_prefix_sum_body_steps_partial * S ((S (fs_i_b5cvpsez_prefix_sum_body_steps)) * fs_v_b5cvpsez_prefix_sum) + (fs_r_b5cvpsez_prefix_sum_body_steps))) /\ ((((exists fs_h_b5cvpsez_prefix_sum_body_steps_successor. fs_h_b5cvpsez_prefix_sum_body_steps_successor + S (fs_s_b5cvpsez_prefix_sum_body_steps) = S ((S (S fs_i_b5cvpsez_prefix_sum_body_steps)) * fs_v_b5cvpsez_prefix_sum)) /\ exists fs_q_b5cvpsez_prefix_sum_body_steps_successor. fs_u_b5cvpsez_prefix_sum = fs_q_b5cvpsez_prefix_sum_body_steps_successor * S ((S (S fs_i_b5cvpsez_prefix_sum_body_steps)) * fs_v_b5cvpsez_prefix_sum) + (fs_s_b5cvpsez_prefix_sum_body_steps))) /\ fs_s_b5cvpsez_prefix_sum_body_steps = fs_r_b5cvpsez_prefix_sum_body_steps + fs_a_b5cvpsez_prefix_sum_body_steps)))))
  73. 0073specialize beta_sum_succ_last_zero b
  74. 0074specialize beta_sum_succ_last_zero c
  75. 0075specialize beta_sum_succ_last_zero (n + g)
  76. 0076specialize beta_sum_succ_last_zero t
  77. 0077apply beta_sum_succ_last_zero
  78. 0078exact hsum
  79. 0079exact hzero
  80. 0080specialize IH t
  81. 0081specialize IH e
  82. 0082apply IH
  83. 0083exact hp
  84. 0084exact hrestricted
  85. 0085exact hprefix_sum
  86. 0086exact hlegendre