BT009X · Bertrand theorem

pow_add

Stable checked-use theorem · independently kernel verified

Relational powers turn addition of exponents into multiplication.

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

∀ a. ∀ e. ∀ f. ∀ s. ∀ x. ∀ y. ∀ z. s = e + f → Pow(a,e,x) → Pow(a,f,y) → Pow(a,s,z) → z = 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

PD0020 Pow

3 occurrences

In local proof propositions

PD0020 Pow

2 occurrences

Exact expanded native-PA statement
forall a e f s x y z. s = e + f -> (exists ff_b_add_left ff_c_add_left. ((forall ff_i_add_left_repeat. (exists ff_lt_add_left_repeat_bound. ff_lt_add_left_repeat_bound + S ff_i_add_left_repeat = e) -> (((exists ff_h_add_left_repeat_decoded. ff_h_add_left_repeat_decoded + S (a) = S ((S (ff_i_add_left_repeat)) * ff_c_add_left)) /\ exists ff_q_add_left_repeat_decoded. ff_b_add_left = ff_q_add_left_repeat_decoded * S ((S (ff_i_add_left_repeat)) * ff_c_add_left) + (a)))) /\ (exists ff_u_add_left_product ff_v_add_left_product. ((((exists ff_h_add_left_product_start. ff_h_add_left_product_start + S (1) = S ((S (0)) * ff_v_add_left_product)) /\ exists ff_q_add_left_product_start. ff_u_add_left_product = ff_q_add_left_product_start * S ((S (0)) * ff_v_add_left_product) + (1))) /\ ((((exists ff_h_add_left_product_terminal. ff_h_add_left_product_terminal + S (x) = S ((S (e)) * ff_v_add_left_product)) /\ exists ff_q_add_left_product_terminal. ff_u_add_left_product = ff_q_add_left_product_terminal * S ((S (e)) * ff_v_add_left_product) + (x))) /\ forall ff_i_add_left_product. (exists ff_lt_add_left_product_bound. ff_lt_add_left_product_bound + S ff_i_add_left_product = e) -> exists ff_p_add_left_product ff_r_add_left_product ff_s_add_left_product. ((((exists ff_h_add_left_product_factor. ff_h_add_left_product_factor + S (ff_p_add_left_product) = S ((S (ff_i_add_left_product)) * ff_c_add_left)) /\ exists ff_q_add_left_product_factor. ff_b_add_left = ff_q_add_left_product_factor * S ((S (ff_i_add_left_product)) * ff_c_add_left) + (ff_p_add_left_product))) /\ ((((exists ff_h_add_left_product_partial. ff_h_add_left_product_partial + S (ff_r_add_left_product) = S ((S (ff_i_add_left_product)) * ff_v_add_left_product)) /\ exists ff_q_add_left_product_partial. ff_u_add_left_product = ff_q_add_left_product_partial * S ((S (ff_i_add_left_product)) * ff_v_add_left_product) + (ff_r_add_left_product))) /\ ((((exists ff_h_add_left_product_successor. ff_h_add_left_product_successor + S (ff_s_add_left_product) = S ((S (S ff_i_add_left_product)) * ff_v_add_left_product)) /\ exists ff_q_add_left_product_successor. ff_u_add_left_product = ff_q_add_left_product_successor * S ((S (S ff_i_add_left_product)) * ff_v_add_left_product) + (ff_s_add_left_product))) /\ ff_s_add_left_product = ff_r_add_left_product * ff_p_add_left_product)))))))) -> (exists ff_b_add_right ff_c_add_right. ((forall ff_i_add_right_repeat. (exists ff_lt_add_right_repeat_bound. ff_lt_add_right_repeat_bound + S ff_i_add_right_repeat = f) -> (((exists ff_h_add_right_repeat_decoded. ff_h_add_right_repeat_decoded + S (a) = S ((S (ff_i_add_right_repeat)) * ff_c_add_right)) /\ exists ff_q_add_right_repeat_decoded. ff_b_add_right = ff_q_add_right_repeat_decoded * S ((S (ff_i_add_right_repeat)) * ff_c_add_right) + (a)))) /\ (exists ff_u_add_right_product ff_v_add_right_product. ((((exists ff_h_add_right_product_start. ff_h_add_right_product_start + S (1) = S ((S (0)) * ff_v_add_right_product)) /\ exists ff_q_add_right_product_start. ff_u_add_right_product = ff_q_add_right_product_start * S ((S (0)) * ff_v_add_right_product) + (1))) /\ ((((exists ff_h_add_right_product_terminal. ff_h_add_right_product_terminal + S (y) = S ((S (f)) * ff_v_add_right_product)) /\ exists ff_q_add_right_product_terminal. ff_u_add_right_product = ff_q_add_right_product_terminal * S ((S (f)) * ff_v_add_right_product) + (y))) /\ forall ff_i_add_right_product. (exists ff_lt_add_right_product_bound. ff_lt_add_right_product_bound + S ff_i_add_right_product = f) -> exists ff_p_add_right_product ff_r_add_right_product ff_s_add_right_product. ((((exists ff_h_add_right_product_factor. ff_h_add_right_product_factor + S (ff_p_add_right_product) = S ((S (ff_i_add_right_product)) * ff_c_add_right)) /\ exists ff_q_add_right_product_factor. ff_b_add_right = ff_q_add_right_product_factor * S ((S (ff_i_add_right_product)) * ff_c_add_right) + (ff_p_add_right_product))) /\ ((((exists ff_h_add_right_product_partial. ff_h_add_right_product_partial + S (ff_r_add_right_product) = S ((S (ff_i_add_right_product)) * ff_v_add_right_product)) /\ exists ff_q_add_right_product_partial. ff_u_add_right_product = ff_q_add_right_product_partial * S ((S (ff_i_add_right_product)) * ff_v_add_right_product) + (ff_r_add_right_product))) /\ ((((exists ff_h_add_right_product_successor. ff_h_add_right_product_successor + S (ff_s_add_right_product) = S ((S (S ff_i_add_right_product)) * ff_v_add_right_product)) /\ exists ff_q_add_right_product_successor. ff_u_add_right_product = ff_q_add_right_product_successor * S ((S (S ff_i_add_right_product)) * ff_v_add_right_product) + (ff_s_add_right_product))) /\ ff_s_add_right_product = ff_r_add_right_product * ff_p_add_right_product)))))))) -> (exists ff_b_add_total ff_c_add_total. ((forall ff_i_add_total_repeat. (exists ff_lt_add_total_repeat_bound. ff_lt_add_total_repeat_bound + S ff_i_add_total_repeat = s) -> (((exists ff_h_add_total_repeat_decoded. ff_h_add_total_repeat_decoded + S (a) = S ((S (ff_i_add_total_repeat)) * ff_c_add_total)) /\ exists ff_q_add_total_repeat_decoded. ff_b_add_total = ff_q_add_total_repeat_decoded * S ((S (ff_i_add_total_repeat)) * ff_c_add_total) + (a)))) /\ (exists ff_u_add_total_product ff_v_add_total_product. ((((exists ff_h_add_total_product_start. ff_h_add_total_product_start + S (1) = S ((S (0)) * ff_v_add_total_product)) /\ exists ff_q_add_total_product_start. ff_u_add_total_product = ff_q_add_total_product_start * S ((S (0)) * ff_v_add_total_product) + (1))) /\ ((((exists ff_h_add_total_product_terminal. ff_h_add_total_product_terminal + S (z) = S ((S (s)) * ff_v_add_total_product)) /\ exists ff_q_add_total_product_terminal. ff_u_add_total_product = ff_q_add_total_product_terminal * S ((S (s)) * ff_v_add_total_product) + (z))) /\ forall ff_i_add_total_product. (exists ff_lt_add_total_product_bound. ff_lt_add_total_product_bound + S ff_i_add_total_product = s) -> exists ff_p_add_total_product ff_r_add_total_product ff_s_add_total_product. ((((exists ff_h_add_total_product_factor. ff_h_add_total_product_factor + S (ff_p_add_total_product) = S ((S (ff_i_add_total_product)) * ff_c_add_total)) /\ exists ff_q_add_total_product_factor. ff_b_add_total = ff_q_add_total_product_factor * S ((S (ff_i_add_total_product)) * ff_c_add_total) + (ff_p_add_total_product))) /\ ((((exists ff_h_add_total_product_partial. ff_h_add_total_product_partial + S (ff_r_add_total_product) = S ((S (ff_i_add_total_product)) * ff_v_add_total_product)) /\ exists ff_q_add_total_product_partial. ff_u_add_total_product = ff_q_add_total_product_partial * S ((S (ff_i_add_total_product)) * ff_v_add_total_product) + (ff_r_add_total_product))) /\ ((((exists ff_h_add_total_product_successor. ff_h_add_total_product_successor + S (ff_s_add_total_product) = S ((S (S ff_i_add_total_product)) * ff_v_add_total_product)) /\ exists ff_q_add_total_product_successor. ff_u_add_total_product = ff_q_add_total_product_successor * S ((S (S ff_i_add_total_product)) * ff_v_add_total_product) + (ff_s_add_total_product))) /\ ff_s_add_total_product = ff_r_add_total_product * ff_p_add_total_product)))))))) -> z = x * y

