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	$⊢ (φ \land (j \in (0 \dots N) \land k \in (0 \dots N - j))) \to A \in ℂ$
	Assertion	fprod0diag	$⊢ φ \to \prod_{j = 0}^{N} \prod_{k = 0}^{N - j} A = \prod_{k = 0}^{N} \prod_{j = 0}^{N - k} A$

Proof

Step	Hyp	Ref	Expression
1		fprod0diag.1	$⊢ (φ \land (j \in (0 \dots N) \land k \in (0 \dots N - j))) \to A \in ℂ$
2		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
3		fzfid	$⊢ (φ \land j \in (0 \dots N)) \to (0 \dots N - j) \in Fin$
4		fsum0diaglem	$⊢ (j \in (0 \dots N) \land k \in (0 \dots N - j)) \to (k \in (0 \dots N) \land j \in (0 \dots N - k))$
5		fsum0diaglem	$⊢ (k \in (0 \dots N) \land j \in (0 \dots N - k)) \to (j \in (0 \dots N) \land k \in (0 \dots N - j))$
6	4 5	impbii	$⊢ (j \in (0 \dots N) \land k \in (0 \dots N - j)) \leftrightarrow (k \in (0 \dots N) \land j \in (0 \dots N - k))$
7	6	a1i	$⊢ φ \to ((j \in (0 \dots N) \land k \in (0 \dots N - j)) \leftrightarrow (k \in (0 \dots N) \land j \in (0 \dots N - k)))$
8	2 2 3 7 1	fprodcom2	$⊢ φ \to \prod_{j = 0}^{N} \prod_{k = 0}^{N - j} A = \prod_{k = 0}^{N} \prod_{j = 0}^{N - k} A$