BT00SJ · Bertrand theorem

power_quotient_prefix_decoded_divrem

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

A decoded quotient-prefix entry exposes its power and canonical division data.

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. ∀ q. PowerQuotPrefix(p,n,b,c,l) → Lt(i,l) → BetaAt(b,c,i,q) → ∃ x. ∃ y. Pow(p,S i,x) ∧ DivRem(n,x,q,y)

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

PD0002 Lt PD0007 DivRem PD0013 BetaAt PD0020 Pow PD0049 PowerQuotPrefix

5 occurrences

In local proof propositions

PD0007 DivRem PD0013 BetaAt PD0020 Pow

3 occurrences

Exact expanded native-PA statement
forall p n b c l i q. (forall bls_index_legendre_successor_projection. (exists bls_gap_legendre_successor_projection_bound. bls_gap_legendre_successor_projection_bound + S (bls_index_legendre_successor_projection) = (l)) -> exists bls_power_legendre_successor_projection bls_quotient_legendre_successor_projection bls_remainder_legendre_successor_projection. ((exists bpvi_b_bls_legendre_successor_projection_power bpvi_c_bls_legendre_successor_projection_power. ((forall bpvi_i_bls_legendre_successor_projection_power. (exists bpvi_repeat_gap_bls_legendre_successor_projection_power. bpvi_repeat_gap_bls_legendre_successor_projection_power + S bpvi_i_bls_legendre_successor_projection_power = S bls_index_legendre_successor_projection) -> (((exists bpvi_h_bls_legendre_successor_projection_power_repeat. bpvi_h_bls_legendre_successor_projection_power_repeat + S (p) = S ((S (bpvi_i_bls_legendre_successor_projection_power)) * bpvi_c_bls_legendre_successor_projection_power)) /\ exists bpvi_q_bls_legendre_successor_projection_power_repeat. bpvi_b_bls_legendre_successor_projection_power = bpvi_q_bls_legendre_successor_projection_power_repeat * S ((S (bpvi_i_bls_legendre_successor_projection_power)) * bpvi_c_bls_legendre_successor_projection_power) + (p)))) /\ (exists bpvi_u_bls_legendre_successor_projection_power bpvi_v_bls_legendre_successor_projection_power. ((((exists bpvi_h_bls_legendre_successor_projection_power_start. bpvi_h_bls_legendre_successor_projection_power_start + S (1) = S ((S (0)) * bpvi_v_bls_legendre_successor_projection_power)) /\ exists bpvi_q_bls_legendre_successor_projection_power_start. bpvi_u_bls_legendre_successor_projection_power = bpvi_q_bls_legendre_successor_projection_power_start * S ((S (0)) * bpvi_v_bls_legendre_successor_projection_power) + (1))) /\ ((((exists bpvi_h_bls_legendre_successor_projection_power_terminal. bpvi_h_bls_legendre_successor_projection_power_terminal + S (bls_power_legendre_successor_projection) = S ((S (S bls_index_legendre_successor_projection)) * bpvi_v_bls_legendre_successor_projection_power)) /\ exists bpvi_q_bls_legendre_successor_projection_power_terminal. bpvi_u_bls_legendre_successor_projection_power = bpvi_q_bls_legendre_successor_projection_power_terminal * S ((S (S bls_index_legendre_successor_projection)) * bpvi_v_bls_legendre_successor_projection_power) + (bls_power_legendre_successor_projection))) /\ forall bpvi_j_bls_legendre_successor_projection_power. (exists bpvi_product_gap_bls_legendre_successor_projection_power. bpvi_product_gap_bls_legendre_successor_projection_power + S bpvi_j_bls_legendre_successor_projection_power = S bls_index_legendre_successor_projection) -> exists bpvi_factor_bls_legendre_successor_projection_power bpvi_partial_bls_legendre_successor_projection_power bpvi_successor_bls_legendre_successor_projection_power. ((((exists bpvi_h_bls_legendre_successor_projection_power_factor. bpvi_h_bls_legendre_successor_projection_power_factor + S (bpvi_factor_bls_legendre_successor_projection_power) = S ((S (bpvi_j_bls_legendre_successor_projection_power)) * bpvi_c_bls_legendre_successor_projection_power)) /\ exists bpvi_q_bls_legendre_successor_projection_power_factor. bpvi_b_bls_legendre_successor_projection_power = bpvi_q_bls_legendre_successor_projection_power_factor * S ((S (bpvi_j_bls_legendre_successor_projection_power)) * bpvi_c_bls_legendre_successor_projection_power) + (bpvi_factor_bls_legendre_successor_projection_power))) /\ ((((exists bpvi_h_bls_legendre_successor_projection_power_partial. bpvi_h_bls_legendre_successor_projection_power_partial + S (bpvi_partial_bls_legendre_successor_projection_power) = S ((S (bpvi_j_bls_legendre_successor_projection_power)) * bpvi_v_bls_legendre_successor_projection_power)) /\ exists bpvi_q_bls_legendre_successor_projection_power_partial. bpvi_u_bls_legendre_successor_projection_power = bpvi_q_bls_legendre_successor_projection_power_partial * S ((S (bpvi_j_bls_legendre_successor_projection_power)) * bpvi_v_bls_legendre_successor_projection_power) + (bpvi_partial_bls_legendre_successor_projection_power))) /\ ((((exists bpvi_h_bls_legendre_successor_projection_power_successor. bpvi_h_bls_legendre_successor_projection_power_successor + S (bpvi_successor_bls_legendre_successor_projection_power) = S ((S (S bpvi_j_bls_legendre_successor_projection_power)) * bpvi_v_bls_legendre_successor_projection_power)) /\ exists bpvi_q_bls_legendre_successor_projection_power_successor. bpvi_u_bls_legendre_successor_projection_power = bpvi_q_bls_legendre_successor_projection_power_successor * S ((S (S bpvi_j_bls_legendre_successor_projection_power)) * bpvi_v_bls_legendre_successor_projection_power) + (bpvi_successor_bls_legendre_successor_projection_power))) /\ bpvi_successor_bls_legendre_successor_projection_power = bpvi_partial_bls_legendre_successor_projection_power * bpvi_factor_bls_legendre_successor_projection_power)))))))) /\ ((((exists ff_h_bls_legendre_successor_projection_quotient_entry. ff_h_bls_legendre_successor_projection_quotient_entry + S (bls_quotient_legendre_successor_projection) = S ((S (bls_index_legendre_successor_projection)) * c)) /\ exists ff_q_bls_legendre_successor_projection_quotient_entry. b = ff_q_bls_legendre_successor_projection_quotient_entry * S ((S (bls_index_legendre_successor_projection)) * c) + (bls_quotient_legendre_successor_projection))) /\ ((n = bls_power_legendre_successor_projection * bls_quotient_legendre_successor_projection + bls_remainder_legendre_successor_projection /\ exists bls_remainder_gap_legendre_successor_projection_division. bls_remainder_gap_legendre_successor_projection_division + S (bls_remainder_legendre_successor_projection) = bls_power_legendre_successor_projection))))) -> (exists blsr_lt_gap_legendre_successor_projection_index. blsr_lt_gap_legendre_successor_projection_index + S (i) = (l)) -> (((exists ff_h_legendre_successor_projection_entry. ff_h_legendre_successor_projection_entry + S (q) = S ((S (i)) * c)) /\ exists ff_q_legendre_successor_projection_entry. b = ff_q_legendre_successor_projection_entry * S ((S (i)) * c) + (q))) -> exists D r. ((exists bpvi_b_legendre_successor_projection_power bpvi_c_legendre_successor_projection_power. ((forall bpvi_i_legendre_successor_projection_power. (exists bpvi_repeat_gap_legendre_successor_projection_power. bpvi_repeat_gap_legendre_successor_projection_power + S bpvi_i_legendre_successor_projection_power = S i) -> (((exists bpvi_h_legendre_successor_projection_power_repeat. bpvi_h_legendre_successor_projection_power_repeat + S (p) = S ((S (bpvi_i_legendre_successor_projection_power)) * bpvi_c_legendre_successor_projection_power)) /\ exists bpvi_q_legendre_successor_projection_power_repeat. bpvi_b_legendre_successor_projection_power = bpvi_q_legendre_successor_projection_power_repeat * S ((S (bpvi_i_legendre_successor_projection_power)) * bpvi_c_legendre_successor_projection_power) + (p)))) /\ (exists bpvi_u_legendre_successor_projection_power bpvi_v_legendre_successor_projection_power. ((((exists bpvi_h_legendre_successor_projection_power_start. bpvi_h_legendre_successor_projection_power_start + S (1) = S ((S (0)) * bpvi_v_legendre_successor_projection_power)) /\ exists bpvi_q_legendre_successor_projection_power_start. bpvi_u_legendre_successor_projection_power = bpvi_q_legendre_successor_projection_power_start * S ((S (0)) * bpvi_v_legendre_successor_projection_power) + (1))) /\ ((((exists bpvi_h_legendre_successor_projection_power_terminal. bpvi_h_legendre_successor_projection_power_terminal + S (D) = S ((S (S i)) * bpvi_v_legendre_successor_projection_power)) /\ exists bpvi_q_legendre_successor_projection_power_terminal. bpvi_u_legendre_successor_projection_power = bpvi_q_legendre_successor_projection_power_terminal * S ((S (S i)) * bpvi_v_legendre_successor_projection_power) + (D))) /\ forall bpvi_j_legendre_successor_projection_power. (exists bpvi_product_gap_legendre_successor_projection_power. bpvi_product_gap_legendre_successor_projection_power + S bpvi_j_legendre_successor_projection_power = S i) -> exists bpvi_factor_legendre_successor_projection_power bpvi_partial_legendre_successor_projection_power bpvi_successor_legendre_successor_projection_power. ((((exists bpvi_h_legendre_successor_projection_power_factor. bpvi_h_legendre_successor_projection_power_factor + S (bpvi_factor_legendre_successor_projection_power) = S ((S (bpvi_j_legendre_successor_projection_power)) * bpvi_c_legendre_successor_projection_power)) /\ exists bpvi_q_legendre_successor_projection_power_factor. bpvi_b_legendre_successor_projection_power = bpvi_q_legendre_successor_projection_power_factor * S ((S (bpvi_j_legendre_successor_projection_power)) * bpvi_c_legendre_successor_projection_power) + (bpvi_factor_legendre_successor_projection_power))) /\ ((((exists bpvi_h_legendre_successor_projection_power_partial. bpvi_h_legendre_successor_projection_power_partial + S (bpvi_partial_legendre_successor_projection_power) = S ((S (bpvi_j_legendre_successor_projection_power)) * bpvi_v_legendre_successor_projection_power)) /\ exists bpvi_q_legendre_successor_projection_power_partial. bpvi_u_legendre_successor_projection_power = bpvi_q_legendre_successor_projection_power_partial * S ((S (bpvi_j_legendre_successor_projection_power)) * bpvi_v_legendre_successor_projection_power) + (bpvi_partial_legendre_successor_projection_power))) /\ ((((exists bpvi_h_legendre_successor_projection_power_successor. bpvi_h_legendre_successor_projection_power_successor + S (bpvi_successor_legendre_successor_projection_power) = S ((S (S bpvi_j_legendre_successor_projection_power)) * bpvi_v_legendre_successor_projection_power)) /\ exists bpvi_q_legendre_successor_projection_power_successor. bpvi_u_legendre_successor_projection_power = bpvi_q_legendre_successor_projection_power_successor * S ((S (S bpvi_j_legendre_successor_projection_power)) * bpvi_v_legendre_successor_projection_power) + (bpvi_successor_legendre_successor_projection_power))) /\ bpvi_successor_legendre_successor_projection_power = bpvi_partial_legendre_successor_projection_power * bpvi_factor_legendre_successor_projection_power)))))))) /\ (((n) = (D) * (q) + (r) /\ exists blsr_lt_gap_legendre_successor_projection_division_bound. blsr_lt_gap_legendre_successor_projection_division_bound + S (r) = (D))))

