Theorem fsumdvdscom

Description: A double commutation of divisor sums based on fsumdvdsdiag . Note that A depends on both j and k . (Contributed by Mario Carneiro, 13-May-2016)

	Ref	Expression
Hypotheses	fsumdvdscom.1	$$⊢\phi \to N\in \mathbb{N}$$
	fsumdvdscom.2	$$⊢j=km\to A=B$$
	fsumdvdscom.3	$$⊢\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 j\right\}\right)\right)\to A\in ℂ$$
Assertion	fsumdvdscom	$$⊢\phi \to \sum _{j\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel j\right\}}A=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}B$$

Proof

Step	Hyp	Ref	Expression
1		fsumdvdscom.1	$$⊢\phi \to N\in \mathbb{N}$$
2		fsumdvdscom.2	$$⊢j=km\to A=B$$
3		fsumdvdscom.3	$$⊢\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 j\right\}\right)\right)\to A\in ℂ$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}u\sum _{k\in \left\{x\in \mathbb{N}|x\parallel j\right\}}A$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}j\left\{x\in \mathbb{N}|x\parallel u\right\}$$
6		nfcsb1v	$$⊢\underset{\_}{Ⅎ}j⦋u/j⦌A$$
7	5 6	nfsum	$$⊢\underset{\_}{Ⅎ}j\sum _{k\in \left\{x\in \mathbb{N}|x\parallel u\right\}}⦋u/j⦌A$$
8		breq2	$$⊢j=u\to \left(x\parallel j\leftrightarrow x\parallel u\right)$$
9	8	rabbidv	$$⊢j=u\to \left\{x\in \mathbb{N}|x\parallel j\right\}=\left\{x\in \mathbb{N}|x\parallel u\right\}$$
10		csbeq1a	$$⊢j=u\to A=⦋u/j⦌A$$
11	10	adantr	$$⊢\left(j=u\wedge k\in \left\{x\in \mathbb{N}|x\parallel j\right\}\right)\to A=⦋u/j⦌A$$
12	9 11	sumeq12dv	$$⊢j=u\to \sum _{k\in \left\{x\in \mathbb{N}|x\parallel j\right\}}A=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel u\right\}}⦋u/j⦌A$$
13	4 7 12	cbvsumi	$$⊢\sum _{j\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel j\right\}}A=\sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel u\right\}}⦋u/j⦌A$$
14		breq2	$$⊢u=\frac{N}{v}\to \left(x\parallel u\leftrightarrow x\parallel \left(\frac{N}{v}\right)\right)$$
15	14	rabbidv	$$⊢u=\frac{N}{v}\to \left\{x\in \mathbb{N}|x\parallel u\right\}=\left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{v}\right)\right\}$$
16		csbeq1	$$⊢u=\frac{N}{v}\to ⦋u/j⦌A=⦋\left(\frac{N}{v}\right)/j⦌A$$
17	16	adantr	$$⊢\left(u=\frac{N}{v}\wedge k\in \left\{x\in \mathbb{N}|x\parallel u\right\}\right)\to ⦋u/j⦌A=⦋\left(\frac{N}{v}\right)/j⦌A$$
18	15 17	sumeq12dv	$$⊢u=\frac{N}{v}\to \sum _{k\in \left\{x\in \mathbb{N}|x\parallel u\right\}}⦋u/j⦌A=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{v}\right)\right\}}⦋\left(\frac{N}{v}\right)/j⦌A$$
19		fzfid	$$⊢\phi \to \left(1\dots N\right)\in \mathrm{Fin}$$
20		dvdsssfz1	$$⊢N\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel N\right\}\subseteq \left(1\dots N\right)$$
21	1 20	syl	$$⊢\phi \to \left\{x\in \mathbb{N}|x\parallel N\right\}\subseteq \left(1\dots N\right)$$
22	19 21	ssfid	$$⊢\phi \to \left\{x\in \mathbb{N}|x\parallel N\right\}\in \mathrm{Fin}$$
23		eqid	$$⊢\left\{x\in \mathbb{N}|x\parallel N\right\}=\left\{x\in \mathbb{N}|x\parallel N\right\}$$
24		eqid	$$⊢\left(z\in \left\{x\in \mathbb{N}|x\parallel N\right\}⟼\frac{N}{z}\right)=\left(z\in \left\{x\in \mathbb{N}|x\parallel N\right\}⟼\frac{N}{z}\right)$$
25	23 24	dvdsflip	$$⊢N\in \mathbb{N}\to \left(z\in \left\{x\in \mathbb{N}|x\parallel N\right\}⟼\frac{N}{z}\right):\left\{x\in \mathbb{N}|x\parallel N\right\}\underset{1-1\; onto}{⟶}\left\{x\in \mathbb{N}|x\parallel N\right\}$$
26	1 25	syl	$$⊢\phi \to \left(z\in \left\{x\in \mathbb{N}|x\parallel N\right\}⟼\frac{N}{z}\right):\left\{x\in \mathbb{N}|x\parallel N\right\}\underset{1-1\; onto}{⟶}\left\{x\in \mathbb{N}|x\parallel N\right\}$$
27		oveq2	$$⊢z=v\to \frac{N}{z}=\frac{N}{v}$$
28		ovex	$$⊢\frac{N}{z}\in \mathrm{V}$$
29	27 24 28	fvmpt3i	$$⊢v\in \left\{x\in \mathbb{N}|x\parallel N\right\}\to \left(z\in \left\{x\in \mathbb{N}|x\parallel N\right\}⟼\frac{N}{z}\right)\left(v\right)=\frac{N}{v}$$
30	29	adantl	$$⊢\left(\phi \wedge v\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left(z\in \left\{x\in \mathbb{N}|x\parallel N\right\}⟼\frac{N}{z}\right)\left(v\right)=\frac{N}{v}$$
31		fzfid	$$⊢\left(\phi \wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left(1\dots u\right)\in \mathrm{Fin}$$
32		ssrab2	$$⊢\left\{x\in \mathbb{N}|x\parallel N\right\}\subseteq \mathbb{N}$$
33		simpr	$$⊢\left(\phi \wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to u\in \left\{x\in \mathbb{N}|x\parallel N\right\}$$
34	32 33	sseldi	$$⊢\left(\phi \wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to u\in \mathbb{N}$$
35		dvdsssfz1	$$⊢u\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel u\right\}\subseteq \left(1\dots u\right)$$
36	34 35	syl	$$⊢\left(\phi \wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left\{x\in \mathbb{N}|x\parallel u\right\}\subseteq \left(1\dots u\right)$$
37	31 36	ssfid	$$⊢\left(\phi \wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left\{x\in \mathbb{N}|x\parallel u\right\}\in \mathrm{Fin}$$
38	3	ralrimivva	$$⊢\phi \to \forall j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\forall k\in \left\{x\in \mathbb{N}|x\parallel j\right\}A\in ℂ$$
39		nfv	$$⊢Ⅎu\forall k\in \left\{x\in \mathbb{N}|x\parallel j\right\}A\in ℂ$$
40	6	nfel1	$$⊢Ⅎj⦋u/j⦌A\in ℂ$$
41	5 40	nfralw	$$⊢Ⅎj\forall k\in \left\{x\in \mathbb{N}|x\parallel u\right\}⦋u/j⦌A\in ℂ$$
42	10	eleq1d	$$⊢j=u\to \left(A\in ℂ\leftrightarrow ⦋u/j⦌A\in ℂ\right)$$
43	9 42	raleqbidv	$$⊢j=u\to \left(\forall k\in \left\{x\in \mathbb{N}|x\parallel j\right\}A\in ℂ\leftrightarrow \forall k\in \left\{x\in \mathbb{N}|x\parallel u\right\}⦋u/j⦌A\in ℂ\right)$$
44	39 41 43	cbvralw	$$⊢\forall j\in \left\{x\in \mathbb{N}|x\parallel N\right\}\forall k\in \left\{x\in \mathbb{N}|x\parallel j\right\}A\in ℂ\leftrightarrow \forall u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\forall k\in \left\{x\in \mathbb{N}|x\parallel u\right\}⦋u/j⦌A\in ℂ$$
45	38 44	sylib	$$⊢\phi \to \forall u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\forall k\in \left\{x\in \mathbb{N}|x\parallel u\right\}⦋u/j⦌A\in ℂ$$
46	45	r19.21bi	$$⊢\left(\phi \wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \forall k\in \left\{x\in \mathbb{N}|x\parallel u\right\}⦋u/j⦌A\in ℂ$$
47	46	r19.21bi	$$⊢\left(\left(\phi \wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel u\right\}\right)\to ⦋u/j⦌A\in ℂ$$
48	37 47	fsumcl	$$⊢\left(\phi \wedge u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \sum _{k\in \left\{x\in \mathbb{N}|x\parallel u\right\}}⦋u/j⦌A\in ℂ$$
49	18 22 26 30 48	fsumf1o	$$⊢\phi \to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel u\right\}}⦋u/j⦌A=\sum _{v\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{v}\right)\right\}}⦋\left(\frac{N}{v}\right)/j⦌A$$
50	16	eleq1d	$$⊢u=\frac{N}{v}\to \left(⦋u/j⦌A\in ℂ\leftrightarrow ⦋\left(\frac{N}{v}\right)/j⦌A\in ℂ\right)$$
51	15 50	raleqbidv	$$⊢u=\frac{N}{v}\to \left(\forall k\in \left\{x\in \mathbb{N}|x\parallel u\right\}⦋u/j⦌A\in ℂ\leftrightarrow \forall k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{v}\right)\right\}⦋\left(\frac{N}{v}\right)/j⦌A\in ℂ\right)$$
52	45	adantr	$$⊢\left(\phi \wedge v\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \forall u\in \left\{x\in \mathbb{N}|x\parallel N\right\}\forall k\in \left\{x\in \mathbb{N}|x\parallel u\right\}⦋u/j⦌A\in ℂ$$
53		dvdsdivcl	$$⊢\left(N\in \mathbb{N}\wedge v\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \frac{N}{v}\in \left\{x\in \mathbb{N}|x\parallel N\right\}$$
54	1 53	sylan	$$⊢\left(\phi \wedge v\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \frac{N}{v}\in \left\{x\in \mathbb{N}|x\parallel N\right\}$$
55	51 52 54	rspcdva	$$⊢\left(\phi \wedge v\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \forall k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{v}\right)\right\}⦋\left(\frac{N}{v}\right)/j⦌A\in ℂ$$
56	55	r19.21bi	$$⊢\left(\left(\phi \wedge v\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{v}\right)\right\}\right)\to ⦋\left(\frac{N}{v}\right)/j⦌A\in ℂ$$
57	56	anasss	$$⊢\left(\phi \wedge \left(v\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{v}\right)\right\}\right)\right)\to ⦋\left(\frac{N}{v}\right)/j⦌A\in ℂ$$
58	1 57	fsumdvdsdiag	$$⊢\phi \to \sum _{v\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{v}\right)\right\}}⦋\left(\frac{N}{v}\right)/j⦌A=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{v\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}⦋\left(\frac{N}{v}\right)/j⦌A$$
59		oveq2	$$⊢v=\frac{\frac{N}{k}}{m}\to \frac{N}{v}=\frac{N}{\frac{\frac{N}{k}}{m}}$$
60	59	csbeq1d	$$⊢v=\frac{\frac{N}{k}}{m}\to ⦋\left(\frac{N}{v}\right)/j⦌A=⦋\left(\frac{N}{\frac{\frac{N}{k}}{m}}\right)/j⦌A$$
61		fzfid	$$⊢\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left(1\dots \frac{N}{k}\right)\in \mathrm{Fin}$$
62		dvdsdivcl	$$⊢\left(N\in \mathbb{N}\wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \frac{N}{k}\in \left\{x\in \mathbb{N}|x\parallel N\right\}$$
63	32 62	sseldi	$$⊢\left(N\in \mathbb{N}\wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \frac{N}{k}\in \mathbb{N}$$
64	1 63	sylan	$$⊢\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \frac{N}{k}\in \mathbb{N}$$
65		dvdsssfz1	$$⊢\frac{N}{k}\in \mathbb{N}\to \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\subseteq \left(1\dots \frac{N}{k}\right)$$
66	64 65	syl	$$⊢\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\subseteq \left(1\dots \frac{N}{k}\right)$$
67	61 66	ssfid	$$⊢\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\in \mathrm{Fin}$$
68		eqid	$$⊢\left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}=\left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}$$
69		eqid	$$⊢\left(z\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}⟼\frac{\frac{N}{k}}{z}\right)=\left(z\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}⟼\frac{\frac{N}{k}}{z}\right)$$
70	68 69	dvdsflip	$$⊢\frac{N}{k}\in \mathbb{N}\to \left(z\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}⟼\frac{\frac{N}{k}}{z}\right):\left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\underset{1-1\; onto}{⟶}\left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}$$
71	64 70	syl	$$⊢\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \left(z\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}⟼\frac{\frac{N}{k}}{z}\right):\left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\underset{1-1\; onto}{⟶}\left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}$$
72		oveq2	$$⊢z=m\to \frac{\frac{N}{k}}{z}=\frac{\frac{N}{k}}{m}$$
73		ovex	$$⊢\frac{\frac{N}{k}}{z}\in \mathrm{V}$$
74	72 69 73	fvmpt3i	$$⊢m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\to \left(z\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}⟼\frac{\frac{N}{k}}{z}\right)\left(m\right)=\frac{\frac{N}{k}}{m}$$
75	74	adantl	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \left(z\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}⟼\frac{\frac{N}{k}}{z}\right)\left(m\right)=\frac{\frac{N}{k}}{m}$$
76	1	fsumdvdsdiaglem	$$⊢\phi \to \left(\left(k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge v\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \left(v\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{v}\right)\right\}\right)\right)$$
77	57	ex	$$⊢\phi \to \left(\left(v\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge k\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{v}\right)\right\}\right)\to ⦋\left(\frac{N}{v}\right)/j⦌A\in ℂ\right)$$
78	76 77	syld	$$⊢\phi \to \left(\left(k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\wedge v\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to ⦋\left(\frac{N}{v}\right)/j⦌A\in ℂ\right)$$
79	78	impl	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge v\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to ⦋\left(\frac{N}{v}\right)/j⦌A\in ℂ$$
80	60 67 71 75 79	fsumf1o	$$⊢\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \sum _{v\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}⦋\left(\frac{N}{v}\right)/j⦌A=\sum _{m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}⦋\left(\frac{N}{\frac{\frac{N}{k}}{m}}\right)/j⦌A$$
81		ovexd	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \frac{N}{\frac{\frac{N}{k}}{m}}\in \mathrm{V}$$
82		nncn	$$⊢N\in \mathbb{N}\to N\in ℂ$$
83		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
84	82 83	jca	$$⊢N\in \mathbb{N}\to \left(N\in ℂ\wedge N\ne 0\right)$$
85	1 84	syl	$$⊢\phi \to \left(N\in ℂ\wedge N\ne 0\right)$$
86	85	ad2antrr	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \left(N\in ℂ\wedge N\ne 0\right)$$
87	86	simpld	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to N\in ℂ$$
88		elrabi	$$⊢k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\to k\in \mathbb{N}$$
89	88	adantl	$$⊢\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to k\in \mathbb{N}$$
90	89	adantr	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to k\in \mathbb{N}$$
91		nncn	$$⊢k\in \mathbb{N}\to k\in ℂ$$
92		nnne0	$$⊢k\in \mathbb{N}\to k\ne 0$$
93	91 92	jca	$$⊢k\in \mathbb{N}\to \left(k\in ℂ\wedge k\ne 0\right)$$
94	90 93	syl	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \left(k\in ℂ\wedge k\ne 0\right)$$
95		elrabi	$$⊢m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\to m\in \mathbb{N}$$
96	95	adantl	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to m\in \mathbb{N}$$
97		nncn	$$⊢m\in \mathbb{N}\to m\in ℂ$$
98		nnne0	$$⊢m\in \mathbb{N}\to m\ne 0$$
99	97 98	jca	$$⊢m\in \mathbb{N}\to \left(m\in ℂ\wedge m\ne 0\right)$$
100	96 99	syl	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \left(m\in ℂ\wedge m\ne 0\right)$$
101		divdiv1	$$⊢\left(N\in ℂ\wedge \left(k\in ℂ\wedge k\ne 0\right)\wedge \left(m\in ℂ\wedge m\ne 0\right)\right)\to \frac{\frac{N}{k}}{m}=\frac{N}{km}$$
102	87 94 100 101	syl3anc	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \frac{\frac{N}{k}}{m}=\frac{N}{km}$$
103	102	oveq2d	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \frac{N}{\frac{\frac{N}{k}}{m}}=\frac{N}{\frac{N}{km}}$$
104		nnmulcl	$$⊢\left(k\in \mathbb{N}\wedge m\in \mathbb{N}\right)\to km\in \mathbb{N}$$
105	89 95 104	syl2an	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to km\in \mathbb{N}$$
106		nncn	$$⊢km\in \mathbb{N}\to km\in ℂ$$
107		nnne0	$$⊢km\in \mathbb{N}\to km\ne 0$$
108	106 107	jca	$$⊢km\in \mathbb{N}\to \left(km\in ℂ\wedge km\ne 0\right)$$
109	105 108	syl	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \left(km\in ℂ\wedge km\ne 0\right)$$
110		ddcan	$$⊢\left(\left(N\in ℂ\wedge N\ne 0\right)\wedge \left(km\in ℂ\wedge km\ne 0\right)\right)\to \frac{N}{\frac{N}{km}}=km$$
111	86 109 110	syl2anc	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \frac{N}{\frac{N}{km}}=km$$
112	103 111	eqtrd	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \frac{N}{\frac{\frac{N}{k}}{m}}=km$$
113	112	eqeq2d	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to \left(j=\frac{N}{\frac{\frac{N}{k}}{m}}\leftrightarrow j=km\right)$$
114	113	biimpa	$$⊢\left(\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\wedge j=\frac{N}{\frac{\frac{N}{k}}{m}}\right)\to j=km$$
115	114 2	syl	$$⊢\left(\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\wedge j=\frac{N}{\frac{\frac{N}{k}}{m}}\right)\to A=B$$
116	81 115	csbied	$$⊢\left(\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\wedge m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}\right)\to ⦋\left(\frac{N}{\frac{\frac{N}{k}}{m}}\right)/j⦌A=B$$
117	116	sumeq2dv	$$⊢\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \sum _{m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}⦋\left(\frac{N}{\frac{\frac{N}{k}}{m}}\right)/j⦌A=\sum _{m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}B$$
118	80 117	eqtrd	$$⊢\left(\phi \wedge k\in \left\{x\in \mathbb{N}|x\parallel N\right\}\right)\to \sum _{v\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}⦋\left(\frac{N}{v}\right)/j⦌A=\sum _{m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}B$$
119	118	sumeq2dv	$$⊢\phi \to \sum _{k\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{v\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}⦋\left(\frac{N}{v}\right)/j⦌A=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}B$$
120	49 58 119	3eqtrd	$$⊢\phi \to \sum _{u\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel u\right\}}⦋u/j⦌A=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}B$$
121	13 120	syl5eq	$$⊢\phi \to \sum _{j\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{k\in \left\{x\in \mathbb{N}|x\parallel j\right\}}A=\sum _{k\in \left\{x\in \mathbb{N}|x\parallel N\right\}}\sum _{m\in \left\{x\in \mathbb{N}|x\parallel \left(\frac{N}{k}\right)\right\}}B$$