BT00XP · Bertrand theorem

power_quotient_prefix_tail_entry_zero

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

Every decoded quotient entry at or beyond the dividend 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. ∀ l. ∀ i. Prime(p) → PowerQuotPrefix(p,n,b,c,l) → Le(n,i) → Lt(i,l) → BetaAt(b,c,i,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

PD0001 Le PD0002 Lt PD0004 Prime PD0013 BetaAt PD0049 PowerQuotPrefix

5 occurrences

In local proof propositions

PD0002 Lt PD0007 DivRem PD0013 BetaAt PD0020 Pow

4 occurrences

Exact expanded native-PA statement
forall p n b c l i. ((~(p = 1) /\ forall frm_prime_left_b5cvptez_prime frm_prime_right_b5cvptez_prime. p = frm_prime_left_b5cvptez_prime * frm_prime_right_b5cvptez_prime -> frm_prime_left_b5cvptez_prime = 1 \/ frm_prime_right_b5cvptez_prime = 1)) -> (forall bls_index_b5cvptez_prefix. (exists bls_gap_b5cvptez_prefix_bound. bls_gap_b5cvptez_prefix_bound + S (bls_index_b5cvptez_prefix) = (l)) -> exists bls_power_b5cvptez_prefix bls_quotient_b5cvptez_prefix bls_remainder_b5cvptez_prefix. ((exists bpvi_b_bls_b5cvptez_prefix_power bpvi_c_bls_b5cvptez_prefix_power. ((forall bpvi_i_bls_b5cvptez_prefix_power. (exists bpvi_repeat_gap_bls_b5cvptez_prefix_power. bpvi_repeat_gap_bls_b5cvptez_prefix_power + S bpvi_i_bls_b5cvptez_prefix_power = S bls_index_b5cvptez_prefix) -> (((exists bpvi_h_bls_b5cvptez_prefix_power_repeat. bpvi_h_bls_b5cvptez_prefix_power_repeat + S (p) = S ((S (bpvi_i_bls_b5cvptez_prefix_power)) * bpvi_c_bls_b5cvptez_prefix_power)) /\ exists bpvi_q_bls_b5cvptez_prefix_power_repeat. bpvi_b_bls_b5cvptez_prefix_power = bpvi_q_bls_b5cvptez_prefix_power_repeat * S ((S (bpvi_i_bls_b5cvptez_prefix_power)) * bpvi_c_bls_b5cvptez_prefix_power) + (p)))) /\ (exists bpvi_u_bls_b5cvptez_prefix_power bpvi_v_bls_b5cvptez_prefix_power. ((((exists bpvi_h_bls_b5cvptez_prefix_power_start. bpvi_h_bls_b5cvptez_prefix_power_start + S (1) = S ((S (0)) * bpvi_v_bls_b5cvptez_prefix_power)) /\ exists bpvi_q_bls_b5cvptez_prefix_power_start. bpvi_u_bls_b5cvptez_prefix_power = bpvi_q_bls_b5cvptez_prefix_power_start * S ((S (0)) * bpvi_v_bls_b5cvptez_prefix_power) + (1))) /\ ((((exists bpvi_h_bls_b5cvptez_prefix_power_terminal. bpvi_h_bls_b5cvptez_prefix_power_terminal + S (bls_power_b5cvptez_prefix) = S ((S (S bls_index_b5cvptez_prefix)) * bpvi_v_bls_b5cvptez_prefix_power)) /\ exists bpvi_q_bls_b5cvptez_prefix_power_terminal. bpvi_u_bls_b5cvptez_prefix_power = bpvi_q_bls_b5cvptez_prefix_power_terminal * S ((S (S bls_index_b5cvptez_prefix)) * bpvi_v_bls_b5cvptez_prefix_power) + (bls_power_b5cvptez_prefix))) /\ forall bpvi_j_bls_b5cvptez_prefix_power. (exists bpvi_product_gap_bls_b5cvptez_prefix_power. bpvi_product_gap_bls_b5cvptez_prefix_power + S bpvi_j_bls_b5cvptez_prefix_power = S bls_index_b5cvptez_prefix) -> exists bpvi_factor_bls_b5cvptez_prefix_power bpvi_partial_bls_b5cvptez_prefix_power bpvi_successor_bls_b5cvptez_prefix_power. ((((exists bpvi_h_bls_b5cvptez_prefix_power_factor. bpvi_h_bls_b5cvptez_prefix_power_factor + S (bpvi_factor_bls_b5cvptez_prefix_power) = S ((S (bpvi_j_bls_b5cvptez_prefix_power)) * bpvi_c_bls_b5cvptez_prefix_power)) /\ exists bpvi_q_bls_b5cvptez_prefix_power_factor. bpvi_b_bls_b5cvptez_prefix_power = bpvi_q_bls_b5cvptez_prefix_power_factor * S ((S (bpvi_j_bls_b5cvptez_prefix_power)) * bpvi_c_bls_b5cvptez_prefix_power) + (bpvi_factor_bls_b5cvptez_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvptez_prefix_power_partial. bpvi_h_bls_b5cvptez_prefix_power_partial + S (bpvi_partial_bls_b5cvptez_prefix_power) = S ((S (bpvi_j_bls_b5cvptez_prefix_power)) * bpvi_v_bls_b5cvptez_prefix_power)) /\ exists bpvi_q_bls_b5cvptez_prefix_power_partial. bpvi_u_bls_b5cvptez_prefix_power = bpvi_q_bls_b5cvptez_prefix_power_partial * S ((S (bpvi_j_bls_b5cvptez_prefix_power)) * bpvi_v_bls_b5cvptez_prefix_power) + (bpvi_partial_bls_b5cvptez_prefix_power))) /\ ((((exists bpvi_h_bls_b5cvptez_prefix_power_successor. bpvi_h_bls_b5cvptez_prefix_power_successor + S (bpvi_successor_bls_b5cvptez_prefix_power) = S ((S (S bpvi_j_bls_b5cvptez_prefix_power)) * bpvi_v_bls_b5cvptez_prefix_power)) /\ exists bpvi_q_bls_b5cvptez_prefix_power_successor. bpvi_u_bls_b5cvptez_prefix_power = bpvi_q_bls_b5cvptez_prefix_power_successor * S ((S (S bpvi_j_bls_b5cvptez_prefix_power)) * bpvi_v_bls_b5cvptez_prefix_power) + (bpvi_successor_bls_b5cvptez_prefix_power))) /\ bpvi_successor_bls_b5cvptez_prefix_power = bpvi_partial_bls_b5cvptez_prefix_power * bpvi_factor_bls_b5cvptez_prefix_power)))))))) /\ ((((exists ff_h_bls_b5cvptez_prefix_quotient_entry. ff_h_bls_b5cvptez_prefix_quotient_entry + S (bls_quotient_b5cvptez_prefix) = S ((S (bls_index_b5cvptez_prefix)) * c)) /\ exists ff_q_bls_b5cvptez_prefix_quotient_entry. b = ff_q_bls_b5cvptez_prefix_quotient_entry * S ((S (bls_index_b5cvptez_prefix)) * c) + (bls_quotient_b5cvptez_prefix))) /\ ((n = bls_power_b5cvptez_prefix * bls_quotient_b5cvptez_prefix + bls_remainder_b5cvptez_prefix /\ exists bls_remainder_gap_b5cvptez_prefix_division. bls_remainder_gap_b5cvptez_prefix_division + S (bls_remainder_b5cvptez_prefix) = bls_power_b5cvptez_prefix))))) -> (exists bcf_le_gap_b5cvptez_start. bcf_le_gap_b5cvptez_start + (n) = i) -> (exists bcf_lt_gap_b5cvptez_bound. bcf_lt_gap_b5cvptez_bound + S (i) = l) -> (((exists fs_h_b5cvptez_result. fs_h_b5cvptez_result + S (0) = S ((S (i)) * c)) /\ exists fs_q_b5cvptez_result. b = fs_q_b5cvptez_result * S ((S (i)) * c) + (0)))