Proof neighborhood

Direct theorem prerequisites

BT0042 beta_at_unique

Direct theorem dependents

BT00SK power_quotient_successor_pointwise_add

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

34 script commands · 9 reading checkpoints · 2 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 at unique
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 q
  8. L8
    intro hprefix
  9. L9
    intro hi
  10. L10
    intro hq
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. ∃ stored. ∃ r. Pow(p,S i,D) ∧ (BetaAt(b,c,i,stored) ∧ DivRem(n,D,stored,r))Definitions: Pow(p,S i,D)BetaAt(b,c,i,stored)DivRem(n,D,stored,r)Original native command in the exact edition
  2. L12
    specialize hprefix i
  3. L13
    apply hprefix
  4. L14
    exact hi
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 hstoredL20–28

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

  1. L20
    have hstored : x1 = q
  2. L21
    specialize beta_at_unique b
  3. L22
    specialize beta_at_unique c
  4. L23
    specialize beta_at_unique i
  5. L24
    specialize beta_at_unique x1
  6. L25
    specialize beta_at_unique q
  7. L26
    apply beta_at_unique
  8. L27
    exact hdata_witness_witness_witness_right_left
  9. L28
    exact hq
05Construct an explicit witnessL29–30

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

  1. L29
    exists x
  2. L30
    exists x2
