Theorem fsumdvdscom 27429

Description: A double commutation of divisor sums based on fsumdvdsdiag 27428. 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 5111	. . . . 5 ⊢ (𝑗 = 𝑢 → (𝑥 ∥ 𝑗 ↔ 𝑥 ∥ 𝑢))
2	1	rabbidv 3421	. . . 4 ⊢ (𝑗 = 𝑢 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢})
3		csbeq1a 3864	. . . . 5 ⊢ (𝑗 = 𝑢 → 𝐴 = ⦋𝑢 / 𝑗⦌𝐴)
4	3	adantr 486	. . . 4 ⊢ ((𝑗 = 𝑢 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}) → 𝐴 = ⦋𝑢 / 𝑗⦌𝐴)
5	2, 4	sumeq12dv 15796	. . 3 ⊢ (𝑗 = 𝑢 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴)
6		nfcv 2924	. . 3 ⊢ Ⅎ𝑢Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴
7		nfcv 2924	. . . 4 ⊢ Ⅎ𝑗{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}
8		nfcsb1v 3874	. . . 4 ⊢ Ⅎ𝑗⦋𝑢 / 𝑗⦌𝐴
9	7, 8	nfsum 15782	. . 3 ⊢ Ⅎ𝑗Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴
10	5, 6, 9	cbvsum 15786	. 2 ⊢ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴
11		breq2 5111	. . . . . 6 ⊢ (𝑢 = (𝑁 / 𝑣) → (𝑥 ∥ 𝑢 ↔ 𝑥 ∥ (𝑁 / 𝑣)))
12	11	rabbidv 3421	. . . . 5 ⊢ (𝑢 = (𝑁 / 𝑣) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})
13		csbeq1 3853	. . . . . 6 ⊢ (𝑢 = (𝑁 / 𝑣) → ⦋𝑢 / 𝑗⦌𝐴 = ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
14	13	adantr 486	. . . . 5 ⊢ ((𝑢 = (𝑁 / 𝑣) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) → ⦋𝑢 / 𝑗⦌𝐴 = ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
15	12, 14	sumeq12dv 15796	. . . 4 ⊢ (𝑢 = (𝑁 / 𝑣) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
16		fzfid 14041	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
17		fsumdvdscom.1	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
18		dvdsssfz1 16414	. . . . . 6 ⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁))
19	17, 18	syl 18	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁))
20	16, 19	ssfid 9243	. . . 4 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin)
21		eqid 2762	. . . . . 6 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}
22		eqid 2762	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))
23	21, 22	dvdsflip 16413	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
24	17, 23	syl 18	. . . 4 ⊢ (𝜑 → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
25		oveq2 7425	. . . . . 6 ⊢ (𝑧 = 𝑣 → (𝑁 / 𝑧) = (𝑁 / 𝑣))
26		ovex 7450	. . . . . 6 ⊢ (𝑁 / 𝑧) ∈ V
27	25, 22, 26	fvmpt3i 6996	. . . . 5 ⊢ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣))
28	27	adantl 487	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣))
29		fzfid 14041	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (1...𝑢) ∈ Fin)
30		ssrab2 4031	. . . . . . . 8 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ ℕ
31		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
32	30, 31	sselid 3932	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑢 ∈ ℕ)
33		dvdsssfz1 16414	. . . . . . 7 ⊢ (𝑢 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢))
34	32, 33	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢))
35	29, 34	ssfid 9243	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ∈ Fin)
36		fsumdvdscom.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ)
37	36	ralrimivva 3207	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ)
38		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑢∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ
39	8	nfel1 2940	. . . . . . . . . 10 ⊢ Ⅎ𝑗⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ
40	7, 39	nfralw 3311	. . . . . . . . 9 ⊢ Ⅎ𝑗∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ
41	3	eleq1d 2847	. . . . . . . . . 10 ⊢ (𝑗 = 𝑢 → (𝐴 ∈ ℂ ↔ ⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ))
42	2, 41	raleqbidv 3336	. . . . . . . . 9 ⊢ (𝑗 = 𝑢 → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ))
43	38, 40, 42	cbvralw 3306	. . . . . . . 8 ⊢ (∀𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ ↔ ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
44	37, 43	sylib 221	. . . . . . 7 ⊢ (𝜑 → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
45	44	r19.21bi 3256	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
46	45	r19.21bi 3256	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) → ⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
47	35, 46	fsumcl 15823	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
48	15, 20, 24, 28, 47	fsumf1o 15813	. . 3 ⊢ (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
49	13	eleq1d 2847	. . . . . . . 8 ⊢ (𝑢 = (𝑁 / 𝑣) → (⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ ↔ ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
50	12, 49	raleqbidv 3336	. . . . . . 7 ⊢ (𝑢 = (𝑁 / 𝑣) → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
51	44	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
52		dvdsdivcl 16412	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
53	17, 52	sylan 592	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
54	50, 51, 53	rspcdva 3580	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
55	54	r19.21bi 3256	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
56	55	anasss 472	. . . 4 ⊢ ((𝜑 ∧ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
57	17, 56	fsumdvdsdiag 27428	. . 3 ⊢ (𝜑 → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
58		oveq2 7425	. . . . . . 7 ⊢ (𝑣 = ((𝑁 / 𝑘) / 𝑚) → (𝑁 / 𝑣) = (𝑁 / ((𝑁 / 𝑘) / 𝑚)))
59	58	csbeq1d 3854	. . . . . 6 ⊢ (𝑣 = ((𝑁 / 𝑘) / 𝑚) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = ⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴)
60		fzfid 14041	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (1...(𝑁 / 𝑘)) ∈ Fin)
61		dvdsdivcl 16412	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
62	30, 61	sselid 3932	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ ℕ)
63	17, 62	sylan 592	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ ℕ)
64		dvdsssfz1 16414	. . . . . . . 8 ⊢ ((𝑁 / 𝑘) ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘)))
65	63, 64	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘)))
66	60, 65	ssfid 9243	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ∈ Fin)
67		eqid 2762	. . . . . . . 8 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}
68		eqid 2762	. . . . . . . 8 ⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))
69	67, 68	dvdsflip 16413	. . . . . . 7 ⊢ ((𝑁 / 𝑘) ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})
70	63, 69	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})
71		oveq2 7425	. . . . . . . 8 ⊢ (𝑧 = 𝑚 → ((𝑁 / 𝑘) / 𝑧) = ((𝑁 / 𝑘) / 𝑚))
72		ovex 7450	. . . . . . . 8 ⊢ ((𝑁 / 𝑘) / 𝑧) ∈ V
73	71, 68, 72	fvmpt3i 6996	. . . . . . 7 ⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚))
74	73	adantl 487	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚))
75	17	fsumdvdsdiaglem 27427	. . . . . . . 8 ⊢ (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})))
76	56	ex 418	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
77	75, 76	syld 48	. . . . . . 7 ⊢ (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
78	77	impl 461	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
79	59, 66, 70, 74, 78	fsumf1o 15813	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴)
80		ovexd 7452	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ∈ V)
81		nncn 12269	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
82		nnne0 12298	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
83	81, 82	jca 521	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
84	17, 83	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
85	84	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
86	85	simpld 500	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑁 ∈ ℂ)
87		elrabi 3644	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑘 ∈ ℕ)
88	87	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑘 ∈ ℕ)
89	88	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑘 ∈ ℕ)
90		nncn 12269	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
91		nnne0 12298	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
92	90, 91	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
93	89, 92	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
94		elrabi 3644	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → 𝑚 ∈ ℕ)
95	94	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑚 ∈ ℕ)
96		nncn 12269	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
97		nnne0 12298	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0)
98	96, 97	jca 521	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
99	95, 98	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
100		divdiv1 11954	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚)))
101	86, 93, 99, 100	syl3anc 1398	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚)))
102	101	oveq2d 7433	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑁 / (𝑁 / (𝑘 · 𝑚))))
103		nnmulcl 12285	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑘 · 𝑚) ∈ ℕ)
104	88, 94, 103	syl2an 608	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 · 𝑚) ∈ ℕ)
105		nncn 12269	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ∈ ℂ)
106		nnne0 12298	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ≠ 0)
107	105, 106	jca 521	. . . . . . . . . . . . 13 ⊢ ((𝑘 · 𝑚) ∈ ℕ → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0))
108	104, 107	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0))
109		ddcan 11957	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0)) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚))
110	85, 108, 109	syl2anc 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚))
111	102, 110	eqtrd 2797	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑘 · 𝑚))
112	111	eqeq2d 2773	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ↔ 𝑗 = (𝑘 · 𝑚)))
113	112	biimpa 482	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝑗 = (𝑘 · 𝑚))
114		fsumdvdscom.2	. . . . . . . 8 ⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵)
115	113, 114	syl 18	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝐴 = 𝐵)
116	80, 115	csbied 3886	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴 = 𝐵)
117	116	sumeq2dv 15793	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
118	79, 117	eqtrd 2797	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
119	118	sumeq2dv 15793	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
120	48, 57, 119	3eqtrd 2801	. 2 ⊢ (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
121	10, 120	eqtrid 2809	1 ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∀wral 3078  {crab 3414  Vcvv 3453  ⦋csb 3850   ⊆ wss 3902   class class class wbr 5107   ↦ cmpt 5190  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7417  ℂcc 11126  0cc0 11128  1c1 11129   · cmul 11133   / cdiv 11899  ℕcn 12261  ...cfz 13565  Σcsu 15777   ∥ cdvds 16348

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740  ax-inf2 9624  ax-cnex 11184  ax-resscn 11185  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-mulcom 11192  ax-addass 11193  ax-mulass 11194  ax-distr 11195  ax-i2m1 11196  ax-1ne0 11197  ax-1rid 11198  ax-rnegex 11199  ax-rrecex 11200  ax-cnre 11201  ax-pre-lttri 11202  ax-pre-lttrn 11203  ax-pre-ltadd 11204  ax-pre-mulgt0 11205  ax-pre-sup 11206

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-int 4911  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-tr 5217  df-id 5554  df-eprel 5559  df-po 5567  df-so 5568  df-fr 5612  df-se 5613  df-we 5614  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7374  df-ov 7420  df-oprab 7421  df-mpo 7422  df-om 7867  df-1st 7990  df-2nd 7991  df-frecs 8284  df-wrecs 8315  df-recs 8364  df-rdg 8403  df-1o 8459  df-er 8700  df-en 8957  df-dom 8958  df-sdom 8959  df-fin 8960  df-sup 9416  df-oi 9486  df-card 9948  df-pnf 11273  df-mnf 11274  df-xr 11275  df-ltxr 11276  df-le 11277  df-sub 11471  df-neg 11472  df-div 11900  df-nn 12262  df-2 12331  df-3 12332  df-n0 12533  df-z 12620  df-uz 12892  df-rp 13047  df-fz 13566  df-fzo 13714  df-seq 14070  df-exp 14130  df-hash 14399  df-cj 15190  df-re 15191  df-im 15192  df-sqrt 15326  df-abs 15327  df-clim 15579  df-sum 15778  df-dvds 16349

This theorem is used by:  logsqvma  27786