PA007Q

beta_product_pointwise_scale_mod

Alpha v34 checked-use theorem · independently closed; not Stable

Pointwise multiplication by a constant scales a finite product by its power.

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 m a b c z d l P Q A. (forall fsp_index_pointwise fsp_source_pointwise fsp_target_pointwise. (exists fsp_gap_pointwise. fsp_gap_pointwise + S fsp_index_pointwise = l) -> (((exists fsp_source_height_pointwise. fsp_source_height_pointwise + S (fsp_source_pointwise) = S ((S (fsp_index_pointwise)) * c)) /\ exists fsp_source_quotient_pointwise. b = fsp_source_quotient_pointwise * S ((S (fsp_index_pointwise)) * c) + (fsp_source_pointwise))) -> (((exists fsp_target_height_pointwise. fsp_target_height_pointwise + S (fsp_target_pointwise) = S ((S (fsp_index_pointwise)) * d)) /\ exists fsp_target_quotient_pointwise. z = fsp_target_quotient_pointwise * S ((S (fsp_index_pointwise)) * d) + (fsp_target_pointwise))) -> (exists fsp_mod_left_pointwise fsp_mod_right_pointwise. a * fsp_source_pointwise + m * fsp_mod_left_pointwise = fsp_target_pointwise + m * fsp_mod_right_pointwise)) -> (exists ff_u_source ff_v_source. ((((exists ff_h_source_start. ff_h_source_start + S (1) = S ((S (0)) * ff_v_source)) /\ exists ff_q_source_start. ff_u_source = ff_q_source_start * S ((S (0)) * ff_v_source) + (1))) /\ ((((exists ff_h_source_terminal. ff_h_source_terminal + S (P) = S ((S (l)) * ff_v_source)) /\ exists ff_q_source_terminal. ff_u_source = ff_q_source_terminal * S ((S (l)) * ff_v_source) + (P))) /\ forall ff_i_source. (exists ff_lt_source_bound. ff_lt_source_bound + S ff_i_source = l) -> exists ff_p_source ff_r_source ff_s_source. ((((exists ff_h_source_factor. ff_h_source_factor + S (ff_p_source) = S ((S (ff_i_source)) * c)) /\ exists ff_q_source_factor. b = ff_q_source_factor * S ((S (ff_i_source)) * c) + (ff_p_source))) /\ ((((exists ff_h_source_partial. ff_h_source_partial + S (ff_r_source) = S ((S (ff_i_source)) * ff_v_source)) /\ exists ff_q_source_partial. ff_u_source = ff_q_source_partial * S ((S (ff_i_source)) * ff_v_source) + (ff_r_source))) /\ ((((exists ff_h_source_successor. ff_h_source_successor + S (ff_s_source) = S ((S (S ff_i_source)) * ff_v_source)) /\ exists ff_q_source_successor. ff_u_source = ff_q_source_successor * S ((S (S ff_i_source)) * ff_v_source) + (ff_s_source))) /\ ff_s_source = ff_r_source * ff_p_source)))))) -> (exists ff_u_target ff_v_target. ((((exists ff_h_target_start. ff_h_target_start + S (1) = S ((S (0)) * ff_v_target)) /\ exists ff_q_target_start. ff_u_target = ff_q_target_start * S ((S (0)) * ff_v_target) + (1))) /\ ((((exists ff_h_target_terminal. ff_h_target_terminal + S (Q) = S ((S (l)) * ff_v_target)) /\ exists ff_q_target_terminal. ff_u_target = ff_q_target_terminal * S ((S (l)) * ff_v_target) + (Q))) /\ forall ff_i_target. (exists ff_lt_target_bound. ff_lt_target_bound + S ff_i_target = l) -> exists ff_p_target ff_r_target ff_s_target. ((((exists ff_h_target_factor. ff_h_target_factor + S (ff_p_target) = S ((S (ff_i_target)) * d)) /\ exists ff_q_target_factor. z = ff_q_target_factor * S ((S (ff_i_target)) * d) + (ff_p_target))) /\ ((((exists ff_h_target_partial. ff_h_target_partial + S (ff_r_target) = S ((S (ff_i_target)) * ff_v_target)) /\ exists ff_q_target_partial. ff_u_target = ff_q_target_partial * S ((S (ff_i_target)) * ff_v_target) + (ff_r_target))) /\ ((((exists ff_h_target_successor. ff_h_target_successor + S (ff_s_target) = S ((S (S ff_i_target)) * ff_v_target)) /\ exists ff_q_target_successor. ff_u_target = ff_q_target_successor * S ((S (S ff_i_target)) * ff_v_target) + (ff_s_target))) /\ ff_s_target = ff_r_target * ff_p_target)))))) -> (exists ff_b_scale_power ff_c_scale_power. ((forall ff_i_scale_power_repeat. (exists ff_lt_scale_power_repeat_bound. ff_lt_scale_power_repeat_bound + S ff_i_scale_power_repeat = l) -> (((exists ff_h_scale_power_repeat_decoded. ff_h_scale_power_repeat_decoded + S (a) = S ((S (ff_i_scale_power_repeat)) * ff_c_scale_power)) /\ exists ff_q_scale_power_repeat_decoded. ff_b_scale_power = ff_q_scale_power_repeat_decoded * S ((S (ff_i_scale_power_repeat)) * ff_c_scale_power) + (a)))) /\ (exists ff_u_scale_power_product ff_v_scale_power_product. ((((exists ff_h_scale_power_product_start. ff_h_scale_power_product_start + S (1) = S ((S (0)) * ff_v_scale_power_product)) /\ exists ff_q_scale_power_product_start. ff_u_scale_power_product = ff_q_scale_power_product_start * S ((S (0)) * ff_v_scale_power_product) + (1))) /\ ((((exists ff_h_scale_power_product_terminal. ff_h_scale_power_product_terminal + S (A) = S ((S (l)) * ff_v_scale_power_product)) /\ exists ff_q_scale_power_product_terminal. ff_u_scale_power_product = ff_q_scale_power_product_terminal * S ((S (l)) * ff_v_scale_power_product) + (A))) /\ forall ff_i_scale_power_product. (exists ff_lt_scale_power_product_bound. ff_lt_scale_power_product_bound + S ff_i_scale_power_product = l) -> exists ff_p_scale_power_product ff_r_scale_power_product ff_s_scale_power_product. ((((exists ff_h_scale_power_product_factor. ff_h_scale_power_product_factor + S (ff_p_scale_power_product) = S ((S (ff_i_scale_power_product)) * ff_c_scale_power)) /\ exists ff_q_scale_power_product_factor. ff_b_scale_power = ff_q_scale_power_product_factor * S ((S (ff_i_scale_power_product)) * ff_c_scale_power) + (ff_p_scale_power_product))) /\ ((((exists ff_h_scale_power_product_partial. ff_h_scale_power_product_partial + S (ff_r_scale_power_product) = S ((S (ff_i_scale_power_product)) * ff_v_scale_power_product)) /\ exists ff_q_scale_power_product_partial. ff_u_scale_power_product = ff_q_scale_power_product_partial * S ((S (ff_i_scale_power_product)) * ff_v_scale_power_product) + (ff_r_scale_power_product))) /\ ((((exists ff_h_scale_power_product_successor. ff_h_scale_power_product_successor + S (ff_s_scale_power_product) = S ((S (S ff_i_scale_power_product)) * ff_v_scale_power_product)) /\ exists ff_q_scale_power_product_successor. ff_u_scale_power_product = ff_q_scale_power_product_successor * S ((S (S ff_i_scale_power_product)) * ff_v_scale_power_product) + (ff_s_scale_power_product))) /\ ff_s_scale_power_product = ff_r_scale_power_product * ff_p_scale_power_product)))))))) -> (exists fsp_product_mod_left_result fsp_product_mod_right_result. (A * P) + m * fsp_product_mod_left_result = Q + m * fsp_product_mod_right_result)

