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 
|- ( x = k -> B = A )
fsum0diag2.2 
|- ( x = ( k - j ) -> B = C )
fsum0diag2.3 
|- ( ( ph /\ ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) ) -> A e. CC )
Assertion fsum0diag2 
|- ( ph -> sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) A = sum_ k e. ( 0 ... N ) sum_ j e. ( 0 ... k ) C )

Proof

Step Hyp Ref Expression
1 fsum0diag2.1 
 |-  ( x = k -> B = A )
2 fsum0diag2.2 
 |-  ( x = ( k - j ) -> B = C )
3 fsum0diag2.3 
 |-  ( ( ph /\ ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) ) -> A e. CC )
4 fznn0sub2 
 |-  ( n e. ( 0 ... ( N - j ) ) -> ( ( N - j ) - n ) e. ( 0 ... ( N - j ) ) )
5 4 ad2antll 
 |-  ( ( ph /\ ( j e. ( 0 ... N ) /\ n e. ( 0 ... ( N - j ) ) ) ) -> ( ( N - j ) - n ) e. ( 0 ... ( N - j ) ) )
6 3 expr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( k e. ( 0 ... ( N - j ) ) -> A e. CC ) )
7 6 ralrimiv 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> A. k e. ( 0 ... ( N - j ) ) A e. CC )
8 1 eleq1d 
 |-  ( x = k -> ( B e. CC <-> A e. CC ) )
9 8 cbvralvw 
 |-  ( A. x e. ( 0 ... ( N - j ) ) B e. CC <-> A. k e. ( 0 ... ( N - j ) ) A e. CC )
10 7 9 sylibr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> A. x e. ( 0 ... ( N - j ) ) B e. CC )
11 10 adantrr 
 |-  ( ( ph /\ ( j e. ( 0 ... N ) /\ n e. ( 0 ... ( N - j ) ) ) ) -> A. x e. ( 0 ... ( N - j ) ) B e. CC )
12 nfcsb1v 
 |-  F/_ x [_ ( ( N - j ) - n ) / x ]_ B
13 12 nfel1 
 |-  F/ x [_ ( ( N - j ) - n ) / x ]_ B e. CC
14 csbeq1a 
 |-  ( x = ( ( N - j ) - n ) -> B = [_ ( ( N - j ) - n ) / x ]_ B )
15 14 eleq1d 
 |-  ( x = ( ( N - j ) - n ) -> ( B e. CC <-> [_ ( ( N - j ) - n ) / x ]_ B e. CC ) )
16 13 15 rspc 
 |-  ( ( ( N - j ) - n ) e. ( 0 ... ( N - j ) ) -> ( A. x e. ( 0 ... ( N - j ) ) B e. CC -> [_ ( ( N - j ) - n ) / x ]_ B e. CC ) )
17 5 11 16 sylc 
 |-  ( ( ph /\ ( j e. ( 0 ... N ) /\ n e. ( 0 ... ( N - j ) ) ) ) -> [_ ( ( N - j ) - n ) / x ]_ B e. CC )
18 17 fsum0diag 
 |-  ( ph -> sum_ j e. ( 0 ... N ) sum_ n e. ( 0 ... ( N - j ) ) [_ ( ( N - j ) - n ) / x ]_ B = sum_ n e. ( 0 ... N ) sum_ j e. ( 0 ... ( N - n ) ) [_ ( ( N - j ) - n ) / x ]_ B )
19 nfcsb1v 
 |-  F/_ x [_ k / x ]_ B
20 19 nfel1 
 |-  F/ x [_ k / x ]_ B e. CC
21 csbeq1a 
 |-  ( x = k -> B = [_ k / x ]_ B )
22 21 eleq1d 
 |-  ( x = k -> ( B e. CC <-> [_ k / x ]_ B e. CC ) )
23 20 22 rspc 
 |-  ( k e. ( 0 ... ( N - j ) ) -> ( A. x e. ( 0 ... ( N - j ) ) B e. CC -> [_ k / x ]_ B e. CC ) )
24 10 23 mpan9 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ k e. ( 0 ... ( N - j ) ) ) -> [_ k / x ]_ B e. CC )
25 csbeq1 
 |-  ( k = ( ( 0 + ( N - j ) ) - n ) -> [_ k / x ]_ B = [_ ( ( 0 + ( N - j ) ) - n ) / x ]_ B )
26 24 25 fsumrev2 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> sum_ k e. ( 0 ... ( N - j ) ) [_ k / x ]_ B = sum_ n e. ( 0 ... ( N - j ) ) [_ ( ( 0 + ( N - j ) ) - n ) / x ]_ B )
27 elfz3nn0 
 |-  ( j e. ( 0 ... N ) -> N e. NN0 )
