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