06Separate the logical casesL31–31

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

  1. L31
    split
07Use earlier factsL32–32

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

  1. L32
    exact hdata_witness_witness_witness_left
08Calculate and transport equalitiesL33–33

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

  1. L33
    rewrite <- hstored
09Use earlier factsL34–34

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

  1. L34
    exact hdata_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro l
  6. 0006intro i
  7. 0007intro q
  8. 0008intro hprefix
  9. 0009intro hi
  10. 0010intro hq
  11. 0011have hdata : ∃ D. ∃ stored. ∃ r. Pow(p,S i,D) ∧ (BetaAt(b,c,i,stored) ∧ DivRem(n,D,stored,r))
    Exact native replay linehave hdata : exists D stored r. ((exists bpvi_b_legendre_successor_projection_stored_power bpvi_c_legendre_successor_projection_stored_power. ((forall bpvi_i_legendre_successor_projection_stored_power. (exists bpvi_repeat_gap_legendre_successor_projection_stored_power. bpvi_repeat_gap_legendre_successor_projection_stored_power + S bpvi_i_legendre_successor_projection_stored_power = S i) -> (((exists bpvi_h_legendre_successor_projection_stored_power_repeat. bpvi_h_legendre_successor_projection_stored_power_repeat + S (p) = S ((S (bpvi_i_legendre_successor_projection_stored_power)) * bpvi_c_legendre_successor_projection_stored_power)) /\ exists bpvi_q_legendre_successor_projection_stored_power_repeat. bpvi_b_legendre_successor_projection_stored_power = bpvi_q_legendre_successor_projection_stored_power_repeat * S ((S (bpvi_i_legendre_successor_projection_stored_power)) * bpvi_c_legendre_successor_projection_stored_power) + (p)))) /\ (exists bpvi_u_legendre_successor_projection_stored_power bpvi_v_legendre_successor_projection_stored_power. ((((exists bpvi_h_legendre_successor_projection_stored_power_start. bpvi_h_legendre_successor_projection_stored_power_start + S (1) = S ((S (0)) * bpvi_v_legendre_successor_projection_stored_power)) /\ exists bpvi_q_legendre_successor_projection_stored_power_start. bpvi_u_legendre_successor_projection_stored_power = bpvi_q_legendre_successor_projection_stored_power_start * S ((S (0)) * bpvi_v_legendre_successor_projection_stored_power) + (1))) /\ ((((exists bpvi_h_legendre_successor_projection_stored_power_terminal. bpvi_h_legendre_successor_projection_stored_power_terminal + S (D) = S ((S (S i)) * bpvi_v_legendre_successor_projection_stored_power)) /\ exists bpvi_q_legendre_successor_projection_stored_power_terminal. bpvi_u_legendre_successor_projection_stored_power = bpvi_q_legendre_successor_projection_stored_power_terminal * S ((S (S i)) * bpvi_v_legendre_successor_projection_stored_power) + (D))) /\ forall bpvi_j_legendre_successor_projection_stored_power. (exists bpvi_product_gap_legendre_successor_projection_stored_power. bpvi_product_gap_legendre_successor_projection_stored_power + S bpvi_j_legendre_successor_projection_stored_power = S i) -> exists bpvi_factor_legendre_successor_projection_stored_power bpvi_partial_legendre_successor_projection_stored_power bpvi_successor_legendre_successor_projection_stored_power. ((((exists bpvi_h_legendre_successor_projection_stored_power_factor. bpvi_h_legendre_successor_projection_stored_power_factor + S (bpvi_factor_legendre_successor_projection_stored_power) = S ((S (bpvi_j_legendre_successor_projection_stored_power)) * bpvi_c_legendre_successor_projection_stored_power)) /\ exists bpvi_q_legendre_successor_projection_stored_power_factor. bpvi_b_legendre_successor_projection_stored_power = bpvi_q_legendre_successor_projection_stored_power_factor * S ((S (bpvi_j_legendre_successor_projection_stored_power)) * bpvi_c_legendre_successor_projection_stored_power) + (bpvi_factor_legendre_successor_projection_stored_power))) /\ ((((exists bpvi_h_legendre_successor_projection_stored_power_partial. bpvi_h_legendre_successor_projection_stored_power_partial + S (bpvi_partial_legendre_successor_projection_stored_power) = S ((S (bpvi_j_legendre_successor_projection_stored_power)) * bpvi_v_legendre_successor_projection_stored_power)) /\ exists bpvi_q_legendre_successor_projection_stored_power_partial. bpvi_u_legendre_successor_projection_stored_power = bpvi_q_legendre_successor_projection_stored_power_partial * S ((S (bpvi_j_legendre_successor_projection_stored_power)) * bpvi_v_legendre_successor_projection_stored_power) + (bpvi_partial_legendre_successor_projection_stored_power))) /\ ((((exists bpvi_h_legendre_successor_projection_stored_power_successor. bpvi_h_legendre_successor_projection_stored_power_successor + S (bpvi_successor_legendre_successor_projection_stored_power) = S ((S (S bpvi_j_legendre_successor_projection_stored_power)) * bpvi_v_legendre_successor_projection_stored_power)) /\ exists bpvi_q_legendre_successor_projection_stored_power_successor. bpvi_u_legendre_successor_projection_stored_power = bpvi_q_legendre_successor_projection_stored_power_successor * S ((S (S bpvi_j_legendre_successor_projection_stored_power)) * bpvi_v_legendre_successor_projection_stored_power) + (bpvi_successor_legendre_successor_projection_stored_power))) /\ bpvi_successor_legendre_successor_projection_stored_power = bpvi_partial_legendre_successor_projection_stored_power * bpvi_factor_legendre_successor_projection_stored_power)))))))) /\ ((((exists ff_h_legendre_successor_projection_stored_entry. ff_h_legendre_successor_projection_stored_entry + S (stored) = S ((S (i)) * c)) /\ exists ff_q_legendre_successor_projection_stored_entry. b = ff_q_legendre_successor_projection_stored_entry * S ((S (i)) * c) + (stored))) /\ (((n) = (D) * (stored) + (r) /\ exists blsr_lt_gap_legendre_successor_projection_stored_division_bound. blsr_lt_gap_legendre_successor_projection_stored_division_bound + S (r) = (D)))))
  12. 0012specialize hprefix i
  13. 0013apply hprefix
  14. 0014exact hi
  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 hstored : x1 = q
  21. 0021specialize beta_at_unique b
  22. 0022specialize beta_at_unique c
  23. 0023specialize beta_at_unique i
  24. 0024specialize beta_at_unique x1
  25. 0025specialize beta_at_unique q
  26. 0026apply beta_at_unique
  27. 0027exact hdata_witness_witness_witness_right_left
  28. 0028exact hq
  29. 0029exists x
  30. 0030exists x2
  31. 0031split
  32. 0032exact hdata_witness_witness_witness_left
  33. 0033rewrite <- hstored
  34. 0034exact hdata_witness_witness_witness_right_right