28 27 ad2antlr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ n e. ( 0 ... ( N - j ) ) ) -> N e. NN0 )
29 elfzelz 
 |-  ( j e. ( 0 ... N ) -> j e. ZZ )
30 29 ad2antlr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ n e. ( 0 ... ( N - j ) ) ) -> j e. ZZ )
31 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
32 zcn 
 |-  ( j e. ZZ -> j e. CC )
33 subcl 
 |-  ( ( N e. CC /\ j e. CC ) -> ( N - j ) e. CC )
34 31 32 33 syl2an 
 |-  ( ( N e. NN0 /\ j e. ZZ ) -> ( N - j ) e. CC )
35 28 30 34 syl2anc 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ n e. ( 0 ... ( N - j ) ) ) -> ( N - j ) e. CC )
36 addlid 
 |-  ( ( N - j ) e. CC -> ( 0 + ( N - j ) ) = ( N - j ) )
37 35 36 syl 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ n e. ( 0 ... ( N - j ) ) ) -> ( 0 + ( N - j ) ) = ( N - j ) )
38 37 oveq1d 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ n e. ( 0 ... ( N - j ) ) ) -> ( ( 0 + ( N - j ) ) - n ) = ( ( N - j ) - n ) )
39 38 csbeq1d 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ n e. ( 0 ... ( N - j ) ) ) -> [_ ( ( 0 + ( N - j ) ) - n ) / x ]_ B = [_ ( ( N - j ) - n ) / x ]_ B )
40 39 sumeq2dv 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> sum_ n e. ( 0 ... ( N - j ) ) [_ ( ( 0 + ( N - j ) ) - n ) / x ]_ B = sum_ n e. ( 0 ... ( N - j ) ) [_ ( ( N - j ) - n ) / x ]_ B )
41 26 40 eqtrd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> sum_ k e. ( 0 ... ( N - j ) ) [_ k / x ]_ B = sum_ n e. ( 0 ... ( N - j ) ) [_ ( ( N - j ) - n ) / x ]_ B )
42 41 sumeq2dv 
 |-  ( ph -> sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) [_ k / x ]_ B = sum_ j e. ( 0 ... N ) sum_ n e. ( 0 ... ( N - j ) ) [_ ( ( N - j ) - n ) / x ]_ B )
43 elfz3nn0 
 |-  ( n e. ( 0 ... N ) -> N e. NN0 )
44 43 adantl 
 |-  ( ( ph /\ n e. ( 0 ... N ) ) -> N e. NN0 )
45 addlid 
 |-  ( N e. CC -> ( 0 + N ) = N )
46 44 31 45 3syl 
 |-  ( ( ph /\ n e. ( 0 ... N ) ) -> ( 0 + N ) = N )
47 46 oveq1d 
 |-  ( ( ph /\ n e. ( 0 ... N ) ) -> ( ( 0 + N ) - n ) = ( N - n ) )
48 47 oveq2d 
 |-  ( ( ph /\ n e. ( 0 ... N ) ) -> ( 0 ... ( ( 0 + N ) - n ) ) = ( 0 ... ( N - n ) ) )
49 47 oveq1d 
 |-  ( ( ph /\ n e. ( 0 ... N ) ) -> ( ( ( 0 + N ) - n ) - j ) = ( ( N - n ) - j ) )
50 49 adantr 
 |-  ( ( ( ph /\ n e. ( 0 ... N ) ) /\ j e. ( 0 ... ( N - n ) ) ) -> ( ( ( 0 + N ) - n ) - j ) = ( ( N - n ) - j ) )
51 43 ad2antlr 
 |-  ( ( ( ph /\ n e. ( 0 ... N ) ) /\ j e. ( 0 ... ( N - n ) ) ) -> N e. NN0 )
52 elfzelz 
 |-  ( n e. ( 0 ... N ) -> n e. ZZ )
53 52 ad2antlr 
 |-  ( ( ( ph /\ n e. ( 0 ... N ) ) /\ j e. ( 0 ... ( N - n ) ) ) -> n e. ZZ )
54 elfzelz 
 |-  ( j e. ( 0 ... ( N - n ) ) -> j e. ZZ )
55 54 adantl 
 |-  ( ( ( ph /\ n e. ( 0 ... N ) ) /\ j e. ( 0 ... ( N - n ) ) ) -> j e. ZZ )
56 zcn 
 |-  ( n e. ZZ -> n e. CC )
