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 | |
|
Assertion | fprod0diag | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fprod0diag.1 | |
|
2 | fzfid | |
|
3 | fzfid | |
|
4 | fsum0diaglem | |
|
5 | fsum0diaglem | |
|
6 | 4 5 | impbii | |
7 | 6 | a1i | |
8 | 2 2 3 7 1 | fprodcom2 | |