Structural proof guide

Generated structural guide

Pointwise multiplication by a constant scales a finite product by its power.

Use the direct prerequisites beta_product_zero, beta_product_succ_decompose, pow_zero, pow_successor_decompose, le_succ, le_refl, mod_eq_refl, mod_eq_mul, mul_assoc, mul_comm, one_mul as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (10), intermediate claims (12), equality transport (8), certified simplification (1).

Referenced ingredients

PA0049 beta_product_zero PA004A beta_product_succ_decompose PA004B pow_zero PA004D pow_successor_decompose PA002O le_succ PA001A le_refl PA0023 mod_eq_refl PA004E mod_eq_mul PA000B mul_assoc PA000H mul_comm PA000M one_mul

Proof neighborhood

Direct dependencies

PA0049 beta_product_zero PA004A beta_product_succ_decompose PA004B pow_zero PA004D pow_successor_decompose PA002O le_succ PA001A le_refl PA0023 mod_eq_refl PA004E mod_eq_mul PA000B mul_assoc PA000H mul_comm PA000M one_mul

Direct dependents

PA007R gauss_signed_pointwise_mul_product_mod PA008J prime_mul_residue_product_balance

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

133 script commands · 19 reading checkpoints · 12 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 (9)
beta product zerobeta product succ decomposepow zeropow successor decomposele succle reflmod eq reflmod eq mulone mul

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–6

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

  1. L1
    intro m
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro z
  6. L6
    intro d