57 sub32 
 |-  ( ( N e. CC /\ n e. CC /\ j e. CC ) -> ( ( N - n ) - j ) = ( ( N - j ) - n ) )
58 31 56 32 57 syl3an 
 |-  ( ( N e. NN0 /\ n e. ZZ /\ j e. ZZ ) -> ( ( N - n ) - j ) = ( ( N - j ) - n ) )
59 51 53 55 58 syl3anc 
 |-  ( ( ( ph /\ n e. ( 0 ... N ) ) /\ j e. ( 0 ... ( N - n ) ) ) -> ( ( N - n ) - j ) = ( ( N - j ) - n ) )
60 50 59 eqtrd 
 |-  ( ( ( ph /\ n e. ( 0 ... N ) ) /\ j e. ( 0 ... ( N - n ) ) ) -> ( ( ( 0 + N ) - n ) - j ) = ( ( N - j ) - n ) )
61 60 csbeq1d 
 |-  ( ( ( ph /\ n e. ( 0 ... N ) ) /\ j e. ( 0 ... ( N - n ) ) ) -> [_ ( ( ( 0 + N ) - n ) - j ) / x ]_ B = [_ ( ( N - j ) - n ) / x ]_ B )
62 48 61 sumeq12rdv 
 |-  ( ( ph /\ n e. ( 0 ... N ) ) -> sum_ j e. ( 0 ... ( ( 0 + N ) - n ) ) [_ ( ( ( 0 + N ) - n ) - j ) / x ]_ B = sum_ j e. ( 0 ... ( N - n ) ) [_ ( ( N - j ) - n ) / x ]_ B )
63 62 sumeq2dv 
 |-  ( ph -> sum_ n e. ( 0 ... N ) sum_ j e. ( 0 ... ( ( 0 + N ) - n ) ) [_ ( ( ( 0 + N ) - n ) - j ) / x ]_ B = sum_ n e. ( 0 ... N ) sum_ j e. ( 0 ... ( N - n ) ) [_ ( ( N - j ) - n ) / x ]_ B )
64 18 42 63 3eqtr4d 
 |-  ( ph -> sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) [_ k / x ]_ B = sum_ n e. ( 0 ... N ) sum_ j e. ( 0 ... ( ( 0 + N ) - n ) ) [_ ( ( ( 0 + N ) - n ) - j ) / x ]_ B )
65 fzfid 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( 0 ... k ) e. Fin )
66 elfzuz3 
 |-  ( j e. ( 0 ... k ) -> k e. ( ZZ>= ` j ) )
67 66 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> k e. ( ZZ>= ` j ) )
68 elfzuz3 
 |-  ( k e. ( 0 ... N ) -> N e. ( ZZ>= ` k ) )
69 68 adantl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> N e. ( ZZ>= ` k ) )
70 69 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> N e. ( ZZ>= ` k ) )
71 elfzuzb 
 |-  ( k e. ( j ... N ) <-> ( k e. ( ZZ>= ` j ) /\ N e. ( ZZ>= ` k ) ) )
72 67 70 71 sylanbrc 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> k e. ( j ... N ) )
73 elfzelz 
 |-  ( j e. ( 0 ... k ) -> j e. ZZ )
74 73 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> j e. ZZ )
75 elfzel2 
 |-  ( k e. ( 0 ... N ) -> N e. ZZ )
76 75 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> N e. ZZ )
77 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
78 77 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> k e. ZZ )
79 fzsubel 
 |-  ( ( ( j e. ZZ /\ N e. ZZ ) /\ ( k e. ZZ /\ j e. ZZ ) ) -> ( k e. ( j ... N ) <-> ( k - j ) e. ( ( j - j ) ... ( N - j ) ) ) )
80 74 76 78 74 79 syl22anc 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> ( k e. ( j ... N ) <-> ( k - j ) e. ( ( j - j ) ... ( N - j ) ) ) )
81 72 80 mpbid 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> ( k - j ) e. ( ( j - j ) ... ( N - j ) ) )
82 subid 
 |-  ( j e. CC -> ( j - j ) = 0 )
83 74 32 82 3syl 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> ( j - j ) = 0 )
84 83 oveq1d 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> ( ( j - j ) ... ( N - j ) ) = ( 0 ... ( N - j ) ) )
85 81 84 eleqtrd 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> ( k - j ) e. ( 0 ... ( N - j ) ) )
86 simpll 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> ph )
87 fzss2 
 |-  ( N e. ( ZZ>= ` k ) -> ( 0 ... k ) C_ ( 0 ... N ) )
