BT00QV · Bertrand theorem

pow_mul_base

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

A relational power of a product is the product of the powers.

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. ∀ b. ∀ e. ∀ x. ∀ y. ∀ z. Pow(a,e,x) → Pow(b,e,y) → Pow(a · b,e,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

3 occurrences

Exact expanded native-PA statement
forall a b e x y z. (exists ff_b_bie_mul_left ff_c_bie_mul_left. ((forall ff_i_bie_mul_left_repeat. (exists ff_lt_bie_mul_left_repeat_bound. ff_lt_bie_mul_left_repeat_bound + S ff_i_bie_mul_left_repeat = e) -> (((exists ff_h_bie_mul_left_repeat_decoded. ff_h_bie_mul_left_repeat_decoded + S (a) = S ((S (ff_i_bie_mul_left_repeat)) * ff_c_bie_mul_left)) /\ exists ff_q_bie_mul_left_repeat_decoded. ff_b_bie_mul_left = ff_q_bie_mul_left_repeat_decoded * S ((S (ff_i_bie_mul_left_repeat)) * ff_c_bie_mul_left) + (a)))) /\ (exists ff_u_bie_mul_left_product ff_v_bie_mul_left_product. ((((exists ff_h_bie_mul_left_product_start. ff_h_bie_mul_left_product_start + S (1) = S ((S (0)) * ff_v_bie_mul_left_product)) /\ exists ff_q_bie_mul_left_product_start. ff_u_bie_mul_left_product = ff_q_bie_mul_left_product_start * S ((S (0)) * ff_v_bie_mul_left_product) + (1))) /\ ((((exists ff_h_bie_mul_left_product_terminal. ff_h_bie_mul_left_product_terminal + S (x) = S ((S (e)) * ff_v_bie_mul_left_product)) /\ exists ff_q_bie_mul_left_product_terminal. ff_u_bie_mul_left_product = ff_q_bie_mul_left_product_terminal * S ((S (e)) * ff_v_bie_mul_left_product) + (x))) /\ forall ff_i_bie_mul_left_product. (exists ff_lt_bie_mul_left_product_bound. ff_lt_bie_mul_left_product_bound + S ff_i_bie_mul_left_product = e) -> exists ff_p_bie_mul_left_product ff_r_bie_mul_left_product ff_s_bie_mul_left_product. ((((exists ff_h_bie_mul_left_product_factor. ff_h_bie_mul_left_product_factor + S (ff_p_bie_mul_left_product) = S ((S (ff_i_bie_mul_left_product)) * ff_c_bie_mul_left)) /\ exists ff_q_bie_mul_left_product_factor. ff_b_bie_mul_left = ff_q_bie_mul_left_product_factor * S ((S (ff_i_bie_mul_left_product)) * ff_c_bie_mul_left) + (ff_p_bie_mul_left_product))) /\ ((((exists ff_h_bie_mul_left_product_partial. ff_h_bie_mul_left_product_partial + S (ff_r_bie_mul_left_product) = S ((S (ff_i_bie_mul_left_product)) * ff_v_bie_mul_left_product)) /\ exists ff_q_bie_mul_left_product_partial. ff_u_bie_mul_left_product = ff_q_bie_mul_left_product_partial * S ((S (ff_i_bie_mul_left_product)) * ff_v_bie_mul_left_product) + (ff_r_bie_mul_left_product))) /\ ((((exists ff_h_bie_mul_left_product_successor. ff_h_bie_mul_left_product_successor + S (ff_s_bie_mul_left_product) = S ((S (S ff_i_bie_mul_left_product)) * ff_v_bie_mul_left_product)) /\ exists ff_q_bie_mul_left_product_successor. ff_u_bie_mul_left_product = ff_q_bie_mul_left_product_successor * S ((S (S ff_i_bie_mul_left_product)) * ff_v_bie_mul_left_product) + (ff_s_bie_mul_left_product))) /\ ff_s_bie_mul_left_product = ff_r_bie_mul_left_product * ff_p_bie_mul_left_product)))))))) -> (exists ff_b_bie_mul_right ff_c_bie_mul_right. ((forall ff_i_bie_mul_right_repeat. (exists ff_lt_bie_mul_right_repeat_bound. ff_lt_bie_mul_right_repeat_bound + S ff_i_bie_mul_right_repeat = e) -> (((exists ff_h_bie_mul_right_repeat_decoded. ff_h_bie_mul_right_repeat_decoded + S (b) = S ((S (ff_i_bie_mul_right_repeat)) * ff_c_bie_mul_right)) /\ exists ff_q_bie_mul_right_repeat_decoded. ff_b_bie_mul_right = ff_q_bie_mul_right_repeat_decoded * S ((S (ff_i_bie_mul_right_repeat)) * ff_c_bie_mul_right) + (b)))) /\ (exists ff_u_bie_mul_right_product ff_v_bie_mul_right_product. ((((exists ff_h_bie_mul_right_product_start. ff_h_bie_mul_right_product_start + S (1) = S ((S (0)) * ff_v_bie_mul_right_product)) /\ exists ff_q_bie_mul_right_product_start. ff_u_bie_mul_right_product = ff_q_bie_mul_right_product_start * S ((S (0)) * ff_v_bie_mul_right_product) + (1))) /\ ((((exists ff_h_bie_mul_right_product_terminal. ff_h_bie_mul_right_product_terminal + S (y) = S ((S (e)) * ff_v_bie_mul_right_product)) /\ exists ff_q_bie_mul_right_product_terminal. ff_u_bie_mul_right_product = ff_q_bie_mul_right_product_terminal * S ((S (e)) * ff_v_bie_mul_right_product) + (y))) /\ forall ff_i_bie_mul_right_product. (exists ff_lt_bie_mul_right_product_bound. ff_lt_bie_mul_right_product_bound + S ff_i_bie_mul_right_product = e) -> exists ff_p_bie_mul_right_product ff_r_bie_mul_right_product ff_s_bie_mul_right_product. ((((exists ff_h_bie_mul_right_product_factor. ff_h_bie_mul_right_product_factor + S (ff_p_bie_mul_right_product) = S ((S (ff_i_bie_mul_right_product)) * ff_c_bie_mul_right)) /\ exists ff_q_bie_mul_right_product_factor. ff_b_bie_mul_right = ff_q_bie_mul_right_product_factor * S ((S (ff_i_bie_mul_right_product)) * ff_c_bie_mul_right) + (ff_p_bie_mul_right_product))) /\ ((((exists ff_h_bie_mul_right_product_partial. ff_h_bie_mul_right_product_partial + S (ff_r_bie_mul_right_product) = S ((S (ff_i_bie_mul_right_product)) * ff_v_bie_mul_right_product)) /\ exists ff_q_bie_mul_right_product_partial. ff_u_bie_mul_right_product = ff_q_bie_mul_right_product_partial * S ((S (ff_i_bie_mul_right_product)) * ff_v_bie_mul_right_product) + (ff_r_bie_mul_right_product))) /\ ((((exists ff_h_bie_mul_right_product_successor. ff_h_bie_mul_right_product_successor + S (ff_s_bie_mul_right_product) = S ((S (S ff_i_bie_mul_right_product)) * ff_v_bie_mul_right_product)) /\ exists ff_q_bie_mul_right_product_successor. ff_u_bie_mul_right_product = ff_q_bie_mul_right_product_successor * S ((S (S ff_i_bie_mul_right_product)) * ff_v_bie_mul_right_product) + (ff_s_bie_mul_right_product))) /\ ff_s_bie_mul_right_product = ff_r_bie_mul_right_product * ff_p_bie_mul_right_product)))))))) -> (exists pa_b_bie_mul_product pa_c_bie_mul_product. ((forall pa_i_bie_mul_product_repeat. (exists pa_lt_bie_mul_product_repeat_bound. pa_lt_bie_mul_product_repeat_bound + S pa_i_bie_mul_product_repeat = e) -> (((exists pa_h_bie_mul_product_repeat_decoded. pa_h_bie_mul_product_repeat_decoded + S (a * b) = S ((S (pa_i_bie_mul_product_repeat)) * pa_c_bie_mul_product)) /\ exists pa_q_bie_mul_product_repeat_decoded. pa_b_bie_mul_product = pa_q_bie_mul_product_repeat_decoded * S ((S (pa_i_bie_mul_product_repeat)) * pa_c_bie_mul_product) + (a * b)))) /\ (exists pa_u_bie_mul_product_product pa_v_bie_mul_product_product. ((((exists pa_h_bie_mul_product_product_start. pa_h_bie_mul_product_product_start + S (1) = S ((S (0)) * pa_v_bie_mul_product_product)) /\ exists pa_q_bie_mul_product_product_start. pa_u_bie_mul_product_product = pa_q_bie_mul_product_product_start * S ((S (0)) * pa_v_bie_mul_product_product) + (1))) /\ ((((exists pa_h_bie_mul_product_product_terminal. pa_h_bie_mul_product_product_terminal + S (z) = S ((S (e)) * pa_v_bie_mul_product_product)) /\ exists pa_q_bie_mul_product_product_terminal. pa_u_bie_mul_product_product = pa_q_bie_mul_product_product_terminal * S ((S (e)) * pa_v_bie_mul_product_product) + (z))) /\ forall pa_i_bie_mul_product_product. (exists pa_lt_bie_mul_product_product_bound. pa_lt_bie_mul_product_product_bound + S pa_i_bie_mul_product_product = e) -> exists pa_p_bie_mul_product_product pa_r_bie_mul_product_product pa_s_bie_mul_product_product. ((((exists pa_h_bie_mul_product_product_factor. pa_h_bie_mul_product_product_factor + S (pa_p_bie_mul_product_product) = S ((S (pa_i_bie_mul_product_product)) * pa_c_bie_mul_product)) /\ exists pa_q_bie_mul_product_product_factor. pa_b_bie_mul_product = pa_q_bie_mul_product_product_factor * S ((S (pa_i_bie_mul_product_product)) * pa_c_bie_mul_product) + (pa_p_bie_mul_product_product))) /\ ((((exists pa_h_bie_mul_product_product_partial. pa_h_bie_mul_product_product_partial + S (pa_r_bie_mul_product_product) = S ((S (pa_i_bie_mul_product_product)) * pa_v_bie_mul_product_product)) /\ exists pa_q_bie_mul_product_product_partial. pa_u_bie_mul_product_product = pa_q_bie_mul_product_product_partial * S ((S (pa_i_bie_mul_product_product)) * pa_v_bie_mul_product_product) + (pa_r_bie_mul_product_product))) /\ ((((exists pa_h_bie_mul_product_product_successor. pa_h_bie_mul_product_product_successor + S (pa_s_bie_mul_product_product) = S ((S (S pa_i_bie_mul_product_product)) * pa_v_bie_mul_product_product)) /\ exists pa_q_bie_mul_product_product_successor. pa_u_bie_mul_product_product = pa_q_bie_mul_product_product_successor * S ((S (S pa_i_bie_mul_product_product)) * pa_v_bie_mul_product_product) + (pa_s_bie_mul_product_product))) /\ pa_s_bie_mul_product_product = pa_r_bie_mul_product_product * pa_p_bie_mul_product_product)))))))) -> z = x * y

Proof neighborhood

Direct theorem prerequisites

BT0081 pow_zero BT0083 pow_successor_decompose BT000A mul_one BT0008 mul_assoc BT0006 mul_comm

Direct theorem dependents

BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_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 BT00WP bertrand_h_root_32_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

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

110 script commands · 28 reading checkpoints · 7 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 successor decomposemul onemul assocmul comm
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro e
02Induction on eL4–10

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

  1. L4
    induction e
  2. L5
    intro x
  3. L6
    intro y
  4. L7
    intro z
  5. L8
    intro hx
  6. L9
    intro hy
  7. L10
    intro hz
03Establish hx1L11–17

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

  1. L11
    have hx1 : x = 1
  2. L12
    specialize pow_zero a
  3. L13
    specialize pow_zero 0
  4. L14
    specialize pow_zero x
  5. L15
    apply pow_zero
  6. L16
    refl
  7. L17
    exact hx
04Establish hy1L18–24

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

  1. L18
    have hy1 : y = 1
  2. L19
    specialize pow_zero b
  3. L20
    specialize pow_zero 0
  4. L21
    specialize pow_zero y
  5. L22
    apply pow_zero
  6. L23
    refl
  7. L24
    exact hy
05Establish hz1L25–34

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

  1. L25
    have hz1 : z = 1
  2. L26
    specialize pow_zero (a * b)
  3. L27
    specialize pow_zero 0
  4. L28
    specialize pow_zero z
  5. L29
    apply pow_zero
  6. L30
    refl
  7. L31
    exact hz
  8. L32
    rewrite hz1
  9. L33
    rewrite hx1
  10. L34
    rewrite hy1
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–37

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

  1. L36
    specialize mul_one 1
  2. L37
    exact mul_one
08Fix variables and assumptionsL38–43

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

  1. L38
    intro x
  2. L39
    intro y
  3. L40
    intro z
  4. L41
    intro hx
  5. L42
    intro hy
  6. L43
    intro hz
09Establish hxstepL44–51

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

  1. L44
    have hxstep : ∃ r. Pow(a,e,r) ∧ x = r · aDefinitions: Pow(a,e,r)Original native command in the exact edition
  2. L45
    specialize pow_successor_decompose a
  3. L46
    specialize pow_successor_decompose e
  4. L47
    specialize pow_successor_decompose (S e)
  5. L48
    specialize pow_successor_decompose x
  6. L49
    apply pow_successor_decompose
  7. L50
    refl
  8. L51
    exact hx
10Separate the logical casesL52–53

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

  1. L52
    cases hxstep
  2. L53
    cases hxstep_witness
11Establish hystepL54–61

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

  1. L54
    have hystep : ∃ r. Pow(b,e,r) ∧ y = r · bDefinitions: Pow(b,e,r)Original native command in the exact edition
  2. L55
    specialize pow_successor_decompose b
  3. L56
    specialize pow_successor_decompose e
  4. L57
    specialize pow_successor_decompose (S e)
  5. L58
    specialize pow_successor_decompose y
  6. L59
    apply pow_successor_decompose
  7. L60
    refl
  8. L61
    exact hy
12Separate the logical casesL62–63

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

  1. L62
    cases hystep
  2. L63
    cases hystep_witness
13Establish hzstepL64–71

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

  1. L64
    have hzstep : ∃ r. Pow(a · b,e,r) ∧ z = r · (a · b)Definitions: Pow(a · b,e,r)Original native command in the exact edition
  2. L65
    specialize pow_successor_decompose (a * b)
  3. L66
    specialize pow_successor_decompose e
  4. L67
    specialize pow_successor_decompose (S e)
  5. L68
    specialize pow_successor_decompose z
  6. L69
    apply pow_successor_decompose
  7. L70
    refl
  8. L71
    exact hz
14Separate the logical casesL72–73

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

  1. L72
    cases hzstep
  2. L73
    cases hzstep_witness
15Establish hprefixL74–83

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

  1. L74
    have hprefix : x3 = x1 * x2
  2. L75
    specialize IH x1
  3. L76
    specialize IH x2
  4. L77
    specialize IH x3
  5. L78
    apply IH
  6. L79
    exact hxstep_witness_left
  7. L80
    exact hystep_witness_left
  8. L81
    exact hzstep_witness_left
  9. L82
    trans x3 * (a * b)
  10. L83
    exact hzstep_witness_right
16Calculate and transport equalitiesL84–85

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

  1. L84
    trans (x1 * x2) * (a * b)
  2. L85
    congr
17Use earlier factsL86–86

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

  1. L86
    exact hprefix
18Calculate and transport equalitiesL87–88

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

  1. L87
    refl
  2. L88
    trans x1 * (x2 * (a * b))
19Use earlier factsL89–89

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

  1. L89
    apply mul_assoc
20Calculate and transport equalitiesL90–93

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

  1. L90
    trans x1 * ((x2 * a) * b)
  2. L91
    congr
  3. L92
    refl
  4. L93
    symm
21Use earlier factsL94–94

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

  1. L94
    apply mul_assoc
22Calculate and transport equalitiesL95–98

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

  1. L95
    trans x1 * ((a * x2) * b)
  2. L96
    congr
  3. L97
    refl
  4. L98
    congr
23Use earlier factsL99–99

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

  1. L99
    apply mul_comm
24Calculate and transport equalitiesL100–103

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

  1. L100
    refl
  2. L101
    trans x1 * (a * (x2 * b))
  3. L102
    congr
  4. L103
    refl
25Use earlier factsL104–104

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

  1. L104
    apply mul_assoc
26Calculate and transport equalitiesL105–106

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

  1. L105
    trans (x1 * a) * (x2 * b)
  2. L106
    symm
27Use earlier factsL107–107

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

  1. L107
    apply mul_assoc
28Calculate and transport equalitiesL108–110

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

  1. L108
    rewrite <- hxstep_witness_right
  2. L109
    rewrite <- hystep_witness_right
  3. L110
    refl

Library-wide reading audit

Original defined command ledger · 110 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro e
  4. 0004induction e
  5. 0005intro x
  6. 0006intro y
  7. 0007intro z
  8. 0008intro hx
  9. 0009intro hy
  10. 0010intro hz
  11. 0011have hx1 : x = 1
  12. 0012specialize pow_zero a
  13. 0013specialize pow_zero 0
  14. 0014specialize pow_zero x
  15. 0015apply pow_zero
  16. 0016refl
  17. 0017exact hx
  18. 0018have hy1 : y = 1
  19. 0019specialize pow_zero b
  20. 0020specialize pow_zero 0
  21. 0021specialize pow_zero y
  22. 0022apply pow_zero
  23. 0023refl
  24. 0024exact hy
  25. 0025have hz1 : z = 1
  26. 0026specialize pow_zero (a * b)
  27. 0027specialize pow_zero 0
  28. 0028specialize pow_zero z
  29. 0029apply pow_zero
  30. 0030refl
  31. 0031exact hz
  32. 0032rewrite hz1
  33. 0033rewrite hx1
  34. 0034rewrite hy1
  35. 0035symm
  36. 0036specialize mul_one 1
  37. 0037exact mul_one
  38. 0038intro x
  39. 0039intro y
  40. 0040intro z
  41. 0041intro hx
  42. 0042intro hy
  43. 0043intro hz
  44. 0044have hxstep : ∃ r. Pow(a,e,r) ∧ x = r · a
    Exact native replay linehave hxstep : exists r. (exists ff_b_bie_mul_left_prefix ff_c_bie_mul_left_prefix. ((forall ff_i_bie_mul_left_prefix_repeat. (exists ff_lt_bie_mul_left_prefix_repeat_bound. ff_lt_bie_mul_left_prefix_repeat_bound + S ff_i_bie_mul_left_prefix_repeat = e) -> (((exists ff_h_bie_mul_left_prefix_repeat_decoded. ff_h_bie_mul_left_prefix_repeat_decoded + S (a) = S ((S (ff_i_bie_mul_left_prefix_repeat)) * ff_c_bie_mul_left_prefix)) /\ exists ff_q_bie_mul_left_prefix_repeat_decoded. ff_b_bie_mul_left_prefix = ff_q_bie_mul_left_prefix_repeat_decoded * S ((S (ff_i_bie_mul_left_prefix_repeat)) * ff_c_bie_mul_left_prefix) + (a)))) /\ (exists ff_u_bie_mul_left_prefix_product ff_v_bie_mul_left_prefix_product. ((((exists ff_h_bie_mul_left_prefix_product_start. ff_h_bie_mul_left_prefix_product_start + S (1) = S ((S (0)) * ff_v_bie_mul_left_prefix_product)) /\ exists ff_q_bie_mul_left_prefix_product_start. ff_u_bie_mul_left_prefix_product = ff_q_bie_mul_left_prefix_product_start * S ((S (0)) * ff_v_bie_mul_left_prefix_product) + (1))) /\ ((((exists ff_h_bie_mul_left_prefix_product_terminal. ff_h_bie_mul_left_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bie_mul_left_prefix_product)) /\ exists ff_q_bie_mul_left_prefix_product_terminal. ff_u_bie_mul_left_prefix_product = ff_q_bie_mul_left_prefix_product_terminal * S ((S (e)) * ff_v_bie_mul_left_prefix_product) + (r))) /\ forall ff_i_bie_mul_left_prefix_product. (exists ff_lt_bie_mul_left_prefix_product_bound. ff_lt_bie_mul_left_prefix_product_bound + S ff_i_bie_mul_left_prefix_product = e) -> exists ff_p_bie_mul_left_prefix_product ff_r_bie_mul_left_prefix_product ff_s_bie_mul_left_prefix_product. ((((exists ff_h_bie_mul_left_prefix_product_factor. ff_h_bie_mul_left_prefix_product_factor + S (ff_p_bie_mul_left_prefix_product) = S ((S (ff_i_bie_mul_left_prefix_product)) * ff_c_bie_mul_left_prefix)) /\ exists ff_q_bie_mul_left_prefix_product_factor. ff_b_bie_mul_left_prefix = ff_q_bie_mul_left_prefix_product_factor * S ((S (ff_i_bie_mul_left_prefix_product)) * ff_c_bie_mul_left_prefix) + (ff_p_bie_mul_left_prefix_product))) /\ ((((exists ff_h_bie_mul_left_prefix_product_partial. ff_h_bie_mul_left_prefix_product_partial + S (ff_r_bie_mul_left_prefix_product) = S ((S (ff_i_bie_mul_left_prefix_product)) * ff_v_bie_mul_left_prefix_product)) /\ exists ff_q_bie_mul_left_prefix_product_partial. ff_u_bie_mul_left_prefix_product = ff_q_bie_mul_left_prefix_product_partial * S ((S (ff_i_bie_mul_left_prefix_product)) * ff_v_bie_mul_left_prefix_product) + (ff_r_bie_mul_left_prefix_product))) /\ ((((exists ff_h_bie_mul_left_prefix_product_successor. ff_h_bie_mul_left_prefix_product_successor + S (ff_s_bie_mul_left_prefix_product) = S ((S (S ff_i_bie_mul_left_prefix_product)) * ff_v_bie_mul_left_prefix_product)) /\ exists ff_q_bie_mul_left_prefix_product_successor. ff_u_bie_mul_left_prefix_product = ff_q_bie_mul_left_prefix_product_successor * S ((S (S ff_i_bie_mul_left_prefix_product)) * ff_v_bie_mul_left_prefix_product) + (ff_s_bie_mul_left_prefix_product))) /\ ff_s_bie_mul_left_prefix_product = ff_r_bie_mul_left_prefix_product * ff_p_bie_mul_left_prefix_product)))))))) /\ x = r * a
  45. 0045specialize pow_successor_decompose a
  46. 0046specialize pow_successor_decompose e
  47. 0047specialize pow_successor_decompose (S e)
  48. 0048specialize pow_successor_decompose x
  49. 0049apply pow_successor_decompose
  50. 0050refl
  51. 0051exact hx
  52. 0052cases hxstep
  53. 0053cases hxstep_witness
  54. 0054have hystep : ∃ r. Pow(b,e,r) ∧ y = r · b
    Exact native replay linehave hystep : exists r. (exists ff_b_bie_mul_right_prefix ff_c_bie_mul_right_prefix. ((forall ff_i_bie_mul_right_prefix_repeat. (exists ff_lt_bie_mul_right_prefix_repeat_bound. ff_lt_bie_mul_right_prefix_repeat_bound + S ff_i_bie_mul_right_prefix_repeat = e) -> (((exists ff_h_bie_mul_right_prefix_repeat_decoded. ff_h_bie_mul_right_prefix_repeat_decoded + S (b) = S ((S (ff_i_bie_mul_right_prefix_repeat)) * ff_c_bie_mul_right_prefix)) /\ exists ff_q_bie_mul_right_prefix_repeat_decoded. ff_b_bie_mul_right_prefix = ff_q_bie_mul_right_prefix_repeat_decoded * S ((S (ff_i_bie_mul_right_prefix_repeat)) * ff_c_bie_mul_right_prefix) + (b)))) /\ (exists ff_u_bie_mul_right_prefix_product ff_v_bie_mul_right_prefix_product. ((((exists ff_h_bie_mul_right_prefix_product_start. ff_h_bie_mul_right_prefix_product_start + S (1) = S ((S (0)) * ff_v_bie_mul_right_prefix_product)) /\ exists ff_q_bie_mul_right_prefix_product_start. ff_u_bie_mul_right_prefix_product = ff_q_bie_mul_right_prefix_product_start * S ((S (0)) * ff_v_bie_mul_right_prefix_product) + (1))) /\ ((((exists ff_h_bie_mul_right_prefix_product_terminal. ff_h_bie_mul_right_prefix_product_terminal + S (r) = S ((S (e)) * ff_v_bie_mul_right_prefix_product)) /\ exists ff_q_bie_mul_right_prefix_product_terminal. ff_u_bie_mul_right_prefix_product = ff_q_bie_mul_right_prefix_product_terminal * S ((S (e)) * ff_v_bie_mul_right_prefix_product) + (r))) /\ forall ff_i_bie_mul_right_prefix_product. (exists ff_lt_bie_mul_right_prefix_product_bound. ff_lt_bie_mul_right_prefix_product_bound + S ff_i_bie_mul_right_prefix_product = e) -> exists ff_p_bie_mul_right_prefix_product ff_r_bie_mul_right_prefix_product ff_s_bie_mul_right_prefix_product. ((((exists ff_h_bie_mul_right_prefix_product_factor. ff_h_bie_mul_right_prefix_product_factor + S (ff_p_bie_mul_right_prefix_product) = S ((S (ff_i_bie_mul_right_prefix_product)) * ff_c_bie_mul_right_prefix)) /\ exists ff_q_bie_mul_right_prefix_product_factor. ff_b_bie_mul_right_prefix = ff_q_bie_mul_right_prefix_product_factor * S ((S (ff_i_bie_mul_right_prefix_product)) * ff_c_bie_mul_right_prefix) + (ff_p_bie_mul_right_prefix_product))) /\ ((((exists ff_h_bie_mul_right_prefix_product_partial. ff_h_bie_mul_right_prefix_product_partial + S (ff_r_bie_mul_right_prefix_product) = S ((S (ff_i_bie_mul_right_prefix_product)) * ff_v_bie_mul_right_prefix_product)) /\ exists ff_q_bie_mul_right_prefix_product_partial. ff_u_bie_mul_right_prefix_product = ff_q_bie_mul_right_prefix_product_partial * S ((S (ff_i_bie_mul_right_prefix_product)) * ff_v_bie_mul_right_prefix_product) + (ff_r_bie_mul_right_prefix_product))) /\ ((((exists ff_h_bie_mul_right_prefix_product_successor. ff_h_bie_mul_right_prefix_product_successor + S (ff_s_bie_mul_right_prefix_product) = S ((S (S ff_i_bie_mul_right_prefix_product)) * ff_v_bie_mul_right_prefix_product)) /\ exists ff_q_bie_mul_right_prefix_product_successor. ff_u_bie_mul_right_prefix_product = ff_q_bie_mul_right_prefix_product_successor * S ((S (S ff_i_bie_mul_right_prefix_product)) * ff_v_bie_mul_right_prefix_product) + (ff_s_bie_mul_right_prefix_product))) /\ ff_s_bie_mul_right_prefix_product = ff_r_bie_mul_right_prefix_product * ff_p_bie_mul_right_prefix_product)))))))) /\ y = r * b
  55. 0055specialize pow_successor_decompose b
  56. 0056specialize pow_successor_decompose e
  57. 0057specialize pow_successor_decompose (S e)
  58. 0058specialize pow_successor_decompose y
  59. 0059apply pow_successor_decompose
  60. 0060refl
  61. 0061exact hy
  62. 0062cases hystep
  63. 0063cases hystep_witness
  64. 0064have hzstep : ∃ r. Pow(a · b,e,r) ∧ z = r · (a · b)
    Exact native replay linehave hzstep : exists r. (exists pa_b_bie_mul_product_prefix pa_c_bie_mul_product_prefix. ((forall pa_i_bie_mul_product_prefix_repeat. (exists pa_lt_bie_mul_product_prefix_repeat_bound. pa_lt_bie_mul_product_prefix_repeat_bound + S pa_i_bie_mul_product_prefix_repeat = e) -> (((exists pa_h_bie_mul_product_prefix_repeat_decoded. pa_h_bie_mul_product_prefix_repeat_decoded + S (a * b) = S ((S (pa_i_bie_mul_product_prefix_repeat)) * pa_c_bie_mul_product_prefix)) /\ exists pa_q_bie_mul_product_prefix_repeat_decoded. pa_b_bie_mul_product_prefix = pa_q_bie_mul_product_prefix_repeat_decoded * S ((S (pa_i_bie_mul_product_prefix_repeat)) * pa_c_bie_mul_product_prefix) + (a * b)))) /\ (exists pa_u_bie_mul_product_prefix_product pa_v_bie_mul_product_prefix_product. ((((exists pa_h_bie_mul_product_prefix_product_start. pa_h_bie_mul_product_prefix_product_start + S (1) = S ((S (0)) * pa_v_bie_mul_product_prefix_product)) /\ exists pa_q_bie_mul_product_prefix_product_start. pa_u_bie_mul_product_prefix_product = pa_q_bie_mul_product_prefix_product_start * S ((S (0)) * pa_v_bie_mul_product_prefix_product) + (1))) /\ ((((exists pa_h_bie_mul_product_prefix_product_terminal. pa_h_bie_mul_product_prefix_product_terminal + S (r) = S ((S (e)) * pa_v_bie_mul_product_prefix_product)) /\ exists pa_q_bie_mul_product_prefix_product_terminal. pa_u_bie_mul_product_prefix_product = pa_q_bie_mul_product_prefix_product_terminal * S ((S (e)) * pa_v_bie_mul_product_prefix_product) + (r))) /\ forall pa_i_bie_mul_product_prefix_product. (exists pa_lt_bie_mul_product_prefix_product_bound. pa_lt_bie_mul_product_prefix_product_bound + S pa_i_bie_mul_product_prefix_product = e) -> exists pa_p_bie_mul_product_prefix_product pa_r_bie_mul_product_prefix_product pa_s_bie_mul_product_prefix_product. ((((exists pa_h_bie_mul_product_prefix_product_factor. pa_h_bie_mul_product_prefix_product_factor + S (pa_p_bie_mul_product_prefix_product) = S ((S (pa_i_bie_mul_product_prefix_product)) * pa_c_bie_mul_product_prefix)) /\ exists pa_q_bie_mul_product_prefix_product_factor. pa_b_bie_mul_product_prefix = pa_q_bie_mul_product_prefix_product_factor * S ((S (pa_i_bie_mul_product_prefix_product)) * pa_c_bie_mul_product_prefix) + (pa_p_bie_mul_product_prefix_product))) /\ ((((exists pa_h_bie_mul_product_prefix_product_partial. pa_h_bie_mul_product_prefix_product_partial + S (pa_r_bie_mul_product_prefix_product) = S ((S (pa_i_bie_mul_product_prefix_product)) * pa_v_bie_mul_product_prefix_product)) /\ exists pa_q_bie_mul_product_prefix_product_partial. pa_u_bie_mul_product_prefix_product = pa_q_bie_mul_product_prefix_product_partial * S ((S (pa_i_bie_mul_product_prefix_product)) * pa_v_bie_mul_product_prefix_product) + (pa_r_bie_mul_product_prefix_product))) /\ ((((exists pa_h_bie_mul_product_prefix_product_successor. pa_h_bie_mul_product_prefix_product_successor + S (pa_s_bie_mul_product_prefix_product) = S ((S (S pa_i_bie_mul_product_prefix_product)) * pa_v_bie_mul_product_prefix_product)) /\ exists pa_q_bie_mul_product_prefix_product_successor. pa_u_bie_mul_product_prefix_product = pa_q_bie_mul_product_prefix_product_successor * S ((S (S pa_i_bie_mul_product_prefix_product)) * pa_v_bie_mul_product_prefix_product) + (pa_s_bie_mul_product_prefix_product))) /\ pa_s_bie_mul_product_prefix_product = pa_r_bie_mul_product_prefix_product * pa_p_bie_mul_product_prefix_product)))))))) /\ z = r * (a * b)
  65. 0065specialize pow_successor_decompose (a * b)
  66. 0066specialize pow_successor_decompose e
  67. 0067specialize pow_successor_decompose (S e)
  68. 0068specialize pow_successor_decompose z
  69. 0069apply pow_successor_decompose
  70. 0070refl
  71. 0071exact hz
  72. 0072cases hzstep
  73. 0073cases hzstep_witness
  74. 0074have hprefix : x3 = x1 * x2
  75. 0075specialize IH x1
  76. 0076specialize IH x2
  77. 0077specialize IH x3
  78. 0078apply IH
  79. 0079exact hxstep_witness_left
  80. 0080exact hystep_witness_left
  81. 0081exact hzstep_witness_left
  82. 0082trans x3 * (a * b)
  83. 0083exact hzstep_witness_right
  84. 0084trans (x1 * x2) * (a * b)
  85. 0085congr
  86. 0086exact hprefix
  87. 0087refl
  88. 0088trans x1 * (x2 * (a * b))
  89. 0089apply mul_assoc
  90. 0090trans x1 * ((x2 * a) * b)
  91. 0091congr
  92. 0092refl
  93. 0093symm
  94. 0094apply mul_assoc
  95. 0095trans x1 * ((a * x2) * b)
  96. 0096congr
  97. 0097refl
  98. 0098congr
  99. 0099apply mul_comm
  100. 0100refl
  101. 0101trans x1 * (a * (x2 * b))
  102. 0102congr
  103. 0103refl
  104. 0104apply mul_assoc
  105. 0105trans (x1 * a) * (x2 * b)
  106. 0106symm
  107. 0107apply mul_assoc
  108. 0108rewrite <- hxstep_witness_right
  109. 0109rewrite <- hystep_witness_right
  110. 0110refl