Metamath Proof Explorer

Theorem fsum0diag2

Description: Two ways to express "the sum of A ( j , k ) over the triangular region 0 <_ j , 0 <_ k , j + k <_ N ". (Contributed by Mario Carneiro, 21-Jul-2014)

Ref Expression
Hypotheses fsum0diag2.1 ⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐴 )
fsum0diag2.2 ⊢ ( 𝑥 = ( 𝑘 − 𝑗 ) → 𝐵 = 𝐶 )
fsum0diag2.3 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ) → 𝐴 ∈ ℂ )
Assertion fsum0diag2 ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐴 = Σ 𝑘 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... 𝑘 ) 𝐶 )

Proof

Step Hyp Ref Expression
1 fsum0diag2.1 ⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐴 )
2 fsum0diag2.2 ⊢ ( 𝑥 = ( 𝑘 − 𝑗 ) → 𝐵 = 𝐶 )
3 fsum0diag2.3 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ) → 𝐴 ∈ ℂ )
4 fznn0sub2 ⊢ ( 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) → ( ( 𝑁 − 𝑗 ) − 𝑛 ) ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) )
5 4 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ) → ( ( 𝑁 − 𝑗 ) − 𝑛 ) ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) )
6 3 expr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) → 𝐴 ∈ ℂ ) )
7 6 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∀ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐴 ∈ ℂ )
8 1 eleq1d ⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∈ ℂ ↔ 𝐴 ∈ ℂ ) )
9 8 cbvralvw ⊢ ( ∀ 𝑥 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐵 ∈ ℂ ↔ ∀ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐴 ∈ ℂ )
10 7 9 sylibr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ∀ 𝑥 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐵 ∈ ℂ )
11 10 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ) → ∀ 𝑥 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐵 ∈ ℂ )
12 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵
13 12 nfel1 ⊢ Ⅎ 𝑥 ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 ∈ ℂ
14 csbeq1a ⊢ ( 𝑥 = ( ( 𝑁 − 𝑗 ) − 𝑛 ) → 𝐵 = ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
15 14 eleq1d ⊢ ( 𝑥 = ( ( 𝑁 − 𝑗 ) − 𝑛 ) → ( 𝐵 ∈ ℂ ↔ ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
16 13 15 rspc ⊢ ( ( ( 𝑁 − 𝑗 ) − 𝑛 ) ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) → ( ∀ 𝑥 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐵 ∈ ℂ → ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
17 5 11 16 sylc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ) → ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 ∈ ℂ )
18 17 fsum0diag ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 = Σ 𝑛 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
19 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑘 / 𝑥 ⦌ 𝐵
20 19 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ℂ
21 csbeq1a ⊢ ( 𝑥 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
22 21 eleq1d ⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∈ ℂ ↔ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
23 20 22 rspc ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) → ( ∀ 𝑥 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐵 ∈ ℂ → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
24 10 23 mpan9 ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ∈ ℂ )
25 csbeq1 ⊢ ( 𝑘 = ( ( 0 + ( 𝑁 − 𝑗 ) ) − 𝑛 ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = ⦋ ( ( 0 + ( 𝑁 − 𝑗 ) ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
26 24 25 fsumrev2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ ( ( 0 + ( 𝑁 − 𝑗 ) ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
27 elfz3nn0 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
28 27 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → 𝑁 ∈ ℕ0 )
29 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℤ )
30 29 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → 𝑗 ∈ ℤ )
31 nn0cn ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
32 zcn ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ℂ )
33 subcl ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝑁 − 𝑗 ) ∈ ℂ )
34 31 32 33 syl2an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) → ( 𝑁 − 𝑗 ) ∈ ℂ )
35 28 30 34 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → ( 𝑁 − 𝑗 ) ∈ ℂ )
36 addlid ⊢ ( ( 𝑁 − 𝑗 ) ∈ ℂ → ( 0 + ( 𝑁 − 𝑗 ) ) = ( 𝑁 − 𝑗 ) )
37 35 36 syl ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → ( 0 + ( 𝑁 − 𝑗 ) ) = ( 𝑁 − 𝑗 ) )
38 37 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → ( ( 0 + ( 𝑁 − 𝑗 ) ) − 𝑛 ) = ( ( 𝑁 − 𝑗 ) − 𝑛 ) )
39 38 csbeq1d ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → ⦋ ( ( 0 + ( 𝑁 − 𝑗 ) ) − 𝑛 ) / 𝑥 ⦌ 𝐵 = ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
40 39 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ ( ( 0 + ( 𝑁 − 𝑗 ) ) − 𝑛 ) / 𝑥 ⦌ 𝐵 = Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
41 26 40 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
42 41 sumeq2dv ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑛 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
43 elfz3nn0 ⊢ ( 𝑛 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
44 43 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
45 addlid ⊢ ( 𝑁 ∈ ℂ → ( 0 + 𝑁 ) = 𝑁 )
46 44 31 45 3syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( 0 + 𝑁 ) = 𝑁 )
47 46 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( ( 0 + 𝑁 ) − 𝑛 ) = ( 𝑁 − 𝑛 ) )
48 47 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( 0 ... ( ( 0 + 𝑁 ) − 𝑛 ) ) = ( 0 ... ( 𝑁 − 𝑛 ) ) )
49 47 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) = ( ( 𝑁 − 𝑛 ) − 𝑗 ) )
50 49 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) ) → ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) = ( ( 𝑁 − 𝑛 ) − 𝑗 ) )
51 43 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) ) → 𝑁 ∈ ℕ0 )
52 elfzelz ⊢ ( 𝑛 ∈ ( 0 ... 𝑁 ) → 𝑛 ∈ ℤ )
53 52 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) ) → 𝑛 ∈ ℤ )
54 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) → 𝑗 ∈ ℤ )
55 54 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) ) → 𝑗 ∈ ℤ )
56 zcn ⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℂ )
57 sub32 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( ( 𝑁 − 𝑛 ) − 𝑗 ) = ( ( 𝑁 − 𝑗 ) − 𝑛 ) )
58 31 56 32 57 syl3an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑛 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( ( 𝑁 − 𝑛 ) − 𝑗 ) = ( ( 𝑁 − 𝑗 ) − 𝑛 ) )
59 51 53 55 58 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) ) → ( ( 𝑁 − 𝑛 ) − 𝑗 ) = ( ( 𝑁 − 𝑗 ) − 𝑛 ) )
60 50 59 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) ) → ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) = ( ( 𝑁 − 𝑗 ) − 𝑛 ) )
61 60 csbeq1d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) ) → ⦋ ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) / 𝑥 ⦌ 𝐵 = ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
62 48 61 sumeq12rdv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ... 𝑁 ) ) → Σ 𝑗 ∈ ( 0 ... ( ( 0 + 𝑁 ) − 𝑛 ) ) ⦋ ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) / 𝑥 ⦌ 𝐵 = Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
63 62 sumeq2dv ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... ( ( 0 + 𝑁 ) − 𝑛 ) ) ⦋ ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) / 𝑥 ⦌ 𝐵 = Σ 𝑛 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑛 ) ) ⦋ ( ( 𝑁 − 𝑗 ) − 𝑛 ) / 𝑥 ⦌ 𝐵 )
64 18 42 63 3eqtr4d ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = Σ 𝑛 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... ( ( 0 + 𝑁 ) − 𝑛 ) ) ⦋ ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) / 𝑥 ⦌ 𝐵 )
65 fzfid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 0 ... 𝑘 ) ∈ Fin )
66 elfzuz3 ⊢ ( 𝑗 ∈ ( 0 ... 𝑘 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) )
67 66 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) )
68 elfzuz3 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
69 68 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
70 69 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) )
71 elfzuzb ⊢ ( 𝑘 ∈ ( 𝑗 ... 𝑁 ) ↔ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) ) )
72 67 70 71 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝑘 ∈ ( 𝑗 ... 𝑁 ) )
73 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑘 ) → 𝑗 ∈ ℤ )
74 73 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝑗 ∈ ℤ )
75 elfzel2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑁 ∈ ℤ )
76 75 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝑁 ∈ ℤ )
77 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
78 77 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝑘 ∈ ℤ )
79 fzsubel ⊢ ( ( ( 𝑗 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ 𝑗 ∈ ℤ ) ) → ( 𝑘 ∈ ( 𝑗 ... 𝑁 ) ↔ ( 𝑘 − 𝑗 ) ∈ ( ( 𝑗 − 𝑗 ) ... ( 𝑁 − 𝑗 ) ) ) )
80 74 76 78 74 79 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 ∈ ( 𝑗 ... 𝑁 ) ↔ ( 𝑘 − 𝑗 ) ∈ ( ( 𝑗 − 𝑗 ) ... ( 𝑁 − 𝑗 ) ) ) )
81 72 80 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 − 𝑗 ) ∈ ( ( 𝑗 − 𝑗 ) ... ( 𝑁 − 𝑗 ) ) )
82 subid ⊢ ( 𝑗 ∈ ℂ → ( 𝑗 − 𝑗 ) = 0 )
83 74 32 82 3syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑗 − 𝑗 ) = 0 )
84 83 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( ( 𝑗 − 𝑗 ) ... ( 𝑁 − 𝑗 ) ) = ( 0 ... ( 𝑁 − 𝑗 ) ) )
85 81 84 eleqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ( 𝑘 − 𝑗 ) ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) )
86 simpll ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝜑 )
87 fzss2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑘 ) → ( 0 ... 𝑘 ) ⊆ ( 0 ... 𝑁 ) )
88 69 87 syl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 0 ... 𝑘 ) ⊆ ( 0 ... 𝑁 ) )
89 88 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → 𝑗 ∈ ( 0 ... 𝑁 ) )
90 86 89 10 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ∀ 𝑥 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐵 ∈ ℂ )
91 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵
92 91 nfel1 ⊢ Ⅎ 𝑥 ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 ∈ ℂ
93 csbeq1a ⊢ ( 𝑥 = ( 𝑘 − 𝑗 ) → 𝐵 = ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 )
94 93 eleq1d ⊢ ( 𝑥 = ( 𝑘 − 𝑗 ) → ( 𝐵 ∈ ℂ ↔ ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
95 92 94 rspc ⊢ ( ( 𝑘 − 𝑗 ) ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) → ( ∀ 𝑥 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐵 ∈ ℂ → ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 ∈ ℂ ) )
96 85 90 95 sylc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 ∈ ℂ )
97 65 96 fsumcl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → Σ 𝑗 ∈ ( 0 ... 𝑘 ) ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 ∈ ℂ )
98 oveq2 ⊢ ( 𝑘 = ( ( 0 + 𝑁 ) − 𝑛 ) → ( 0 ... 𝑘 ) = ( 0 ... ( ( 0 + 𝑁 ) − 𝑛 ) ) )
99 oveq1 ⊢ ( 𝑘 = ( ( 0 + 𝑁 ) − 𝑛 ) → ( 𝑘 − 𝑗 ) = ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) )
100 99 csbeq1d ⊢ ( 𝑘 = ( ( 0 + 𝑁 ) − 𝑛 ) → ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 = ⦋ ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) / 𝑥 ⦌ 𝐵 )
101 100 adantr ⊢ ( ( 𝑘 = ( ( 0 + 𝑁 ) − 𝑛 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 = ⦋ ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) / 𝑥 ⦌ 𝐵 )
102 98 101 sumeq12dv ⊢ ( 𝑘 = ( ( 0 + 𝑁 ) − 𝑛 ) → Σ 𝑗 ∈ ( 0 ... 𝑘 ) ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 = Σ 𝑗 ∈ ( 0 ... ( ( 0 + 𝑁 ) − 𝑛 ) ) ⦋ ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) / 𝑥 ⦌ 𝐵 )
103 97 102 fsumrev2 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... 𝑘 ) ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 = Σ 𝑛 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... ( ( 0 + 𝑁 ) − 𝑛 ) ) ⦋ ( ( ( 0 + 𝑁 ) − 𝑛 ) − 𝑗 ) / 𝑥 ⦌ 𝐵 )
104 64 103 eqtr4d ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = Σ 𝑘 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... 𝑘 ) ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 )
105 vex ⊢ 𝑘 ∈ V
106 105 1 csbie ⊢ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = 𝐴
107 106 a1i ⊢ ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = 𝐴 )
108 107 sumeq2dv ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐴 )
109 108 sumeq2i ⊢ Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐴
110 ovex ⊢ ( 𝑘 − 𝑗 ) ∈ V
111 110 2 csbie ⊢ ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 = 𝐶
112 111 a1i ⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... 𝑘 ) ) → ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 = 𝐶 )
113 112 sumeq2dv ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → Σ 𝑗 ∈ ( 0 ... 𝑘 ) ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 = Σ 𝑗 ∈ ( 0 ... 𝑘 ) 𝐶 )
114 113 sumeq2i ⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... 𝑘 ) ⦋ ( 𝑘 − 𝑗 ) / 𝑥 ⦌ 𝐵 = Σ 𝑘 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... 𝑘 ) 𝐶
115 104 109 114 3eqtr3g ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐴 = Σ 𝑘 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... 𝑘 ) 𝐶 )