Proof neighborhood

Direct theorem prerequisites

BT00XO prime_power_quotient_zero_of_exponent_gt

Direct theorem dependents

BT00XQ power_quotient_prefix_sum_extend_zero

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

40 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 (1)
prime power quotient zero of exponent gt
01Fix variables and assumptionsL1–10

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 l
  6. L6
    intro i
  7. L7
    intro hp
  8. L8
    intro hprefix
  9. L9
    intro hstart
  10. L10
    intro hibound
02Establish hdataL11–14

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

  1. L11
    have hdata : ∃ d. ∃ q. ∃ r. Pow(p,S i,d) ∧ (BetaAt(b,c,i,q) ∧ DivRem(n,d,q,r))Definitions: Pow(p,S i,d)BetaAt(b,c,i,q)DivRem(n,d,q,r)Original native command in the exact edition
  2. L12
    specialize hprefix i
  3. L13
    apply hprefix
  4. L14
    exact hibound
03Separate the logical casesL15–19

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

  1. L15
    cases hdata
  2. L16
    cases hdata_witness
  3. L17
    cases hdata_witness_witness
  4. L18
    cases hdata_witness_witness_witness
  5. L19
    cases hdata_witness_witness_witness_right
04Establish hexponentL20–20

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

  1. L20
    have hexponent : Lt(n,S i)Definitions: Lt(n,S i)Original native command in the exact edition
