PA005Y · theorem

pow_mul_exp

Stable checked-use theorem · independently closed

Iterated relational powers multiply their exponents.

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

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

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 p x y z. p = e * f -> (exists ff_b_mul_base ff_c_mul_base. ((forall ff_i_mul_base_repeat. (exists ff_lt_mul_base_repeat_bound. ff_lt_mul_base_repeat_bound + S ff_i_mul_base_repeat = e) -> (((exists ff_h_mul_base_repeat_decoded. ff_h_mul_base_repeat_decoded + S (a) = S ((S (ff_i_mul_base_repeat)) * ff_c_mul_base)) /\ exists ff_q_mul_base_repeat_decoded. ff_b_mul_base = ff_q_mul_base_repeat_decoded * S ((S (ff_i_mul_base_repeat)) * ff_c_mul_base) + (a)))) /\ (exists ff_u_mul_base_product ff_v_mul_base_product. ((((exists ff_h_mul_base_product_start. ff_h_mul_base_product_start + S (1) = S ((S (0)) * ff_v_mul_base_product)) /\ exists ff_q_mul_base_product_start. ff_u_mul_base_product = ff_q_mul_base_product_start * S ((S (0)) * ff_v_mul_base_product) + (1))) /\ ((((exists ff_h_mul_base_product_terminal. ff_h_mul_base_product_terminal + S (x) = S ((S (e)) * ff_v_mul_base_product)) /\ exists ff_q_mul_base_product_terminal. ff_u_mul_base_product = ff_q_mul_base_product_terminal * S ((S (e)) * ff_v_mul_base_product) + (x))) /\ forall ff_i_mul_base_product. (exists ff_lt_mul_base_product_bound. ff_lt_mul_base_product_bound + S ff_i_mul_base_product = e) -> exists ff_p_mul_base_product ff_r_mul_base_product ff_s_mul_base_product. ((((exists ff_h_mul_base_product_factor. ff_h_mul_base_product_factor + S (ff_p_mul_base_product) = S ((S (ff_i_mul_base_product)) * ff_c_mul_base)) /\ exists ff_q_mul_base_product_factor. ff_b_mul_base = ff_q_mul_base_product_factor * S ((S (ff_i_mul_base_product)) * ff_c_mul_base) + (ff_p_mul_base_product))) /\ ((((exists ff_h_mul_base_product_partial. ff_h_mul_base_product_partial + S (ff_r_mul_base_product) = S ((S (ff_i_mul_base_product)) * ff_v_mul_base_product)) /\ exists ff_q_mul_base_product_partial. ff_u_mul_base_product = ff_q_mul_base_product_partial * S ((S (ff_i_mul_base_product)) * ff_v_mul_base_product) + (ff_r_mul_base_product))) /\ ((((exists ff_h_mul_base_product_successor. ff_h_mul_base_product_successor + S (ff_s_mul_base_product) = S ((S (S ff_i_mul_base_product)) * ff_v_mul_base_product)) /\ exists ff_q_mul_base_product_successor. ff_u_mul_base_product = ff_q_mul_base_product_successor * S ((S (S ff_i_mul_base_product)) * ff_v_mul_base_product) + (ff_s_mul_base_product))) /\ ff_s_mul_base_product = ff_r_mul_base_product * ff_p_mul_base_product)))))))) -> (exists ff_b_mul_outer ff_c_mul_outer. ((forall ff_i_mul_outer_repeat. (exists ff_lt_mul_outer_repeat_bound. ff_lt_mul_outer_repeat_bound + S ff_i_mul_outer_repeat = f) -> (((exists ff_h_mul_outer_repeat_decoded. ff_h_mul_outer_repeat_decoded + S (x) = S ((S (ff_i_mul_outer_repeat)) * ff_c_mul_outer)) /\ exists ff_q_mul_outer_repeat_decoded. ff_b_mul_outer = ff_q_mul_outer_repeat_decoded * S ((S (ff_i_mul_outer_repeat)) * ff_c_mul_outer) + (x)))) /\ (exists ff_u_mul_outer_product ff_v_mul_outer_product. ((((exists ff_h_mul_outer_product_start. ff_h_mul_outer_product_start + S (1) = S ((S (0)) * ff_v_mul_outer_product)) /\ exists ff_q_mul_outer_product_start. ff_u_mul_outer_product = ff_q_mul_outer_product_start * S ((S (0)) * ff_v_mul_outer_product) + (1))) /\ ((((exists ff_h_mul_outer_product_terminal. ff_h_mul_outer_product_terminal + S (y) = S ((S (f)) * ff_v_mul_outer_product)) /\ exists ff_q_mul_outer_product_terminal. ff_u_mul_outer_product = ff_q_mul_outer_product_terminal * S ((S (f)) * ff_v_mul_outer_product) + (y))) /\ forall ff_i_mul_outer_product. (exists ff_lt_mul_outer_product_bound. ff_lt_mul_outer_product_bound + S ff_i_mul_outer_product = f) -> exists ff_p_mul_outer_product ff_r_mul_outer_product ff_s_mul_outer_product. ((((exists ff_h_mul_outer_product_factor. ff_h_mul_outer_product_factor + S (ff_p_mul_outer_product) = S ((S (ff_i_mul_outer_product)) * ff_c_mul_outer)) /\ exists ff_q_mul_outer_product_factor. ff_b_mul_outer = ff_q_mul_outer_product_factor * S ((S (ff_i_mul_outer_product)) * ff_c_mul_outer) + (ff_p_mul_outer_product))) /\ ((((exists ff_h_mul_outer_product_partial. ff_h_mul_outer_product_partial + S (ff_r_mul_outer_product) = S ((S (ff_i_mul_outer_product)) * ff_v_mul_outer_product)) /\ exists ff_q_mul_outer_product_partial. ff_u_mul_outer_product = ff_q_mul_outer_product_partial * S ((S (ff_i_mul_outer_product)) * ff_v_mul_outer_product) + (ff_r_mul_outer_product))) /\ ((((exists ff_h_mul_outer_product_successor. ff_h_mul_outer_product_successor + S (ff_s_mul_outer_product) = S ((S (S ff_i_mul_outer_product)) * ff_v_mul_outer_product)) /\ exists ff_q_mul_outer_product_successor. ff_u_mul_outer_product = ff_q_mul_outer_product_successor * S ((S (S ff_i_mul_outer_product)) * ff_v_mul_outer_product) + (ff_s_mul_outer_product))) /\ ff_s_mul_outer_product = ff_r_mul_outer_product * ff_p_mul_outer_product)))))))) -> (exists ff_b_mul_total ff_c_mul_total. ((forall ff_i_mul_total_repeat. (exists ff_lt_mul_total_repeat_bound. ff_lt_mul_total_repeat_bound + S ff_i_mul_total_repeat = p) -> (((exists ff_h_mul_total_repeat_decoded. ff_h_mul_total_repeat_decoded + S (a) = S ((S (ff_i_mul_total_repeat)) * ff_c_mul_total)) /\ exists ff_q_mul_total_repeat_decoded. ff_b_mul_total = ff_q_mul_total_repeat_decoded * S ((S (ff_i_mul_total_repeat)) * ff_c_mul_total) + (a)))) /\ (exists ff_u_mul_total_product ff_v_mul_total_product. ((((exists ff_h_mul_total_product_start. ff_h_mul_total_product_start + S (1) = S ((S (0)) * ff_v_mul_total_product)) /\ exists ff_q_mul_total_product_start. ff_u_mul_total_product = ff_q_mul_total_product_start * S ((S (0)) * ff_v_mul_total_product) + (1))) /\ ((((exists ff_h_mul_total_product_terminal. ff_h_mul_total_product_terminal + S (z) = S ((S (p)) * ff_v_mul_total_product)) /\ exists ff_q_mul_total_product_terminal. ff_u_mul_total_product = ff_q_mul_total_product_terminal * S ((S (p)) * ff_v_mul_total_product) + (z))) /\ forall ff_i_mul_total_product. (exists ff_lt_mul_total_product_bound. ff_lt_mul_total_product_bound + S ff_i_mul_total_product = p) -> exists ff_p_mul_total_product ff_r_mul_total_product ff_s_mul_total_product. ((((exists ff_h_mul_total_product_factor. ff_h_mul_total_product_factor + S (ff_p_mul_total_product) = S ((S (ff_i_mul_total_product)) * ff_c_mul_total)) /\ exists ff_q_mul_total_product_factor. ff_b_mul_total = ff_q_mul_total_product_factor * S ((S (ff_i_mul_total_product)) * ff_c_mul_total) + (ff_p_mul_total_product))) /\ ((((exists ff_h_mul_total_product_partial. ff_h_mul_total_product_partial + S (ff_r_mul_total_product) = S ((S (ff_i_mul_total_product)) * ff_v_mul_total_product)) /\ exists ff_q_mul_total_product_partial. ff_u_mul_total_product = ff_q_mul_total_product_partial * S ((S (ff_i_mul_total_product)) * ff_v_mul_total_product) + (ff_r_mul_total_product))) /\ ((((exists ff_h_mul_total_product_successor. ff_h_mul_total_product_successor + S (ff_s_mul_total_product) = S ((S (S ff_i_mul_total_product)) * ff_v_mul_total_product)) /\ exists ff_q_mul_total_product_successor. ff_u_mul_total_product = ff_q_mul_total_product_successor * S ((S (S ff_i_mul_total_product)) * ff_v_mul_total_product) + (ff_s_mul_total_product))) /\ ff_s_mul_total_product = ff_r_mul_total_product * ff_p_mul_total_product)))))))) -> y = z

