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 ( ( 𝜑 ∧ ( 𝑗 ∈ ( 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 ... ( 𝑁𝑘 ) ) 𝐴 )