BT0095

pow_successor_pair_mul

Stable checked-use theorem · independently kernel verified

A successor power paired with its predecessor equals predecessor times base.

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.

Exact expanded PA statement

forall a e se r n. se = S e -> (exists ff_b_pair_predecessor ff_c_pair_predecessor. ((forall ff_i_pair_predecessor_repeat. (exists ff_lt_pair_predecessor_repeat_bound. ff_lt_pair_predecessor_repeat_bound + S ff_i_pair_predecessor_repeat = e) -> (((exists ff_h_pair_predecessor_repeat_decoded. ff_h_pair_predecessor_repeat_decoded + S (a) = S ((S (ff_i_pair_predecessor_repeat)) * ff_c_pair_predecessor)) /\ exists ff_q_pair_predecessor_repeat_decoded. ff_b_pair_predecessor = ff_q_pair_predecessor_repeat_decoded * S ((S (ff_i_pair_predecessor_repeat)) * ff_c_pair_predecessor) + (a)))) /\ (exists ff_u_pair_predecessor_product ff_v_pair_predecessor_product. ((((exists ff_h_pair_predecessor_product_start. ff_h_pair_predecessor_product_start + S (1) = S ((S (0)) * ff_v_pair_predecessor_product)) /\ exists ff_q_pair_predecessor_product_start. ff_u_pair_predecessor_product = ff_q_pair_predecessor_product_start * S ((S (0)) * ff_v_pair_predecessor_product) + (1))) /\ ((((exists ff_h_pair_predecessor_product_terminal. ff_h_pair_predecessor_product_terminal + S (r) = S ((S (e)) * ff_v_pair_predecessor_product)) /\ exists ff_q_pair_predecessor_product_terminal. ff_u_pair_predecessor_product = ff_q_pair_predecessor_product_terminal * S ((S (e)) * ff_v_pair_predecessor_product) + (r))) /\ forall ff_i_pair_predecessor_product. (exists ff_lt_pair_predecessor_product_bound. ff_lt_pair_predecessor_product_bound + S ff_i_pair_predecessor_product = e) -> exists ff_p_pair_predecessor_product ff_r_pair_predecessor_product ff_s_pair_predecessor_product. ((((exists ff_h_pair_predecessor_product_factor. ff_h_pair_predecessor_product_factor + S (ff_p_pair_predecessor_product) = S ((S (ff_i_pair_predecessor_product)) * ff_c_pair_predecessor)) /\ exists ff_q_pair_predecessor_product_factor. ff_b_pair_predecessor = ff_q_pair_predecessor_product_factor * S ((S (ff_i_pair_predecessor_product)) * ff_c_pair_predecessor) + (ff_p_pair_predecessor_product))) /\ ((((exists ff_h_pair_predecessor_product_partial. ff_h_pair_predecessor_product_partial + S (ff_r_pair_predecessor_product) = S ((S (ff_i_pair_predecessor_product)) * ff_v_pair_predecessor_product)) /\ exists ff_q_pair_predecessor_product_partial. ff_u_pair_predecessor_product = ff_q_pair_predecessor_product_partial * S ((S (ff_i_pair_predecessor_product)) * ff_v_pair_predecessor_product) + (ff_r_pair_predecessor_product))) /\ ((((exists ff_h_pair_predecessor_product_successor. ff_h_pair_predecessor_product_successor + S (ff_s_pair_predecessor_product) = S ((S (S ff_i_pair_predecessor_product)) * ff_v_pair_predecessor_product)) /\ exists ff_q_pair_predecessor_product_successor. ff_u_pair_predecessor_product = ff_q_pair_predecessor_product_successor * S ((S (S ff_i_pair_predecessor_product)) * ff_v_pair_predecessor_product) + (ff_s_pair_predecessor_product))) /\ ff_s_pair_predecessor_product = ff_r_pair_predecessor_product * ff_p_pair_predecessor_product)))))))) -> (exists ff_b_pair_successor ff_c_pair_successor. ((forall ff_i_pair_successor_repeat. (exists ff_lt_pair_successor_repeat_bound. ff_lt_pair_successor_repeat_bound + S ff_i_pair_successor_repeat = se) -> (((exists ff_h_pair_successor_repeat_decoded. ff_h_pair_successor_repeat_decoded + S (a) = S ((S (ff_i_pair_successor_repeat)) * ff_c_pair_successor)) /\ exists ff_q_pair_successor_repeat_decoded. ff_b_pair_successor = ff_q_pair_successor_repeat_decoded * S ((S (ff_i_pair_successor_repeat)) * ff_c_pair_successor) + (a)))) /\ (exists ff_u_pair_successor_product ff_v_pair_successor_product. ((((exists ff_h_pair_successor_product_start. ff_h_pair_successor_product_start + S (1) = S ((S (0)) * ff_v_pair_successor_product)) /\ exists ff_q_pair_successor_product_start. ff_u_pair_successor_product = ff_q_pair_successor_product_start * S ((S (0)) * ff_v_pair_successor_product) + (1))) /\ ((((exists ff_h_pair_successor_product_terminal. ff_h_pair_successor_product_terminal + S (n) = S ((S (se)) * ff_v_pair_successor_product)) /\ exists ff_q_pair_successor_product_terminal. ff_u_pair_successor_product = ff_q_pair_successor_product_terminal * S ((S (se)) * ff_v_pair_successor_product) + (n))) /\ forall ff_i_pair_successor_product. (exists ff_lt_pair_successor_product_bound. ff_lt_pair_successor_product_bound + S ff_i_pair_successor_product = se) -> exists ff_p_pair_successor_product ff_r_pair_successor_product ff_s_pair_successor_product. ((((exists ff_h_pair_successor_product_factor. ff_h_pair_successor_product_factor + S (ff_p_pair_successor_product) = S ((S (ff_i_pair_successor_product)) * ff_c_pair_successor)) /\ exists ff_q_pair_successor_product_factor. ff_b_pair_successor = ff_q_pair_successor_product_factor * S ((S (ff_i_pair_successor_product)) * ff_c_pair_successor) + (ff_p_pair_successor_product))) /\ ((((exists ff_h_pair_successor_product_partial. ff_h_pair_successor_product_partial + S (ff_r_pair_successor_product) = S ((S (ff_i_pair_successor_product)) * ff_v_pair_successor_product)) /\ exists ff_q_pair_successor_product_partial. ff_u_pair_successor_product = ff_q_pair_successor_product_partial * S ((S (ff_i_pair_successor_product)) * ff_v_pair_successor_product) + (ff_r_pair_successor_product))) /\ ((((exists ff_h_pair_successor_product_successor. ff_h_pair_successor_product_successor + S (ff_s_pair_successor_product) = S ((S (S ff_i_pair_successor_product)) * ff_v_pair_successor_product)) /\ exists ff_q_pair_successor_product_successor. ff_u_pair_successor_product = ff_q_pair_successor_product_successor * S ((S (S ff_i_pair_successor_product)) * ff_v_pair_successor_product) + (ff_s_pair_successor_product))) /\ ff_s_pair_successor_product = ff_r_pair_successor_product * ff_p_pair_successor_product)))))))) -> n = r * a