Proof neighborhood

Direct theorem prerequisites

PA004B pow_zero PA004D pow_successor_decompose PA0046 pow_exists PA005X pow_add

Direct theorem dependents

PA008M quadratic_residue_half_power_mod_one

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

92 script commands · 21 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 (4)
pow zeropow successor decomposepow existspow add
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 p
  3. L5
    intro x
  4. L6
    intro y
  5. L7
    intro z
  6. L8
    intro hp
  7. L9
    intro hx
  8. L10
    intro hy
  9. L11
    intro hz
  10. L12
    rewrite PA5 at hp
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 hp at hz
  2. L14
    rewrite hp at hz
  3. L15
    rewrite hp at hz
  4. L16
    rewrite hp at hz
04Establish hy1L17–23

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

  1. L17
    have hy1 : y = 1
  2. L18
    specialize pow_zero x
  3. L19
    specialize pow_zero 0
  4. L20
    specialize pow_zero y
  5. L21
    apply pow_zero
  6. L22
    refl
  7. L23
    exact hy
05Establish hz1L24–33

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

  1. L24
    have hz1 : z = 1
  2. L25
    specialize pow_zero a
  3. L26
    specialize pow_zero 0
  4. L27
    specialize pow_zero z
  5. L28
    apply pow_zero
  6. L29
    refl
  7. L30
    exact hz
  8. L31
    trans 1
  9. L32
    exact hy1
  10. L33
    symm
