BT00S1 · Bertrand theorem

power_quotient_prefix_transport

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

Equivalent power-quotient prefixes transport decoded quotients pointwise.

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. ∀ z. ∀ d. ∀ l. PowerQuotPrefix(p,n,b,c,l) → PowerQuotPrefix(p,n,z,d,l) → ∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,d,x,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 PD0013 BetaAt PD0049 PowerQuotPrefix

5 occurrences

In local proof propositions

PD0007 DivRem PD0013 BetaAt PD0020 Pow

6 occurrences

Exact expanded native-PA statement
forall p n b c z d l. (forall bls_index_bls_transport_source. (exists bls_gap_bls_transport_source_bound. bls_gap_bls_transport_source_bound + S (bls_index_bls_transport_source) = (l)) -> exists bls_power_bls_transport_source bls_quotient_bls_transport_source bls_remainder_bls_transport_source. ((exists bpvi_b_bls_bls_transport_source_power bpvi_c_bls_bls_transport_source_power. ((forall bpvi_i_bls_bls_transport_source_power. (exists bpvi_repeat_gap_bls_bls_transport_source_power. bpvi_repeat_gap_bls_bls_transport_source_power + S bpvi_i_bls_bls_transport_source_power = S bls_index_bls_transport_source) -> (((exists bpvi_h_bls_bls_transport_source_power_repeat. bpvi_h_bls_bls_transport_source_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_transport_source_power)) * bpvi_c_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_repeat. bpvi_b_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_repeat * S ((S (bpvi_i_bls_bls_transport_source_power)) * bpvi_c_bls_bls_transport_source_power) + (p)))) /\ (exists bpvi_u_bls_bls_transport_source_power bpvi_v_bls_bls_transport_source_power. ((((exists bpvi_h_bls_bls_transport_source_power_start. bpvi_h_bls_bls_transport_source_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_start. bpvi_u_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_start * S ((S (0)) * bpvi_v_bls_bls_transport_source_power) + (1))) /\ ((((exists bpvi_h_bls_bls_transport_source_power_terminal. bpvi_h_bls_bls_transport_source_power_terminal + S (bls_power_bls_transport_source) = S ((S (S bls_index_bls_transport_source)) * bpvi_v_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_terminal. bpvi_u_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_terminal * S ((S (S bls_index_bls_transport_source)) * bpvi_v_bls_bls_transport_source_power) + (bls_power_bls_transport_source))) /\ forall bpvi_j_bls_bls_transport_source_power. (exists bpvi_product_gap_bls_bls_transport_source_power. bpvi_product_gap_bls_bls_transport_source_power + S bpvi_j_bls_bls_transport_source_power = S bls_index_bls_transport_source) -> exists bpvi_factor_bls_bls_transport_source_power bpvi_partial_bls_bls_transport_source_power bpvi_successor_bls_bls_transport_source_power. ((((exists bpvi_h_bls_bls_transport_source_power_factor. bpvi_h_bls_bls_transport_source_power_factor + S (bpvi_factor_bls_bls_transport_source_power) = S ((S (bpvi_j_bls_bls_transport_source_power)) * bpvi_c_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_factor. bpvi_b_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_factor * S ((S (bpvi_j_bls_bls_transport_source_power)) * bpvi_c_bls_bls_transport_source_power) + (bpvi_factor_bls_bls_transport_source_power))) /\ ((((exists bpvi_h_bls_bls_transport_source_power_partial. bpvi_h_bls_bls_transport_source_power_partial + S (bpvi_partial_bls_bls_transport_source_power) = S ((S (bpvi_j_bls_bls_transport_source_power)) * bpvi_v_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_partial. bpvi_u_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_partial * S ((S (bpvi_j_bls_bls_transport_source_power)) * bpvi_v_bls_bls_transport_source_power) + (bpvi_partial_bls_bls_transport_source_power))) /\ ((((exists bpvi_h_bls_bls_transport_source_power_successor. bpvi_h_bls_bls_transport_source_power_successor + S (bpvi_successor_bls_bls_transport_source_power) = S ((S (S bpvi_j_bls_bls_transport_source_power)) * bpvi_v_bls_bls_transport_source_power)) /\ exists bpvi_q_bls_bls_transport_source_power_successor. bpvi_u_bls_bls_transport_source_power = bpvi_q_bls_bls_transport_source_power_successor * S ((S (S bpvi_j_bls_bls_transport_source_power)) * bpvi_v_bls_bls_transport_source_power) + (bpvi_successor_bls_bls_transport_source_power))) /\ bpvi_successor_bls_bls_transport_source_power = bpvi_partial_bls_bls_transport_source_power * bpvi_factor_bls_bls_transport_source_power)))))))) /\ ((((exists ff_h_bls_bls_transport_source_quotient_entry. ff_h_bls_bls_transport_source_quotient_entry + S (bls_quotient_bls_transport_source) = S ((S (bls_index_bls_transport_source)) * c)) /\ exists ff_q_bls_bls_transport_source_quotient_entry. b = ff_q_bls_bls_transport_source_quotient_entry * S ((S (bls_index_bls_transport_source)) * c) + (bls_quotient_bls_transport_source))) /\ ((n = bls_power_bls_transport_source * bls_quotient_bls_transport_source + bls_remainder_bls_transport_source /\ exists bls_remainder_gap_bls_transport_source_division. bls_remainder_gap_bls_transport_source_division + S (bls_remainder_bls_transport_source) = bls_power_bls_transport_source))))) -> (forall bls_index_bls_transport_target. (exists bls_gap_bls_transport_target_bound. bls_gap_bls_transport_target_bound + S (bls_index_bls_transport_target) = (l)) -> exists bls_power_bls_transport_target bls_quotient_bls_transport_target bls_remainder_bls_transport_target. ((exists bpvi_b_bls_bls_transport_target_power bpvi_c_bls_bls_transport_target_power. ((forall bpvi_i_bls_bls_transport_target_power. (exists bpvi_repeat_gap_bls_bls_transport_target_power. bpvi_repeat_gap_bls_bls_transport_target_power + S bpvi_i_bls_bls_transport_target_power = S bls_index_bls_transport_target) -> (((exists bpvi_h_bls_bls_transport_target_power_repeat. bpvi_h_bls_bls_transport_target_power_repeat + S (p) = S ((S (bpvi_i_bls_bls_transport_target_power)) * bpvi_c_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_repeat. bpvi_b_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_repeat * S ((S (bpvi_i_bls_bls_transport_target_power)) * bpvi_c_bls_bls_transport_target_power) + (p)))) /\ (exists bpvi_u_bls_bls_transport_target_power bpvi_v_bls_bls_transport_target_power. ((((exists bpvi_h_bls_bls_transport_target_power_start. bpvi_h_bls_bls_transport_target_power_start + S (1) = S ((S (0)) * bpvi_v_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_start. bpvi_u_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_start * S ((S (0)) * bpvi_v_bls_bls_transport_target_power) + (1))) /\ ((((exists bpvi_h_bls_bls_transport_target_power_terminal. bpvi_h_bls_bls_transport_target_power_terminal + S (bls_power_bls_transport_target) = S ((S (S bls_index_bls_transport_target)) * bpvi_v_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_terminal. bpvi_u_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_terminal * S ((S (S bls_index_bls_transport_target)) * bpvi_v_bls_bls_transport_target_power) + (bls_power_bls_transport_target))) /\ forall bpvi_j_bls_bls_transport_target_power. (exists bpvi_product_gap_bls_bls_transport_target_power. bpvi_product_gap_bls_bls_transport_target_power + S bpvi_j_bls_bls_transport_target_power = S bls_index_bls_transport_target) -> exists bpvi_factor_bls_bls_transport_target_power bpvi_partial_bls_bls_transport_target_power bpvi_successor_bls_bls_transport_target_power. ((((exists bpvi_h_bls_bls_transport_target_power_factor. bpvi_h_bls_bls_transport_target_power_factor + S (bpvi_factor_bls_bls_transport_target_power) = S ((S (bpvi_j_bls_bls_transport_target_power)) * bpvi_c_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_factor. bpvi_b_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_factor * S ((S (bpvi_j_bls_bls_transport_target_power)) * bpvi_c_bls_bls_transport_target_power) + (bpvi_factor_bls_bls_transport_target_power))) /\ ((((exists bpvi_h_bls_bls_transport_target_power_partial. bpvi_h_bls_bls_transport_target_power_partial + S (bpvi_partial_bls_bls_transport_target_power) = S ((S (bpvi_j_bls_bls_transport_target_power)) * bpvi_v_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_partial. bpvi_u_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_partial * S ((S (bpvi_j_bls_bls_transport_target_power)) * bpvi_v_bls_bls_transport_target_power) + (bpvi_partial_bls_bls_transport_target_power))) /\ ((((exists bpvi_h_bls_bls_transport_target_power_successor. bpvi_h_bls_bls_transport_target_power_successor + S (bpvi_successor_bls_bls_transport_target_power) = S ((S (S bpvi_j_bls_bls_transport_target_power)) * bpvi_v_bls_bls_transport_target_power)) /\ exists bpvi_q_bls_bls_transport_target_power_successor. bpvi_u_bls_bls_transport_target_power = bpvi_q_bls_bls_transport_target_power_successor * S ((S (S bpvi_j_bls_bls_transport_target_power)) * bpvi_v_bls_bls_transport_target_power) + (bpvi_successor_bls_bls_transport_target_power))) /\ bpvi_successor_bls_bls_transport_target_power = bpvi_partial_bls_bls_transport_target_power * bpvi_factor_bls_bls_transport_target_power)))))))) /\ ((((exists ff_h_bls_bls_transport_target_quotient_entry. ff_h_bls_bls_transport_target_quotient_entry + S (bls_quotient_bls_transport_target) = S ((S (bls_index_bls_transport_target)) * d)) /\ exists ff_q_bls_bls_transport_target_quotient_entry. z = ff_q_bls_bls_transport_target_quotient_entry * S ((S (bls_index_bls_transport_target)) * d) + (bls_quotient_bls_transport_target))) /\ ((n = bls_power_bls_transport_target * bls_quotient_bls_transport_target + bls_remainder_bls_transport_target /\ exists bls_remainder_gap_bls_transport_target_division. bls_remainder_gap_bls_transport_target_division + S (bls_remainder_bls_transport_target) = bls_power_bls_transport_target))))) -> forall i q. (exists bls_gap_bls_transport_bound. bls_gap_bls_transport_bound + S (i) = (l)) -> (((exists ff_h_bls_transport_given. ff_h_bls_transport_given + S (q) = S ((S (i)) * c)) /\ exists ff_q_bls_transport_given. b = ff_q_bls_transport_given * S ((S (i)) * c) + (q))) -> (((exists ff_h_bls_transport_result. ff_h_bls_transport_result + S (q) = S ((S (i)) * d)) /\ exists ff_q_bls_transport_result. z = ff_q_bls_transport_result * S ((S (i)) * d) + (q)))

Proof neighborhood

Direct theorem prerequisites

BT0042 beta_at_unique BT0082 pow_functional BT001U division_remainder_unique

Direct theorem dependents

BT00S3 legendre_sum_functional

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

72 script commands · 14 reading checkpoints · 6 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)
beta at uniquepow functionaldivision remainder 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 z
  6. L6
    intro d
  7. L7
    intro l
  8. L8
    intro hsource
  9. L9
    intro htarget
  10. L10
    intro i
02Fix variables and assumptionsL11–13

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

  1. L11
    intro q
  2. L12
    intro hi
  3. L13
    intro hq
03Establish hsL14–17

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

  1. L14
    have hs : ∃ D. ∃ u. ∃ r. Pow(p,S i,D) ∧ (BetaAt(b,c,i,u) ∧ DivRem(n,D,u,r))Definitions: Pow(p,S i,D)BetaAt(b,c,i,u)DivRem(n,D,u,r)Original native command in the exact edition
  2. L15
    specialize hsource i
  3. L16
    apply hsource
  4. L17
    exact hi
04Establish htL18–21

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

  1. L18
    have ht : ∃ E. ∃ v. ∃ s. Pow(p,S i,E) ∧ (BetaAt(z,d,i,v) ∧ DivRem(n,E,v,s))Definitions: Pow(p,S i,E)BetaAt(z,d,i,v)DivRem(n,E,v,s)Original native command in the exact edition
  2. L19
    specialize htarget i
  3. L20
    apply htarget
  4. L21
    exact hi
05Separate the logical casesL22–31

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

  1. L22
    cases hs
  2. L23
    cases hs_witness
  3. L24
    cases hs_witness_witness
  4. L25
    cases hs_witness_witness_witness
  5. L26
    cases hs_witness_witness_witness_right
  6. L27
    cases hs_witness_witness_witness_right_right
  7. L28
    cases ht
  8. L29
    cases ht_witness
  9. L30
    cases ht_witness_witness
  10. L31
    cases ht_witness_witness_witness
06Separate the logical casesL32–33

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

  1. L32
    cases ht_witness_witness_witness_right
  2. L33
    cases ht_witness_witness_witness_right_right
07Establish hDL34–43

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

  1. L34
    have hD : x = x3
  2. L35
    specialize pow_functional p
  3. L36
    specialize pow_functional (S i)
  4. L37
    specialize pow_functional x
  5. L38
    specialize pow_functional x3
  6. L39
    apply pow_functional
  7. L40
    exact hs_witness_witness_witness_left
  8. L41
    exact ht_witness_witness_witness_left
  9. L42
    rewrite <- hD at ht_witness_witness_witness_right_right_left
  10. L43
    rewrite <- hD at ht_witness_witness_witness_right_right_right
08Establish hquotientsL44–50

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

  1. L44
    have hquotients : x1 = x4
  2. L45
    specialize division_remainder_unique x
  3. L46
    specialize division_remainder_unique n
  4. L47
    specialize division_remainder_unique x1
  5. L48
    specialize division_remainder_unique x2
  6. L49
    specialize division_remainder_unique x4
  7. L50
    specialize division_remainder_unique x5
09Establish hdivision_uniqueL51–56

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

  1. L51
    have hdivision_unique : x1 = x4 /\ x2 = x5
  2. L52
    apply division_remainder_unique
  3. L53
    exact hs_witness_witness_witness_right_right_left
  4. L54
    exact hs_witness_witness_witness_right_right_right
  5. L55
    exact ht_witness_witness_witness_right_right_left
  6. L56
    exact ht_witness_witness_witness_right_right_right
10Separate the logical casesL57–57

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

  1. L57
    cases hdivision_unique
11Use earlier factsL58–58

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

  1. L58
    exact hdivision_unique_left
12Establish hstoredL59–68

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

  1. L59
    have hstored : x1 = q
  2. L60
    specialize beta_at_unique b
  3. L61
    specialize beta_at_unique c
  4. L62
    specialize beta_at_unique i
  5. L63
    specialize beta_at_unique x1
  6. L64
    specialize beta_at_unique q
  7. L65
    apply beta_at_unique
  8. L66
    exact hs_witness_witness_witness_right_left
  9. L67
    exact hq
  10. L68
    rewrite <- hstored
13Calculate and transport equalitiesL69–71

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

  1. L69
    rewrite hquotients
  2. L70
    rewrite <- hstored
  3. L71
    rewrite hquotients
14Use earlier factsL72–72

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

  1. L72
    exact ht_witness_witness_witness_right_left

Library-wide reading audit

Original defined command ledger · 72 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007intro l
  8. 0008intro hsource
  9. 0009intro htarget
  10. 0010intro i
  11. 0011intro q
  12. 0012intro hi
  13. 0013intro hq
  14. 0014have hs : ∃ D. ∃ u. ∃ r. Pow(p,S i,D) ∧ (BetaAt(b,c,i,u) ∧ DivRem(n,D,u,r))
    Exact native replay linehave hs : exists D u r. ((exists bpvi_b_bls_transport_source_power bpvi_c_bls_transport_source_power. ((forall bpvi_i_bls_transport_source_power. (exists bpvi_repeat_gap_bls_transport_source_power. bpvi_repeat_gap_bls_transport_source_power + S bpvi_i_bls_transport_source_power = S i) -> (((exists bpvi_h_bls_transport_source_power_repeat. bpvi_h_bls_transport_source_power_repeat + S (p) = S ((S (bpvi_i_bls_transport_source_power)) * bpvi_c_bls_transport_source_power)) /\ exists bpvi_q_bls_transport_source_power_repeat. bpvi_b_bls_transport_source_power = bpvi_q_bls_transport_source_power_repeat * S ((S (bpvi_i_bls_transport_source_power)) * bpvi_c_bls_transport_source_power) + (p)))) /\ (exists bpvi_u_bls_transport_source_power bpvi_v_bls_transport_source_power. ((((exists bpvi_h_bls_transport_source_power_start. bpvi_h_bls_transport_source_power_start + S (1) = S ((S (0)) * bpvi_v_bls_transport_source_power)) /\ exists bpvi_q_bls_transport_source_power_start. bpvi_u_bls_transport_source_power = bpvi_q_bls_transport_source_power_start * S ((S (0)) * bpvi_v_bls_transport_source_power) + (1))) /\ ((((exists bpvi_h_bls_transport_source_power_terminal. bpvi_h_bls_transport_source_power_terminal + S (D) = S ((S (S i)) * bpvi_v_bls_transport_source_power)) /\ exists bpvi_q_bls_transport_source_power_terminal. bpvi_u_bls_transport_source_power = bpvi_q_bls_transport_source_power_terminal * S ((S (S i)) * bpvi_v_bls_transport_source_power) + (D))) /\ forall bpvi_j_bls_transport_source_power. (exists bpvi_product_gap_bls_transport_source_power. bpvi_product_gap_bls_transport_source_power + S bpvi_j_bls_transport_source_power = S i) -> exists bpvi_factor_bls_transport_source_power bpvi_partial_bls_transport_source_power bpvi_successor_bls_transport_source_power. ((((exists bpvi_h_bls_transport_source_power_factor. bpvi_h_bls_transport_source_power_factor + S (bpvi_factor_bls_transport_source_power) = S ((S (bpvi_j_bls_transport_source_power)) * bpvi_c_bls_transport_source_power)) /\ exists bpvi_q_bls_transport_source_power_factor. bpvi_b_bls_transport_source_power = bpvi_q_bls_transport_source_power_factor * S ((S (bpvi_j_bls_transport_source_power)) * bpvi_c_bls_transport_source_power) + (bpvi_factor_bls_transport_source_power))) /\ ((((exists bpvi_h_bls_transport_source_power_partial. bpvi_h_bls_transport_source_power_partial + S (bpvi_partial_bls_transport_source_power) = S ((S (bpvi_j_bls_transport_source_power)) * bpvi_v_bls_transport_source_power)) /\ exists bpvi_q_bls_transport_source_power_partial. bpvi_u_bls_transport_source_power = bpvi_q_bls_transport_source_power_partial * S ((S (bpvi_j_bls_transport_source_power)) * bpvi_v_bls_transport_source_power) + (bpvi_partial_bls_transport_source_power))) /\ ((((exists bpvi_h_bls_transport_source_power_successor. bpvi_h_bls_transport_source_power_successor + S (bpvi_successor_bls_transport_source_power) = S ((S (S bpvi_j_bls_transport_source_power)) * bpvi_v_bls_transport_source_power)) /\ exists bpvi_q_bls_transport_source_power_successor. bpvi_u_bls_transport_source_power = bpvi_q_bls_transport_source_power_successor * S ((S (S bpvi_j_bls_transport_source_power)) * bpvi_v_bls_transport_source_power) + (bpvi_successor_bls_transport_source_power))) /\ bpvi_successor_bls_transport_source_power = bpvi_partial_bls_transport_source_power * bpvi_factor_bls_transport_source_power)))))))) /\ ((((exists ff_h_bls_transport_source_stored. ff_h_bls_transport_source_stored + S (u) = S ((S (i)) * c)) /\ exists ff_q_bls_transport_source_stored. b = ff_q_bls_transport_source_stored * S ((S (i)) * c) + (u))) /\ ((n = D * u + r /\ exists bls_remainder_gap_bls_transport_source_division. bls_remainder_gap_bls_transport_source_division + S (r) = D))))
  15. 0015specialize hsource i
  16. 0016apply hsource
  17. 0017exact hi
  18. 0018have ht : ∃ E. ∃ v. ∃ s. Pow(p,S i,E) ∧ (BetaAt(z,d,i,v) ∧ DivRem(n,E,v,s))
    Exact native replay linehave ht : exists E v s. ((exists bpvi_b_bls_transport_target_power bpvi_c_bls_transport_target_power. ((forall bpvi_i_bls_transport_target_power. (exists bpvi_repeat_gap_bls_transport_target_power. bpvi_repeat_gap_bls_transport_target_power + S bpvi_i_bls_transport_target_power = S i) -> (((exists bpvi_h_bls_transport_target_power_repeat. bpvi_h_bls_transport_target_power_repeat + S (p) = S ((S (bpvi_i_bls_transport_target_power)) * bpvi_c_bls_transport_target_power)) /\ exists bpvi_q_bls_transport_target_power_repeat. bpvi_b_bls_transport_target_power = bpvi_q_bls_transport_target_power_repeat * S ((S (bpvi_i_bls_transport_target_power)) * bpvi_c_bls_transport_target_power) + (p)))) /\ (exists bpvi_u_bls_transport_target_power bpvi_v_bls_transport_target_power. ((((exists bpvi_h_bls_transport_target_power_start. bpvi_h_bls_transport_target_power_start + S (1) = S ((S (0)) * bpvi_v_bls_transport_target_power)) /\ exists bpvi_q_bls_transport_target_power_start. bpvi_u_bls_transport_target_power = bpvi_q_bls_transport_target_power_start * S ((S (0)) * bpvi_v_bls_transport_target_power) + (1))) /\ ((((exists bpvi_h_bls_transport_target_power_terminal. bpvi_h_bls_transport_target_power_terminal + S (E) = S ((S (S i)) * bpvi_v_bls_transport_target_power)) /\ exists bpvi_q_bls_transport_target_power_terminal. bpvi_u_bls_transport_target_power = bpvi_q_bls_transport_target_power_terminal * S ((S (S i)) * bpvi_v_bls_transport_target_power) + (E))) /\ forall bpvi_j_bls_transport_target_power. (exists bpvi_product_gap_bls_transport_target_power. bpvi_product_gap_bls_transport_target_power + S bpvi_j_bls_transport_target_power = S i) -> exists bpvi_factor_bls_transport_target_power bpvi_partial_bls_transport_target_power bpvi_successor_bls_transport_target_power. ((((exists bpvi_h_bls_transport_target_power_factor. bpvi_h_bls_transport_target_power_factor + S (bpvi_factor_bls_transport_target_power) = S ((S (bpvi_j_bls_transport_target_power)) * bpvi_c_bls_transport_target_power)) /\ exists bpvi_q_bls_transport_target_power_factor. bpvi_b_bls_transport_target_power = bpvi_q_bls_transport_target_power_factor * S ((S (bpvi_j_bls_transport_target_power)) * bpvi_c_bls_transport_target_power) + (bpvi_factor_bls_transport_target_power))) /\ ((((exists bpvi_h_bls_transport_target_power_partial. bpvi_h_bls_transport_target_power_partial + S (bpvi_partial_bls_transport_target_power) = S ((S (bpvi_j_bls_transport_target_power)) * bpvi_v_bls_transport_target_power)) /\ exists bpvi_q_bls_transport_target_power_partial. bpvi_u_bls_transport_target_power = bpvi_q_bls_transport_target_power_partial * S ((S (bpvi_j_bls_transport_target_power)) * bpvi_v_bls_transport_target_power) + (bpvi_partial_bls_transport_target_power))) /\ ((((exists bpvi_h_bls_transport_target_power_successor. bpvi_h_bls_transport_target_power_successor + S (bpvi_successor_bls_transport_target_power) = S ((S (S bpvi_j_bls_transport_target_power)) * bpvi_v_bls_transport_target_power)) /\ exists bpvi_q_bls_transport_target_power_successor. bpvi_u_bls_transport_target_power = bpvi_q_bls_transport_target_power_successor * S ((S (S bpvi_j_bls_transport_target_power)) * bpvi_v_bls_transport_target_power) + (bpvi_successor_bls_transport_target_power))) /\ bpvi_successor_bls_transport_target_power = bpvi_partial_bls_transport_target_power * bpvi_factor_bls_transport_target_power)))))))) /\ ((((exists ff_h_bls_transport_target_stored. ff_h_bls_transport_target_stored + S (v) = S ((S (i)) * d)) /\ exists ff_q_bls_transport_target_stored. z = ff_q_bls_transport_target_stored * S ((S (i)) * d) + (v))) /\ ((n = E * v + s /\ exists bls_remainder_gap_bls_transport_target_division. bls_remainder_gap_bls_transport_target_division + S (s) = E))))
  19. 0019specialize htarget i
  20. 0020apply htarget
  21. 0021exact hi
  22. 0022cases hs
  23. 0023cases hs_witness
  24. 0024cases hs_witness_witness
  25. 0025cases hs_witness_witness_witness
  26. 0026cases hs_witness_witness_witness_right
  27. 0027cases hs_witness_witness_witness_right_right
  28. 0028cases ht
  29. 0029cases ht_witness
  30. 0030cases ht_witness_witness
  31. 0031cases ht_witness_witness_witness
  32. 0032cases ht_witness_witness_witness_right
  33. 0033cases ht_witness_witness_witness_right_right
  34. 0034have hD : x = x3
  35. 0035specialize pow_functional p
  36. 0036specialize pow_functional (S i)
  37. 0037specialize pow_functional x
  38. 0038specialize pow_functional x3
  39. 0039apply pow_functional
  40. 0040exact hs_witness_witness_witness_left
  41. 0041exact ht_witness_witness_witness_left
  42. 0042rewrite <- hD at ht_witness_witness_witness_right_right_left
  43. 0043rewrite <- hD at ht_witness_witness_witness_right_right_right
  44. 0044have hquotients : x1 = x4
  45. 0045specialize division_remainder_unique x
  46. 0046specialize division_remainder_unique n
  47. 0047specialize division_remainder_unique x1
  48. 0048specialize division_remainder_unique x2
  49. 0049specialize division_remainder_unique x4
  50. 0050specialize division_remainder_unique x5
  51. 0051have hdivision_unique : x1 = x4 /\ x2 = x5
  52. 0052apply division_remainder_unique
  53. 0053exact hs_witness_witness_witness_right_right_left
  54. 0054exact hs_witness_witness_witness_right_right_right
  55. 0055exact ht_witness_witness_witness_right_right_left
  56. 0056exact ht_witness_witness_witness_right_right_right
  57. 0057cases hdivision_unique
  58. 0058exact hdivision_unique_left
  59. 0059have hstored : x1 = q
  60. 0060specialize beta_at_unique b
  61. 0061specialize beta_at_unique c
  62. 0062specialize beta_at_unique i
  63. 0063specialize beta_at_unique x1
  64. 0064specialize beta_at_unique q
  65. 0065apply beta_at_unique
  66. 0066exact hs_witness_witness_witness_right_left
  67. 0067exact hq
  68. 0068rewrite <- hstored
  69. 0069rewrite hquotients
  70. 0070rewrite <- hstored
  71. 0071rewrite hquotients
  72. 0072exact ht_witness_witness_witness_right_left