Structural proof guide

A successor power paired with its predecessor equals predecessor times base.

Direct prerequisites: pow_successor_decompose, pow_functional. The authored body proceeds by case analysis (2), intermediate claims (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT0083 pow_successor_decompose BT0082 pow_functional

Direct dependents

BT00QM power_divides_successor_of_cofactor BT00QN prime_power_successor_cancel_cofactor BT00S5 pow_successor_compose BT00SL pow_successor_compose_from_total

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

30 script commands · 5 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.

Named ingredients (2)
pow successor decomposepow functional

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–8

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

  1. L1
    intro a
  2. L2
    intro e
  3. L3
    intro se
  4. L4
    intro r
  5. L5
    intro n
  6. L6
    intro hse
  7. L7
    intro hprevious
  8. L8
    intro hsuccessor
02Establish hstepL9–16

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

  1. L9
    have hstep : ∃ z. Pow(a,e,z) ∧ n = z · aDefinitions: Pow
  2. L10
    specialize pow_successor_decompose a
  3. L11
    specialize pow_successor_decompose e
  4. L12
    specialize pow_successor_decompose se
  5. L13
    specialize pow_successor_decompose n
  6. L14
    apply pow_successor_decompose
  7. L15
    exact hse
  8. L16
    exact hsuccessor
03Separate the logical casesL17–18

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

  1. L17
    cases hstep
  2. L18
    cases hstep_witness
04Establish hzL19–28

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

  1. L19
    have hz : x = r
  2. L20
    specialize pow_functional a
  3. L21
    specialize pow_functional e
  4. L22
    specialize pow_functional x
  5. L23
    specialize pow_functional r
  6. L24
    apply pow_functional
  7. L25
    exact hstep_witness_left
  8. L26
    exact hprevious
  9. L27
    trans x * a
  10. L28
    exact hstep_witness_right
05Calculate and transport equalitiesL29–30

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

  1. L29
    rewrite hz
  2. L30
    refl

Library-wide reading audit

Original exact command ledger · 30 lines
  1. 0001intro a
  2. 0002intro e
  3. 0003intro se
  4. 0004intro r
  5. 0005intro n
  6. 0006intro hse
  7. 0007intro hprevious
  8. 0008intro hsuccessor
  9. 0009have hstep : exists z. (exists ff_b_pair_decomposed ff_c_pair_decomposed. ((forall ff_i_pair_decomposed_repeat. (exists ff_lt_pair_decomposed_repeat_bound. ff_lt_pair_decomposed_repeat_bound + S ff_i_pair_decomposed_repeat = e) -> (((exists ff_h_pair_decomposed_repeat_decoded. ff_h_pair_decomposed_repeat_decoded + S (a) = S ((S (ff_i_pair_decomposed_repeat)) * ff_c_pair_decomposed)) /\ exists ff_q_pair_decomposed_repeat_decoded. ff_b_pair_decomposed = ff_q_pair_decomposed_repeat_decoded * S ((S (ff_i_pair_decomposed_repeat)) * ff_c_pair_decomposed) + (a)))) /\ (exists ff_u_pair_decomposed_product ff_v_pair_decomposed_product. ((((exists ff_h_pair_decomposed_product_start. ff_h_pair_decomposed_product_start + S (1) = S ((S (0)) * ff_v_pair_decomposed_product)) /\ exists ff_q_pair_decomposed_product_start. ff_u_pair_decomposed_product = ff_q_pair_decomposed_product_start * S ((S (0)) * ff_v_pair_decomposed_product) + (1))) /\ ((((exists ff_h_pair_decomposed_product_terminal. ff_h_pair_decomposed_product_terminal + S (z) = S ((S (e)) * ff_v_pair_decomposed_product)) /\ exists ff_q_pair_decomposed_product_terminal. ff_u_pair_decomposed_product = ff_q_pair_decomposed_product_terminal * S ((S (e)) * ff_v_pair_decomposed_product) + (z))) /\ forall ff_i_pair_decomposed_product. (exists ff_lt_pair_decomposed_product_bound. ff_lt_pair_decomposed_product_bound + S ff_i_pair_decomposed_product = e) -> exists ff_p_pair_decomposed_product ff_r_pair_decomposed_product ff_s_pair_decomposed_product. ((((exists ff_h_pair_decomposed_product_factor. ff_h_pair_decomposed_product_factor + S (ff_p_pair_decomposed_product) = S ((S (ff_i_pair_decomposed_product)) * ff_c_pair_decomposed)) /\ exists ff_q_pair_decomposed_product_factor. ff_b_pair_decomposed = ff_q_pair_decomposed_product_factor * S ((S (ff_i_pair_decomposed_product)) * ff_c_pair_decomposed) + (ff_p_pair_decomposed_product))) /\ ((((exists ff_h_pair_decomposed_product_partial. ff_h_pair_decomposed_product_partial + S (ff_r_pair_decomposed_product) = S ((S (ff_i_pair_decomposed_product)) * ff_v_pair_decomposed_product)) /\ exists ff_q_pair_decomposed_product_partial. ff_u_pair_decomposed_product = ff_q_pair_decomposed_product_partial * S ((S (ff_i_pair_decomposed_product)) * ff_v_pair_decomposed_product) + (ff_r_pair_decomposed_product))) /\ ((((exists ff_h_pair_decomposed_product_successor. ff_h_pair_decomposed_product_successor + S (ff_s_pair_decomposed_product) = S ((S (S ff_i_pair_decomposed_product)) * ff_v_pair_decomposed_product)) /\ exists ff_q_pair_decomposed_product_successor. ff_u_pair_decomposed_product = ff_q_pair_decomposed_product_successor * S ((S (S ff_i_pair_decomposed_product)) * ff_v_pair_decomposed_product) + (ff_s_pair_decomposed_product))) /\ ff_s_pair_decomposed_product = ff_r_pair_decomposed_product * ff_p_pair_decomposed_product)))))))) /\ n = z * a
  10. 0010specialize pow_successor_decompose a
  11. 0011specialize pow_successor_decompose e
  12. 0012specialize pow_successor_decompose se
  13. 0013specialize pow_successor_decompose n
  14. 0014apply pow_successor_decompose
  15. 0015exact hse
  16. 0016exact hsuccessor
  17. 0017cases hstep
  18. 0018cases hstep_witness
  19. 0019have hz : x = r
  20. 0020specialize pow_functional a
  21. 0021specialize pow_functional e
  22. 0022specialize pow_functional x
  23. 0023specialize pow_functional r
  24. 0024apply pow_functional
  25. 0025exact hstep_witness_left
  26. 0026exact hprevious
  27. 0027trans x * a
  28. 0028exact hstep_witness_right
  29. 0029rewrite hz
  30. 0030refl