Metamath Proof Explorer

Theorem fsumparts

Description: Summation by parts. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Hypotheses fsumparts.b ⊢ ( 𝑘 = 𝑗 → ( 𝐴 = 𝐵 ∧ 𝑉 = 𝑊 ) )
fsumparts.c ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 = 𝐶 ∧ 𝑉 = 𝑋 ) )
fsumparts.d ⊢ ( 𝑘 = 𝑀 → ( 𝐴 = 𝐷 ∧ 𝑉 = 𝑌 ) )
fsumparts.e ⊢ ( 𝑘 = 𝑁 → ( 𝐴 = 𝐸 ∧ 𝑉 = 𝑍 ) )
fsumparts.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
fsumparts.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
fsumparts.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑉 ∈ ℂ )
Assertion fsumparts ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · ( 𝑋 − 𝑊 ) ) = ( ( ( 𝐸 · 𝑍 ) − ( 𝐷 · 𝑌 ) ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 fsumparts.b ⊢ ( 𝑘 = 𝑗 → ( 𝐴 = 𝐵 ∧ 𝑉 = 𝑊 ) )
2 fsumparts.c ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 = 𝐶 ∧ 𝑉 = 𝑋 ) )
3 fsumparts.d ⊢ ( 𝑘 = 𝑀 → ( 𝐴 = 𝐷 ∧ 𝑉 = 𝑌 ) )
4 fsumparts.e ⊢ ( 𝑘 = 𝑁 → ( 𝐴 = 𝐸 ∧ 𝑉 = 𝑍 ) )
5 fsumparts.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
6 fsumparts.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
7 fsumparts.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑉 ∈ ℂ )
8 sum0 ⊢ Σ 𝑗 ∈ ∅ ( 𝐵 · ( 𝑋 − 𝑊 ) ) = 0
9 0m0e0 ⊢ ( 0 − 0 ) = 0
10 8 9 eqtr4i ⊢ Σ 𝑗 ∈ ∅ ( 𝐵 · ( 𝑋 − 𝑊 ) ) = ( 0 − 0 )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → 𝑁 = 𝑀 )
12 11 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ..^ 𝑀 ) )
13 fzo0 ⊢ ( 𝑀 ..^ 𝑀 ) = ∅
14 12 13 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( 𝑀 ..^ 𝑁 ) = ∅ )
15 14 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · ( 𝑋 − 𝑊 ) ) = Σ 𝑗 ∈ ∅ ( 𝐵 · ( 𝑋 − 𝑊 ) ) )
16 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
17 5 16 syl ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑀 ... 𝑁 ) )
18 eqtr3 ⊢ ( ( 𝑘 = 𝑀 ∧ 𝑁 = 𝑀 ) → 𝑘 = 𝑁 )
19 oveq12 ⊢ ( ( 𝐴 = 𝐸 ∧ 𝑉 = 𝑍 ) → ( 𝐴 · 𝑉 ) = ( 𝐸 · 𝑍 ) )
20 18 4 19 3syl ⊢ ( ( 𝑘 = 𝑀 ∧ 𝑁 = 𝑀 ) → ( 𝐴 · 𝑉 ) = ( 𝐸 · 𝑍 ) )
21 oveq12 ⊢ ( ( 𝐴 = 𝐷 ∧ 𝑉 = 𝑌 ) → ( 𝐴 · 𝑉 ) = ( 𝐷 · 𝑌 ) )
22 3 21 syl ⊢ ( 𝑘 = 𝑀 → ( 𝐴 · 𝑉 ) = ( 𝐷 · 𝑌 ) )
23 22 adantr ⊢ ( ( 𝑘 = 𝑀 ∧ 𝑁 = 𝑀 ) → ( 𝐴 · 𝑉 ) = ( 𝐷 · 𝑌 ) )
24 20 23 eqeq12d ⊢ ( ( 𝑘 = 𝑀 ∧ 𝑁 = 𝑀 ) → ( ( 𝐴 · 𝑉 ) = ( 𝐴 · 𝑉 ) ↔ ( 𝐸 · 𝑍 ) = ( 𝐷 · 𝑌 ) ) )
25 24 pm5.74da ⊢ ( 𝑘 = 𝑀 → ( ( 𝑁 = 𝑀 → ( 𝐴 · 𝑉 ) = ( 𝐴 · 𝑉 ) ) ↔ ( 𝑁 = 𝑀 → ( 𝐸 · 𝑍 ) = ( 𝐷 · 𝑌 ) ) ) )
26 eqidd ⊢ ( 𝑁 = 𝑀 → ( 𝐴 · 𝑉 ) = ( 𝐴 · 𝑉 ) )
27 25 26 vtoclg ⊢ ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑁 = 𝑀 → ( 𝐸 · 𝑍 ) = ( 𝐷 · 𝑌 ) ) )
28 27 imp ⊢ ( ( 𝑀 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑁 = 𝑀 ) → ( 𝐸 · 𝑍 ) = ( 𝐷 · 𝑌 ) )
29 17 28 sylan ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( 𝐸 · 𝑍 ) = ( 𝐷 · 𝑌 ) )
30 29 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( ( 𝐸 · 𝑍 ) − ( 𝐷 · 𝑌 ) ) = ( ( 𝐷 · 𝑌 ) − ( 𝐷 · 𝑌 ) ) )
31 3 simpld ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐷 )
32 31 eleq1d ⊢ ( 𝑘 = 𝑀 → ( 𝐴 ∈ ℂ ↔ 𝐷 ∈ ℂ ) )
33 6 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ )
34 32 33 17 rspcdva ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
35 3 simprd ⊢ ( 𝑘 = 𝑀 → 𝑉 = 𝑌 )
36 35 eleq1d ⊢ ( 𝑘 = 𝑀 → ( 𝑉 ∈ ℂ ↔ 𝑌 ∈ ℂ ) )
37 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝑉 ∈ ℂ )
38 36 37 17 rspcdva ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
39 34 38 mulcld ⊢ ( 𝜑 → ( 𝐷 · 𝑌 ) ∈ ℂ )
40 39 subidd ⊢ ( 𝜑 → ( ( 𝐷 · 𝑌 ) − ( 𝐷 · 𝑌 ) ) = 0 )
41 40 adantr ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( ( 𝐷 · 𝑌 ) − ( 𝐷 · 𝑌 ) ) = 0 )
42 30 41 eqtrd ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( ( 𝐸 · 𝑍 ) − ( 𝐷 · 𝑌 ) ) = 0 )
43 14 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) = Σ 𝑗 ∈ ∅ ( ( 𝐶 − 𝐵 ) · 𝑋 ) )
44 sum0 ⊢ Σ 𝑗 ∈ ∅ ( ( 𝐶 − 𝐵 ) · 𝑋 ) = 0
45 43 44 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) = 0 )
46 42 45 oveq12d ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → ( ( ( 𝐸 · 𝑍 ) − ( 𝐷 · 𝑌 ) ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) ) = ( 0 − 0 ) )
47 10 15 46 3eqtr4a ⊢ ( ( 𝜑 ∧ 𝑁 = 𝑀 ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · ( 𝑋 − 𝑊 ) ) = ( ( ( 𝐸 · 𝑍 ) − ( 𝐷 · 𝑌 ) ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) ) )
48 fzofi ⊢ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∈ Fin
49 48 a1i ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑀 + 1 ) ..^ 𝑁 ) ∈ Fin )
50 eluzel2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑀 ∈ ℤ )
51 5 50 syl ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑀 ∈ ℤ )
53 uzid ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) )
54 peano2uz ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
55 fzoss1 ⊢ ( ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( 𝑀 + 1 ) ..^ 𝑁 ) ⊆ ( 𝑀 ..^ 𝑁 ) )
56 52 53 54 55 4syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑀 + 1 ) ..^ 𝑁 ) ⊆ ( 𝑀 ..^ 𝑁 ) )
57 56 sselda ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) )
58 elfzofz ⊢ ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
59 6 7 mulcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐴 · 𝑉 ) ∈ ℂ )
60 58 59 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐴 · 𝑉 ) ∈ ℂ )
61 60 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐴 · 𝑉 ) ∈ ℂ )
62 57 61 syldan ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ) → ( 𝐴 · 𝑉 ) ∈ ℂ )
63 49 62 fsumcl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ∈ ℂ )
64 4 simpld ⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐸 )
65 64 eleq1d ⊢ ( 𝑘 = 𝑁 → ( 𝐴 ∈ ℂ ↔ 𝐸 ∈ ℂ ) )
66 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
67 5 66 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑀 ... 𝑁 ) )
68 65 33 67 rspcdva ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
69 4 simprd ⊢ ( 𝑘 = 𝑁 → 𝑉 = 𝑍 )
70 69 eleq1d ⊢ ( 𝑘 = 𝑁 → ( 𝑉 ∈ ℂ ↔ 𝑍 ∈ ℂ ) )
71 70 37 67 rspcdva ⊢ ( 𝜑 → 𝑍 ∈ ℂ )
72 68 71 mulcld ⊢ ( 𝜑 → ( 𝐸 · 𝑍 ) ∈ ℂ )
73 72 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐸 · 𝑍 ) ∈ ℂ )
74 simpr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) )
75 fzp1ss ⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
76 52 75 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑀 + 1 ) ... 𝑁 ) ⊆ ( 𝑀 ... 𝑁 ) )
77 76 sselda ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
78 59 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐴 · 𝑉 ) ∈ ℂ )
79 77 78 syldan ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ) → ( 𝐴 · 𝑉 ) ∈ ℂ )
80 4 19 syl ⊢ ( 𝑘 = 𝑁 → ( 𝐴 · 𝑉 ) = ( 𝐸 · 𝑍 ) )
81 74 79 80 fsumm1 ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ( 𝐴 · 𝑉 ) = ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 · 𝑉 ) + ( 𝐸 · 𝑍 ) ) )
82 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
83 5 82 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
84 83 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑁 ∈ ℤ )
85 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
86 84 85 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
87 52 zcnd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑀 ∈ ℂ )
88 ax-1cn ⊢ 1 ∈ ℂ
89 pncan ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
90 87 88 89 sylancl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑀 + 1 ) − 1 ) = 𝑀 )
91 90 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
92 86 91 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑀 ..^ 𝑁 ) = ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) )
93 92 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 · 𝑋 ) = Σ 𝑗 ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) ( 𝐶 · 𝑋 ) )
94 1zzd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 1 ∈ ℤ )
95 52 peano2zd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑀 + 1 ) ∈ ℤ )
96 oveq12 ⊢ ( ( 𝐴 = 𝐶 ∧ 𝑉 = 𝑋 ) → ( 𝐴 · 𝑉 ) = ( 𝐶 · 𝑋 ) )
97 2 96 syl ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 · 𝑉 ) = ( 𝐶 · 𝑋 ) )
98 94 95 84 79 97 fsumshftm ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ( 𝐴 · 𝑉 ) = Σ 𝑗 ∈ ( ( ( 𝑀 + 1 ) − 1 ) ... ( 𝑁 − 1 ) ) ( 𝐶 · 𝑋 ) )
99 93 98 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 · 𝑋 ) = Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... 𝑁 ) ( 𝐴 · 𝑉 ) )
100 fzoval ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑀 + 1 ) ..^ 𝑁 ) = ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) )
101 84 100 syl ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝑀 + 1 ) ..^ 𝑁 ) = ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) )
102 101 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) = Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 · 𝑉 ) )
103 102 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) + ( 𝐸 · 𝑍 ) ) = ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 · 𝑉 ) + ( 𝐸 · 𝑍 ) ) )
104 81 99 103 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 · 𝑋 ) = ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) + ( 𝐸 · 𝑍 ) ) )
105 63 73 104 comraddd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 · 𝑋 ) = ( ( 𝐸 · 𝑍 ) + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) )
106 105 oveq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 · 𝑋 ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) ) = ( ( ( 𝐸 · 𝑍 ) + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) ) )
107 fzofzp1 ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) )
108 2 simpld ⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝐴 = 𝐶 )
109 108 eleq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐴 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
110 109 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ ∧ ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝐶 ∈ ℂ )
111 33 107 110 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐶 ∈ ℂ )
112 elfzofz ⊢ ( 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑗 ∈ ( 𝑀 ... 𝑁 ) )
113 1 simpld ⊢ ( 𝑘 = 𝑗 → 𝐴 = 𝐵 )
114 113 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝐴 ∈ ℂ ↔ 𝐵 ∈ ℂ ) )
115 114 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐵 ∈ ℂ )
116 33 112 115 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐵 ∈ ℂ )
117 2 simprd ⊢ ( 𝑘 = ( 𝑗 + 1 ) → 𝑉 = 𝑋 )
118 117 eleq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑉 ∈ ℂ ↔ 𝑋 ∈ ℂ ) )
119 118 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝑉 ∈ ℂ ∧ ( 𝑗 + 1 ) ∈ ( 𝑀 ... 𝑁 ) ) → 𝑋 ∈ ℂ )
120 37 107 119 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑋 ∈ ℂ )
121 111 116 120 subdird ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( ( 𝐶 − 𝐵 ) · 𝑋 ) = ( ( 𝐶 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )
122 121 sumeq2dv ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) )
123 fzofi ⊢ ( 𝑀 ..^ 𝑁 ) ∈ Fin
124 123 a1i ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) ∈ Fin )
125 111 120 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐶 · 𝑋 ) ∈ ℂ )
126 116 120 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐵 · 𝑋 ) ∈ ℂ )
127 124 125 126 fsumsub ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 · 𝑋 ) − ( 𝐵 · 𝑋 ) ) = ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 · 𝑋 ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) ) )
128 122 127 eqtrd ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) = ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 · 𝑋 ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) ) )
129 128 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) = ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐶 · 𝑋 ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) ) )
130 124 126 fsumcl ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) ∈ ℂ )
131 130 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) ∈ ℂ )
132 73 131 63 subsub3d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐸 · 𝑍 ) − ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) ) = ( ( ( 𝐸 · 𝑍 ) + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) ) )
133 106 129 132 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) = ( ( 𝐸 · 𝑍 ) − ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) ) )
134 133 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( ( 𝐸 · 𝑍 ) − ( 𝐷 · 𝑌 ) ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) ) = ( ( ( 𝐸 · 𝑍 ) − ( 𝐷 · 𝑌 ) ) − ( ( 𝐸 · 𝑍 ) − ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) ) ) )
135 39 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐷 · 𝑌 ) ∈ ℂ )
136 131 63 subcld ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) ∈ ℂ )
137 73 135 136 nnncan1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( ( 𝐸 · 𝑍 ) − ( 𝐷 · 𝑌 ) ) − ( ( 𝐸 · 𝑍 ) − ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) ) ) = ( ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) − ( 𝐷 · 𝑌 ) ) )
138 63 135 addcomd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) + ( 𝐷 · 𝑌 ) ) = ( ( 𝐷 · 𝑌 ) + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) )
139 eluzp1m1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
140 51 139 sylan ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
141 86 eleq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ↔ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) )
142 141 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) )
143 142 61 syldan ⊢ ( ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐴 · 𝑉 ) ∈ ℂ )
144 140 143 22 fsum1p ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐴 · 𝑉 ) = ( ( 𝐷 · 𝑌 ) + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 · 𝑉 ) ) )
145 86 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 · 𝑉 ) = Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ( 𝐴 · 𝑉 ) )
146 102 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( 𝐷 · 𝑌 ) + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) = ( ( 𝐷 · 𝑌 ) + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ... ( 𝑁 − 1 ) ) ( 𝐴 · 𝑉 ) ) )
147 144 145 146 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 · 𝑉 ) = ( ( 𝐷 · 𝑌 ) + Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) )
148 138 147 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) + ( 𝐷 · 𝑌 ) ) = Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 · 𝑉 ) )
149 oveq12 ⊢ ( ( 𝐴 = 𝐵 ∧ 𝑉 = 𝑊 ) → ( 𝐴 · 𝑉 ) = ( 𝐵 · 𝑊 ) )
150 1 149 syl ⊢ ( 𝑘 = 𝑗 → ( 𝐴 · 𝑉 ) = ( 𝐵 · 𝑊 ) )
151 150 cbvsumv ⊢ Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐴 · 𝑉 ) = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑊 )
152 148 151 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) + ( 𝐷 · 𝑌 ) ) = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑊 ) )
153 152 oveq2d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) + ( 𝐷 · 𝑌 ) ) ) = ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑊 ) ) )
154 131 63 135 subsub4d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) − ( 𝐷 · 𝑌 ) ) = ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − ( Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) + ( 𝐷 · 𝑌 ) ) ) )
155 1 simprd ⊢ ( 𝑘 = 𝑗 → 𝑉 = 𝑊 )
156 155 eleq1d ⊢ ( 𝑘 = 𝑗 → ( 𝑉 ∈ ℂ ↔ 𝑊 ∈ ℂ ) )
157 156 rspccva ⊢ ( ( ∀ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝑉 ∈ ℂ ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑊 ∈ ℂ )
158 37 112 157 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝑊 ∈ ℂ )
159 116 120 158 subdid ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐵 · ( 𝑋 − 𝑊 ) ) = ( ( 𝐵 · 𝑋 ) − ( 𝐵 · 𝑊 ) ) )
160 159 sumeq2dv ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · ( 𝑋 − 𝑊 ) ) = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐵 · 𝑋 ) − ( 𝐵 · 𝑊 ) ) )
161 116 158 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ) → ( 𝐵 · 𝑊 ) ∈ ℂ )
162 124 126 161 fsumsub ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐵 · 𝑋 ) − ( 𝐵 · 𝑊 ) ) = ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑊 ) ) )
163 160 162 eqtrd ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · ( 𝑋 − 𝑊 ) ) = ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑊 ) ) )
164 163 adantr ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · ( 𝑋 − 𝑊 ) ) = ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑊 ) ) )
165 153 154 164 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → ( ( Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · 𝑋 ) − Σ 𝑘 ∈ ( ( 𝑀 + 1 ) ..^ 𝑁 ) ( 𝐴 · 𝑉 ) ) − ( 𝐷 · 𝑌 ) ) = Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · ( 𝑋 − 𝑊 ) ) )
166 134 137 165 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · ( 𝑋 − 𝑊 ) ) = ( ( ( 𝐸 · 𝑍 ) − ( 𝐷 · 𝑌 ) ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) ) )
167 uzp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
168 5 167 syl ⊢ ( 𝜑 → ( 𝑁 = 𝑀 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) )
169 47 166 168 mpjaodan ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( 𝐵 · ( 𝑋 − 𝑊 ) ) = ( ( ( 𝐸 · 𝑍 ) − ( 𝐷 · 𝑌 ) ) − Σ 𝑗 ∈ ( 𝑀 ..^ 𝑁 ) ( ( 𝐶 − 𝐵 ) · 𝑋 ) ) )