Metamath Proof Explorer

Theorem fprod0diag

Description: Two ways to express "the product of A ( j , k ) over the triangular region M <_ j , M <_ k , j + k <_ N . Compare fsum0diag . (Contributed by Scott Fenton, 2-Feb-2018)

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

Proof

Step Hyp Ref Expression
1 fprod0diag.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 fprodcom2 
 |-  ( ph -> prod_ j e. ( 0 ... N ) prod_ k e. ( 0 ... ( N - j ) ) A = prod_ k e. ( 0 ... N ) prod_ j e. ( 0 ... ( N - k ) ) A )