02Induction on lL7–14

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

  1. L7
    induction l
  2. L8
    intro P
  3. L9
    intro Q
  4. L10
    intro A
  5. L11
    intro hpw
  6. L12
    intro hP
  7. L13
    intro hQ
  8. L14
    intro hA
03Establish hP1L15–20

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

  1. L15
    have hP1 : P = 1
  2. L16
    specialize beta_product_zero b
  3. L17
    specialize beta_product_zero c
  4. L18
    specialize beta_product_zero P
  5. L19
    apply beta_product_zero
  6. L20
    exact hP
04Establish hQ1L21–26

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

  1. L21
    have hQ1 : Q = 1
  2. L22
    specialize beta_product_zero z
  3. L23
    specialize beta_product_zero d
  4. L24
    specialize beta_product_zero Q
  5. L25
    apply beta_product_zero
  6. L26
    exact hQ
05Establish hA1L27–36

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

  1. L27
    have hA1 : A = 1
  2. L28
    specialize pow_zero a
  3. L29
    specialize pow_zero 0
  4. L30
    specialize pow_zero A
  5. L31
    apply pow_zero
  6. L32
    refl
  7. L33
    exact hA
  8. L34
    rewrite hA1
  9. L35
    rewrite hP1
  10. L36
    rewrite hQ1
06Establish honeL37–46

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

  1. L37
    have hone : 1 * 1 = 1
  2. L38
    specialize one_mul 1
  3. L39
    exact one_mul
  4. L40
    rewrite hone
  5. L41
    specialize mod_eq_refl m
  6. L42
    specialize mod_eq_refl 1
  7. L43
    exact mod_eq_refl
  8. L44
    intro P
  9. L45
    intro Q
  10. L46
    intro A
07Fix variables and assumptionsL47–50

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

  1. L47
    intro hpw
  2. L48
    intro hP
  3. L49
    intro hQ
  4. L50
    intro hA
08Establish hPdL51–57

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

  1. L51
    have hPd : ∃ fsp_decomposition_factor_source_decomposition. ∃ fsp_decomposition_prefix_source_decomposition. BetaAt(b,c,l,fsp_decomposition_factor_source_decomposition) ∧ (Product(b,c,l,fsp_decomposition_prefix_source_decomposition) ∧ P = fsp_decomposition_prefix_source_decomposition · fsp_decomposition_factor_source_decomposition)Definitions: BetaAtProduct
  2. L52
    specialize beta_product_succ_decompose b
  3. L53
    specialize beta_product_succ_decompose c
  4. L54
    specialize beta_product_succ_decompose l
  5. L55
    specialize beta_product_succ_decompose P
  6. L56
    apply beta_product_succ_decompose
  7. L57
    exact hP
09Separate the logical casesL58–61

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

  1. L58
    cases hPd
  2. L59
    cases hPd_witness
  3. L60
    cases hPd_witness_witness
  4. L61
    cases hPd_witness_witness_right
10Establish hQdL62–68

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

  1. L62
    have hQd : ∃ fsp_decomposition_factor_target_decomposition. ∃ fsp_decomposition_prefix_target_decomposition. BetaAt(z,d,l,fsp_decomposition_factor_target_decomposition) ∧ (Product(z,d,l,fsp_decomposition_prefix_target_decomposition) ∧ Q = fsp_decomposition_prefix_target_decomposition · fsp_decomposition_factor_target_decomposition)Definitions: BetaAtProduct
  2. L63
    specialize beta_product_succ_decompose z
  3. L64
    specialize beta_product_succ_decompose d
  4. L65
    specialize beta_product_succ_decompose l
  5. L66
    specialize beta_product_succ_decompose Q
  6. L67
    apply beta_product_succ_decompose
  7. L68
    exact hQ