Proof neighborhood

Direct theorem prerequisites

BT0081 pow_zero BT0082 pow_functional BT0083 pow_successor_decompose BT000A mul_one BT0008 mul_assoc

Direct theorem dependents

BT00QK power_divides_exponent_antitone BT00QL power_divides_add_mul BT00QQ power_valuation_mul_successor_not_divides BT00SM pow_mul_exp_from_total BT00SN pow_exponent_monotone_from_total BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00VV primorial_le_four_pow_bounded BT00W5 pow_eleven_two_le_pow_two_seven_from_total BT00W6 pow_six_ten_le_pow_four_thirteen_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WH pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total BT00WJ pow_two_successor_double_le_pow_four_successor_from_total BT00WP bertrand_h_root_32_from_total BT00WQ bertrand_h_root_33_from_total BT00WS bertrand_h_root_35_from_total BT00WT bertrand_h_root_36_from_total BT00WU bertrand_h_root_37_from_total BT00WV bertrand_j_base_thirty_two_window_from_total BT00X4 bertrand_floor_power_product_le_h_from_total BT00X5 bertrand_four_power_product_le_of_sum_from_total BT00XJ pow_le_pow_of_exponent_le

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

90 script commands · 22 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 (5)
pow zeropow functionalpow successor decomposemul onemul assoc
01Fix variables and assumptionsL1–2

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

  1. L1
    intro a
  2. L2
    intro e