05Separate the logical casesL21–21

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

  1. L21
    cases hstart
06Construct an explicit witnessL22–22

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

  1. L22
    exists x3
07Calculate and transport equalitiesL23–24

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

  1. L23
    rewrite PA4
  2. L24
    congr
08Use earlier factsL25–25

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

  1. L25
    exact hstart_witness
09Establish hzeroL26–35

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

  1. L26
    have hzero : x1 = 0
  2. L27
    specialize prime_power_quotient_zero_of_exponent_gt p
  3. L28
    specialize prime_power_quotient_zero_of_exponent_gt n
  4. L29
    specialize prime_power_quotient_zero_of_exponent_gt (S i)
  5. L30
    specialize prime_power_quotient_zero_of_exponent_gt x
  6. L31
    specialize prime_power_quotient_zero_of_exponent_gt x1
  7. L32
    specialize prime_power_quotient_zero_of_exponent_gt x2
  8. L33
    apply prime_power_quotient_zero_of_exponent_gt
  9. L34
    exact hp
  10. L35
    exact hexponent
10Use earlier factsL36–37

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

  1. L36
    exact hdata_witness_witness_witness_left
  2. L37
    exact hdata_witness_witness_witness_right_right
11Calculate and transport equalitiesL38–39

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

  1. L38
    rewrite <- hzero
  2. L39
    rewrite <- hzero
