Theorem fsumdvdscom 27327

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

Hypotheses

Ref	Expression
fsumdvdscom.1	⊢ (𝜑 → 𝑁 ∈ ℕ)
fsumdvdscom.2	⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵)
fsumdvdscom.3	⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ)

Assertion

Ref	Expression
fsumdvdscom	⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)

Distinct variable groups:   𝐴,𝑚   𝐵,𝑗   𝑗,𝑘,𝑚,𝑥,𝑁   𝜑,𝑗,𝑘,𝑚

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥,𝑗,𝑘)   𝐵(𝑥,𝑘,𝑚)

Proof of Theorem fsumdvdscom

Dummy variables 𝑢 𝑣 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq2 5114	. . . . 5 ⊢ (𝑗 = 𝑢 → (𝑥 ∥ 𝑗 ↔ 𝑥 ∥ 𝑢))
2	1	rabbidv 3423	. . . 4 ⊢ (𝑗 = 𝑢 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢})
3		csbeq1a 3868	. . . . 5 ⊢ (𝑗 = 𝑢 → 𝐴 = ⦋𝑢 / 𝑗⦌𝐴)
4	3	adantr 485	. . . 4 ⊢ ((𝑗 = 𝑢 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}) → 𝐴 = ⦋𝑢 / 𝑗⦌𝐴)
5	2, 4	sumeq12dv 15759	. . 3 ⊢ (𝑗 = 𝑢 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴)
6		nfcv 2925	. . 3 ⊢ Ⅎ𝑢Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴
7		nfcv 2925	. . . 4 ⊢ Ⅎ𝑗{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}
8		nfcsb1v 3878	. . . 4 ⊢ Ⅎ𝑗⦋𝑢 / 𝑗⦌𝐴
9	7, 8	nfsum 15744	. . 3 ⊢ Ⅎ𝑗Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴
10	5, 6, 9	cbvsum 15748	. 2 ⊢ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴
11		breq2 5114	. . . . . 6 ⊢ (𝑢 = (𝑁 / 𝑣) → (𝑥 ∥ 𝑢 ↔ 𝑥 ∥ (𝑁 / 𝑣)))
12	11	rabbidv 3423	. . . . 5 ⊢ (𝑢 = (𝑁 / 𝑣) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})
13		csbeq1 3857	. . . . . 6 ⊢ (𝑢 = (𝑁 / 𝑣) → ⦋𝑢 / 𝑗⦌𝐴 = ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
14	13	adantr 485	. . . . 5 ⊢ ((𝑢 = (𝑁 / 𝑣) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) → ⦋𝑢 / 𝑗⦌𝐴 = ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
15	12, 14	sumeq12dv 15759	. . . 4 ⊢ (𝑢 = (𝑁 / 𝑣) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
16		fzfid 14011	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
17		fsumdvdscom.1	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
18		dvdsssfz1 16377	. . . . . 6 ⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁))
19	17, 18	syl 18	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁))
20	16, 19	ssfid 9230	. . . 4 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin)
21		eqid 2763	. . . . . 6 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}
22		eqid 2763	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))
23	21, 22	dvdsflip 16376	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
24	17, 23	syl 18	. . . 4 ⊢ (𝜑 → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
25		oveq2 7420	. . . . . 6 ⊢ (𝑧 = 𝑣 → (𝑁 / 𝑧) = (𝑁 / 𝑣))
26		ovex 7445	. . . . . 6 ⊢ (𝑁 / 𝑧) ∈ V
27	25, 22, 26	fvmpt3i 6997	. . . . 5 ⊢ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣))
28	27	adantl 486	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣))
29		fzfid 14011	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (1...𝑢) ∈ Fin)
30		ssrab2 4035	. . . . . . . 8 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ ℕ
31		simpr 489	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
32	30, 31	sselid 3936	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑢 ∈ ℕ)
33		dvdsssfz1 16377	. . . . . . 7 ⊢ (𝑢 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢))
34	32, 33	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢))
35	29, 34	ssfid 9230	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ∈ Fin)
36		fsumdvdscom.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ)
37	36	ralrimivva 3208	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ)
38		nfv 1944	. . . . . . . . 9 ⊢ Ⅎ𝑢∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ
39	8	nfel1 2941	. . . . . . . . . 10 ⊢ Ⅎ𝑗⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ
40	7, 39	nfralw 3312	. . . . . . . . 9 ⊢ Ⅎ𝑗∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ
41	3	eleq1d 2848	. . . . . . . . . 10 ⊢ (𝑗 = 𝑢 → (𝐴 ∈ ℂ ↔ ⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ))
42	2, 41	raleqbidv 3338	. . . . . . . . 9 ⊢ (𝑗 = 𝑢 → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ))
43	38, 40, 42	cbvralw 3307	. . . . . . . 8 ⊢ (∀𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ ↔ ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
44	37, 43	sylib 221	. . . . . . 7 ⊢ (𝜑 → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
45	44	r19.21bi 3257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
46	45	r19.21bi 3257	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) → ⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
47	35, 46	fsumcl 15786	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
48	15, 20, 24, 28, 47	fsumf1o 15776	. . 3 ⊢ (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
49	13	eleq1d 2848	. . . . . . . 8 ⊢ (𝑢 = (𝑁 / 𝑣) → (⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ ↔ ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
50	12, 49	raleqbidv 3338	. . . . . . 7 ⊢ (𝑢 = (𝑁 / 𝑣) → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
51	44	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
52		dvdsdivcl 16375	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
53	17, 52	sylan 591	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
54	50, 51, 53	rspcdva 3583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
55	54	r19.21bi 3257	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
56	55	anasss 471	. . . 4 ⊢ ((𝜑 ∧ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
57	17, 56	fsumdvdsdiag 27326	. . 3 ⊢ (𝜑 → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
58		oveq2 7420	. . . . . . 7 ⊢ (𝑣 = ((𝑁 / 𝑘) / 𝑚) → (𝑁 / 𝑣) = (𝑁 / ((𝑁 / 𝑘) / 𝑚)))
59	58	csbeq1d 3858	. . . . . 6 ⊢ (𝑣 = ((𝑁 / 𝑘) / 𝑚) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = ⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴)
60		fzfid 14011	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (1...(𝑁 / 𝑘)) ∈ Fin)
61		dvdsdivcl 16375	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
62	30, 61	sselid 3936	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ ℕ)
63	17, 62	sylan 591	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ ℕ)
64		dvdsssfz1 16377	. . . . . . . 8 ⊢ ((𝑁 / 𝑘) ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘)))
65	63, 64	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘)))
66	60, 65	ssfid 9230	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ∈ Fin)
67		eqid 2763	. . . . . . . 8 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}
68		eqid 2763	. . . . . . . 8 ⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))
69	67, 68	dvdsflip 16376	. . . . . . 7 ⊢ ((𝑁 / 𝑘) ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})
70	63, 69	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})
71		oveq2 7420	. . . . . . . 8 ⊢ (𝑧 = 𝑚 → ((𝑁 / 𝑘) / 𝑧) = ((𝑁 / 𝑘) / 𝑚))
72		ovex 7445	. . . . . . . 8 ⊢ ((𝑁 / 𝑘) / 𝑧) ∈ V
73	71, 68, 72	fvmpt3i 6997	. . . . . . 7 ⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚))
74	73	adantl 486	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚))
75	17	fsumdvdsdiaglem 27325	. . . . . . . 8 ⊢ (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})))
76	56	ex 417	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
77	75, 76	syld 48	. . . . . . 7 ⊢ (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
78	77	impl 460	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
79	59, 66, 70, 74, 78	fsumf1o 15776	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴)
80		ovexd 7447	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ∈ V)
81		nncn 12242	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
82		nnne0 12271	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
83	81, 82	jca 520	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
84	17, 83	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
85	84	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
86	85	simpld 499	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑁 ∈ ℂ)
87		elrabi 3647	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑘 ∈ ℕ)
88	87	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑘 ∈ ℕ)
89	88	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑘 ∈ ℕ)
90		nncn 12242	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
91		nnne0 12271	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
92	90, 91	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
93	89, 92	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
94		elrabi 3647	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → 𝑚 ∈ ℕ)
95	94	adantl 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑚 ∈ ℕ)
96		nncn 12242	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
97		nnne0 12271	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0)
98	96, 97	jca 520	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
99	95, 98	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
100		divdiv1 11927	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚)))
101	86, 93, 99, 100	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚)))
102	101	oveq2d 7428	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑁 / (𝑁 / (𝑘 · 𝑚))))
103		nnmulcl 12258	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑘 · 𝑚) ∈ ℕ)
104	88, 94, 103	syl2an 607	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 · 𝑚) ∈ ℕ)
105		nncn 12242	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ∈ ℂ)
106		nnne0 12271	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ≠ 0)
107	105, 106	jca 520	. . . . . . . . . . . . 13 ⊢ ((𝑘 · 𝑚) ∈ ℕ → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0))
108	104, 107	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0))
109		ddcan 11930	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0)) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚))
110	85, 108, 109	syl2anc 595	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚))
111	102, 110	eqtrd 2798	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑘 · 𝑚))
112	111	eqeq2d 2774	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ↔ 𝑗 = (𝑘 · 𝑚)))
113	112	biimpa 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝑗 = (𝑘 · 𝑚))
114		fsumdvdscom.2	. . . . . . . 8 ⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵)
115	113, 114	syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝐴 = 𝐵)
116	80, 115	csbied 3890	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴 = 𝐵)
117	116	sumeq2dv 15755	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
118	79, 117	eqtrd 2798	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
119	118	sumeq2dv 15755	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
120	48, 57, 119	3eqtrd 2802	. 2 ⊢ (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
121	10, 120	eqtrid 2810	1 ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  {crab 3416  Vcvv 3455  ⦋csb 3854   ⊆ wss 3906   class class class wbr 5110   ↦ cmpt 5193  –1-1-onto→wf1o 6537  ‘cfv 6538  (class class class)co 7412  ℂcc 11099  0cc0 11101  1c1 11102   · cmul 11106   / cdiv 11872  ℕcn 12234  ...cfz 13536  Σcsu 15739   ∥ cdvds 16311

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5239  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-inf2 9611  ax-cnex 11157  ax-resscn 11158  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-addrcl 11162  ax-mulcl 11163  ax-mulrcl 11164  ax-mulcom 11165  ax-addass 11166  ax-mulass 11167  ax-distr 11168  ax-i2m1 11169  ax-1ne0 11170  ax-1rid 11171  ax-rnegex 11172  ax-rrecex 11173  ax-cnre 11174  ax-pre-lttri 11175  ax-pre-lttrn 11176  ax-pre-ltadd 11177  ax-pre-mulgt0 11178  ax-pre-sup 11179

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-int 4914  df-iun 4959  df-br 5111  df-opab 5175  df-mpt 5194  df-tr 5220  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-se 5617  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6304  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-isom 6547  df-riota 7369  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7864  df-1st 7987  df-2nd 7988  df-frecs 8279  df-wrecs 8310  df-recs 8359  df-rdg 8398  df-1o 8454  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-fin 8948  df-sup 9403  df-oi 9473  df-card 9926  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11444  df-neg 11445  df-div 11873  df-nn 12235  df-2 12304  df-3 12305  df-n0 12506  df-z 12593  df-uz 12864  df-rp 13018  df-fz 13537  df-fzo 13685  df-seq 14040  df-exp 14100  df-hash 14369  df-cj 15152  df-re 15153  df-im 15154  df-sqrt 15288  df-abs 15289  df-clim 15541  df-sum 15740  df-dvds 16312

This theorem is referenced by:  logsqvma  27684