11Separate the logical casesL69–72

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

  1. L69
    cases hQd
  2. L70
    cases hQd_witness
  3. L71
    cases hQd_witness_witness
  4. L72
    cases hQd_witness_witness_right
12Establish hAdL73–80

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

  1. L73
    have hAd : ∃ fsp_power_prefix_power_decomposition. Pow(a,l,fsp_power_prefix_power_decomposition) ∧ A = fsp_power_prefix_power_decomposition · aDefinitions: Pow
  2. L74
    specialize pow_successor_decompose a
  3. L75
    specialize pow_successor_decompose l
  4. L76
    specialize pow_successor_decompose (S l)
  5. L77
    specialize pow_successor_decompose A
  6. L78
    apply pow_successor_decompose
  7. L79
    refl
  8. L80
    exact hA
13Separate the logical casesL81–82

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

  1. L81
    cases hAd
  2. L82
    cases hAd_witness
14Establish hpw_prefixL83–92

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

  1. L83
    have hpw_prefix : ∀ fsp_index_pointwise_prefix. ∀ fsp_source_pointwise_prefix. ∀ fsp_target_pointwise_prefix. Lt(fsp_index_pointwise_prefix,l) → BetaAt(b,c,fsp_index_pointwise_prefix,fsp_source_pointwise_prefix) → BetaAt(z,d,fsp_index_pointwise_prefix,fsp_target_pointwise_prefix) → ModEq(m,a · fsp_source_pointwise_prefix,fsp_target_pointwise_prefix)Definitions: LtModEqBetaAt
  2. L84
    intro i
  3. L85
    intro v
  4. L86
    intro w
  5. L87
    intro hi
  6. L88
    intro hv
  7. L89
    intro hw
  8. L90
    specialize hpw i
  9. L91
    specialize hpw v
  10. L92
    specialize hpw w
15Use earlier factsL93–99

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

  1. L93
    apply hpw
  2. L94
    specialize le_succ (S i)
  3. L95
    specialize le_succ l
  4. L96
    apply le_succ
  5. L97
    exact hi
  6. L98
    exact hv
  7. L99
    exact hw
16Establish hprefixL100–108

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

  1. L100
    have hprefix : exists u v. (x4 * x1) + m * u = x3 + m * v
  2. L101
    specialize IH x1
  3. L102
    specialize IH x3
  4. L103
    specialize IH x4
  5. L104
    apply IH
  6. L105
    exact hpw_prefix
  7. L106
    exact hPd_witness_witness_right_left
  8. L107
    exact hQd_witness_witness_right_left
  9. L108
    exact hAd_witness_left
17Establish hentryL109–117

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

  1. L109
    have hentry : exists u v. (a * x) + m * u = x2 + m * v
  2. L110
    specialize hpw l
  3. L111
    specialize hpw x
  4. L112
    specialize hpw x2
  5. L113
    apply hpw
  6. L114
    specialize le_refl (S l)
  7. L115
    exact le_refl
  8. L116
    exact hPd_witness_witness_left
  9. L117
    exact hQd_witness_witness_left
18Establish hfoldL118–126

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

  1. L118
    have hfold : exists u v. ((x4 * x1) * (a * x)) + m * u = (x3 * x2) + m * v
  2. L119
    specialize mod_eq_mul m
  3. L120
    specialize mod_eq_mul (x4 * x1)
  4. L121
    specialize mod_eq_mul x3
  5. L122
    specialize mod_eq_mul (a * x)
  6. L123
    specialize mod_eq_mul x2
  7. L124
    apply mod_eq_mul
  8. L125
    exact hprefix
  9. L126
    exact hentry
19Establish hshuffleL127–133

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

  1. L127
    have hshuffle : (x4 * a) * (x1 * x) = (x4 * x1) * (a * x)
  2. L128
    simp [mul_assoc, mul_comm]
  3. L129
    rewrite hAd_witness_right
  4. L130
    rewrite hPd_witness_witness_right_right
  5. L131
    rewrite hQd_witness_witness_right_right
  6. L132
    rewrite hshuffle
  7. L133
    exact hfold

Library-wide reading audit