06Use earlier factsL34–34

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

  1. L34
    exact hz1
07Fix variables and assumptionsL35–42

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

  1. L35
    intro p
  2. L36
    intro x
  3. L37
    intro y
  4. L38
    intro z
  5. L39
    intro hp
  6. L40
    intro hx
  7. L41
    intro hy
  8. L42
    intro hz
08Establish hy_stepL43–50

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

  1. L43
    have hy_step : ∃ r. Pow(x,f,r) ∧ y = r · xDefinitions: Pow(x,f,r)Original native command in the exact edition
  2. L44
    specialize pow_successor_decompose x
  3. L45
    specialize pow_successor_decompose f
  4. L46
    specialize pow_successor_decompose (S f)
  5. L47
    specialize pow_successor_decompose y
  6. L48
    apply pow_successor_decompose
  7. L49
    refl
  8. L50
    exact hy
09Separate the logical casesL51–52

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

  1. L51
    cases hy_step
  2. L52
    cases hy_step_witness
10Establish hqpowL53–56

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

  1. L53
    have hqpow : ∃ r. Pow(a,e · f,r)Definitions: Pow(a,e · f,r)Original native command in the exact edition
  2. L54
    specialize pow_exists a
  3. L55
    specialize pow_exists (e * f)
  4. L56
    exact pow_exists
11Separate the logical casesL57–57

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

  1. L57
    cases hqpow
