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

Proof

Step	Hyp	Ref	Expression
1		fsum0diag.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	fsumcom2	$⊢ φ \to \sum_{j = 0}^{N} \sum_{k = 0}^{N - j} A = \sum_{k = 0}^{N} \sum_{j = 0}^{N - k} A$