Metamath Proof Explorer

Theorem fsum0diag

Description: Two ways to express "the sum of A ( j , k ) over the triangular region M <_ j , M <_ k , j + k <_ N ". (Contributed by NM, 31-Dec-2005) (Proof shortened by Mario Carneiro, 28-Apr-2014) (Revised by Mario Carneiro, 8-Apr-2016)

Ref Expression
Hypothesis fsum0diag.1 
|- ( ( ph /\ ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) ) -> A e. CC )
Assertion fsum0diag 
|- ( ph -> sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) A = sum_ k e. ( 0 ... N ) sum_ j e. ( 0 ... ( N - k ) ) A )

Proof

Step Hyp Ref Expression
1 fsum0diag.1 
 |-  ( ( ph /\ ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) ) -> A e. CC )
2 fzfid 
 |-  ( ph -> ( 0 ... N ) e. Fin )
3 fzfid 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( 0 ... ( N - j ) ) e. Fin )
4 fsum0diaglem 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) -> ( k e. ( 0 ... N ) /\ j e. ( 0 ... ( N - k ) ) ) )
5 fsum0diaglem 
 |-  ( ( k e. ( 0 ... N ) /\ j e. ( 0 ... ( N - k ) ) ) -> ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) )
6 4 5 impbii 
 |-  ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) <-> ( k e. ( 0 ... N ) /\ j e. ( 0 ... ( N - k ) ) ) )
7 6 a1i 
 |-  ( ph -> ( ( j e. ( 0 ... N ) /\ k e. ( 0 ... ( N - j ) ) ) <-> ( k e. ( 0 ... N ) /\ j e. ( 0 ... ( N - k ) ) ) ) )
8 2 2 3 7 1 fsumcom2 
 |-  ( ph -> sum_ j e. ( 0 ... N ) sum_ k e. ( 0 ... ( N - j ) ) A = sum_ k e. ( 0 ... N ) sum_ j e. ( 0 ... ( N - k ) ) A )