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 φj0Nk0NjA
Assertion fprod0diag φj=0Nk=0NjA=k=0Nj=0NkA

Proof

Step Hyp Ref Expression
1 fprod0diag.1 φj0Nk0NjA
2 fzfid φ0NFin
3 fzfid φj0N0NjFin
4 fsum0diaglem j0Nk0Njk0Nj0Nk
5 fsum0diaglem k0Nj0Nkj0Nk0Nj
6 4 5 impbii j0Nk0Njk0Nj0Nk
7 6 a1i φj0Nk0Njk0Nj0Nk
8 2 2 3 7 1 fprodcom2 φj=0Nk=0NjA=k=0Nj=0NkA