phisum

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

		Ref	Expression
	Assertion	phisum	$⊢ N \in ℕ \to \sum_{d \in \{x \in ℕ \| x ∥ N\}} ϕ (d) = N$

Proof

Step	Hyp	Ref	Expression
1		breq1	$⊢ x = y \to (x ∥ N \leftrightarrow y ∥ N)$
2	1	elrab	$⊢ y \in \{x \in ℕ \| x ∥ N\} \leftrightarrow (y \in ℕ \land y ∥ N)$
3		hashgcdeq	$⊢ (N \in ℕ \land y \in ℕ) \to \|\{z \in (0 ..^N) \| z \gcd N = y\}\| = if (y ∥ N, ϕ (\frac{N}{y}), 0)$
4	3	adantrr	$⊢ (N \in ℕ \land (y \in ℕ \land y ∥ N)) \to \|\{z \in (0 ..^N) \| z \gcd N = y\}\| = if (y ∥ N, ϕ (\frac{N}{y}), 0)$
5		iftrue	$⊢ y ∥ N \to if (y ∥ N, ϕ (\frac{N}{y}), 0) = ϕ (\frac{N}{y})$
6	5	ad2antll	$⊢ (N \in ℕ \land (y \in ℕ \land y ∥ N)) \to if (y ∥ N, ϕ (\frac{N}{y}), 0) = ϕ (\frac{N}{y})$
7	4 6	eqtrd	$⊢ (N \in ℕ \land (y \in ℕ \land y ∥ N)) \to \|\{z \in (0 ..^N) \| z \gcd N = y\}\| = ϕ (\frac{N}{y})$
8	2 7	sylan2b	$⊢ (N \in ℕ \land y \in \{x \in ℕ \| x ∥ N\}) \to \|\{z \in (0 ..^N) \| z \gcd N = y\}\| = ϕ (\frac{N}{y})$
9	8	sumeq2dv	$⊢ N \in ℕ \to \sum_{y \in \{x \in ℕ \| x ∥ N\}} \|\{z \in (0 ..^N) \| z \gcd N = y\}\| = \sum_{y \in \{x \in ℕ \| x ∥ N\}} ϕ (\frac{N}{y})$
10		fzfi	$⊢ (1 \dots N) \in Fin$
11		dvdsssfz1	$⊢ N \in ℕ \to \{x \in ℕ \| x ∥ N\} \subseteq (1 \dots N)$
12		ssfi	$⊢ ((1 \dots N) \in Fin \land \{x \in ℕ \| x ∥ N\} \subseteq (1 \dots N)) \to \{x \in ℕ \| x ∥ N\} \in Fin$
13	10 11 12	sylancr	$⊢ N \in ℕ \to \{x \in ℕ \| x ∥ N\} \in Fin$
14		fzofi	$⊢ (0 ..^N) \in Fin$
15		ssrab2	$⊢ \{z \in (0 ..^N) \| z \gcd N = y\} \subseteq (0 ..^N)$
16		ssfi	$⊢ ((0 ..^N) \in Fin \land \{z \in (0 ..^N) \| z \gcd N = y\} \subseteq (0 ..^N)) \to \{z \in (0 ..^N) \| z \gcd N = y\} \in Fin$
17	14 15 16	mp2an	$⊢ \{z \in (0 ..^N) \| z \gcd N = y\} \in Fin$
18	17	a1i	$⊢ (N \in ℕ \land y \in \{x \in ℕ \| x ∥ N\}) \to \{z \in (0 ..^N) \| z \gcd N = y\} \in Fin$
19		oveq1	$⊢ z = w \to z \gcd N = w \gcd N$
20	19	eqeq1d	$⊢ z = w \to (z \gcd N = y \leftrightarrow w \gcd N = y)$
21	20	elrab	$⊢ w \in \{z \in (0 ..^N) \| z \gcd N = y\} \leftrightarrow (w \in (0 ..^N) \land w \gcd N = y)$
22	21	simprbi	$⊢ w \in \{z \in (0 ..^N) \| z \gcd N = y\} \to w \gcd N = y$
23	22	rgen	$⊢ \forall w \in \{z \in (0 ..^N) \| z \gcd N = y\} w \gcd N = y$
24	23	rgenw	$⊢ \forall y \in \{x \in ℕ \| x ∥ N\} \forall w \in \{z \in (0 ..^N) \| z \gcd N = y\} w \gcd N = y$
25		invdisj	$⊢ \forall y \in \{x \in ℕ \| x ∥ N\} \forall w \in \{z \in (0 ..^N) \| z \gcd N = y\} w \gcd N = y \to \underset{y \in \{x \in ℕ \| x ∥ N\}}{Disj} \{z \in (0 ..^N) \| z \gcd N = y\}$
26	24 25	mp1i	$⊢ N \in ℕ \to \underset{y \in \{x \in ℕ \| x ∥ N\}}{Disj} \{z \in (0 ..^N) \| z \gcd N = y\}$
27	13 18 26	hashiun	$⊢ N \in ℕ \to \|⋃_{y \in \{x \in ℕ \| x ∥ N\}} \{z \in (0 ..^N) \| z \gcd N = y\}\| = \sum_{y \in \{x \in ℕ \| x ∥ N\}} \|\{z \in (0 ..^N) \| z \gcd N = y\}\|$
28		fveq2	$⊢ d = \frac{N}{y} \to ϕ (d) = ϕ (\frac{N}{y})$
29		eqid	$⊢ \{x \in ℕ \| x ∥ N\} = \{x \in ℕ \| x ∥ N\}$
30		eqid	$⊢ (z \in \{x \in ℕ \| x ∥ N\} ⟼ \frac{N}{z}) = (z \in \{x \in ℕ \| x ∥ N\} ⟼ \frac{N}{z})$
31	29 30	dvdsflip	$⊢ N \in ℕ \to (z \in \{x \in ℕ \| x ∥ N\} ⟼ \frac{N}{z}) : \{x \in ℕ \| x ∥ N\} \underset{1-1 onto}{⟶} \{x \in ℕ \| x ∥ N\}$
32		oveq2	$⊢ z = y \to \frac{N}{z} = \frac{N}{y}$
33		ovex	$⊢ \frac{N}{y} \in V$
34	32 30 33	fvmpt	$⊢ y \in \{x \in ℕ \| x ∥ N\} \to (z \in \{x \in ℕ \| x ∥ N\} ⟼ \frac{N}{z}) (y) = \frac{N}{y}$
35	34	adantl	$⊢ (N \in ℕ \land y \in \{x \in ℕ \| x ∥ N\}) \to (z \in \{x \in ℕ \| x ∥ N\} ⟼ \frac{N}{z}) (y) = \frac{N}{y}$
36		elrabi	$⊢ d \in \{x \in ℕ \| x ∥ N\} \to d \in ℕ$
37	36	adantl	$⊢ (N \in ℕ \land d \in \{x \in ℕ \| x ∥ N\}) \to d \in ℕ$
38	37	phicld	$⊢ (N \in ℕ \land d \in \{x \in ℕ \| x ∥ N\}) \to ϕ (d) \in ℕ$
39	38	nncnd	$⊢ (N \in ℕ \land d \in \{x \in ℕ \| x ∥ N\}) \to ϕ (d) \in ℂ$
40	28 13 31 35 39	fsumf1o	$⊢ N \in ℕ \to \sum_{d \in \{x \in ℕ \| x ∥ N\}} ϕ (d) = \sum_{y \in \{x \in ℕ \| x ∥ N\}} ϕ (\frac{N}{y})$
41	9 27 40	3eqtr4rd	$⊢ N \in ℕ \to \sum_{d \in \{x \in ℕ \| x ∥ N\}} ϕ (d) = \|⋃_{y \in \{x \in ℕ \| x ∥ N\}} \{z \in (0 ..^N) \| z \gcd N = y\}\|$
42		breq1	$⊢ x = z \gcd N \to (x ∥ N \leftrightarrow (z \gcd N) ∥ N)$
43		elfzoelz	$⊢ z \in (0 ..^N) \to z \in ℤ$
44	43	adantl	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to z \in ℤ$
45		nnz	$⊢ N \in ℕ \to N \in ℤ$
46	45	adantr	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to N \in ℤ$
47		nnne0	$⊢ N \in ℕ \to N \neq 0$
48	47	neneqd	$⊢ N \in ℕ \to \neg N = 0$
49	48	intnand	$⊢ N \in ℕ \to \neg (z = 0 \land N = 0)$
50	49	adantr	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to \neg (z = 0 \land N = 0)$
51		gcdn0cl	$⊢ ((z \in ℤ \land N \in ℤ) \land \neg (z = 0 \land N = 0)) \to z \gcd N \in ℕ$
52	44 46 50 51	syl21anc	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to z \gcd N \in ℕ$
53		gcddvds	$⊢ (z \in ℤ \land N \in ℤ) \to ((z \gcd N) ∥ z \land (z \gcd N) ∥ N)$
54	44 46 53	syl2anc	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to ((z \gcd N) ∥ z \land (z \gcd N) ∥ N)$
55	54	simprd	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to (z \gcd N) ∥ N$
56	42 52 55	elrabd	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to z \gcd N \in \{x \in ℕ \| x ∥ N\}$
57		clel5	$⊢ z \gcd N \in \{x \in ℕ \| x ∥ N\} \leftrightarrow \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y$
58	56 57	sylib	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y$
59	58	ralrimiva	$⊢ N \in ℕ \to \forall z \in (0 ..^N) \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y$
60		rabid2	$⊢ (0 ..^N) = \{z \in (0 ..^N) \| \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y\} \leftrightarrow \forall z \in (0 ..^N) \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y$
61	59 60	sylibr	$⊢ N \in ℕ \to (0 ..^N) = \{z \in (0 ..^N) \| \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y\}$
62		iunrab	$⊢ ⋃_{y \in \{x \in ℕ \| x ∥ N\}} \{z \in (0 ..^N) \| z \gcd N = y\} = \{z \in (0 ..^N) \| \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y\}$
63	61 62	syl6reqr	$⊢ N \in ℕ \to ⋃_{y \in \{x \in ℕ \| x ∥ N\}} \{z \in (0 ..^N) \| z \gcd N = y\} = (0 ..^N)$
64	63	fveq2d	$⊢ N \in ℕ \to \|⋃_{y \in \{x \in ℕ \| x ∥ N\}} \{z \in (0 ..^N) \| z \gcd N = y\}\| = \|(0 ..^N)\|$
65		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
66		hashfzo0	$⊢ N \in ℕ_{0} \to \|(0 ..^N)\| = N$
67	65 66	syl	$⊢ N \in ℕ \to \|(0 ..^N)\| = N$
68	64 67	eqtrd	$⊢ N \in ℕ \to \|⋃_{y \in \{x \in ℕ \| x ∥ N\}} \{z \in (0 ..^N) \| z \gcd N = y\}\| = N$
69	41 68	eqtrd	$⊢ N \in ℕ \to \sum_{d \in \{x \in ℕ \| x ∥ N\}} ϕ (d) = N$

Metamath Proof Explorer

Theorem phisum

Proof