Metamath Proof Explorer


Theorem fsumshftd

Description: Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft . The proof demonstrates how this can be derived starting from from fsumshft . (Contributed by NM, 1-Nov-2019)

Ref Expression
Hypotheses fsumshftd.1 ( 𝜑𝐾 ∈ ℤ )
fsumshftd.2 ( 𝜑𝑀 ∈ ℤ )
fsumshftd.3 ( 𝜑𝑁 ∈ ℤ )
fsumshftd.4 ( ( 𝜑𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
fsumshftd.5 ( ( 𝜑𝑗 = ( 𝑘𝐾 ) ) → 𝐴 = 𝐵 )
Assertion fsumshftd ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )

Proof

Step Hyp Ref Expression
1 fsumshftd.1 ( 𝜑𝐾 ∈ ℤ )
2 fsumshftd.2 ( 𝜑𝑀 ∈ ℤ )
3 fsumshftd.3 ( 𝜑𝑁 ∈ ℤ )
4 fsumshftd.4 ( ( 𝜑𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5 fsumshftd.5 ( ( 𝜑𝑗 = ( 𝑘𝐾 ) ) → 𝐴 = 𝐵 )
6 nfcv 𝑤 𝐴
7 nfcsb1v 𝑗 𝑤 / 𝑗 𝐴
8 csbeq1a ( 𝑗 = 𝑤𝐴 = 𝑤 / 𝑗 𝐴 )
9 6 7 8 cbvsumi Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑤 ∈ ( 𝑀 ... 𝑁 ) 𝑤 / 𝑗 𝐴
10 nfv 𝑗 ( 𝜑𝑤 ∈ ( 𝑀 ... 𝑁 ) )
11 7 nfel1 𝑗 𝑤 / 𝑗 𝐴 ∈ ℂ
12 10 11 nfim 𝑗 ( ( 𝜑𝑤 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑤 / 𝑗 𝐴 ∈ ℂ )
13 eleq1w ( 𝑗 = 𝑤 → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑤 ∈ ( 𝑀 ... 𝑁 ) ) )
14 13 anbi2d ( 𝑗 = 𝑤 → ( ( 𝜑𝑗 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑𝑤 ∈ ( 𝑀 ... 𝑁 ) ) ) )
15 8 eleq1d ( 𝑗 = 𝑤 → ( 𝐴 ∈ ℂ ↔ 𝑤 / 𝑗 𝐴 ∈ ℂ ) )
16 14 15 imbi12d ( 𝑗 = 𝑤 → ( ( ( 𝜑𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ ) ↔ ( ( 𝜑𝑤 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑤 / 𝑗 𝐴 ∈ ℂ ) ) )
17 12 16 4 chvarfv ( ( 𝜑𝑤 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑤 / 𝑗 𝐴 ∈ ℂ )
18 csbeq1 ( 𝑤 = ( 𝑘𝐾 ) → 𝑤 / 𝑗 𝐴 = ( 𝑘𝐾 ) / 𝑗 𝐴 )
19 1 2 3 17 18 fsumshft ( 𝜑 → Σ 𝑤 ∈ ( 𝑀 ... 𝑁 ) 𝑤 / 𝑗 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ( 𝑘𝐾 ) / 𝑗 𝐴 )
20 ovexd ( 𝜑 → ( 𝑘𝐾 ) ∈ V )
21 20 5 csbied ( 𝜑 ( 𝑘𝐾 ) / 𝑗 𝐴 = 𝐵 )
22 21 sumeq2sdv ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ( 𝑘𝐾 ) / 𝑗 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )
23 19 22 eqtrd ( 𝜑 → Σ 𝑤 ∈ ( 𝑀 ... 𝑁 ) 𝑤 / 𝑗 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )
24 9 23 syl5eq ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) 𝐵 )