BT00S4 · Bertrand theorem

legendre_sum_zero

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

The finite Legendre sum at zero is 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. n = 0 → LegendreSum(p,n,e) → e = 0

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

PD0050 LegendreSum

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall p n e. n = 0 -> (exists bls_code_bls_zero bls_scale_bls_zero. ((forall bls_index_bls_zero_prefix. (exists bls_gap_bls_zero_prefix_bound. bls_gap_bls_zero_prefix_bound + S (bls_index_bls_zero_prefix) = (n)) -> exists bls_power_bls_zero_prefix bls_quotient_bls_zero_prefix bls_remainder_bls_zero_prefix. ((exists bpvi_b_bls_bls_zero_prefix_power bpvi_c_bls_bls_zero_prefix_power. ((forall bpvi_i_bls_bls_zero_prefix_power. (exists bpvi_repeat_gap_bls_bls_zero_prefix_power. bpvi_repeat_gap_bls_bls_zero_prefix_power + S bpvi_i_bls_bls_zero_prefix_power = S bls_index_bls_zero_prefix) -> (((exists bpvi_h_bls_bls_zero_prefix_power_repeat. bpvi_h_bls_bls_zero_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_zero_prefix_power)) * bpvi_c_bls_bls_zero_prefix_power)) /\ exists bpvi_q_bls_bls_zero_prefix_power_repeat. bpvi_b_bls_bls_zero_prefix_power = bpvi_q_bls_bls_zero_prefix_power_repeat * S ((S (bpvi_i_bls_bls_zero_prefix_power)) * bpvi_c_bls_bls_zero_prefix_power) + (p)))) /\ (exists bpvi_u_bls_bls_zero_prefix_power bpvi_v_bls_bls_zero_prefix_power. ((((exists bpvi_h_bls_bls_zero_prefix_power_start. bpvi_h_bls_bls_zero_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_zero_prefix_power)) /\ exists bpvi_q_bls_bls_zero_prefix_power_start. bpvi_u_bls_bls_zero_prefix_power = bpvi_q_bls_bls_zero_prefix_power_start * S ((S (0)) * bpvi_v_bls_bls_zero_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_bls_zero_prefix_power_terminal. bpvi_h_bls_bls_zero_prefix_power_terminal + S (bls_power_bls_zero_prefix) = S ((S (S bls_index_bls_zero_prefix)) * bpvi_v_bls_bls_zero_prefix_power)) /\ exists bpvi_q_bls_bls_zero_prefix_power_terminal. bpvi_u_bls_bls_zero_prefix_power = bpvi_q_bls_bls_zero_prefix_power_terminal * S ((S (S bls_index_bls_zero_prefix)) * bpvi_v_bls_bls_zero_prefix_power) + (bls_power_bls_zero_prefix))) /\ forall bpvi_j_bls_bls_zero_prefix_power. (exists bpvi_product_gap_bls_bls_zero_prefix_power. bpvi_product_gap_bls_bls_zero_prefix_power + S bpvi_j_bls_bls_zero_prefix_power = S bls_index_bls_zero_prefix) -> exists bpvi_factor_bls_bls_zero_prefix_power bpvi_partial_bls_bls_zero_prefix_power bpvi_successor_bls_bls_zero_prefix_power. ((((exists bpvi_h_bls_bls_zero_prefix_power_factor. bpvi_h_bls_bls_zero_prefix_power_factor + S (bpvi_factor_bls_bls_zero_prefix_power) = S ((S (bpvi_j_bls_bls_zero_prefix_power)) * bpvi_c_bls_bls_zero_prefix_power)) /\ exists bpvi_q_bls_bls_zero_prefix_power_factor. bpvi_b_bls_bls_zero_prefix_power = bpvi_q_bls_bls_zero_prefix_power_factor * S ((S (bpvi_j_bls_bls_zero_prefix_power)) * bpvi_c_bls_bls_zero_prefix_power) + (bpvi_factor_bls_bls_zero_prefix_power))) /\ ((((exists bpvi_h_bls_bls_zero_prefix_power_partial. bpvi_h_bls_bls_zero_prefix_power_partial + S (bpvi_partial_bls_bls_zero_prefix_power) = S ((S (bpvi_j_bls_bls_zero_prefix_power)) * bpvi_v_bls_bls_zero_prefix_power)) /\ exists bpvi_q_bls_bls_zero_prefix_power_partial. bpvi_u_bls_bls_zero_prefix_power = bpvi_q_bls_bls_zero_prefix_power_partial * S ((S (bpvi_j_bls_bls_zero_prefix_power)) * bpvi_v_bls_bls_zero_prefix_power) + (bpvi_partial_bls_bls_zero_prefix_power))) /\ ((((exists bpvi_h_bls_bls_zero_prefix_power_successor. bpvi_h_bls_bls_zero_prefix_power_successor + S (bpvi_successor_bls_bls_zero_prefix_power) = S ((S (S bpvi_j_bls_bls_zero_prefix_power)) * bpvi_v_bls_bls_zero_prefix_power)) /\ exists bpvi_q_bls_bls_zero_prefix_power_successor. bpvi_u_bls_bls_zero_prefix_power = bpvi_q_bls_bls_zero_prefix_power_successor * S ((S (S bpvi_j_bls_bls_zero_prefix_power)) * bpvi_v_bls_bls_zero_prefix_power) + (bpvi_successor_bls_bls_zero_prefix_power))) /\ bpvi_successor_bls_bls_zero_prefix_power = bpvi_partial_bls_bls_zero_prefix_power * bpvi_factor_bls_bls_zero_prefix_power)))))))) /\ ((((exists ff_h_bls_bls_zero_prefix_quotient_entry. ff_h_bls_bls_zero_prefix_quotient_entry + S (bls_quotient_bls_zero_prefix) = S ((S (bls_index_bls_zero_prefix)) * bls_scale_bls_zero)) /\ exists ff_q_bls_bls_zero_prefix_quotient_entry. bls_code_bls_zero = ff_q_bls_bls_zero_prefix_quotient_entry * S ((S (bls_index_bls_zero_prefix)) * bls_scale_bls_zero) + (bls_quotient_bls_zero_prefix))) /\ ((n = bls_power_bls_zero_prefix * bls_quotient_bls_zero_prefix + bls_remainder_bls_zero_prefix /\ exists bls_remainder_gap_bls_zero_prefix_division. bls_remainder_gap_bls_zero_prefix_division + S (bls_remainder_bls_zero_prefix) = bls_power_bls_zero_prefix))))) /\ (exists ff_u_bls_bls_zero_sum ff_v_bls_bls_zero_sum. ((((exists ff_h_bls_bls_zero_sum_start. ff_h_bls_bls_zero_sum_start + S (0) = S ((S (0)) * ff_v_bls_bls_zero_sum)) /\ exists ff_q_bls_bls_zero_sum_start. ff_u_bls_bls_zero_sum = ff_q_bls_bls_zero_sum_start * S ((S (0)) * ff_v_bls_bls_zero_sum) + (0))) /\ ((((exists ff_h_bls_bls_zero_sum_terminal. ff_h_bls_bls_zero_sum_terminal + S (e) = S ((S (n)) * ff_v_bls_bls_zero_sum)) /\ exists ff_q_bls_bls_zero_sum_terminal. ff_u_bls_bls_zero_sum = ff_q_bls_bls_zero_sum_terminal * S ((S (n)) * ff_v_bls_bls_zero_sum) + (e))) /\ forall ff_i_bls_bls_zero_sum. (exists ff_lt_bls_bls_zero_sum_bound. ff_lt_bls_bls_zero_sum_bound + S ff_i_bls_bls_zero_sum = n) -> exists ff_a_bls_bls_zero_sum ff_r_bls_bls_zero_sum ff_s_bls_bls_zero_sum. ((((exists ff_h_bls_bls_zero_sum_summand. ff_h_bls_bls_zero_sum_summand + S (ff_a_bls_bls_zero_sum) = S ((S (ff_i_bls_bls_zero_sum)) * bls_scale_bls_zero)) /\ exists ff_q_bls_bls_zero_sum_summand. bls_code_bls_zero = ff_q_bls_bls_zero_sum_summand * S ((S (ff_i_bls_bls_zero_sum)) * bls_scale_bls_zero) + (ff_a_bls_bls_zero_sum))) /\ ((((exists ff_h_bls_bls_zero_sum_partial. ff_h_bls_bls_zero_sum_partial + S (ff_r_bls_bls_zero_sum) = S ((S (ff_i_bls_bls_zero_sum)) * ff_v_bls_bls_zero_sum)) /\ exists ff_q_bls_bls_zero_sum_partial. ff_u_bls_bls_zero_sum = ff_q_bls_bls_zero_sum_partial * S ((S (ff_i_bls_bls_zero_sum)) * ff_v_bls_bls_zero_sum) + (ff_r_bls_bls_zero_sum))) /\ ((((exists ff_h_bls_bls_zero_sum_successor. ff_h_bls_bls_zero_sum_successor + S (ff_s_bls_bls_zero_sum) = S ((S (S ff_i_bls_bls_zero_sum)) * ff_v_bls_bls_zero_sum)) /\ exists ff_q_bls_bls_zero_sum_successor. ff_u_bls_bls_zero_sum = ff_q_bls_bls_zero_sum_successor * S ((S (S ff_i_bls_bls_zero_sum)) * ff_v_bls_bls_zero_sum) + (ff_s_bls_bls_zero_sum))) /\ ff_s_bls_bls_zero_sum = ff_r_bls_bls_zero_sum + ff_a_bls_bls_zero_sum)))))))) -> e = 0