02Induction on fL3–12

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

  1. L3
    induction f
  2. L4
    intro s
  3. L5
    intro x
  4. L6
    intro y
  5. L7
    intro z
  6. L8
    intro hs
  7. L9
    intro hx
  8. L10
    intro hy
  9. L11
    intro hz
  10. L12
    rewrite PA3 at hs
03Calculate and transport equalitiesL13–16

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

  1. L13
    rewrite hs at hz
  2. L14
    rewrite hs at hz
  3. L15
    rewrite hs at hz
  4. L16
    rewrite hs at hz
04Establish hzxL17–24

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

  1. L17
    have hzx : z = x
  2. L18
    specialize pow_functional a
  3. L19
    specialize pow_functional e
  4. L20
    specialize pow_functional z
  5. L21
    specialize pow_functional x
  6. L22
    apply pow_functional
  7. L23
    exact hz
  8. L24
    exact hx
05Establish hy1L25–34

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

  1. L25
    have hy1 : y = 1
  2. L26
    specialize pow_zero a
  3. L27
    specialize pow_zero 0
  4. L28
    specialize pow_zero y
  5. L29
    apply pow_zero
  6. L30
    refl
  7. L31
    exact hy
  8. L32
    rewrite hzx
  9. L33
    rewrite hy1
  10. L34
    specialize mul_one x
06Calculate and transport equalitiesL35–35

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

  1. L35
    symm
07Use earlier factsL36–36

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

  1. L36
    exact mul_one
08Fix variables and assumptionsL37–44

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

  1. L37
    intro s
  2. L38
    intro x
  3. L39
    intro y
  4. L40
    intro z
  5. L41
    intro hs
  6. L42
    intro hx
  7. L43
    intro hy
  8. L44
    intro hz
09Establish hy_stepL45–52

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

  1. L45
    have hy_step : ∃ r. Pow(a,f,r) ∧ y = r · aDefinitions: Pow(a,f,r)Original native command in the exact edition
  2. L46
    specialize pow_successor_decompose a
  3. L47
    specialize pow_successor_decompose f
  4. L48
    specialize pow_successor_decompose (S f)
  5. L49
    specialize pow_successor_decompose y
  6. L50
    apply pow_successor_decompose
  7. L51
    refl
  8. L52
    exact hy
