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		dvdsfi	$⊢ N \in ℕ \to \{x \in ℕ \| x ∥ N\} \in Fin$
11		fzofi	$⊢ (0 ..^N) \in Fin$
12		ssrab2	$⊢ \{z \in (0 ..^N) \| z \gcd N = y\} \subseteq (0 ..^N)$
13		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$
14	11 12 13	mp2an	$⊢ \{z \in (0 ..^N) \| z \gcd N = y\} \in Fin$
15	14	a1i	$⊢ (N \in ℕ \land y \in \{x \in ℕ \| x ∥ N\}) \to \{z \in (0 ..^N) \| z \gcd N = y\} \in Fin$
16		oveq1	$⊢ z = w \to z \gcd N = w \gcd N$
17	16	eqeq1d	$⊢ z = w \to (z \gcd N = y \leftrightarrow w \gcd N = y)$
18	17	elrab	$⊢ w \in \{z \in (0 ..^N) \| z \gcd N = y\} \leftrightarrow (w \in (0 ..^N) \land w \gcd N = y)$
19	18	simprbi	$⊢ w \in \{z \in (0 ..^N) \| z \gcd N = y\} \to w \gcd N = y$
20	19	rgen	$⊢ \forall w \in \{z \in (0 ..^N) \| z \gcd N = y\} w \gcd N = y$
21	20	rgenw	$⊢ \forall y \in \{x \in ℕ \| x ∥ N\} \forall w \in \{z \in (0 ..^N) \| z \gcd N = y\} w \gcd N = y$
22		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\}$
23	21 22	mp1i	$⊢ N \in ℕ \to \underset{y \in \{x \in ℕ \| x ∥ N\}}{Disj} \{z \in (0 ..^N) \| z \gcd N = y\}$
24	10 15 23	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\}\|$
25		fveq2	$⊢ d = \frac{N}{y} \to ϕ (d) = ϕ (\frac{N}{y})$
26		eqid	$⊢ \{x \in ℕ \| x ∥ N\} = \{x \in ℕ \| x ∥ N\}$
27		eqid	$⊢ (z \in \{x \in ℕ \| x ∥ N\} ⟼ \frac{N}{z}) = (z \in \{x \in ℕ \| x ∥ N\} ⟼ \frac{N}{z})$
28	26 27	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\}$
29		oveq2	$⊢ z = y \to \frac{N}{z} = \frac{N}{y}$
30		ovex	$⊢ \frac{N}{y} \in V$
31	29 27 30	fvmpt	$⊢ y \in \{x \in ℕ \| x ∥ N\} \to (z \in \{x \in ℕ \| x ∥ N\} ⟼ \frac{N}{z}) (y) = \frac{N}{y}$
32	31	adantl	$⊢ (N \in ℕ \land y \in \{x \in ℕ \| x ∥ N\}) \to (z \in \{x \in ℕ \| x ∥ N\} ⟼ \frac{N}{z}) (y) = \frac{N}{y}$
33		elrabi	$⊢ d \in \{x \in ℕ \| x ∥ N\} \to d \in ℕ$
34	33	adantl	$⊢ (N \in ℕ \land d \in \{x \in ℕ \| x ∥ N\}) \to d \in ℕ$
35	34	phicld	$⊢ (N \in ℕ \land d \in \{x \in ℕ \| x ∥ N\}) \to ϕ (d) \in ℕ$
36	35	nncnd	$⊢ (N \in ℕ \land d \in \{x \in ℕ \| x ∥ N\}) \to ϕ (d) \in ℂ$
37	25 10 28 32 36	fsumf1o	$⊢ N \in ℕ \to \sum_{d \in \{x \in ℕ \| x ∥ N\}} ϕ (d) = \sum_{y \in \{x \in ℕ \| x ∥ N\}} ϕ (\frac{N}{y})$
38	9 24 37	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\}\|$
39		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\}$
40		breq1	$⊢ x = z \gcd N \to (x ∥ N \leftrightarrow (z \gcd N) ∥ N)$
41		elfzoelz	$⊢ z \in (0 ..^N) \to z \in ℤ$
42	41	adantl	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to z \in ℤ$
43		nnz	$⊢ N \in ℕ \to N \in ℤ$
44	43	adantr	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to N \in ℤ$
45		nnne0	$⊢ N \in ℕ \to N \neq 0$
46	45	neneqd	$⊢ N \in ℕ \to \neg N = 0$
47	46	intnand	$⊢ N \in ℕ \to \neg (z = 0 \land N = 0)$
48	47	adantr	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to \neg (z = 0 \land N = 0)$
49		gcdn0cl	$⊢ ((z \in ℤ \land N \in ℤ) \land \neg (z = 0 \land N = 0)) \to z \gcd N \in ℕ$
50	42 44 48 49	syl21anc	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to z \gcd N \in ℕ$
51		gcddvds	$⊢ (z \in ℤ \land N \in ℤ) \to ((z \gcd N) ∥ z \land (z \gcd N) ∥ N)$
52	42 44 51	syl2anc	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to ((z \gcd N) ∥ z \land (z \gcd N) ∥ N)$
53	52	simprd	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to (z \gcd N) ∥ N$
54	40 50 53	elrabd	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to z \gcd N \in \{x \in ℕ \| x ∥ N\}$
55		clel5	$⊢ z \gcd N \in \{x \in ℕ \| x ∥ N\} \leftrightarrow \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y$
56	54 55	sylib	$⊢ (N \in ℕ \land z \in (0 ..^N)) \to \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y$
57	56	ralrimiva	$⊢ N \in ℕ \to \forall z \in (0 ..^N) \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y$
58		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$
59	57 58	sylibr	$⊢ N \in ℕ \to (0 ..^N) = \{z \in (0 ..^N) \| \exists y \in \{x \in ℕ \| x ∥ N\} z \gcd N = y\}$
60	39 59	eqtr4id	$⊢ N \in ℕ \to ⋃_{y \in \{x \in ℕ \| x ∥ N\}} \{z \in (0 ..^N) \| z \gcd N = y\} = (0 ..^N)$
61	60	fveq2d	$⊢ N \in ℕ \to \|⋃_{y \in \{x \in ℕ \| x ∥ N\}} \{z \in (0 ..^N) \| z \gcd N = y\}\| = \|(0 ..^N)\|$
62		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
63		hashfzo0	$⊢ N \in ℕ_{0} \to \|(0 ..^N)\| = N$
64	62 63	syl	$⊢ N \in ℕ \to \|(0 ..^N)\| = N$
65	61 64	eqtrd	$⊢ N \in ℕ \to \|⋃_{y \in \{x \in ℕ \| x ∥ N\}} \{z \in (0 ..^N) \| z \gcd N = y\}\| = N$
66	38 65	eqtrd	$⊢ N \in ℕ \to \sum_{d \in \{x \in ℕ \| x ∥ N\}} ϕ (d) = N$

Metamath Proof Explorer

Theorem phisum

Proof