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	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ) → 𝐴 ∈ ℂ )
Assertion	fsum0diag	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐴 = Σ 𝑘 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fsum0diag.1	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ) → 𝐴 ∈ ℂ )
2		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
3		fzfid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 0 ... ( 𝑁 − 𝑗 ) ) ∈ Fin )
4		fsum0diaglem	⊢ ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) ) )
5		fsum0diaglem	⊢ ( ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) )
6	4 5	impbii	⊢ ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) ) )
7	6	a1i	⊢ ( 𝜑 → ( ( 𝑗 ∈ ( 0 ... 𝑁 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) ) ↔ ( 𝑘 ∈ ( 0 ... 𝑁 ) ∧ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) ) ) )
8	2 2 3 7 1	fsumcom2	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 𝑗 ) ) 𝐴 = Σ 𝑘 ∈ ( 0 ... 𝑁 ) Σ 𝑗 ∈ ( 0 ... ( 𝑁 − 𝑘 ) ) 𝐴 )