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	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	fsumdvdsdiag.2	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝐴 ∈ ℂ )
Assertion	fsumdvdsdiag	⊢ ( 𝜑 → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		fsumdvdsdiag.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		fsumdvdsdiag.2	⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) → 𝐴 ∈ ℂ )
3		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
4		dvdsssfz1	⊢ ( 𝑁 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
5	1 4	syl	⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ( 1 ... 𝑁 ) )
6	3 5	ssfid	⊢ ( 𝜑 → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∈ Fin )
7		fzfid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 1 ... ( 𝑁 / 𝑗 ) ) ∈ Fin )
8		ssrab2	⊢ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ⊆ ℕ
9		dvdsdivcl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑗 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
10	1 9	sylan	⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑗 ) ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } )
11	8 10	sseldi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → ( 𝑁 / 𝑗 ) ∈ ℕ )
12		dvdsssfz1	⊢ ( ( 𝑁 / 𝑗 ) ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ⊆ ( 1 ... ( 𝑁 / 𝑗 ) ) )
13	11 12	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ⊆ ( 1 ... ( 𝑁 / 𝑗 ) ) )
14	7 13	ssfid	⊢ ( ( 𝜑 ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ∈ Fin )
15	1	fsumdvdsdiaglem	⊢ ( 𝜑 → ( ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) → ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) ) )
16	1	fsumdvdsdiaglem	⊢ ( 𝜑 → ( ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) → ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ) )
17	15 16	impbid	⊢ ( 𝜑 → ( ( 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } ) ↔ ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } ∧ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } ) ) )
18	6 6 14 17 2	fsumcom2	⊢ ( 𝜑 → Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑗 ) } 𝐴 = Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁 } Σ 𝑗 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ ( 𝑁 / 𝑘 ) } 𝐴 )