Proof neighborhood

Direct theorem prerequisites

BT008E beta_sum_zero

Direct theorem dependents

BT00T1 prime_factorial_valuation_eq_legendre_sum

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

16 script commands · 5 reading checkpoints · 0 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 (1)
beta sum zero
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 hn
  5. L5
    intro hsum
02Separate the logical casesL6–8

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

  1. L6
    cases hsum
  2. L7
    cases hsum_witness
  3. L8
    cases hsum_witness_witness
03Use earlier factsL9–12

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

  1. L9
    specialize beta_sum_zero x
  2. L10
    specialize beta_sum_zero x1
  3. L11
    specialize beta_sum_zero e
  4. L12
    apply beta_sum_zero
04Calculate and transport equalitiesL13–15

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

  1. L13
    rewrite hn at hsum_witness_witness_right
  2. L14
    rewrite hn at hsum_witness_witness_right
  3. L15
    rewrite hn at hsum_witness_witness_right
05Use earlier factsL16–16

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

  1. L16
    exact hsum_witness_witness_right

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro e
  4. 0004intro hn
  5. 0005intro hsum
  6. 0006cases hsum
  7. 0007cases hsum_witness
  8. 0008cases hsum_witness_witness
  9. 0009specialize beta_sum_zero x
  10. 0010specialize beta_sum_zero x1
  11. 0011specialize beta_sum_zero e
  12. 0012apply beta_sum_zero
  13. 0013rewrite hn at hsum_witness_witness_right
  14. 0014rewrite hn at hsum_witness_witness_right
  15. 0015rewrite hn at hsum_witness_witness_right
  16. 0016exact hsum_witness_witness_right