This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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