88 69 87 syl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( 0 ... k ) C_ ( 0 ... N ) )
89 88 sselda 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> j e. ( 0 ... N ) )
90 86 89 10 syl2anc 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> A. x e. ( 0 ... ( N - j ) ) B e. CC )
91 nfcsb1v 
 |-  F/_ x [_ ( k - j ) / x ]_ B
92 91 nfel1 
 |-  F/ x [_ ( k - j ) / x ]_ B e. CC
93 csbeq1a 
 |-  ( x = ( k - j ) -> B = [_ ( k - j ) / x ]_ B )
94 93 eleq1d 
 |-  ( x = ( k - j ) -> ( B e. CC <-> [_ ( k - j ) / x ]_ B e. CC ) )
95 92 94 rspc 
 |-  ( ( k - j ) e. ( 0 ... ( N - j ) ) -> ( A. x e. ( 0 ... ( N - j ) ) B e. CC -> [_ ( k - j ) / x ]_ B e. CC ) )
96 85 90 95 sylc 
 |-  ( ( ( ph /\ k e. ( 0 ... N ) ) /\ j e. ( 0 ... k ) ) -> [_ ( k - j ) / x ]_ B e. CC )
97 65 96 fsumcl 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> sum_ j e. ( 0 ... k ) [_ ( k - j ) / x ]_ B e. CC )
98 oveq2 
 |-  ( k = ( ( 0 + N ) - n ) -> ( 0 ... k ) = ( 0 ... ( ( 0 + N ) - n ) ) )
99 oveq1 
 |-  ( k = ( ( 0 + N ) - n ) -> ( k - j ) = ( ( ( 0 + N ) - n ) - j ) )
100 99 csbeq1d 
 |-  ( k = ( ( 0 + N ) - n ) -> [_ ( k - j ) / x ]_ B = [_ ( ( ( 0 + N ) - n ) - j ) / x ]_ B )
101 100 adantr 
 |-  ( ( k = ( ( 0 + N ) - n ) /\ j e. ( 0 ... k ) ) -> [_ ( k - j ) / x ]_ B = [_ ( ( ( 0 + N ) - n ) - j ) / x ]_ B )
102 98 101 sumeq12dv 
 |-  ( k = ( ( 0 + N ) - n ) -> sum_ j e. ( 0 ... k ) [_ ( k - j ) / x ]_ B = sum_ j e. ( 0 ... ( ( 0 + N ) - n ) ) [_ ( ( ( 0 + N ) - n ) - j ) / x ]_ B )
103 97 102 fsumrev2 
 |-  ( ph -> sum_ k e. ( 0 ... N ) sum_ j e. ( 0 ... k ) [_ ( k - j ) / x ]_ B = sum_ n e. ( 0 ... N ) sum_ j e. ( 0 ... ( ( 0 + N ) - n ) ) [_ ( ( ( 0 + N ) - n ) - j ) / x ]_ B )
104 64 103 eqtr4d 
 |-  ( ph -> sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) [_ k / x ]_ B = sum_ k e. ( 0 ... N ) sum_ j e. ( 0 ... k ) [_ ( k - j ) / x ]_ B )
105 vex 
 |-  k e. _V
106 105 1 csbie 
 |-  [_ k / x ]_ B = A
107 106 a1i 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> [_ k / x ]_ B = A )
108 107 sumeq2dv 
 |-  ( j e. ( 0 ... N ) -> sum_ k e. ( 0 ... ( N - j ) ) [_ k / x ]_ B = sum_ k e. ( 0 ... ( N - j ) ) A )
109 108 sumeq2i 
 |-  sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) [_ k / x ]_ B = sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) A
110 ovex 
 |-  ( k - j ) e. _V
111 110 2 csbie 
 |-  [_ ( k - j ) / x ]_ B = C
112 111 a1i 
 |-  ( ( k e. ( 0 ... N ) /\ j e. ( 0 ... k ) ) -> [_ ( k - j ) / x ]_ B = C )
113 112 sumeq2dv 
 |-  ( k e. ( 0 ... N ) -> sum_ j e. ( 0 ... k ) [_ ( k - j ) / x ]_ B = sum_ j e. ( 0 ... k ) C )
114 113 sumeq2i 
 |-  sum_ k e. ( 0 ... N ) sum_ j e. ( 0 ... k ) [_ ( k - j ) / x ]_ B = sum_ k e. ( 0 ... N ) sum_ j e. ( 0 ... k ) C
115 104 109 114 3eqtr3g 
 |-  ( ph -> sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) A = sum_ k e. ( 0 ... N ) sum_ j e. ( 0 ... k ) C )