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

Metamath Proof Explorer

Theorem fsumfldivdiag

Description: The right-hand side of dvdsflsumcom is commutative in the variables, because it can be written as the manifestly symmetric sum over those <. m , n >. such that m x. n <_ A . (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses fsumfldivdiag.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fsumfldivdiag.2 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝐵 ∈ ℂ )
Assertion fsumfldivdiag ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) 𝐵 = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) 𝐵 )

Proof

Step Hyp Ref Expression
1 fsumfldivdiag.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 fsumfldivdiag.2 ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) → 𝐵 ∈ ℂ )
3 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
4 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ∈ Fin )
5 1 fsumfldivdiaglem ⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) ) )
6 1 fsumfldivdiaglem ⊢ ( 𝜑 → ( ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ) )
7 5 6 impbid ⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) ) ↔ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) ) ) )
8 3 3 4 7 2 fsumcom2 ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑛 ) ) ) 𝐵 = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) 𝐵 )