12Establish hprefixL58–67

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

  1. L58
    have hprefix : x1 = x2
  2. L59
    specialize IH (e * f)
  3. L60
    specialize IH x
  4. L61
    specialize IH x1
  5. L62
    specialize IH x2
  6. L63
    apply IH
  7. L64
    refl
  8. L65
    exact hx
  9. L66
    exact hy_step_witness_left
  10. L67
    exact hqpow_witness
13Establish hpsumL68–71

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

  1. L68
    have hpsum : p = (e * f) + e
  2. L69
    trans e * S f
  3. L70
    exact hp
  4. L71
    apply PA6
14Establish htotalL72–81

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

  1. L72
    have htotal : z = x2 * x
  2. L73
    specialize pow_add a
  3. L74
    specialize pow_add (e * f)
  4. L75
    specialize pow_add e
  5. L76
    specialize pow_add p
  6. L77
    specialize pow_add x2
  7. L78
    specialize pow_add x
  8. L79
    specialize pow_add z
  9. L80
    apply pow_add
  10. L81
    exact hpsum
15Use earlier factsL82–84

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

  1. L82
    exact hqpow_witness
  2. L83
    exact hx
  3. L84
    exact hz
16Calculate and transport equalitiesL85–85

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

  1. L85
    trans x1 * x
17Use earlier factsL86–86

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

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

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

  1. L87
    trans x2 * x
  2. L88
    congr
19Use earlier factsL89–89

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

  1. L89
    exact hprefix
20Calculate and transport equalitiesL90–91

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

  1. L90
    refl
  2. L91
    symm
21Use earlier factsL92–92

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

  1. L92
    exact htotal

Library-wide reading audit