Original exact command ledger · 133 lines
  1. 0001intro m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro z
  6. 0006intro d
  7. 0007induction l
  8. 0008intro P
  9. 0009intro Q
  10. 0010intro A
  11. 0011intro hpw
  12. 0012intro hP
  13. 0013intro hQ
  14. 0014intro hA
  15. 0015have hP1 : P = 1
  16. 0016specialize beta_product_zero b
  17. 0017specialize beta_product_zero c
  18. 0018specialize beta_product_zero P
  19. 0019apply beta_product_zero
  20. 0020exact hP
  21. 0021have hQ1 : Q = 1
  22. 0022specialize beta_product_zero z
  23. 0023specialize beta_product_zero d
  24. 0024specialize beta_product_zero Q
  25. 0025apply beta_product_zero
  26. 0026exact hQ
  27. 0027have hA1 : A = 1
  28. 0028specialize pow_zero a
  29. 0029specialize pow_zero 0
  30. 0030specialize pow_zero A
  31. 0031apply pow_zero
  32. 0032refl
  33. 0033exact hA
  34. 0034rewrite hA1
  35. 0035rewrite hP1
  36. 0036rewrite hQ1
  37. 0037have hone : 1 * 1 = 1
  38. 0038specialize one_mul 1
  39. 0039exact one_mul
  40. 0040rewrite hone
  41. 0041specialize mod_eq_refl m
  42. 0042specialize mod_eq_refl 1
  43. 0043exact mod_eq_refl
  44. 0044intro P
  45. 0045intro Q
  46. 0046intro A
  47. 0047intro hpw
  48. 0048intro hP
  49. 0049intro hQ
  50. 0050intro hA
  51. 0051have hPd : exists fsp_decomposition_factor_source_decomposition fsp_decomposition_prefix_source_decomposition. (((exists ff_h_source_decomposition_factor. ff_h_source_decomposition_factor + S (fsp_decomposition_factor_source_decomposition) = S ((S (l)) * c)) /\ exists ff_q_source_decomposition_factor. b = ff_q_source_decomposition_factor * S ((S (l)) * c) + (fsp_decomposition_factor_source_decomposition))) /\ ((exists ff_u_source_decomposition_prefix ff_v_source_decomposition_prefix. ((((exists ff_h_source_decomposition_prefix_start. ff_h_source_decomposition_prefix_start + S (1) = S ((S (0)) * ff_v_source_decomposition_prefix)) /\ exists ff_q_source_decomposition_prefix_start. ff_u_source_decomposition_prefix = ff_q_source_decomposition_prefix_start * S ((S (0)) * ff_v_source_decomposition_prefix) + (1))) /\ ((((exists ff_h_source_decomposition_prefix_terminal. ff_h_source_decomposition_prefix_terminal + S (fsp_decomposition_prefix_source_decomposition) = S ((S (l)) * ff_v_source_decomposition_prefix)) /\ exists ff_q_source_decomposition_prefix_terminal. ff_u_source_decomposition_prefix = ff_q_source_decomposition_prefix_terminal * S ((S (l)) * ff_v_source_decomposition_prefix) + (fsp_decomposition_prefix_source_decomposition))) /\ forall ff_i_source_decomposition_prefix. (exists ff_lt_source_decomposition_prefix_bound. ff_lt_source_decomposition_prefix_bound + S ff_i_source_decomposition_prefix = l) -> exists ff_p_source_decomposition_prefix ff_r_source_decomposition_prefix ff_s_source_decomposition_prefix. ((((exists ff_h_source_decomposition_prefix_factor. ff_h_source_decomposition_prefix_factor + S (ff_p_source_decomposition_prefix) = S ((S (ff_i_source_decomposition_prefix)) * c)) /\ exists ff_q_source_decomposition_prefix_factor. b = ff_q_source_decomposition_prefix_factor * S ((S (ff_i_source_decomposition_prefix)) * c) + (ff_p_source_decomposition_prefix))) /\ ((((exists ff_h_source_decomposition_prefix_partial. ff_h_source_decomposition_prefix_partial + S (ff_r_source_decomposition_prefix) = S ((S (ff_i_source_decomposition_prefix)) * ff_v_source_decomposition_prefix)) /\ exists ff_q_source_decomposition_prefix_partial. ff_u_source_decomposition_prefix = ff_q_source_decomposition_prefix_partial * S ((S (ff_i_source_decomposition_prefix)) * ff_v_source_decomposition_prefix) + (ff_r_source_decomposition_prefix))) /\ ((((exists ff_h_source_decomposition_prefix_successor. ff_h_source_decomposition_prefix_successor + S (ff_s_source_decomposition_prefix) = S ((S (S ff_i_source_decomposition_prefix)) * ff_v_source_decomposition_prefix)) /\ exists ff_q_source_decomposition_prefix_successor. ff_u_source_decomposition_prefix = ff_q_source_decomposition_prefix_successor * S ((S (S ff_i_source_decomposition_prefix)) * ff_v_source_decomposition_prefix) + (ff_s_source_decomposition_prefix))) /\ ff_s_source_decomposition_prefix = ff_r_source_decomposition_prefix * ff_p_source_decomposition_prefix)))))) /\ P = fsp_decomposition_prefix_source_decomposition * fsp_decomposition_factor_source_decomposition)
  52. 0052specialize beta_product_succ_decompose b
  53. 0053specialize beta_product_succ_decompose c
  54. 0054specialize beta_product_succ_decompose l
  55. 0055specialize beta_product_succ_decompose P
  56. 0056apply beta_product_succ_decompose
  57. 0057exact hP
  58. 0058cases hPd
  59. 0059cases hPd_witness
  60. 0060cases hPd_witness_witness
  61. 0061cases hPd_witness_witness_right
  62. 0062have hQd : exists fsp_decomposition_factor_target_decomposition fsp_decomposition_prefix_target_decomposition. (((exists ff_h_target_decomposition_factor. ff_h_target_decomposition_factor + S (fsp_decomposition_factor_target_decomposition) = S ((S (l)) * d)) /\ exists ff_q_target_decomposition_factor. z = ff_q_target_decomposition_factor * S ((S (l)) * d) + (fsp_decomposition_factor_target_decomposition))) /\ ((exists ff_u_target_decomposition_prefix ff_v_target_decomposition_prefix. ((((exists ff_h_target_decomposition_prefix_start. ff_h_target_decomposition_prefix_start + S (1) = S ((S (0)) * ff_v_target_decomposition_prefix)) /\ exists ff_q_target_decomposition_prefix_start. ff_u_target_decomposition_prefix = ff_q_target_decomposition_prefix_start * S ((S (0)) * ff_v_target_decomposition_prefix) + (1))) /\ ((((exists ff_h_target_decomposition_prefix_terminal. ff_h_target_decomposition_prefix_terminal + S (fsp_decomposition_prefix_target_decomposition) = S ((S (l)) * ff_v_target_decomposition_prefix)) /\ exists ff_q_target_decomposition_prefix_terminal. ff_u_target_decomposition_prefix = ff_q_target_decomposition_prefix_terminal * S ((S (l)) * ff_v_target_decomposition_prefix) + (fsp_decomposition_prefix_target_decomposition))) /\ forall ff_i_target_decomposition_prefix. (exists ff_lt_target_decomposition_prefix_bound. ff_lt_target_decomposition_prefix_bound + S ff_i_target_decomposition_prefix = l) -> exists ff_p_target_decomposition_prefix ff_r_target_decomposition_prefix ff_s_target_decomposition_prefix. ((((exists ff_h_target_decomposition_prefix_factor. ff_h_target_decomposition_prefix_factor + S (ff_p_target_decomposition_prefix) = S ((S (ff_i_target_decomposition_prefix)) * d)) /\ exists ff_q_target_decomposition_prefix_factor. z = ff_q_target_decomposition_prefix_factor * S ((S (ff_i_target_decomposition_prefix)) * d) + (ff_p_target_decomposition_prefix))) /\ ((((exists ff_h_target_decomposition_prefix_partial. ff_h_target_decomposition_prefix_partial + S (ff_r_target_decomposition_prefix) = S ((S (ff_i_target_decomposition_prefix)) * ff_v_target_decomposition_prefix)) /\ exists ff_q_target_decomposition_prefix_partial. ff_u_target_decomposition_prefix = ff_q_target_decomposition_prefix_partial * S ((S (ff_i_target_decomposition_prefix)) * ff_v_target_decomposition_prefix) + (ff_r_target_decomposition_prefix))) /\ ((((exists ff_h_target_decomposition_prefix_successor. ff_h_target_decomposition_prefix_successor + S (ff_s_target_decomposition_prefix) = S ((S (S ff_i_target_decomposition_prefix)) * ff_v_target_decomposition_prefix)) /\ exists ff_q_target_decomposition_prefix_successor. ff_u_target_decomposition_prefix = ff_q_target_decomposition_prefix_successor * S ((S (S ff_i_target_decomposition_prefix)) * ff_v_target_decomposition_prefix) + (ff_s_target_decomposition_prefix))) /\ ff_s_target_decomposition_prefix = ff_r_target_decomposition_prefix * ff_p_target_decomposition_prefix)))))) /\ Q = fsp_decomposition_prefix_target_decomposition * fsp_decomposition_factor_target_decomposition)
  63. 0063specialize beta_product_succ_decompose z
  64. 0064specialize beta_product_succ_decompose d
  65. 0065specialize beta_product_succ_decompose l
  66. 0066specialize beta_product_succ_decompose Q
  67. 0067apply beta_product_succ_decompose
  68. 0068exact hQ
  69. 0069cases hQd
  70. 0070cases hQd_witness
  71. 0071cases hQd_witness_witness
  72. 0072cases hQd_witness_witness_right
  73. 0073have hAd : exists fsp_power_prefix_power_decomposition. (exists ff_b_power_decomposition_relation ff_c_power_decomposition_relation. ((forall ff_i_power_decomposition_relation_repeat. (exists ff_lt_power_decomposition_relation_repeat_bound. ff_lt_power_decomposition_relation_repeat_bound + S ff_i_power_decomposition_relation_repeat = l) -> (((exists ff_h_power_decomposition_relation_repeat_decoded. ff_h_power_decomposition_relation_repeat_decoded + S (a) = S ((S (ff_i_power_decomposition_relation_repeat)) * ff_c_power_decomposition_relation)) /\ exists ff_q_power_decomposition_relation_repeat_decoded. ff_b_power_decomposition_relation = ff_q_power_decomposition_relation_repeat_decoded * S ((S (ff_i_power_decomposition_relation_repeat)) * ff_c_power_decomposition_relation) + (a)))) /\ (exists ff_u_power_decomposition_relation_product ff_v_power_decomposition_relation_product. ((((exists ff_h_power_decomposition_relation_product_start. ff_h_power_decomposition_relation_product_start + S (1) = S ((S (0)) * ff_v_power_decomposition_relation_product)) /\ exists ff_q_power_decomposition_relation_product_start. ff_u_power_decomposition_relation_product = ff_q_power_decomposition_relation_product_start * S ((S (0)) * ff_v_power_decomposition_relation_product) + (1))) /\ ((((exists ff_h_power_decomposition_relation_product_terminal. ff_h_power_decomposition_relation_product_terminal + S (fsp_power_prefix_power_decomposition) = S ((S (l)) * ff_v_power_decomposition_relation_product)) /\ exists ff_q_power_decomposition_relation_product_terminal. ff_u_power_decomposition_relation_product = ff_q_power_decomposition_relation_product_terminal * S ((S (l)) * ff_v_power_decomposition_relation_product) + (fsp_power_prefix_power_decomposition))) /\ forall ff_i_power_decomposition_relation_product. (exists ff_lt_power_decomposition_relation_product_bound. ff_lt_power_decomposition_relation_product_bound + S ff_i_power_decomposition_relation_product = l) -> exists ff_p_power_decomposition_relation_product ff_r_power_decomposition_relation_product ff_s_power_decomposition_relation_product. ((((exists ff_h_power_decomposition_relation_product_factor. ff_h_power_decomposition_relation_product_factor + S (ff_p_power_decomposition_relation_product) = S ((S (ff_i_power_decomposition_relation_product)) * ff_c_power_decomposition_relation)) /\ exists ff_q_power_decomposition_relation_product_factor. ff_b_power_decomposition_relation = ff_q_power_decomposition_relation_product_factor * S ((S (ff_i_power_decomposition_relation_product)) * ff_c_power_decomposition_relation) + (ff_p_power_decomposition_relation_product))) /\ ((((exists ff_h_power_decomposition_relation_product_partial. ff_h_power_decomposition_relation_product_partial + S (ff_r_power_decomposition_relation_product) = S ((S (ff_i_power_decomposition_relation_product)) * ff_v_power_decomposition_relation_product)) /\ exists ff_q_power_decomposition_relation_product_partial. ff_u_power_decomposition_relation_product = ff_q_power_decomposition_relation_product_partial * S ((S (ff_i_power_decomposition_relation_product)) * ff_v_power_decomposition_relation_product) + (ff_r_power_decomposition_relation_product))) /\ ((((exists ff_h_power_decomposition_relation_product_successor. ff_h_power_decomposition_relation_product_successor + S (ff_s_power_decomposition_relation_product) = S ((S (S ff_i_power_decomposition_relation_product)) * ff_v_power_decomposition_relation_product)) /\ exists ff_q_power_decomposition_relation_product_successor. ff_u_power_decomposition_relation_product = ff_q_power_decomposition_relation_product_successor * S ((S (S ff_i_power_decomposition_relation_product)) * ff_v_power_decomposition_relation_product) + (ff_s_power_decomposition_relation_product))) /\ ff_s_power_decomposition_relation_product = ff_r_power_decomposition_relation_product * ff_p_power_decomposition_relation_product)))))))) /\ A = fsp_power_prefix_power_decomposition * a
  74. 0074specialize pow_successor_decompose a
  75. 0075specialize pow_successor_decompose l
  76. 0076specialize pow_successor_decompose (S l)
  77. 0077specialize pow_successor_decompose A
  78. 0078apply pow_successor_decompose
  79. 0079refl
  80. 0080exact hA
  81. 0081cases hAd
  82. 0082cases hAd_witness
  83. 0083have hpw_prefix : forall fsp_index_pointwise_prefix fsp_source_pointwise_prefix fsp_target_pointwise_prefix. (exists fsp_gap_pointwise_prefix. fsp_gap_pointwise_prefix + S fsp_index_pointwise_prefix = l) -> (((exists fsp_source_height_pointwise_prefix. fsp_source_height_pointwise_prefix + S (fsp_source_pointwise_prefix) = S ((S (fsp_index_pointwise_prefix)) * c)) /\ exists fsp_source_quotient_pointwise_prefix. b = fsp_source_quotient_pointwise_prefix * S ((S (fsp_index_pointwise_prefix)) * c) + (fsp_source_pointwise_prefix))) -> (((exists fsp_target_height_pointwise_prefix. fsp_target_height_pointwise_prefix + S (fsp_target_pointwise_prefix) = S ((S (fsp_index_pointwise_prefix)) * d)) /\ exists fsp_target_quotient_pointwise_prefix. z = fsp_target_quotient_pointwise_prefix * S ((S (fsp_index_pointwise_prefix)) * d) + (fsp_target_pointwise_prefix))) -> (exists fsp_mod_left_pointwise_prefix fsp_mod_right_pointwise_prefix. a * fsp_source_pointwise_prefix + m * fsp_mod_left_pointwise_prefix = fsp_target_pointwise_prefix + m * fsp_mod_right_pointwise_prefix)
  84. 0084intro i
  85. 0085intro v
  86. 0086intro w
  87. 0087intro hi
  88. 0088intro hv
  89. 0089intro hw
  90. 0090specialize hpw i
  91. 0091specialize hpw v
  92. 0092specialize hpw w
  93. 0093apply hpw
  94. 0094specialize le_succ (S i)
  95. 0095specialize le_succ l
  96. 0096apply le_succ
  97. 0097exact hi
  98. 0098exact hv
  99. 0099exact hw
  100. 0100have hprefix : exists u v. (x4 * x1) + m * u = x3 + m * v
  101. 0101specialize IH x1
  102. 0102specialize IH x3
  103. 0103specialize IH x4
  104. 0104apply IH
  105. 0105exact hpw_prefix
  106. 0106exact hPd_witness_witness_right_left
  107. 0107exact hQd_witness_witness_right_left
  108. 0108exact hAd_witness_left
  109. 0109have hentry : exists u v. (a * x) + m * u = x2 + m * v
  110. 0110specialize hpw l
  111. 0111specialize hpw x
  112. 0112specialize hpw x2
  113. 0113apply hpw
  114. 0114specialize le_refl (S l)
  115. 0115exact le_refl
  116. 0116exact hPd_witness_witness_left
  117. 0117exact hQd_witness_witness_left
  118. 0118have hfold : exists u v. ((x4 * x1) * (a * x)) + m * u = (x3 * x2) + m * v
  119. 0119specialize mod_eq_mul m
  120. 0120specialize mod_eq_mul (x4 * x1)
  121. 0121specialize mod_eq_mul x3
  122. 0122specialize mod_eq_mul (a * x)
  123. 0123specialize mod_eq_mul x2
  124. 0124apply mod_eq_mul
  125. 0125exact hprefix
  126. 0126exact hentry
  127. 0127have hshuffle : (x4 * a) * (x1 * x) = (x4 * x1) * (a * x)
  128. 0128simp [mul_assoc, mul_comm]
  129. 0129rewrite hAd_witness_right
  130. 0130rewrite hPd_witness_witness_right_right
  131. 0131rewrite hQd_witness_witness_right_right
  132. 0132rewrite hshuffle
  133. 0133exact hfold