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	$⊢ φ \to A \in ℝ$
		fsumfldivdiag.2	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to B \in ℂ$
	Assertion	fsumfldivdiag	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} \sum_{m = 1}^{⌊\frac{A}{n}⌋} B = \sum_{m = 1}^{⌊A⌋} \sum_{n = 1}^{⌊\frac{A}{m}⌋} B$

Proof

Step	Hyp	Ref	Expression
1		fsumfldivdiag.1	$⊢ φ \to A \in ℝ$
2		fsumfldivdiag.2	$⊢ (φ \land (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋))) \to B \in ℂ$
3		fzfid	$⊢ φ \to (1 \dots ⌊A⌋) \in Fin$
4		fzfid	$⊢ (φ \land n \in (1 \dots ⌊A⌋)) \to (1 \dots ⌊\frac{A}{n}⌋) \in Fin$
5	1	fsumfldivdiaglem	$⊢ φ \to ((n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋)) \to (m \in (1 \dots ⌊A⌋) \land n \in (1 \dots ⌊\frac{A}{m}⌋)))$
6	1	fsumfldivdiaglem	$⊢ φ \to ((m \in (1 \dots ⌊A⌋) \land n \in (1 \dots ⌊\frac{A}{m}⌋)) \to (n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋)))$
7	5 6	impbid	$⊢ φ \to ((n \in (1 \dots ⌊A⌋) \land m \in (1 \dots ⌊\frac{A}{n}⌋)) \leftrightarrow (m \in (1 \dots ⌊A⌋) \land n \in (1 \dots ⌊\frac{A}{m}⌋)))$
8	3 3 4 7 2	fsumcom2	$⊢ φ \to \sum_{n = 1}^{⌊A⌋} \sum_{m = 1}^{⌊\frac{A}{n}⌋} B = \sum_{m = 1}^{⌊A⌋} \sum_{n = 1}^{⌊\frac{A}{m}⌋} B$