Metamath Proof Explorer

Theorem fsumdvdsdiag

Description: A "diagonal commutation" of divisor sums analogous to fsum0diag . (Contributed by Mario Carneiro, 2-Jul-2015) (Revised by Mario Carneiro, 8-Apr-2016)

Ref Expression
Hypotheses fsumdvdsdiag.1 ⊢ φ → N ∈ ℕ
fsumdvdsdiag.2 ⊢ φ ∧ j ∈ x ∈ ℕ | x ∥ N ∧ k ∈ x ∈ ℕ | x ∥ N j → A ∈ ℂ
Assertion fsumdvdsdiag ⊢ φ → ∑ j ∈ x ∈ ℕ | x ∥ N ∑ k ∈ x ∈ ℕ | x ∥ N j A = ∑ k ∈ x ∈ ℕ | x ∥ N ∑ j ∈ x ∈ ℕ | x ∥ N k A

Proof

Step Hyp Ref Expression
1 fsumdvdsdiag.1 ⊢ φ → N ∈ ℕ
2 fsumdvdsdiag.2 ⊢ φ ∧ j ∈ x ∈ ℕ | x ∥ N ∧ k ∈ x ∈ ℕ | x ∥ N j → A ∈ ℂ
3 fzfid ⊢ φ → 1 … N ∈ Fin
4 dvdsssfz1 ⊢ N ∈ ℕ → x ∈ ℕ | x ∥ N ⊆ 1 … N
5 1 4 syl ⊢ φ → x ∈ ℕ | x ∥ N ⊆ 1 … N
6 3 5 ssfid ⊢ φ → x ∈ ℕ | x ∥ N ∈ Fin
7 fzfid ⊢ φ ∧ j ∈ x ∈ ℕ | x ∥ N → 1 … N j ∈ Fin
8 ssrab2 ⊢ x ∈ ℕ | x ∥ N ⊆ ℕ
9 dvdsdivcl ⊢ N ∈ ℕ ∧ j ∈ x ∈ ℕ | x ∥ N → N j ∈ x ∈ ℕ | x ∥ N
10 1 9 sylan ⊢ φ ∧ j ∈ x ∈ ℕ | x ∥ N → N j ∈ x ∈ ℕ | x ∥ N
11 8 10 sseldi ⊢ φ ∧ j ∈ x ∈ ℕ | x ∥ N → N j ∈ ℕ
12 dvdsssfz1 ⊢ N j ∈ ℕ → x ∈ ℕ | x ∥ N j ⊆ 1 … N j
13 11 12 syl ⊢ φ ∧ j ∈ x ∈ ℕ | x ∥ N → x ∈ ℕ | x ∥ N j ⊆ 1 … N j
14 7 13 ssfid ⊢ φ ∧ j ∈ x ∈ ℕ | x ∥ N → x ∈ ℕ | x ∥ N j ∈ Fin
15 1 fsumdvdsdiaglem ⊢ φ → j ∈ x ∈ ℕ | x ∥ N ∧ k ∈ x ∈ ℕ | x ∥ N j → k ∈ x ∈ ℕ | x ∥ N ∧ j ∈ x ∈ ℕ | x ∥ N k
16 1 fsumdvdsdiaglem ⊢ φ → k ∈ x ∈ ℕ | x ∥ N ∧ j ∈ x ∈ ℕ | x ∥ N k → j ∈ x ∈ ℕ | x ∥ N ∧ k ∈ x ∈ ℕ | x ∥ N j
17 15 16 impbid ⊢ φ → j ∈ x ∈ ℕ | x ∥ N ∧ k ∈ x ∈ ℕ | x ∥ N j ↔ k ∈ x ∈ ℕ | x ∥ N ∧ j ∈ x ∈ ℕ | x ∥ N k
18 6 6 14 17 2 fsumcom2 ⊢ φ → ∑ j ∈ x ∈ ℕ | x ∥ N ∑ k ∈ x ∈ ℕ | x ∥ N j A = ∑ k ∈ x ∈ ℕ | x ∥ N ∑ j ∈ x ∈ ℕ | x ∥ N k A