fsumdvdscom - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fsumdvdscom		Structured version Visualization version GIF version

Theorem fsumdvdscom 27133

Description: A double commutation of divisor sums based on fsumdvdsdiag 27132. 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		nfcv 2892	. . 3 ⊢ Ⅎ𝑢Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴
2		nfcv 2892	. . . 4 ⊢ Ⅎ𝑗{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}
3		nfcsb1v 3910	. . . 4 ⊢ Ⅎ𝑗⦋𝑢 / 𝑗⦌𝐴
4	2, 3	nfsum 15667	. . 3 ⊢ Ⅎ𝑗Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴
5		breq2 5147	. . . . 5 ⊢ (𝑗 = 𝑢 → (𝑥 ∥ 𝑗 ↔ 𝑥 ∥ 𝑢))
6	5	rabbidv 3427	. . . 4 ⊢ (𝑗 = 𝑢 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢})
7		csbeq1a 3899	. . . . 5 ⊢ (𝑗 = 𝑢 → 𝐴 = ⦋𝑢 / 𝑗⦌𝐴)
8	7	adantr 479	. . . 4 ⊢ ((𝑗 = 𝑢 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}) → 𝐴 = ⦋𝑢 / 𝑗⦌𝐴)
9	6, 8	sumeq12dv 15682	. . 3 ⊢ (𝑗 = 𝑢 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴)
10	1, 4, 9	cbvsumi 15673	. 2 ⊢ Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴
11		breq2 5147	. . . . . 6 ⊢ (𝑢 = (𝑁 / 𝑣) → (𝑥 ∥ 𝑢 ↔ 𝑥 ∥ (𝑁 / 𝑣)))
12	11	rabbidv 3427	. . . . 5 ⊢ (𝑢 = (𝑁 / 𝑣) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})
13		csbeq1 3888	. . . . . 6 ⊢ (𝑢 = (𝑁 / 𝑣) → ⦋𝑢 / 𝑗⦌𝐴 = ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
14	13	adantr 479	. . . . 5 ⊢ ((𝑢 = (𝑁 / 𝑣) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) → ⦋𝑢 / 𝑗⦌𝐴 = ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
15	12, 14	sumeq12dv 15682	. . . 4 ⊢ (𝑢 = (𝑁 / 𝑣) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
16		fzfid 13968	. . . . 5 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
17		fsumdvdscom.1	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℕ)
18		dvdsssfz1 16292	. . . . . 6 ⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁))
19	17, 18	syl 17	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ (1...𝑁))
20	16, 19	ssfid 9288	. . . 4 ⊢ (𝜑 → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin)
21		eqid 2725	. . . . . 6 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}
22		eqid 2725	. . . . . 6 ⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))
23	21, 22	dvdsflip 16291	. . . . 5 ⊢ (𝑁 ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
24	17, 23	syl 17	. . . 4 ⊢ (𝜑 → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
25		oveq2 7423	. . . . . 6 ⊢ (𝑧 = 𝑣 → (𝑁 / 𝑧) = (𝑁 / 𝑣))
26		ovex 7448	. . . . . 6 ⊢ (𝑁 / 𝑧) ∈ V
27	25, 22, 26	fvmpt3i 7004	. . . . 5 ⊢ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣))
28	27	adantl 480	. . . 4 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑣) = (𝑁 / 𝑣))
29		fzfid 13968	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (1...𝑢) ∈ Fin)
30		ssrab2 4069	. . . . . . . 8 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ⊆ ℕ
31		simpr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
32	30, 31	sselid 3970	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑢 ∈ ℕ)
33		dvdsssfz1 16292	. . . . . . 7 ⊢ (𝑢 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢))
34	32, 33	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ⊆ (1...𝑢))
35	29, 34	ssfid 9288	. . . . 5 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢} ∈ Fin)
36		fsumdvdscom.3	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗})) → 𝐴 ∈ ℂ)
37	36	ralrimivva 3191	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ)
38		nfv 1909	. . . . . . . . 9 ⊢ Ⅎ𝑢∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ
39	3	nfel1 2909	. . . . . . . . . 10 ⊢ Ⅎ𝑗⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ
40	2, 39	nfralw 3299	. . . . . . . . 9 ⊢ Ⅎ𝑗∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ
41	7	eleq1d 2810	. . . . . . . . . 10 ⊢ (𝑗 = 𝑢 → (𝐴 ∈ ℂ ↔ ⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ))
42	6, 41	raleqbidv 3330	. . . . . . . . 9 ⊢ (𝑗 = 𝑢 → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ))
43	38, 40, 42	cbvralw 3294	. . . . . . . 8 ⊢ (∀𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 ∈ ℂ ↔ ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
44	37, 43	sylib 217	. . . . . . 7 ⊢ (𝜑 → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
45	44	r19.21bi 3239	. . . . . 6 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
46	45	r19.21bi 3239	. . . . 5 ⊢ (((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}) → ⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
47	35, 46	fsumcl 15709	. . . 4 ⊢ ((𝜑 ∧ 𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
48	15, 20, 24, 28, 47	fsumf1o 15699	. . 3 ⊢ (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
49	13	eleq1d 2810	. . . . . . . 8 ⊢ (𝑢 = (𝑁 / 𝑣) → (⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ ↔ ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
50	12, 49	raleqbidv 3330	. . . . . . 7 ⊢ (𝑢 = (𝑁 / 𝑣) → (∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ ↔ ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
51	44	adantr 479	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 ∈ ℂ)
52		dvdsdivcl 16290	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
53	17, 52	sylan 578	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑣) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
54	50, 51, 53	rspcdva 3603	. . . . . 6 ⊢ ((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ∀𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
55	54	r19.21bi 3239	. . . . 5 ⊢ (((𝜑 ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
56	55	anasss 465	. . . 4 ⊢ ((𝜑 ∧ (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
57	17, 56	fsumdvdsdiag 27132	. . 3 ⊢ (𝜑 → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴)
58		oveq2 7423	. . . . . . 7 ⊢ (𝑣 = ((𝑁 / 𝑘) / 𝑚) → (𝑁 / 𝑣) = (𝑁 / ((𝑁 / 𝑘) / 𝑚)))
59	58	csbeq1d 3889	. . . . . 6 ⊢ (𝑣 = ((𝑁 / 𝑘) / 𝑚) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = ⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴)
60		fzfid 13968	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (1...(𝑁 / 𝑘)) ∈ Fin)
61		dvdsdivcl 16290	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
62	30, 61	sselid 3970	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ ℕ)
63	17, 62	sylan 578	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑁 / 𝑘) ∈ ℕ)
64		dvdsssfz1 16292	. . . . . . . 8 ⊢ ((𝑁 / 𝑘) ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘)))
65	63, 64	syl 17	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ⊆ (1...(𝑁 / 𝑘)))
66	60, 65	ssfid 9288	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ∈ Fin)
67		eqid 2725	. . . . . . . 8 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}
68		eqid 2725	. . . . . . . 8 ⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))
69	67, 68	dvdsflip 16291	. . . . . . 7 ⊢ ((𝑁 / 𝑘) ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})
70	63, 69	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)})
71		oveq2 7423	. . . . . . . 8 ⊢ (𝑧 = 𝑚 → ((𝑁 / 𝑘) / 𝑧) = ((𝑁 / 𝑘) / 𝑚))
72		ovex 7448	. . . . . . . 8 ⊢ ((𝑁 / 𝑘) / 𝑧) ∈ V
73	71, 68, 72	fvmpt3i 7004	. . . . . . 7 ⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚))
74	73	adantl 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} ↦ ((𝑁 / 𝑘) / 𝑧))‘𝑚) = ((𝑁 / 𝑘) / 𝑚))
75	17	fsumdvdsdiaglem 27131	. . . . . . . 8 ⊢ (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)})))
76	56	ex 411	. . . . . . . 8 ⊢ (𝜑 → ((𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑣)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
77	75, 76	syld 47	. . . . . . 7 ⊢ (𝜑 → ((𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ))
78	77	impl 454	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 ∈ ℂ)
79	59, 66, 70, 74, 78	fsumf1o 15699	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴)
80		ovexd 7450	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ∈ V)
81		nncn 12248	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
82		nnne0 12274	. . . . . . . . . . . . . . . . 17 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
83	81, 82	jca 510	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
84	17, 83	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
85	84	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 ∈ ℂ ∧ 𝑁 ≠ 0))
86	85	simpld 493	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑁 ∈ ℂ)
87		elrabi 3669	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑘 ∈ ℕ)
88	87	adantl 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑘 ∈ ℕ)
89	88	adantr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑘 ∈ ℕ)
90		nncn 12248	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
91		nnne0 12274	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0)
92	90, 91	jca 510	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
93	89, 92	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0))
94		elrabi 3669	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)} → 𝑚 ∈ ℕ)
95	94	adantl 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → 𝑚 ∈ ℕ)
96		nncn 12248	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
97		nnne0 12274	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ℕ → 𝑚 ≠ 0)
98	96, 97	jca 510	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ ℕ → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
99	95, 98	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0))
100		divdiv1 11953	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℂ ∧ (𝑘 ∈ ℂ ∧ 𝑘 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚)))
101	86, 93, 99, 100	syl3anc 1368	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑁 / 𝑘) / 𝑚) = (𝑁 / (𝑘 · 𝑚)))
102	101	oveq2d 7431	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑁 / (𝑁 / (𝑘 · 𝑚))))
103		nnmulcl 12264	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑘 · 𝑚) ∈ ℕ)
104	88, 94, 103	syl2an 594	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑘 · 𝑚) ∈ ℕ)
105		nncn 12248	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ∈ ℂ)
106		nnne0 12274	. . . . . . . . . . . . . 14 ⊢ ((𝑘 · 𝑚) ∈ ℕ → (𝑘 · 𝑚) ≠ 0)
107	105, 106	jca 510	. . . . . . . . . . . . 13 ⊢ ((𝑘 · 𝑚) ∈ ℕ → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0))
108	104, 107	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0))
109		ddcan 11956	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ ℂ ∧ 𝑁 ≠ 0) ∧ ((𝑘 · 𝑚) ∈ ℂ ∧ (𝑘 · 𝑚) ≠ 0)) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚))
110	85, 108, 109	syl2anc 582	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / (𝑁 / (𝑘 · 𝑚))) = (𝑘 · 𝑚))
111	102, 110	eqtrd 2765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑁 / ((𝑁 / 𝑘) / 𝑚)) = (𝑘 · 𝑚))
112	111	eqeq2d 2736	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → (𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚)) ↔ 𝑗 = (𝑘 · 𝑚)))
113	112	biimpa 475	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝑗 = (𝑘 · 𝑚))
114		fsumdvdscom.2	. . . . . . . 8 ⊢ (𝑗 = (𝑘 · 𝑚) → 𝐴 = 𝐵)
115	113, 114	syl 17	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) ∧ 𝑗 = (𝑁 / ((𝑁 / 𝑘) / 𝑚))) → 𝐴 = 𝐵)
116	80, 115	csbied 3923	. . . . . 6 ⊢ (((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) ∧ 𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}) → ⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴 = 𝐵)
117	116	sumeq2dv 15679	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / ((𝑁 / 𝑘) / 𝑚)) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
118	79, 117	eqtrd 2765	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
119	118	sumeq2dv 15679	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑣 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}⦋(𝑁 / 𝑣) / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
120	48, 57, 119	3eqtrd 2769	. 2 ⊢ (𝜑 → Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑢}⦋𝑢 / 𝑗⦌𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)
121	10, 120	eqtrid 2777	1 ⊢ (𝜑 → Σ𝑗 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑗}𝐴 = Σ𝑘 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}Σ𝑚 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ (𝑁 / 𝑘)}𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 ≠ wne 2930 ∀wral 3051 {crab 3419 Vcvv 3463 ⦋csb 3885 ⊆ wss 3940 class class class wbr 5143 ↦ cmpt 5226 –1-1-onto→wf1o 6541 ‘cfv 6542 (class class class)co 7415 ℂcc 11134 0cc0 11136 1c1 11137 · cmul 11141 / cdiv 11899 ℕcn 12240 ...cfz 13514 Σcsu 15662 ∥ cdvds 16228

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5280 ax-sep 5294 ax-nul 5301 ax-pow 5359 ax-pr 5423 ax-un 7737 ax-inf2 9662 ax-cnex 11192 ax-resscn 11193 ax-1cn 11194 ax-icn 11195 ax-addcl 11196 ax-addrcl 11197 ax-mulcl 11198 ax-mulrcl 11199 ax-mulcom 11200 ax-addass 11201 ax-mulass 11202 ax-distr 11203 ax-i2m1 11204 ax-1ne0 11205 ax-1rid 11206 ax-rnegex 11207 ax-rrecex 11208 ax-cnre 11209 ax-pre-lttri 11210 ax-pre-lttrn 11211 ax-pre-ltadd 11212 ax-pre-mulgt0 11213 ax-pre-sup 11214

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-pss 3960 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-int 4945 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5227 df-tr 5261 df-id 5570 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-se 5628 df-we 5629 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-isom 6551 df-riota 7371 df-ov 7418 df-oprab 7419 df-mpo 7420 df-om 7868 df-1st 7989 df-2nd 7990 df-frecs 8283 df-wrecs 8314 df-recs 8388 df-rdg 8427 df-1o 8483 df-er 8721 df-en 8961 df-dom 8962 df-sdom 8963 df-fin 8964 df-sup 9463 df-oi 9531 df-card 9960 df-pnf 11278 df-mnf 11279 df-xr 11280 df-ltxr 11281 df-le 11282 df-sub 11474 df-neg 11475 df-div 11900 df-nn 12241 df-2 12303 df-3 12304 df-n0 12501 df-z 12587 df-uz 12851 df-rp 13005 df-fz 13515 df-fzo 13658 df-seq 13997 df-exp 14057 df-hash 14320 df-cj 15076 df-re 15077 df-im 15078 df-sqrt 15212 df-abs 15213 df-clim 15462 df-sum 15663 df-dvds 16229

This theorem is referenced by: logsqvma 27491

W3C validator