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 ... ( ⌊ ‘ ( 𝐴 / 𝑚 ) ) ) 𝐵 )