Original defined command ledger · 92 lines
  1. 0001intro a
  2. 0002intro e
  3. 0003induction f
  4. 0004intro p
  5. 0005intro x
  6. 0006intro y
  7. 0007intro z
  8. 0008intro hp
  9. 0009intro hx
  10. 0010intro hy
  11. 0011intro hz
  12. 0012rewrite PA5 at hp
  13. 0013rewrite hp at hz
  14. 0014rewrite hp at hz
  15. 0015rewrite hp at hz
  16. 0016rewrite hp at hz
  17. 0017have hy1 : y = 1
  18. 0018specialize pow_zero x
  19. 0019specialize pow_zero 0
  20. 0020specialize pow_zero y
  21. 0021apply pow_zero
  22. 0022refl
  23. 0023exact hy
  24. 0024have hz1 : z = 1
  25. 0025specialize pow_zero a
  26. 0026specialize pow_zero 0
  27. 0027specialize pow_zero z
  28. 0028apply pow_zero
  29. 0029refl
  30. 0030exact hz
  31. 0031trans 1
  32. 0032exact hy1
  33. 0033symm
  34. 0034exact hz1
  35. 0035intro p
  36. 0036intro x
  37. 0037intro y
  38. 0038intro z
  39. 0039intro hp
  40. 0040intro hx
  41. 0041intro hy
  42. 0042intro hz
  43. 0043have hy_step : ∃ r. Pow(x,f,r) ∧ y = r · x
    Exact native replay linehave hy_step : exists r. (exists ff_b_mul_y_prefix ff_c_mul_y_prefix. ((forall ff_i_mul_y_prefix_repeat. (exists ff_lt_mul_y_prefix_repeat_bound. ff_lt_mul_y_prefix_repeat_bound + S ff_i_mul_y_prefix_repeat = f) -> (((exists ff_h_mul_y_prefix_repeat_decoded. ff_h_mul_y_prefix_repeat_decoded + S (x) = S ((S (ff_i_mul_y_prefix_repeat)) * ff_c_mul_y_prefix)) /\ exists ff_q_mul_y_prefix_repeat_decoded. ff_b_mul_y_prefix = ff_q_mul_y_prefix_repeat_decoded * S ((S (ff_i_mul_y_prefix_repeat)) * ff_c_mul_y_prefix) + (x)))) /\ (exists ff_u_mul_y_prefix_product ff_v_mul_y_prefix_product. ((((exists ff_h_mul_y_prefix_product_start. ff_h_mul_y_prefix_product_start + S (1) = S ((S (0)) * ff_v_mul_y_prefix_product)) /\ exists ff_q_mul_y_prefix_product_start. ff_u_mul_y_prefix_product = ff_q_mul_y_prefix_product_start * S ((S (0)) * ff_v_mul_y_prefix_product) + (1))) /\ ((((exists ff_h_mul_y_prefix_product_terminal. ff_h_mul_y_prefix_product_terminal + S (r) = S ((S (f)) * ff_v_mul_y_prefix_product)) /\ exists ff_q_mul_y_prefix_product_terminal. ff_u_mul_y_prefix_product = ff_q_mul_y_prefix_product_terminal * S ((S (f)) * ff_v_mul_y_prefix_product) + (r))) /\ forall ff_i_mul_y_prefix_product. (exists ff_lt_mul_y_prefix_product_bound. ff_lt_mul_y_prefix_product_bound + S ff_i_mul_y_prefix_product = f) -> exists ff_p_mul_y_prefix_product ff_r_mul_y_prefix_product ff_s_mul_y_prefix_product. ((((exists ff_h_mul_y_prefix_product_factor. ff_h_mul_y_prefix_product_factor + S (ff_p_mul_y_prefix_product) = S ((S (ff_i_mul_y_prefix_product)) * ff_c_mul_y_prefix)) /\ exists ff_q_mul_y_prefix_product_factor. ff_b_mul_y_prefix = ff_q_mul_y_prefix_product_factor * S ((S (ff_i_mul_y_prefix_product)) * ff_c_mul_y_prefix) + (ff_p_mul_y_prefix_product))) /\ ((((exists ff_h_mul_y_prefix_product_partial. ff_h_mul_y_prefix_product_partial + S (ff_r_mul_y_prefix_product) = S ((S (ff_i_mul_y_prefix_product)) * ff_v_mul_y_prefix_product)) /\ exists ff_q_mul_y_prefix_product_partial. ff_u_mul_y_prefix_product = ff_q_mul_y_prefix_product_partial * S ((S (ff_i_mul_y_prefix_product)) * ff_v_mul_y_prefix_product) + (ff_r_mul_y_prefix_product))) /\ ((((exists ff_h_mul_y_prefix_product_successor. ff_h_mul_y_prefix_product_successor + S (ff_s_mul_y_prefix_product) = S ((S (S ff_i_mul_y_prefix_product)) * ff_v_mul_y_prefix_product)) /\ exists ff_q_mul_y_prefix_product_successor. ff_u_mul_y_prefix_product = ff_q_mul_y_prefix_product_successor * S ((S (S ff_i_mul_y_prefix_product)) * ff_v_mul_y_prefix_product) + (ff_s_mul_y_prefix_product))) /\ ff_s_mul_y_prefix_product = ff_r_mul_y_prefix_product * ff_p_mul_y_prefix_product)))))))) /\ y = r * x
  44. 0044specialize pow_successor_decompose x
  45. 0045specialize pow_successor_decompose f
  46. 0046specialize pow_successor_decompose (S f)
  47. 0047specialize pow_successor_decompose y
  48. 0048apply pow_successor_decompose
  49. 0049refl
  50. 0050exact hy
  51. 0051cases hy_step
  52. 0052cases hy_step_witness
  53. 0053have hqpow : ∃ r. Pow(a,e · f,r)
    Exact native replay linehave hqpow : exists r. (exists pa_b_mul_total_prefix pa_c_mul_total_prefix. ((forall pa_i_mul_total_prefix_repeat. (exists pa_lt_mul_total_prefix_repeat_bound. pa_lt_mul_total_prefix_repeat_bound + S pa_i_mul_total_prefix_repeat = e * f) -> (((exists pa_h_mul_total_prefix_repeat_decoded. pa_h_mul_total_prefix_repeat_decoded + S (a) = S ((S (pa_i_mul_total_prefix_repeat)) * pa_c_mul_total_prefix)) /\ exists pa_q_mul_total_prefix_repeat_decoded. pa_b_mul_total_prefix = pa_q_mul_total_prefix_repeat_decoded * S ((S (pa_i_mul_total_prefix_repeat)) * pa_c_mul_total_prefix) + (a)))) /\ (exists pa_u_mul_total_prefix_product pa_v_mul_total_prefix_product. ((((exists pa_h_mul_total_prefix_product_start. pa_h_mul_total_prefix_product_start + S (1) = S ((S (0)) * pa_v_mul_total_prefix_product)) /\ exists pa_q_mul_total_prefix_product_start. pa_u_mul_total_prefix_product = pa_q_mul_total_prefix_product_start * S ((S (0)) * pa_v_mul_total_prefix_product) + (1))) /\ ((((exists pa_h_mul_total_prefix_product_terminal. pa_h_mul_total_prefix_product_terminal + S (r) = S ((S (e * f)) * pa_v_mul_total_prefix_product)) /\ exists pa_q_mul_total_prefix_product_terminal. pa_u_mul_total_prefix_product = pa_q_mul_total_prefix_product_terminal * S ((S (e * f)) * pa_v_mul_total_prefix_product) + (r))) /\ forall pa_i_mul_total_prefix_product. (exists pa_lt_mul_total_prefix_product_bound. pa_lt_mul_total_prefix_product_bound + S pa_i_mul_total_prefix_product = e * f) -> exists pa_p_mul_total_prefix_product pa_r_mul_total_prefix_product pa_s_mul_total_prefix_product. ((((exists pa_h_mul_total_prefix_product_factor. pa_h_mul_total_prefix_product_factor + S (pa_p_mul_total_prefix_product) = S ((S (pa_i_mul_total_prefix_product)) * pa_c_mul_total_prefix)) /\ exists pa_q_mul_total_prefix_product_factor. pa_b_mul_total_prefix = pa_q_mul_total_prefix_product_factor * S ((S (pa_i_mul_total_prefix_product)) * pa_c_mul_total_prefix) + (pa_p_mul_total_prefix_product))) /\ ((((exists pa_h_mul_total_prefix_product_partial. pa_h_mul_total_prefix_product_partial + S (pa_r_mul_total_prefix_product) = S ((S (pa_i_mul_total_prefix_product)) * pa_v_mul_total_prefix_product)) /\ exists pa_q_mul_total_prefix_product_partial. pa_u_mul_total_prefix_product = pa_q_mul_total_prefix_product_partial * S ((S (pa_i_mul_total_prefix_product)) * pa_v_mul_total_prefix_product) + (pa_r_mul_total_prefix_product))) /\ ((((exists pa_h_mul_total_prefix_product_successor. pa_h_mul_total_prefix_product_successor + S (pa_s_mul_total_prefix_product) = S ((S (S pa_i_mul_total_prefix_product)) * pa_v_mul_total_prefix_product)) /\ exists pa_q_mul_total_prefix_product_successor. pa_u_mul_total_prefix_product = pa_q_mul_total_prefix_product_successor * S ((S (S pa_i_mul_total_prefix_product)) * pa_v_mul_total_prefix_product) + (pa_s_mul_total_prefix_product))) /\ pa_s_mul_total_prefix_product = pa_r_mul_total_prefix_product * pa_p_mul_total_prefix_product))))))))
  54. 0054specialize pow_exists a
  55. 0055specialize pow_exists (e * f)
  56. 0056exact pow_exists
  57. 0057cases hqpow
  58. 0058have hprefix : x1 = x2
  59. 0059specialize IH (e * f)
  60. 0060specialize IH x
  61. 0061specialize IH x1
  62. 0062specialize IH x2
  63. 0063apply IH
  64. 0064refl
  65. 0065exact hx
  66. 0066exact hy_step_witness_left
  67. 0067exact hqpow_witness
  68. 0068have hpsum : p = (e * f) + e
  69. 0069trans e * S f
  70. 0070exact hp
  71. 0071apply PA6
  72. 0072have htotal : z = x2 * x
  73. 0073specialize pow_add a
  74. 0074specialize pow_add (e * f)
  75. 0075specialize pow_add e
  76. 0076specialize pow_add p
  77. 0077specialize pow_add x2
  78. 0078specialize pow_add x
  79. 0079specialize pow_add z
  80. 0080apply pow_add
  81. 0081exact hpsum
  82. 0082exact hqpow_witness
  83. 0083exact hx
  84. 0084exact hz
  85. 0085trans x1 * x
  86. 0086exact hy_step_witness_right
  87. 0087trans x2 * x
  88. 0088congr
  89. 0089exact hprefix
  90. 0090refl
  91. 0091symm
  92. 0092exact htotal