BT00S0 · Bertrand theorem

prime_power_quotient_prefix_exists

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

Every prime-power quotient prefix has a finite beta code.

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. ∀ l. Prime(p) → ∃ x. ∃ y. PowerQuotPrefix(p,n,x,y,l)

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 PD0049 PowerQuotPrefix

2 occurrences

In local proof propositions

PD0002 Lt PD0007 DivRem PD0013 BetaAt PD0020 Pow PD0049 PowerQuotPrefix

12 occurrences

Exact expanded native-PA statement
forall p n l. ((~(p = 1) /\ forall frm_prime_left_bls_prime frm_prime_right_bls_prime. p = frm_prime_left_bls_prime * frm_prime_right_bls_prime -> frm_prime_left_bls_prime = 1 \/ frm_prime_right_bls_prime = 1)) -> exists b c. (forall bls_index_bls_exists. (exists bls_gap_bls_exists_bound. bls_gap_bls_exists_bound + S (bls_index_bls_exists) = (l)) -> exists bls_power_bls_exists bls_quotient_bls_exists bls_remainder_bls_exists. ((exists bpvi_b_bls_bls_exists_power bpvi_c_bls_bls_exists_power. ((forall bpvi_i_bls_bls_exists_power. (exists bpvi_repeat_gap_bls_bls_exists_power. bpvi_repeat_gap_bls_bls_exists_power + S bpvi_i_bls_bls_exists_power = S bls_index_bls_exists) -> (((exists bpvi_h_bls_bls_exists_power_repeat. bpvi_h_bls_bls_exists_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_exists_power)) * bpvi_c_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_repeat. bpvi_b_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_repeat * S ((S (bpvi_i_bls_bls_exists_power)) * bpvi_c_bls_bls_exists_power) + (p)))) /\ (exists bpvi_u_bls_bls_exists_power bpvi_v_bls_bls_exists_power. ((((exists bpvi_h_bls_bls_exists_power_start. bpvi_h_bls_bls_exists_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_start. bpvi_u_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_start * S ((S (0)) * bpvi_v_bls_bls_exists_power) + (1))) /\ ((((exists bpvi_h_bls_bls_exists_power_terminal. bpvi_h_bls_bls_exists_power_terminal + S (bls_power_bls_exists) = S ((S (S bls_index_bls_exists)) * bpvi_v_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_terminal. bpvi_u_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_terminal * S ((S (S bls_index_bls_exists)) * bpvi_v_bls_bls_exists_power) + (bls_power_bls_exists))) /\ forall bpvi_j_bls_bls_exists_power. (exists bpvi_product_gap_bls_bls_exists_power. bpvi_product_gap_bls_bls_exists_power + S bpvi_j_bls_bls_exists_power = S bls_index_bls_exists) -> exists bpvi_factor_bls_bls_exists_power bpvi_partial_bls_bls_exists_power bpvi_successor_bls_bls_exists_power. ((((exists bpvi_h_bls_bls_exists_power_factor. bpvi_h_bls_bls_exists_power_factor + S (bpvi_factor_bls_bls_exists_power) = S ((S (bpvi_j_bls_bls_exists_power)) * bpvi_c_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_factor. bpvi_b_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_factor * S ((S (bpvi_j_bls_bls_exists_power)) * bpvi_c_bls_bls_exists_power) + (bpvi_factor_bls_bls_exists_power))) /\ ((((exists bpvi_h_bls_bls_exists_power_partial. bpvi_h_bls_bls_exists_power_partial + S (bpvi_partial_bls_bls_exists_power) = S ((S (bpvi_j_bls_bls_exists_power)) * bpvi_v_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_partial. bpvi_u_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_partial * S ((S (bpvi_j_bls_bls_exists_power)) * bpvi_v_bls_bls_exists_power) + (bpvi_partial_bls_bls_exists_power))) /\ ((((exists bpvi_h_bls_bls_exists_power_successor. bpvi_h_bls_bls_exists_power_successor + S (bpvi_successor_bls_bls_exists_power) = S ((S (S bpvi_j_bls_bls_exists_power)) * bpvi_v_bls_bls_exists_power)) /\ exists bpvi_q_bls_bls_exists_power_successor. bpvi_u_bls_bls_exists_power = bpvi_q_bls_bls_exists_power_successor * S ((S (S bpvi_j_bls_bls_exists_power)) * bpvi_v_bls_bls_exists_power) + (bpvi_successor_bls_bls_exists_power))) /\ bpvi_successor_bls_bls_exists_power = bpvi_partial_bls_bls_exists_power * bpvi_factor_bls_bls_exists_power)))))))) /\ ((((exists ff_h_bls_bls_exists_quotient_entry. ff_h_bls_bls_exists_quotient_entry + S (bls_quotient_bls_exists) = S ((S (bls_index_bls_exists)) * c)) /\ exists ff_q_bls_bls_exists_quotient_entry. b = ff_q_bls_bls_exists_quotient_entry * S ((S (bls_index_bls_exists)) * c) + (bls_quotient_bls_exists))) /\ ((n = bls_power_bls_exists * bls_quotient_bls_exists + bls_remainder_bls_exists /\ exists bls_remainder_gap_bls_exists_division. bls_remainder_gap_bls_exists_division + S (bls_remainder_bls_exists) = bls_power_bls_exists)))))

Proof neighborhood

Direct theorem prerequisites

BT000L add_eq_zero_right BT000C succ_ne_zero BT0080 pow_exists BT003G prime_nonzero BT0010 one_le_of_ne_zero BT00Q1 pow_nonzero_of_one_le BT001P division_remainder_exists BT005D beta_prefix_extend BT00AA finite_lt_succ_eq_or_lt

Direct theorem dependents

BT00S2 prime_legendre_sum_exists BT00ST legendre_sum_zero_extended_prefix 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

109 script commands · 34 reading checkpoints · 10 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 (9)
add eq zero rightsucc ne zeropow existsprime nonzeroone le of ne zeropow nonzero of one ledivision remainder existsbeta prefix extendfinite lt succ eq or lt
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro n
02Induction on lL3–4

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

  1. L3
    induction l
  2. L4
    intro hp
03Construct an explicit witnessL5–6

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

  1. L5
    exists 0
  2. L6
    exists 0
04Fix variables and assumptionsL7–8

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

  1. L7
    intro i
  2. L8
    intro hi
05Separate the logical casesL9–10

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

  1. L9
    exfalso
  2. L10
    cases hi
06Establish hsiL11–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L11
    have hsi : S i = 0
  2. L12
    specialize add_eq_zero_right x
  3. L13
    specialize add_eq_zero_right (S i)
  4. L14
    apply add_eq_zero_right
  5. L15
    exact hi_witness
  6. L16
    specialize succ_ne_zero i
  7. L17
    apply succ_ne_zero
  8. L18
    exact hsi
  9. L19
    intro hp
07Establish hpreviousL20–22

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

  1. L20
    have hprevious : ∃ b. ∃ c. PowerQuotPrefix(p,n,b,c,l)Definitions: PowerQuotPrefix(p,n,b,c,l)Original native command in the exact edition
  2. L21
    apply IH
  3. L22
    exact hp
08Separate the logical casesL23–24

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

  1. L23
    cases hprevious
  2. L24
    cases hprevious_witness
09Establish hpowerL25–28

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

  1. L25
    have hpower : ∃ D. Pow(p,S l,D)Definitions: Pow(p,S l,D)Original native command in the exact edition
  2. L26
    specialize pow_exists p
  3. L27
    specialize pow_exists (S l)
  4. L28
    exact pow_exists
10Separate the logical casesL29–29

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

  1. L29
    cases hpower
11Establish hp0L30–35

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

  1. L30
    have hp0 : ~(p = 0)
  2. L31
    intro hpzero
  3. L32
    specialize prime_nonzero p
  4. L33
    apply prime_nonzero
  5. L34
    exact hp
  6. L35
    exact hpzero
12Establish hp1L36–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L36
  2. L37
    specialize one_le_of_ne_zero p
  3. L38
    apply one_le_of_ne_zero
  4. L39
    exact hp0
13Establish hD0L40–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow nonzero of one le.

  1. L40
    have hD0 : ~(x2 = 0)
  2. L41
    intro hzero
  3. L42
    specialize pow_nonzero_of_one_le p
  4. L43
    specialize pow_nonzero_of_one_le (S l)
  5. L44
    specialize pow_nonzero_of_one_le x2
  6. L45
    apply pow_nonzero_of_one_le
  7. L46
    exact hp1
  8. L47
    exact hpower_witness
  9. L48
    exact hzero
14Establish hdivisionL49–53

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

  1. L49
    have hdivision : ∃ q. ∃ r. DivRem(n,x2,q,r)Definitions: DivRem(n,x2,q,r)Original native command in the exact edition
  2. L50
    specialize division_remainder_exists x2
  3. L51
    specialize division_remainder_exists n
  4. L52
    apply division_remainder_exists
  5. L53
    exact hD0
15Separate the logical casesL54–55

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

  1. L54
    cases hdivision
  2. L55
    cases hdivision_witness
16Establish hextensionL56–61

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

  1. L56
    have hextension : ∃ z. ∃ d. BetaAt(z,d,l,x3) ∧ (∀ y. ∀ n. Lt(y,l) → BetaAt(x,x1,y,n) → BetaAt(z,d,y,n))Definitions: BetaAt(z,d,l,x3)Lt(y,l)BetaAt(x,x1,y,n)BetaAt(z,d,y,n)Original native command in the exact edition
  2. L57
    specialize beta_prefix_extend l
  3. L58
    specialize beta_prefix_extend x
  4. L59
    specialize beta_prefix_extend x1
  5. L60
    specialize beta_prefix_extend x3
  6. L61
    exact beta_prefix_extend
17Separate the logical casesL62–64

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

  1. L62
    cases hextension
  2. L63
    cases hextension_witness
  3. L64
    cases hextension_witness_witness
18Construct an explicit witnessL65–66

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

  1. L65
    exists x5
  2. L66
    exists x6
19Fix variables and assumptionsL67–68

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

  1. L67
    intro i
  2. L68
    intro hi
20Establish hsplitL69–73

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L69
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L70
    specialize finite_lt_succ_eq_or_lt l
  3. L71
    specialize finite_lt_succ_eq_or_lt i
  4. L72
    apply finite_lt_succ_eq_or_lt
  5. L73
    exact hi
21Separate the logical casesL74–74

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

  1. L74
    cases hsplit
22Construct an explicit witnessL75–77

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

  1. L75
    exists x2
  2. L76
    exists x3
  3. L77
    exists x4
23Calculate and transport equalitiesL78–83

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

  1. L78
    rewrite hsplit_left
  2. L79
    rewrite hsplit_left
  3. L80
    rewrite hsplit_left
  4. L81
    rewrite hsplit_left
  5. L82
    rewrite hsplit_left
  6. L83
    rewrite hsplit_left
24Separate the logical casesL84–84

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

  1. L84
    split
25Use earlier factsL85–85

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

  1. L85
    exact hpower_witness
26Separate the logical casesL86–86

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

  1. L86
    split
27Use earlier factsL87–88

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

  1. L87
    exact hextension_witness_witness_left
  2. L88
    exact hdivision_witness_witness
28Establish holdL89–92

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

  1. L89
    have hold : ∃ D. ∃ q. ∃ r. Pow(p,S i,D) ∧ (BetaAt(x,x1,i,q) ∧ DivRem(n,D,q,r))Definitions: Pow(p,S i,D)BetaAt(x,x1,i,q)DivRem(n,D,q,r)Original native command in the exact edition
  2. L90
    specialize hprevious_witness_witness i
  3. L91
    apply hprevious_witness_witness
  4. L92
    exact hsplit_right
29Separate the logical casesL93–97

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

  1. L93
    cases hold
  2. L94
    cases hold_witness
  3. L95
    cases hold_witness_witness
  4. L96
    cases hold_witness_witness_witness
  5. L97
    cases hold_witness_witness_witness_right
30Construct an explicit witnessL98–100

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

  1. L98
    exists x7
  2. L99
    exists x8
  3. L100
    exists x9
31Separate the logical casesL101–101

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

  1. L101
    split
32Use earlier factsL102–102

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

  1. L102
    exact hold_witness_witness_witness_left
33Separate the logical casesL103–103

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

  1. L103
    split
34Use earlier factsL104–109

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

  1. L104
    specialize hextension_witness_witness_right i
  2. L105
    specialize hextension_witness_witness_right x8
  3. L106
    apply hextension_witness_witness_right
  4. L107
    exact hsplit_right
  5. L108
    exact hold_witness_witness_witness_right_left
  6. L109
    exact hold_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 109 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003induction l
  4. 0004intro hp
  5. 0005exists 0
  6. 0006exists 0
  7. 0007intro i
  8. 0008intro hi
  9. 0009exfalso
  10. 0010cases hi
  11. 0011have hsi : S i = 0
  12. 0012specialize add_eq_zero_right x
  13. 0013specialize add_eq_zero_right (S i)
  14. 0014apply add_eq_zero_right
  15. 0015exact hi_witness
  16. 0016specialize succ_ne_zero i
  17. 0017apply succ_ne_zero
  18. 0018exact hsi
  19. 0019intro hp
  20. 0020have hprevious : ∃ b. ∃ c. PowerQuotPrefix(p,n,b,c,l)
    Exact native replay linehave hprevious : exists b c. (forall bls_index_bls_exists_previous. (exists bls_gap_bls_exists_previous_bound. bls_gap_bls_exists_previous_bound + S (bls_index_bls_exists_previous) = (l)) -> exists bls_power_bls_exists_previous bls_quotient_bls_exists_previous bls_remainder_bls_exists_previous. ((exists bpvi_b_bls_bls_exists_previous_power bpvi_c_bls_bls_exists_previous_power. ((forall bpvi_i_bls_bls_exists_previous_power. (exists bpvi_repeat_gap_bls_bls_exists_previous_power. bpvi_repeat_gap_bls_bls_exists_previous_power + S bpvi_i_bls_bls_exists_previous_power = S bls_index_bls_exists_previous) -> (((exists bpvi_h_bls_bls_exists_previous_power_repeat. bpvi_h_bls_bls_exists_previous_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_exists_previous_power)) * bpvi_c_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_repeat. bpvi_b_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_repeat * S ((S (bpvi_i_bls_bls_exists_previous_power)) * bpvi_c_bls_bls_exists_previous_power) + (p)))) /\ (exists bpvi_u_bls_bls_exists_previous_power bpvi_v_bls_bls_exists_previous_power. ((((exists bpvi_h_bls_bls_exists_previous_power_start. bpvi_h_bls_bls_exists_previous_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_start. bpvi_u_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_start * S ((S (0)) * bpvi_v_bls_bls_exists_previous_power) + (1))) /\ ((((exists bpvi_h_bls_bls_exists_previous_power_terminal. bpvi_h_bls_bls_exists_previous_power_terminal + S (bls_power_bls_exists_previous) = S ((S (S bls_index_bls_exists_previous)) * bpvi_v_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_terminal. bpvi_u_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_terminal * S ((S (S bls_index_bls_exists_previous)) * bpvi_v_bls_bls_exists_previous_power) + (bls_power_bls_exists_previous))) /\ forall bpvi_j_bls_bls_exists_previous_power. (exists bpvi_product_gap_bls_bls_exists_previous_power. bpvi_product_gap_bls_bls_exists_previous_power + S bpvi_j_bls_bls_exists_previous_power = S bls_index_bls_exists_previous) -> exists bpvi_factor_bls_bls_exists_previous_power bpvi_partial_bls_bls_exists_previous_power bpvi_successor_bls_bls_exists_previous_power. ((((exists bpvi_h_bls_bls_exists_previous_power_factor. bpvi_h_bls_bls_exists_previous_power_factor + S (bpvi_factor_bls_bls_exists_previous_power) = S ((S (bpvi_j_bls_bls_exists_previous_power)) * bpvi_c_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_factor. bpvi_b_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_factor * S ((S (bpvi_j_bls_bls_exists_previous_power)) * bpvi_c_bls_bls_exists_previous_power) + (bpvi_factor_bls_bls_exists_previous_power))) /\ ((((exists bpvi_h_bls_bls_exists_previous_power_partial. bpvi_h_bls_bls_exists_previous_power_partial + S (bpvi_partial_bls_bls_exists_previous_power) = S ((S (bpvi_j_bls_bls_exists_previous_power)) * bpvi_v_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_partial. bpvi_u_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_partial * S ((S (bpvi_j_bls_bls_exists_previous_power)) * bpvi_v_bls_bls_exists_previous_power) + (bpvi_partial_bls_bls_exists_previous_power))) /\ ((((exists bpvi_h_bls_bls_exists_previous_power_successor. bpvi_h_bls_bls_exists_previous_power_successor + S (bpvi_successor_bls_bls_exists_previous_power) = S ((S (S bpvi_j_bls_bls_exists_previous_power)) * bpvi_v_bls_bls_exists_previous_power)) /\ exists bpvi_q_bls_bls_exists_previous_power_successor. bpvi_u_bls_bls_exists_previous_power = bpvi_q_bls_bls_exists_previous_power_successor * S ((S (S bpvi_j_bls_bls_exists_previous_power)) * bpvi_v_bls_bls_exists_previous_power) + (bpvi_successor_bls_bls_exists_previous_power))) /\ bpvi_successor_bls_bls_exists_previous_power = bpvi_partial_bls_bls_exists_previous_power * bpvi_factor_bls_bls_exists_previous_power)))))))) /\ ((((exists ff_h_bls_bls_exists_previous_quotient_entry. ff_h_bls_bls_exists_previous_quotient_entry + S (bls_quotient_bls_exists_previous) = S ((S (bls_index_bls_exists_previous)) * c)) /\ exists ff_q_bls_bls_exists_previous_quotient_entry. b = ff_q_bls_bls_exists_previous_quotient_entry * S ((S (bls_index_bls_exists_previous)) * c) + (bls_quotient_bls_exists_previous))) /\ ((n = bls_power_bls_exists_previous * bls_quotient_bls_exists_previous + bls_remainder_bls_exists_previous /\ exists bls_remainder_gap_bls_exists_previous_division. bls_remainder_gap_bls_exists_previous_division + S (bls_remainder_bls_exists_previous) = bls_power_bls_exists_previous)))))
  21. 0021apply IH
  22. 0022exact hp
  23. 0023cases hprevious
  24. 0024cases hprevious_witness
  25. 0025have hpower : ∃ D. Pow(p,S l,D)
    Exact native replay linehave hpower : exists D. (exists bpvi_b_bls_exists_last_power bpvi_c_bls_exists_last_power. ((forall bpvi_i_bls_exists_last_power. (exists bpvi_repeat_gap_bls_exists_last_power. bpvi_repeat_gap_bls_exists_last_power + S bpvi_i_bls_exists_last_power = S l) -> (((exists bpvi_h_bls_exists_last_power_repeat. bpvi_h_bls_exists_last_power_repeat + S (p) = S ((S (bpvi_i_bls_exists_last_power)) * bpvi_c_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_repeat. bpvi_b_bls_exists_last_power = bpvi_q_bls_exists_last_power_repeat * S ((S (bpvi_i_bls_exists_last_power)) * bpvi_c_bls_exists_last_power) + (p)))) /\ (exists bpvi_u_bls_exists_last_power bpvi_v_bls_exists_last_power. ((((exists bpvi_h_bls_exists_last_power_start. bpvi_h_bls_exists_last_power_start + S (1) = S ((S (0)) * bpvi_v_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_start. bpvi_u_bls_exists_last_power = bpvi_q_bls_exists_last_power_start * S ((S (0)) * bpvi_v_bls_exists_last_power) + (1))) /\ ((((exists bpvi_h_bls_exists_last_power_terminal. bpvi_h_bls_exists_last_power_terminal + S (D) = S ((S (S l)) * bpvi_v_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_terminal. bpvi_u_bls_exists_last_power = bpvi_q_bls_exists_last_power_terminal * S ((S (S l)) * bpvi_v_bls_exists_last_power) + (D))) /\ forall bpvi_j_bls_exists_last_power. (exists bpvi_product_gap_bls_exists_last_power. bpvi_product_gap_bls_exists_last_power + S bpvi_j_bls_exists_last_power = S l) -> exists bpvi_factor_bls_exists_last_power bpvi_partial_bls_exists_last_power bpvi_successor_bls_exists_last_power. ((((exists bpvi_h_bls_exists_last_power_factor. bpvi_h_bls_exists_last_power_factor + S (bpvi_factor_bls_exists_last_power) = S ((S (bpvi_j_bls_exists_last_power)) * bpvi_c_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_factor. bpvi_b_bls_exists_last_power = bpvi_q_bls_exists_last_power_factor * S ((S (bpvi_j_bls_exists_last_power)) * bpvi_c_bls_exists_last_power) + (bpvi_factor_bls_exists_last_power))) /\ ((((exists bpvi_h_bls_exists_last_power_partial. bpvi_h_bls_exists_last_power_partial + S (bpvi_partial_bls_exists_last_power) = S ((S (bpvi_j_bls_exists_last_power)) * bpvi_v_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_partial. bpvi_u_bls_exists_last_power = bpvi_q_bls_exists_last_power_partial * S ((S (bpvi_j_bls_exists_last_power)) * bpvi_v_bls_exists_last_power) + (bpvi_partial_bls_exists_last_power))) /\ ((((exists bpvi_h_bls_exists_last_power_successor. bpvi_h_bls_exists_last_power_successor + S (bpvi_successor_bls_exists_last_power) = S ((S (S bpvi_j_bls_exists_last_power)) * bpvi_v_bls_exists_last_power)) /\ exists bpvi_q_bls_exists_last_power_successor. bpvi_u_bls_exists_last_power = bpvi_q_bls_exists_last_power_successor * S ((S (S bpvi_j_bls_exists_last_power)) * bpvi_v_bls_exists_last_power) + (bpvi_successor_bls_exists_last_power))) /\ bpvi_successor_bls_exists_last_power = bpvi_partial_bls_exists_last_power * bpvi_factor_bls_exists_last_power))))))))
  26. 0026specialize pow_exists p
  27. 0027specialize pow_exists (S l)
  28. 0028exact pow_exists
  29. 0029cases hpower
  30. 0030have hp0 : ~(p = 0)
  31. 0031intro hpzero
  32. 0032specialize prime_nonzero p
  33. 0033apply prime_nonzero
  34. 0034exact hp
  35. 0035exact hpzero
  36. 0036have hp1 : Lt(0,p)
    Exact native replay linehave hp1 : exists k. k + 1 = p
  37. 0037specialize one_le_of_ne_zero p
  38. 0038apply one_le_of_ne_zero
  39. 0039exact hp0
  40. 0040have hD0 : ~(x2 = 0)
  41. 0041intro hzero
  42. 0042specialize pow_nonzero_of_one_le p
  43. 0043specialize pow_nonzero_of_one_le (S l)
  44. 0044specialize pow_nonzero_of_one_le x2
  45. 0045apply pow_nonzero_of_one_le
  46. 0046exact hp1
  47. 0047exact hpower_witness
  48. 0048exact hzero
  49. 0049have hdivision : ∃ q. ∃ r. DivRem(n,x2,q,r)
    Exact native replay linehave hdivision : exists q r. ((n = x2 * q + r /\ exists bls_remainder_gap_bls_exists_division_witness. bls_remainder_gap_bls_exists_division_witness + S (r) = x2))
  50. 0050specialize division_remainder_exists x2
  51. 0051specialize division_remainder_exists n
  52. 0052apply division_remainder_exists
  53. 0053exact hD0
  54. 0054cases hdivision
  55. 0055cases hdivision_witness
  56. 0056have hextension : ∃ z. ∃ d. BetaAt(z,d,l,x3) ∧ (∀ y. ∀ n. Lt(y,l) → BetaAt(x,x1,y,n) → BetaAt(z,d,y,n))
    Exact native replay linehave hextension : exists z d. ((((exists ff_h_bls_exists_extension_last. ff_h_bls_exists_extension_last + S (x3) = S ((S (l)) * d)) /\ exists ff_q_bls_exists_extension_last. z = ff_q_bls_exists_extension_last * S ((S (l)) * d) + (x3))) /\ forall i a. (exists h. h + S i = l) -> (((exists ff_h_bls_exists_extension_old. ff_h_bls_exists_extension_old + S (a) = S ((S (i)) * x1)) /\ exists ff_q_bls_exists_extension_old. x = ff_q_bls_exists_extension_old * S ((S (i)) * x1) + (a))) -> (((exists ff_h_bls_exists_extension_new. ff_h_bls_exists_extension_new + S (a) = S ((S (i)) * d)) /\ exists ff_q_bls_exists_extension_new. z = ff_q_bls_exists_extension_new * S ((S (i)) * d) + (a))))
  57. 0057specialize beta_prefix_extend l
  58. 0058specialize beta_prefix_extend x
  59. 0059specialize beta_prefix_extend x1
  60. 0060specialize beta_prefix_extend x3
  61. 0061exact beta_prefix_extend
  62. 0062cases hextension
  63. 0063cases hextension_witness
  64. 0064cases hextension_witness_witness
  65. 0065exists x5
  66. 0066exists x6
  67. 0067intro i
  68. 0068intro hi
  69. 0069have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists gap. gap + S i = l
  70. 0070specialize finite_lt_succ_eq_or_lt l
  71. 0071specialize finite_lt_succ_eq_or_lt i
  72. 0072apply finite_lt_succ_eq_or_lt
  73. 0073exact hi
  74. 0074cases hsplit
  75. 0075exists x2
  76. 0076exists x3
  77. 0077exists x4
  78. 0078rewrite hsplit_left
  79. 0079rewrite hsplit_left
  80. 0080rewrite hsplit_left
  81. 0081rewrite hsplit_left
  82. 0082rewrite hsplit_left
  83. 0083rewrite hsplit_left
  84. 0084split
  85. 0085exact hpower_witness
  86. 0086split
  87. 0087exact hextension_witness_witness_left
  88. 0088exact hdivision_witness_witness
  89. 0089have hold : ∃ D. ∃ q. ∃ r. Pow(p,S i,D) ∧ (BetaAt(x,x1,i,q) ∧ DivRem(n,D,q,r))
    Exact native replay linehave hold : exists D q r. ((exists bpvi_b_bls_exists_old_power bpvi_c_bls_exists_old_power. ((forall bpvi_i_bls_exists_old_power. (exists bpvi_repeat_gap_bls_exists_old_power. bpvi_repeat_gap_bls_exists_old_power + S bpvi_i_bls_exists_old_power = S i) -> (((exists bpvi_h_bls_exists_old_power_repeat. bpvi_h_bls_exists_old_power_repeat + S (p) = S ((S (bpvi_i_bls_exists_old_power)) * bpvi_c_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_repeat. bpvi_b_bls_exists_old_power = bpvi_q_bls_exists_old_power_repeat * S ((S (bpvi_i_bls_exists_old_power)) * bpvi_c_bls_exists_old_power) + (p)))) /\ (exists bpvi_u_bls_exists_old_power bpvi_v_bls_exists_old_power. ((((exists bpvi_h_bls_exists_old_power_start. bpvi_h_bls_exists_old_power_start + S (1) = S ((S (0)) * bpvi_v_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_start. bpvi_u_bls_exists_old_power = bpvi_q_bls_exists_old_power_start * S ((S (0)) * bpvi_v_bls_exists_old_power) + (1))) /\ ((((exists bpvi_h_bls_exists_old_power_terminal. bpvi_h_bls_exists_old_power_terminal + S (D) = S ((S (S i)) * bpvi_v_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_terminal. bpvi_u_bls_exists_old_power = bpvi_q_bls_exists_old_power_terminal * S ((S (S i)) * bpvi_v_bls_exists_old_power) + (D))) /\ forall bpvi_j_bls_exists_old_power. (exists bpvi_product_gap_bls_exists_old_power. bpvi_product_gap_bls_exists_old_power + S bpvi_j_bls_exists_old_power = S i) -> exists bpvi_factor_bls_exists_old_power bpvi_partial_bls_exists_old_power bpvi_successor_bls_exists_old_power. ((((exists bpvi_h_bls_exists_old_power_factor. bpvi_h_bls_exists_old_power_factor + S (bpvi_factor_bls_exists_old_power) = S ((S (bpvi_j_bls_exists_old_power)) * bpvi_c_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_factor. bpvi_b_bls_exists_old_power = bpvi_q_bls_exists_old_power_factor * S ((S (bpvi_j_bls_exists_old_power)) * bpvi_c_bls_exists_old_power) + (bpvi_factor_bls_exists_old_power))) /\ ((((exists bpvi_h_bls_exists_old_power_partial. bpvi_h_bls_exists_old_power_partial + S (bpvi_partial_bls_exists_old_power) = S ((S (bpvi_j_bls_exists_old_power)) * bpvi_v_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_partial. bpvi_u_bls_exists_old_power = bpvi_q_bls_exists_old_power_partial * S ((S (bpvi_j_bls_exists_old_power)) * bpvi_v_bls_exists_old_power) + (bpvi_partial_bls_exists_old_power))) /\ ((((exists bpvi_h_bls_exists_old_power_successor. bpvi_h_bls_exists_old_power_successor + S (bpvi_successor_bls_exists_old_power) = S ((S (S bpvi_j_bls_exists_old_power)) * bpvi_v_bls_exists_old_power)) /\ exists bpvi_q_bls_exists_old_power_successor. bpvi_u_bls_exists_old_power = bpvi_q_bls_exists_old_power_successor * S ((S (S bpvi_j_bls_exists_old_power)) * bpvi_v_bls_exists_old_power) + (bpvi_successor_bls_exists_old_power))) /\ bpvi_successor_bls_exists_old_power = bpvi_partial_bls_exists_old_power * bpvi_factor_bls_exists_old_power)))))))) /\ ((((exists ff_h_bls_exists_old_entry. ff_h_bls_exists_old_entry + S (q) = S ((S (i)) * x1)) /\ exists ff_q_bls_exists_old_entry. x = ff_q_bls_exists_old_entry * S ((S (i)) * x1) + (q))) /\ ((n = D * q + r /\ exists bls_remainder_gap_bls_exists_old_division. bls_remainder_gap_bls_exists_old_division + S (r) = D))))
  90. 0090specialize hprevious_witness_witness i
  91. 0091apply hprevious_witness_witness
  92. 0092exact hsplit_right
  93. 0093cases hold
  94. 0094cases hold_witness
  95. 0095cases hold_witness_witness
  96. 0096cases hold_witness_witness_witness
  97. 0097cases hold_witness_witness_witness_right
  98. 0098exists x7
  99. 0099exists x8
  100. 0100exists x9
  101. 0101split
  102. 0102exact hold_witness_witness_witness_left
  103. 0103split
  104. 0104specialize hextension_witness_witness_right i
  105. 0105specialize hextension_witness_witness_right x8
  106. 0106apply hextension_witness_witness_right
  107. 0107exact hsplit_right
  108. 0108exact hold_witness_witness_witness_right_left
  109. 0109exact hold_witness_witness_witness_right_right