10Separate the logical casesL53–54

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

  1. L53
    cases hy_step
  2. L54
    cases hy_step_witness
11Establish hstL55–58

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

  1. L55
    have hst : s = S (e + f)
  2. L56
    trans e + S f
  3. L57
    exact hs
  4. L58
    apply PA4
12Establish hz_stepL59–66

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

  1. L59
    have hz_step : ∃ r. Pow(a,e + f,r) ∧ z = r · aDefinitions: Pow(a,e + f,r)Original native command in the exact edition
  2. L60
    specialize pow_successor_decompose a
  3. L61
    specialize pow_successor_decompose (e + f)
  4. L62
    specialize pow_successor_decompose s
  5. L63
    specialize pow_successor_decompose z
  6. L64
    apply pow_successor_decompose
  7. L65
    exact hst
  8. L66
    exact hz
13Separate the logical casesL67–68

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

  1. L67
    cases hz_step
  2. L68
    cases hz_step_witness
14Establish hprefixL69–78

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

  1. L69
    have hprefix : x2 = x * x1
  2. L70
    specialize IH (e + f)
  3. L71
    specialize IH x
  4. L72
    specialize IH x1
  5. L73
    specialize IH x2
  6. L74
    apply IH
  7. L75
    refl
  8. L76
    exact hx
  9. L77
    exact hy_step_witness_left
  10. L78
    exact hz_step_witness_left
15Calculate and transport equalitiesL79–79

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

  1. L79
    trans x2 * a
16Use earlier factsL80–80

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

  1. L80
    exact hz_step_witness_right
17Calculate and transport equalitiesL81–82

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

  1. L81
    trans (x * x1) * a
  2. L82
    congr
18Use earlier factsL83–83

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

  1. L83
    exact hprefix
19Calculate and transport equalitiesL84–85

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

  1. L84
    refl
  2. L85
    trans x * (x1 * a)
20Use earlier factsL86–86

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

  1. L86
    apply mul_assoc
21Calculate and transport equalitiesL87–89

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

  1. L87
    congr
  2. L88
    refl
  3. L89
    symm
22Use earlier factsL90–90

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

  1. L90
    exact hy_step_witness_right

Library-wide reading audit

