BT00SS · Bertrand theorem

prime_power_quotient_prefix_last_zero

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

The final entry of a length-(n+1) old quotient prefix 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. ∀ b. ∀ c. Prime(p) → PowerQuotPrefix(p,n,b,c,S n) → BetaAt(b,c,n,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

PD0004 Prime PD0013 BetaAt PD0049 PowerQuotPrefix

3 occurrences

In local proof propositions

PD0007 DivRem PD0013 BetaAt PD0020 Pow

4 occurrences

Exact expanded native-PA statement
forall p n b c. ((~(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)) -> (forall bls_index_blrr_tail_prefix. (exists bls_gap_blrr_tail_prefix_bound. bls_gap_blrr_tail_prefix_bound + S (bls_index_blrr_tail_prefix) = (S n)) -> exists bls_power_blrr_tail_prefix bls_quotient_blrr_tail_prefix bls_remainder_blrr_tail_prefix. ((exists bpvi_b_bls_blrr_tail_prefix_power bpvi_c_bls_blrr_tail_prefix_power. ((forall bpvi_i_bls_blrr_tail_prefix_power. (exists bpvi_repeat_gap_bls_blrr_tail_prefix_power. bpvi_repeat_gap_bls_blrr_tail_prefix_power + S bpvi_i_bls_blrr_tail_prefix_power = S bls_index_blrr_tail_prefix) -> (((exists bpvi_h_bls_blrr_tail_prefix_power_repeat. bpvi_h_bls_blrr_tail_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_blrr_tail_prefix_power)) * bpvi_c_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_repeat. bpvi_b_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_repeat * S ((S (bpvi_i_bls_blrr_tail_prefix_power)) * bpvi_c_bls_blrr_tail_prefix_power) + (p)))) /\ (exists bpvi_u_bls_blrr_tail_prefix_power bpvi_v_bls_blrr_tail_prefix_power. ((((exists bpvi_h_bls_blrr_tail_prefix_power_start. bpvi_h_bls_blrr_tail_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_start. bpvi_u_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_start * S ((S (0)) * bpvi_v_bls_blrr_tail_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_blrr_tail_prefix_power_terminal. bpvi_h_bls_blrr_tail_prefix_power_terminal + S (bls_power_blrr_tail_prefix) = S ((S (S bls_index_blrr_tail_prefix)) * bpvi_v_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_terminal. bpvi_u_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_terminal * S ((S (S bls_index_blrr_tail_prefix)) * bpvi_v_bls_blrr_tail_prefix_power) + (bls_power_blrr_tail_prefix))) /\ forall bpvi_j_bls_blrr_tail_prefix_power. (exists bpvi_product_gap_bls_blrr_tail_prefix_power. bpvi_product_gap_bls_blrr_tail_prefix_power + S bpvi_j_bls_blrr_tail_prefix_power = S bls_index_blrr_tail_prefix) -> exists bpvi_factor_bls_blrr_tail_prefix_power bpvi_partial_bls_blrr_tail_prefix_power bpvi_successor_bls_blrr_tail_prefix_power. ((((exists bpvi_h_bls_blrr_tail_prefix_power_factor. bpvi_h_bls_blrr_tail_prefix_power_factor + S (bpvi_factor_bls_blrr_tail_prefix_power) = S ((S (bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_c_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_factor. bpvi_b_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_factor * S ((S (bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_c_bls_blrr_tail_prefix_power) + (bpvi_factor_bls_blrr_tail_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_tail_prefix_power_partial. bpvi_h_bls_blrr_tail_prefix_power_partial + S (bpvi_partial_bls_blrr_tail_prefix_power) = S ((S (bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_v_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_partial. bpvi_u_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_partial * S ((S (bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_v_bls_blrr_tail_prefix_power) + (bpvi_partial_bls_blrr_tail_prefix_power))) /\ ((((exists bpvi_h_bls_blrr_tail_prefix_power_successor. bpvi_h_bls_blrr_tail_prefix_power_successor + S (bpvi_successor_bls_blrr_tail_prefix_power) = S ((S (S bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_v_bls_blrr_tail_prefix_power)) /\ exists bpvi_q_bls_blrr_tail_prefix_power_successor. bpvi_u_bls_blrr_tail_prefix_power = bpvi_q_bls_blrr_tail_prefix_power_successor * S ((S (S bpvi_j_bls_blrr_tail_prefix_power)) * bpvi_v_bls_blrr_tail_prefix_power) + (bpvi_successor_bls_blrr_tail_prefix_power))) /\ bpvi_successor_bls_blrr_tail_prefix_power = bpvi_partial_bls_blrr_tail_prefix_power * bpvi_factor_bls_blrr_tail_prefix_power)))))))) /\ ((((exists ff_h_bls_blrr_tail_prefix_quotient_entry. ff_h_bls_blrr_tail_prefix_quotient_entry + S (bls_quotient_blrr_tail_prefix) = S ((S (bls_index_blrr_tail_prefix)) * c)) /\ exists ff_q_bls_blrr_tail_prefix_quotient_entry. b = ff_q_bls_blrr_tail_prefix_quotient_entry * S ((S (bls_index_blrr_tail_prefix)) * c) + (bls_quotient_blrr_tail_prefix))) /\ ((n = bls_power_blrr_tail_prefix * bls_quotient_blrr_tail_prefix + bls_remainder_blrr_tail_prefix /\ exists bls_remainder_gap_blrr_tail_prefix_division. bls_remainder_gap_blrr_tail_prefix_division + S (bls_remainder_blrr_tail_prefix) = bls_power_blrr_tail_prefix))))) -> (((exists fs_h_blrr_tail_zero. fs_h_blrr_tail_zero + S (0) = S ((S (n)) * c)) /\ exists fs_q_blrr_tail_zero. b = fs_q_blrr_tail_zero * S ((S (n)) * c) + (0)))

Proof neighborhood

Direct theorem prerequisites

BT00SA prime_power_quotient_tail_zero BT001U division_remainder_unique BT0000 zero_add

Direct theorem dependents

BT00ST legendre_sum_zero_extended_prefix

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

42 script commands · 12 reading checkpoints · 3 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 (3)
prime power quotient tail zerodivision remainder uniquezero add
01Fix variables and assumptionsL1–6

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
  5. L5
    intro hp
  6. L6
    intro hprefix
02Establish hdataL7–9

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

  1. L7
    have hdata : ∃ D. ∃ q. ∃ r. Pow(p,S n,D) ∧ (BetaAt(b,c,n,q) ∧ DivRem(n,D,q,r))Definitions: Pow(p,S n,D)BetaAt(b,c,n,q)DivRem(n,D,q,r)Original native command in the exact edition
  2. L8
    specialize hprefix n
  3. L9
    apply hprefix
03Construct an explicit witnessL10–10

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

  1. L10
    exists 0
04Use earlier factsL11–12

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

  1. L11
    specialize zero_add (S n)
  2. L12
    exact zero_add
05Separate the logical casesL13–18

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

  1. L13
    cases hdata
  2. L14
    cases hdata_witness
  3. L15
    cases hdata_witness_witness
  4. L16
    cases hdata_witness_witness_witness
  5. L17
    cases hdata_witness_witness_witness_right
  6. L18
    cases hdata_witness_witness_witness_right_right
06Establish htailL19–25

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

  1. L19
    have htail : DivRem(n,x,0,n)Definitions: DivRem(n,x,0,n)Original native command in the exact edition
  2. L20
    specialize prime_power_quotient_tail_zero p
  3. L21
    specialize prime_power_quotient_tail_zero n
  4. L22
    specialize prime_power_quotient_tail_zero x
  5. L23
    apply prime_power_quotient_tail_zero
  6. L24
    exact hp
  7. L25
    exact hdata_witness_witness_witness_left
07Separate the logical casesL26–26

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

  1. L26
    cases htail
08Establish huniqueL27–36

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

  1. L27
    have hunique : x1 = 0 /\ x2 = n
  2. L28
    specialize division_remainder_unique x
  3. L29
    specialize division_remainder_unique n
  4. L30
    specialize division_remainder_unique x1
  5. L31
    specialize division_remainder_unique x2
  6. L32
    specialize division_remainder_unique 0
  7. L33
    specialize division_remainder_unique n
  8. L34
    apply division_remainder_unique
  9. L35
    exact hdata_witness_witness_witness_right_right_left
  10. L36
    exact hdata_witness_witness_witness_right_right_right
09Use earlier factsL37–38

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

  1. L37
    exact htail_left
  2. L38
    exact htail_right
10Separate the logical casesL39–39

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

  1. L39
    cases hunique
11Calculate and transport equalitiesL40–41

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

  1. L40
    rewrite <- hunique_left
  2. L41
    rewrite <- hunique_left
12Use earlier factsL42–42

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

  1. L42
    exact hdata_witness_witness_witness_right_left

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hp
  6. 0006intro hprefix
  7. 0007have hdata : ∃ D. ∃ q. ∃ r. Pow(p,S n,D) ∧ (BetaAt(b,c,n,q) ∧ DivRem(n,D,q,r))
    Exact native replay linehave hdata : exists D q r. ((exists bpvi_b_blrr_tail_stored_power bpvi_c_blrr_tail_stored_power. ((forall bpvi_i_blrr_tail_stored_power. (exists bpvi_repeat_gap_blrr_tail_stored_power. bpvi_repeat_gap_blrr_tail_stored_power + S bpvi_i_blrr_tail_stored_power = S n) -> (((exists bpvi_h_blrr_tail_stored_power_repeat. bpvi_h_blrr_tail_stored_power_repeat + S (p) = S ((S (bpvi_i_blrr_tail_stored_power)) * bpvi_c_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_repeat. bpvi_b_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_repeat * S ((S (bpvi_i_blrr_tail_stored_power)) * bpvi_c_blrr_tail_stored_power) + (p)))) /\ (exists bpvi_u_blrr_tail_stored_power bpvi_v_blrr_tail_stored_power. ((((exists bpvi_h_blrr_tail_stored_power_start. bpvi_h_blrr_tail_stored_power_start + S (1) = S ((S (0)) * bpvi_v_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_start. bpvi_u_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_start * S ((S (0)) * bpvi_v_blrr_tail_stored_power) + (1))) /\ ((((exists bpvi_h_blrr_tail_stored_power_terminal. bpvi_h_blrr_tail_stored_power_terminal + S (D) = S ((S (S n)) * bpvi_v_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_terminal. bpvi_u_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_terminal * S ((S (S n)) * bpvi_v_blrr_tail_stored_power) + (D))) /\ forall bpvi_j_blrr_tail_stored_power. (exists bpvi_product_gap_blrr_tail_stored_power. bpvi_product_gap_blrr_tail_stored_power + S bpvi_j_blrr_tail_stored_power = S n) -> exists bpvi_factor_blrr_tail_stored_power bpvi_partial_blrr_tail_stored_power bpvi_successor_blrr_tail_stored_power. ((((exists bpvi_h_blrr_tail_stored_power_factor. bpvi_h_blrr_tail_stored_power_factor + S (bpvi_factor_blrr_tail_stored_power) = S ((S (bpvi_j_blrr_tail_stored_power)) * bpvi_c_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_factor. bpvi_b_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_factor * S ((S (bpvi_j_blrr_tail_stored_power)) * bpvi_c_blrr_tail_stored_power) + (bpvi_factor_blrr_tail_stored_power))) /\ ((((exists bpvi_h_blrr_tail_stored_power_partial. bpvi_h_blrr_tail_stored_power_partial + S (bpvi_partial_blrr_tail_stored_power) = S ((S (bpvi_j_blrr_tail_stored_power)) * bpvi_v_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_partial. bpvi_u_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_partial * S ((S (bpvi_j_blrr_tail_stored_power)) * bpvi_v_blrr_tail_stored_power) + (bpvi_partial_blrr_tail_stored_power))) /\ ((((exists bpvi_h_blrr_tail_stored_power_successor. bpvi_h_blrr_tail_stored_power_successor + S (bpvi_successor_blrr_tail_stored_power) = S ((S (S bpvi_j_blrr_tail_stored_power)) * bpvi_v_blrr_tail_stored_power)) /\ exists bpvi_q_blrr_tail_stored_power_successor. bpvi_u_blrr_tail_stored_power = bpvi_q_blrr_tail_stored_power_successor * S ((S (S bpvi_j_blrr_tail_stored_power)) * bpvi_v_blrr_tail_stored_power) + (bpvi_successor_blrr_tail_stored_power))) /\ bpvi_successor_blrr_tail_stored_power = bpvi_partial_blrr_tail_stored_power * bpvi_factor_blrr_tail_stored_power)))))))) /\ ((((exists ff_h_blrr_tail_stored_entry. ff_h_blrr_tail_stored_entry + S (q) = S ((S (n)) * c)) /\ exists ff_q_blrr_tail_stored_entry. b = ff_q_blrr_tail_stored_entry * S ((S (n)) * c) + (q))) /\ ((n = D * q + r /\ exists gap. gap + S r = D))))
  8. 0008specialize hprefix n
  9. 0009apply hprefix
  10. 0010exists 0
  11. 0011specialize zero_add (S n)
  12. 0012exact zero_add
  13. 0013cases hdata
  14. 0014cases hdata_witness
  15. 0015cases hdata_witness_witness
  16. 0016cases hdata_witness_witness_witness
  17. 0017cases hdata_witness_witness_witness_right
  18. 0018cases hdata_witness_witness_witness_right_right
  19. 0019have htail : DivRem(n,x,0,n)
    Exact native replay linehave htail : ((n = x * 0 + n /\ exists gap. gap + S n = x))
  20. 0020specialize prime_power_quotient_tail_zero p
  21. 0021specialize prime_power_quotient_tail_zero n
  22. 0022specialize prime_power_quotient_tail_zero x
  23. 0023apply prime_power_quotient_tail_zero
  24. 0024exact hp
  25. 0025exact hdata_witness_witness_witness_left
  26. 0026cases htail
  27. 0027have hunique : x1 = 0 /\ x2 = n
  28. 0028specialize division_remainder_unique x
  29. 0029specialize division_remainder_unique n
  30. 0030specialize division_remainder_unique x1
  31. 0031specialize division_remainder_unique x2
  32. 0032specialize division_remainder_unique 0
  33. 0033specialize division_remainder_unique n
  34. 0034apply division_remainder_unique
  35. 0035exact hdata_witness_witness_witness_right_right_left
  36. 0036exact hdata_witness_witness_witness_right_right_right
  37. 0037exact htail_left
  38. 0038exact htail_right
  39. 0039cases hunique
  40. 0040rewrite <- hunique_left
  41. 0041rewrite <- hunique_left
  42. 0042exact hdata_witness_witness_witness_right_left