Theorem phisum 16828

Description: The divisor sum identity of the totient function. Theorem 2.2 in [ApostolNT] p. 26. (Contributed by Stefan O'Rear, 12-Sep-2015.)

Assertion

Ref	Expression
phisum	⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = 𝑁)

Distinct variable group:   𝑥,𝑁,𝑑

Proof of Theorem phisum

Dummy variables 𝑧 𝑦 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 5146	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 ∥ 𝑁 ↔ 𝑦 ∥ 𝑁))
2	1	elrab 3692	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁))
3		hashgcdeq 16827	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ ℕ) → (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0))
4	3	adantrr 717	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0))
5		iftrue 4531	. . . . . . 7 ⊢ (𝑦 ∥ 𝑁 → if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0) = (ϕ‘(𝑁 / 𝑦)))
6	5	ad2antll 729	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → if(𝑦 ∥ 𝑁, (ϕ‘(𝑁 / 𝑦)), 0) = (ϕ‘(𝑁 / 𝑦)))
7	4, 6	eqtrd 2777	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑦 ∈ ℕ ∧ 𝑦 ∥ 𝑁)) → (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (ϕ‘(𝑁 / 𝑦)))
8	2, 7	sylan2b 594	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (ϕ‘(𝑁 / 𝑦)))
9	8	sumeq2dv 15738	. . 3 ⊢ (𝑁 ∈ ℕ → Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘(𝑁 / 𝑦)))
10		dvdsfi 16826	. . . 4 ⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin)
11		fzofi 14015	. . . . . 6 ⊢ (0..^𝑁) ∈ Fin
12		ssrab2 4080	. . . . . 6 ⊢ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ⊆ (0..^𝑁)
13		ssfi 9213	. . . . . 6 ⊢ (((0..^𝑁) ∈ Fin ∧ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ⊆ (0..^𝑁)) → {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin)
14	11, 12, 13	mp2an 692	. . . . 5 ⊢ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin
15	14	a1i 11	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ∈ Fin)
16		oveq1 7438	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (𝑧 gcd 𝑁) = (𝑤 gcd 𝑁))
17	16	eqeq1d 2739	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → ((𝑧 gcd 𝑁) = 𝑦 ↔ (𝑤 gcd 𝑁) = 𝑦))
18	17	elrab 3692	. . . . . . . 8 ⊢ (𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} ↔ (𝑤 ∈ (0..^𝑁) ∧ (𝑤 gcd 𝑁) = 𝑦))
19	18	simprbi 496	. . . . . . 7 ⊢ (𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} → (𝑤 gcd 𝑁) = 𝑦)
20	19	rgen 3063	. . . . . 6 ⊢ ∀𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦
21	20	rgenw 3065	. . . . 5 ⊢ ∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦
22		invdisj 5129	. . . . 5 ⊢ (∀𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}∀𝑤 ∈ {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} (𝑤 gcd 𝑁) = 𝑦 → Disj 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})
23	21, 22	mp1i 13	. . . 4 ⊢ (𝑁 ∈ ℕ → Disj 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦})
24	10, 15, 23	hashiun 15858	. . 3 ⊢ (𝑁 ∈ ℕ → (♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (♯‘{𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}))
25		fveq2 6906	. . . 4 ⊢ (𝑑 = (𝑁 / 𝑦) → (ϕ‘𝑑) = (ϕ‘(𝑁 / 𝑦)))
26		eqid 2737	. . . . 5 ⊢ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} = {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}
27		eqid 2737	. . . . 5 ⊢ (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)) = (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))
28	26, 27	dvdsflip 16354	. . . 4 ⊢ (𝑁 ∈ ℕ → (𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧)):{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}–1-1-onto→{𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
29		oveq2 7439	. . . . . 6 ⊢ (𝑧 = 𝑦 → (𝑁 / 𝑧) = (𝑁 / 𝑦))
30		ovex 7464	. . . . . 6 ⊢ (𝑁 / 𝑦) ∈ V
31	29, 27, 30	fvmpt 7016	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑦) = (𝑁 / 𝑦))
32	31	adantl 481	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → ((𝑧 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↦ (𝑁 / 𝑧))‘𝑦) = (𝑁 / 𝑦))
33		elrabi 3687	. . . . . . 7 ⊢ (𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} → 𝑑 ∈ ℕ)
34	33	adantl 481	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → 𝑑 ∈ ℕ)
35	34	phicld 16809	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (ϕ‘𝑑) ∈ ℕ)
36	35	nncnd 12282	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁}) → (ϕ‘𝑑) ∈ ℂ)
37	25, 10, 28, 32, 36	fsumf1o 15759	. . 3 ⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = Σ𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘(𝑁 / 𝑦)))
38	9, 24, 37	3eqtr4rd 2788	. 2 ⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = (♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}))
39		iunrab 5052	. . . . 5 ⊢ ∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦}
40		breq1 5146	. . . . . . . . 9 ⊢ (𝑥 = (𝑧 gcd 𝑁) → (𝑥 ∥ 𝑁 ↔ (𝑧 gcd 𝑁) ∥ 𝑁))
41		elfzoelz 13699	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (0..^𝑁) → 𝑧 ∈ ℤ)
42	41	adantl 481	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → 𝑧 ∈ ℤ)
43		nnz 12634	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
44	43	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → 𝑁 ∈ ℤ)
45		nnne0 12300	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
46	45	neneqd 2945	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ¬ 𝑁 = 0)
47	46	intnand 488	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ¬ (𝑧 = 0 ∧ 𝑁 = 0))
48	47	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ¬ (𝑧 = 0 ∧ 𝑁 = 0))
49		gcdn0cl 16539	. . . . . . . . . 10 ⊢ (((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑧 = 0 ∧ 𝑁 = 0)) → (𝑧 gcd 𝑁) ∈ ℕ)
50	42, 44, 48, 49	syl21anc 838	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∈ ℕ)
51		gcddvds 16540	. . . . . . . . . . 11 ⊢ ((𝑧 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑧 gcd 𝑁) ∥ 𝑧 ∧ (𝑧 gcd 𝑁) ∥ 𝑁))
52	42, 44, 51	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ((𝑧 gcd 𝑁) ∥ 𝑧 ∧ (𝑧 gcd 𝑁) ∥ 𝑁))
53	52	simprd 495	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∥ 𝑁)
54	40, 50, 53	elrabd 3694	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → (𝑧 gcd 𝑁) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁})
55		clel5 3665	. . . . . . . 8 ⊢ ((𝑧 gcd 𝑁) ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ↔ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦)
56	54, 55	sylib 218	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ (0..^𝑁)) → ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦)
57	56	ralrimiva 3146	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ∀𝑧 ∈ (0..^𝑁)∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦)
58		rabid2 3470	. . . . . 6 ⊢ ((0..^𝑁) = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦} ↔ ∀𝑧 ∈ (0..^𝑁)∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦)
59	57, 58	sylibr 234	. . . . 5 ⊢ (𝑁 ∈ ℕ → (0..^𝑁) = {𝑧 ∈ (0..^𝑁) ∣ ∃𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (𝑧 gcd 𝑁) = 𝑦})
60	39, 59	eqtr4id 2796	. . . 4 ⊢ (𝑁 ∈ ℕ → ∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦} = (0..^𝑁))
61	60	fveq2d 6910	. . 3 ⊢ (𝑁 ∈ ℕ → (♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = (♯‘(0..^𝑁)))
62		nnnn0 12533	. . . 4 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
63		hashfzo0 14469	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (♯‘(0..^𝑁)) = 𝑁)
64	62, 63	syl 17	. . 3 ⊢ (𝑁 ∈ ℕ → (♯‘(0..^𝑁)) = 𝑁)
65	61, 64	eqtrd 2777	. 2 ⊢ (𝑁 ∈ ℕ → (♯‘∪ 𝑦 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} {𝑧 ∈ (0..^𝑁) ∣ (𝑧 gcd 𝑁) = 𝑦}) = 𝑁)
66	38, 65	eqtrd 2777	1 ⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = 𝑁)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3061  ∃wrex 3070  {crab 3436   ⊆ wss 3951  ifcif 4525  ∪ ciun 4991  Disj wdisj 5110   class class class wbr 5143   ↦ cmpt 5225  ‘cfv 6561  (class class class)co 7431  Fincfn 8985  0cc0 11155   / cdiv 11920  ℕcn 12266  ℕ₀cn0 12526  ℤcz 12613  ..^cfzo 13694  ♯chash 14369  Σcsu 15722   ∥ cdvds 16290   gcd cgcd 16531  ϕcphi 16801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-disj 5111  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723  df-dvds 16291  df-gcd 16532  df-phi 16803

This theorem is referenced by:  unitscyglem2  42197  unitscyglem4  42199