Original defined command ledger · 90 lines
  1. 0001intro a
  2. 0002intro e
  3. 0003induction f
  4. 0004intro s
  5. 0005intro x
  6. 0006intro y
  7. 0007intro z
  8. 0008intro hs
  9. 0009intro hx
  10. 0010intro hy
  11. 0011intro hz
  12. 0012rewrite PA3 at hs
  13. 0013rewrite hs at hz
  14. 0014rewrite hs at hz
  15. 0015rewrite hs at hz
  16. 0016rewrite hs at hz
  17. 0017have hzx : z = x
  18. 0018specialize pow_functional a
  19. 0019specialize pow_functional e
  20. 0020specialize pow_functional z
  21. 0021specialize pow_functional x
  22. 0022apply pow_functional
  23. 0023exact hz
  24. 0024exact hx
  25. 0025have hy1 : y = 1
  26. 0026specialize pow_zero a
  27. 0027specialize pow_zero 0
  28. 0028specialize pow_zero y
  29. 0029apply pow_zero
  30. 0030refl
  31. 0031exact hy
  32. 0032rewrite hzx
  33. 0033rewrite hy1
  34. 0034specialize mul_one x
  35. 0035symm
  36. 0036exact mul_one
  37. 0037intro s
  38. 0038intro x
  39. 0039intro y
  40. 0040intro z
  41. 0041intro hs
  42. 0042intro hx
  43. 0043intro hy
  44. 0044intro hz
  45. 0045have hy_step : ∃ r. Pow(a,f,r) ∧ y = r · a
    Exact native replay linehave hy_step : exists r. (exists ff_b_add_y_prefix ff_c_add_y_prefix. ((forall ff_i_add_y_prefix_repeat. (exists ff_lt_add_y_prefix_repeat_bound. ff_lt_add_y_prefix_repeat_bound + S ff_i_add_y_prefix_repeat = f) -> (((exists ff_h_add_y_prefix_repeat_decoded. ff_h_add_y_prefix_repeat_decoded + S (a) = S ((S (ff_i_add_y_prefix_repeat)) * ff_c_add_y_prefix)) /\ exists ff_q_add_y_prefix_repeat_decoded. ff_b_add_y_prefix = ff_q_add_y_prefix_repeat_decoded * S ((S (ff_i_add_y_prefix_repeat)) * ff_c_add_y_prefix) + (a)))) /\ (exists ff_u_add_y_prefix_product ff_v_add_y_prefix_product. ((((exists ff_h_add_y_prefix_product_start. ff_h_add_y_prefix_product_start + S (1) = S ((S (0)) * ff_v_add_y_prefix_product)) /\ exists ff_q_add_y_prefix_product_start. ff_u_add_y_prefix_product = ff_q_add_y_prefix_product_start * S ((S (0)) * ff_v_add_y_prefix_product) + (1))) /\ ((((exists ff_h_add_y_prefix_product_terminal. ff_h_add_y_prefix_product_terminal + S (r) = S ((S (f)) * ff_v_add_y_prefix_product)) /\ exists ff_q_add_y_prefix_product_terminal. ff_u_add_y_prefix_product = ff_q_add_y_prefix_product_terminal * S ((S (f)) * ff_v_add_y_prefix_product) + (r))) /\ forall ff_i_add_y_prefix_product. (exists ff_lt_add_y_prefix_product_bound. ff_lt_add_y_prefix_product_bound + S ff_i_add_y_prefix_product = f) -> exists ff_p_add_y_prefix_product ff_r_add_y_prefix_product ff_s_add_y_prefix_product. ((((exists ff_h_add_y_prefix_product_factor. ff_h_add_y_prefix_product_factor + S (ff_p_add_y_prefix_product) = S ((S (ff_i_add_y_prefix_product)) * ff_c_add_y_prefix)) /\ exists ff_q_add_y_prefix_product_factor. ff_b_add_y_prefix = ff_q_add_y_prefix_product_factor * S ((S (ff_i_add_y_prefix_product)) * ff_c_add_y_prefix) + (ff_p_add_y_prefix_product))) /\ ((((exists ff_h_add_y_prefix_product_partial. ff_h_add_y_prefix_product_partial + S (ff_r_add_y_prefix_product) = S ((S (ff_i_add_y_prefix_product)) * ff_v_add_y_prefix_product)) /\ exists ff_q_add_y_prefix_product_partial. ff_u_add_y_prefix_product = ff_q_add_y_prefix_product_partial * S ((S (ff_i_add_y_prefix_product)) * ff_v_add_y_prefix_product) + (ff_r_add_y_prefix_product))) /\ ((((exists ff_h_add_y_prefix_product_successor. ff_h_add_y_prefix_product_successor + S (ff_s_add_y_prefix_product) = S ((S (S ff_i_add_y_prefix_product)) * ff_v_add_y_prefix_product)) /\ exists ff_q_add_y_prefix_product_successor. ff_u_add_y_prefix_product = ff_q_add_y_prefix_product_successor * S ((S (S ff_i_add_y_prefix_product)) * ff_v_add_y_prefix_product) + (ff_s_add_y_prefix_product))) /\ ff_s_add_y_prefix_product = ff_r_add_y_prefix_product * ff_p_add_y_prefix_product)))))))) /\ y = r * a
  46. 0046specialize pow_successor_decompose a
  47. 0047specialize pow_successor_decompose f
  48. 0048specialize pow_successor_decompose (S f)
  49. 0049specialize pow_successor_decompose y
  50. 0050apply pow_successor_decompose
  51. 0051refl
  52. 0052exact hy
  53. 0053cases hy_step
  54. 0054cases hy_step_witness
  55. 0055have hst : s = S (e + f)
  56. 0056trans e + S f
  57. 0057exact hs
  58. 0058apply PA4
  59. 0059have hz_step : ∃ r. Pow(a,e + f,r) ∧ z = r · a
    Exact native replay linehave hz_step : exists r. (exists pa_b_add_z_prefix pa_c_add_z_prefix. ((forall pa_i_add_z_prefix_repeat. (exists pa_lt_add_z_prefix_repeat_bound. pa_lt_add_z_prefix_repeat_bound + S pa_i_add_z_prefix_repeat = e + f) -> (((exists pa_h_add_z_prefix_repeat_decoded. pa_h_add_z_prefix_repeat_decoded + S (a) = S ((S (pa_i_add_z_prefix_repeat)) * pa_c_add_z_prefix)) /\ exists pa_q_add_z_prefix_repeat_decoded. pa_b_add_z_prefix = pa_q_add_z_prefix_repeat_decoded * S ((S (pa_i_add_z_prefix_repeat)) * pa_c_add_z_prefix) + (a)))) /\ (exists pa_u_add_z_prefix_product pa_v_add_z_prefix_product. ((((exists pa_h_add_z_prefix_product_start. pa_h_add_z_prefix_product_start + S (1) = S ((S (0)) * pa_v_add_z_prefix_product)) /\ exists pa_q_add_z_prefix_product_start. pa_u_add_z_prefix_product = pa_q_add_z_prefix_product_start * S ((S (0)) * pa_v_add_z_prefix_product) + (1))) /\ ((((exists pa_h_add_z_prefix_product_terminal. pa_h_add_z_prefix_product_terminal + S (r) = S ((S (e + f)) * pa_v_add_z_prefix_product)) /\ exists pa_q_add_z_prefix_product_terminal. pa_u_add_z_prefix_product = pa_q_add_z_prefix_product_terminal * S ((S (e + f)) * pa_v_add_z_prefix_product) + (r))) /\ forall pa_i_add_z_prefix_product. (exists pa_lt_add_z_prefix_product_bound. pa_lt_add_z_prefix_product_bound + S pa_i_add_z_prefix_product = e + f) -> exists pa_p_add_z_prefix_product pa_r_add_z_prefix_product pa_s_add_z_prefix_product. ((((exists pa_h_add_z_prefix_product_factor. pa_h_add_z_prefix_product_factor + S (pa_p_add_z_prefix_product) = S ((S (pa_i_add_z_prefix_product)) * pa_c_add_z_prefix)) /\ exists pa_q_add_z_prefix_product_factor. pa_b_add_z_prefix = pa_q_add_z_prefix_product_factor * S ((S (pa_i_add_z_prefix_product)) * pa_c_add_z_prefix) + (pa_p_add_z_prefix_product))) /\ ((((exists pa_h_add_z_prefix_product_partial. pa_h_add_z_prefix_product_partial + S (pa_r_add_z_prefix_product) = S ((S (pa_i_add_z_prefix_product)) * pa_v_add_z_prefix_product)) /\ exists pa_q_add_z_prefix_product_partial. pa_u_add_z_prefix_product = pa_q_add_z_prefix_product_partial * S ((S (pa_i_add_z_prefix_product)) * pa_v_add_z_prefix_product) + (pa_r_add_z_prefix_product))) /\ ((((exists pa_h_add_z_prefix_product_successor. pa_h_add_z_prefix_product_successor + S (pa_s_add_z_prefix_product) = S ((S (S pa_i_add_z_prefix_product)) * pa_v_add_z_prefix_product)) /\ exists pa_q_add_z_prefix_product_successor. pa_u_add_z_prefix_product = pa_q_add_z_prefix_product_successor * S ((S (S pa_i_add_z_prefix_product)) * pa_v_add_z_prefix_product) + (pa_s_add_z_prefix_product))) /\ pa_s_add_z_prefix_product = pa_r_add_z_prefix_product * pa_p_add_z_prefix_product)))))))) /\ z = r * a
  60. 0060specialize pow_successor_decompose a
  61. 0061specialize pow_successor_decompose (e + f)
  62. 0062specialize pow_successor_decompose s
  63. 0063specialize pow_successor_decompose z
  64. 0064apply pow_successor_decompose
  65. 0065exact hst
  66. 0066exact hz
  67. 0067cases hz_step
  68. 0068cases hz_step_witness
  69. 0069have hprefix : x2 = x * x1
  70. 0070specialize IH (e + f)
  71. 0071specialize IH x
  72. 0072specialize IH x1
  73. 0073specialize IH x2
  74. 0074apply IH
  75. 0075refl
  76. 0076exact hx
  77. 0077exact hy_step_witness_left
  78. 0078exact hz_step_witness_left
  79. 0079trans x2 * a
  80. 0080exact hz_step_witness_right
  81. 0081trans (x * x1) * a
  82. 0082congr
  83. 0083exact hprefix
  84. 0084refl
  85. 0085trans x * (x1 * a)
  86. 0086apply mul_assoc
  87. 0087congr
  88. 0088refl
  89. 0089symm
  90. 0090exact hy_step_witness_right