12Use earlier factsL40–40

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

  1. L40
    exact hdata_witness_witness_witness_right_left

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro i
  7. 0007intro hp
  8. 0008intro hprefix
  9. 0009intro hstart
  10. 0010intro hibound
  11. 0011have hdata : ∃ d. ∃ q. ∃ r. Pow(p,S i,d) ∧ (BetaAt(b,c,i,q) ∧ DivRem(n,d,q,r))
    Exact native replay linehave hdata : exists d q r. (exists bpvi_b_b5cvptez_data_power bpvi_c_b5cvptez_data_power. ((forall bpvi_i_b5cvptez_data_power. (exists bpvi_repeat_gap_b5cvptez_data_power. bpvi_repeat_gap_b5cvptez_data_power + S bpvi_i_b5cvptez_data_power = S i) -> (((exists bpvi_h_b5cvptez_data_power_repeat. bpvi_h_b5cvptez_data_power_repeat + S (p) = S ((S (bpvi_i_b5cvptez_data_power)) * bpvi_c_b5cvptez_data_power)) /\ exists bpvi_q_b5cvptez_data_power_repeat. bpvi_b_b5cvptez_data_power = bpvi_q_b5cvptez_data_power_repeat * S ((S (bpvi_i_b5cvptez_data_power)) * bpvi_c_b5cvptez_data_power) + (p)))) /\ (exists bpvi_u_b5cvptez_data_power bpvi_v_b5cvptez_data_power. ((((exists bpvi_h_b5cvptez_data_power_start. bpvi_h_b5cvptez_data_power_start + S (1) = S ((S (0)) * bpvi_v_b5cvptez_data_power)) /\ exists bpvi_q_b5cvptez_data_power_start. bpvi_u_b5cvptez_data_power = bpvi_q_b5cvptez_data_power_start * S ((S (0)) * bpvi_v_b5cvptez_data_power) + (1))) /\ ((((exists bpvi_h_b5cvptez_data_power_terminal. bpvi_h_b5cvptez_data_power_terminal + S (d) = S ((S (S i)) * bpvi_v_b5cvptez_data_power)) /\ exists bpvi_q_b5cvptez_data_power_terminal. bpvi_u_b5cvptez_data_power = bpvi_q_b5cvptez_data_power_terminal * S ((S (S i)) * bpvi_v_b5cvptez_data_power) + (d))) /\ forall bpvi_j_b5cvptez_data_power. (exists bpvi_product_gap_b5cvptez_data_power. bpvi_product_gap_b5cvptez_data_power + S bpvi_j_b5cvptez_data_power = S i) -> exists bpvi_factor_b5cvptez_data_power bpvi_partial_b5cvptez_data_power bpvi_successor_b5cvptez_data_power. ((((exists bpvi_h_b5cvptez_data_power_factor. bpvi_h_b5cvptez_data_power_factor + S (bpvi_factor_b5cvptez_data_power) = S ((S (bpvi_j_b5cvptez_data_power)) * bpvi_c_b5cvptez_data_power)) /\ exists bpvi_q_b5cvptez_data_power_factor. bpvi_b_b5cvptez_data_power = bpvi_q_b5cvptez_data_power_factor * S ((S (bpvi_j_b5cvptez_data_power)) * bpvi_c_b5cvptez_data_power) + (bpvi_factor_b5cvptez_data_power))) /\ ((((exists bpvi_h_b5cvptez_data_power_partial. bpvi_h_b5cvptez_data_power_partial + S (bpvi_partial_b5cvptez_data_power) = S ((S (bpvi_j_b5cvptez_data_power)) * bpvi_v_b5cvptez_data_power)) /\ exists bpvi_q_b5cvptez_data_power_partial. bpvi_u_b5cvptez_data_power = bpvi_q_b5cvptez_data_power_partial * S ((S (bpvi_j_b5cvptez_data_power)) * bpvi_v_b5cvptez_data_power) + (bpvi_partial_b5cvptez_data_power))) /\ ((((exists bpvi_h_b5cvptez_data_power_successor. bpvi_h_b5cvptez_data_power_successor + S (bpvi_successor_b5cvptez_data_power) = S ((S (S bpvi_j_b5cvptez_data_power)) * bpvi_v_b5cvptez_data_power)) /\ exists bpvi_q_b5cvptez_data_power_successor. bpvi_u_b5cvptez_data_power = bpvi_q_b5cvptez_data_power_successor * S ((S (S bpvi_j_b5cvptez_data_power)) * bpvi_v_b5cvptez_data_power) + (bpvi_successor_b5cvptez_data_power))) /\ bpvi_successor_b5cvptez_data_power = bpvi_partial_b5cvptez_data_power * bpvi_factor_b5cvptez_data_power)))))))) /\ ((((exists fs_h_b5cvptez_data_entry. fs_h_b5cvptez_data_entry + S (q) = S ((S (i)) * c)) /\ exists fs_q_b5cvptez_data_entry. b = fs_q_b5cvptez_data_entry * S ((S (i)) * c) + (q))) /\ (((n) = (d) * (q) + (r) /\ (exists bcf_lt_gap_b5cvptez_data_division_bound. bcf_lt_gap_b5cvptez_data_division_bound + S (r) = d))))
  12. 0012specialize hprefix i
  13. 0013apply hprefix
  14. 0014exact hibound
  15. 0015cases hdata
  16. 0016cases hdata_witness
  17. 0017cases hdata_witness_witness
  18. 0018cases hdata_witness_witness_witness
  19. 0019cases hdata_witness_witness_witness_right
  20. 0020have hexponent : Lt(n,S i)
    Exact native replay linehave hexponent : exists g. g + S n = S i
  21. 0021cases hstart
  22. 0022exists x3
  23. 0023rewrite PA4
  24. 0024congr
  25. 0025exact hstart_witness
  26. 0026have hzero : x1 = 0
  27. 0027specialize prime_power_quotient_zero_of_exponent_gt p
  28. 0028specialize prime_power_quotient_zero_of_exponent_gt n
  29. 0029specialize prime_power_quotient_zero_of_exponent_gt (S i)
  30. 0030specialize prime_power_quotient_zero_of_exponent_gt x
  31. 0031specialize prime_power_quotient_zero_of_exponent_gt x1
  32. 0032specialize prime_power_quotient_zero_of_exponent_gt x2
  33. 0033apply prime_power_quotient_zero_of_exponent_gt
  34. 0034exact hp
  35. 0035exact hexponent
  36. 0036exact hdata_witness_witness_witness_left
  37. 0037exact hdata_witness_witness_witness_right_right
  38. 0038rewrite <- hzero
  39. 0039rewrite <- hzero
  40. 0040exact hdata_witness_witness_witness_right_left