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	$$⊢\phi \to N\in \mathbb{N}$$
	fsumdvdsdiag.2	$$⊢\left(\phi \wedge \left(j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{j}\right)\right\}\right)\right)\to A\in ℂ$$
Assertion	fsumdvdsdiag	$$⊢\phi \to \sum _{j\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{j}\right)\right\}}A=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{j\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}A$$

Proof

Step	Hyp	Ref	Expression
1		fsumdvdsdiag.1	$$⊢\phi \to N\in \mathbb{N}$$
2		fsumdvdsdiag.2	$$⊢\left(\phi \wedge \left(j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{j}\right)\right\}\right)\right)\to A\in ℂ$$
3		fzfid	$$⊢\phi \to \left(1\dots N\right)\in \mathrm{Fin}$$
4		dvdsssfz1	$$⊢N\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel N\right\}\subseteq \left(1\dots N\right)$$
5	1 4	syl	$$⊢\phi \to \left\{x\in \mathbb{N}|x\parallel N\right\}\subseteq \left(1\dots N\right)$$
6	3 5	ssfid	$$⊢\phi \to \left\{x\in \mathbb{N}|x\parallel N\right\}\in \mathrm{Fin}$$
7		fzfid	$$⊢\left(\phi \wedge j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left(1\dots \frac{N}{j}\right)\in \mathrm{Fin}$$
8		ssrab2	$$⊢\left\{x\in \mathbb{N}|x\parallel N\right\}\subseteq \mathbb{N}$$
9		dvdsdivcl	$$⊢\left(N\in \mathbb{N}\wedge j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \frac{N}{j}\in \left\{x\in \mathbb{N}|x\parallel N\right\}$$
10	1 9	sylan	$$⊢\left(\phi \wedge j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \frac{N}{j}\in \left\{x\in \mathbb{N}|x\parallel N\right\}$$
11	8 10	sselid	$$⊢\left(\phi \wedge j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \frac{N}{j}\in \mathbb{N}$$
12		dvdsssfz1	$$⊢\frac{N}{j}\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{j}\right)\right\}\subseteq \left(1\dots \frac{N}{j}\right)$$
13	11 12	syl	$$⊢\left(\phi \wedge j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{j}\right)\right\}\subseteq \left(1\dots \frac{N}{j}\right)$$
14	7 13	ssfid	$$⊢\left(\phi \wedge j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{j}\right)\right\}\in \mathrm{Fin}$$
15	1	fsumdvdsdiaglem	$$⊢\phi \to \left(\left(j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{j}\right)\right\}\right)\to \left(k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge j\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\right)$$
16	1	fsumdvdsdiaglem	$$⊢\phi \to \left(\left(k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge j\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \left(j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{j}\right)\right\}\right)\right)$$
17	15 16	impbid	$$⊢\phi \to \left(\left(j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{j}\right)\right\}\right)\leftrightarrow \left(k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge j\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\right)$$
18	6 6 14 17 2	fsumcom2	$$⊢\phi \to \sum _{j\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{j}\right)\right\}}A=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{j\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}A$$