musum

Description: The sum of the Möbius function over the divisors of N gives one if N = 1 , but otherwise always sums to zero. Theorem 2.1 in ApostolNT p. 25. This makes the Möbius function useful for inverting divisor sums; see also muinv . (Contributed by Mario Carneiro, 2-Jul-2015)

		Ref	Expression
	Assertion	musum	$⊢ N \in ℕ \to \sum_{k \in \{n \in ℕ \| n ∥ N\}} μ (k) = if (N = 1, 1, 0)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ n = k \to μ (n) = μ (k)$
2	1	neeq1d	$⊢ n = k \to (μ (n) \neq 0 \leftrightarrow μ (k) \neq 0)$
3		breq1	$⊢ n = k \to (n ∥ N \leftrightarrow k ∥ N)$
4	2 3	anbi12d	$⊢ n = k \to ((μ (n) \neq 0 \land n ∥ N) \leftrightarrow (μ (k) \neq 0 \land k ∥ N))$
5	4	elrab	$⊢ k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} \leftrightarrow (k \in ℕ \land (μ (k) \neq 0 \land k ∥ N))$
6		muval2	$⊢ (k \in ℕ \land μ (k) \neq 0) \to μ (k) = {(- 1)}^{\|\{p \in ℙ \| p ∥ k\}\|}$
7	6	adantrr	$⊢ (k \in ℕ \land (μ (k) \neq 0 \land k ∥ N)) \to μ (k) = {(- 1)}^{\|\{p \in ℙ \| p ∥ k\}\|}$
8	5 7	sylbi	$⊢ k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} \to μ (k) = {(- 1)}^{\|\{p \in ℙ \| p ∥ k\}\|}$
9	8	adantl	$⊢ (N \in ℕ \land k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}) \to μ (k) = {(- 1)}^{\|\{p \in ℙ \| p ∥ k\}\|}$
10	9	sumeq2dv	$⊢ N \in ℕ \to \sum_{k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}} μ (k) = \sum_{k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}} {(- 1)}^{\|\{p \in ℙ \| p ∥ k\}\|}$
11		simpr	$⊢ (μ (n) \neq 0 \land n ∥ N) \to n ∥ N$
12	11	a1i	$⊢ (N \in ℕ \land n \in ℕ) \to ((μ (n) \neq 0 \land n ∥ N) \to n ∥ N)$
13	12	ss2rabdv	$⊢ N \in ℕ \to \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} \subseteq \{n \in ℕ \| n ∥ N\}$
14		ssrab2	$⊢ \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} \subseteq ℕ$
15		simpr	$⊢ (N \in ℕ \land k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}) \to k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}$
16	14 15	sselid	$⊢ (N \in ℕ \land k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}) \to k \in ℕ$
17		mucl	$⊢ k \in ℕ \to μ (k) \in ℤ$
18	16 17	syl	$⊢ (N \in ℕ \land k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}) \to μ (k) \in ℤ$
19	18	zcnd	$⊢ (N \in ℕ \land k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}) \to μ (k) \in ℂ$
20		difrab	$⊢ \{n \in ℕ \| n ∥ N\} ∖ \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} = \{n \in ℕ \| (n ∥ N \land \neg (μ (n) \neq 0 \land n ∥ N))\}$
21		pm3.21	$⊢ n ∥ N \to (μ (n) \neq 0 \to (μ (n) \neq 0 \land n ∥ N))$
22	21	necon1bd	$⊢ n ∥ N \to (\neg (μ (n) \neq 0 \land n ∥ N) \to μ (n) = 0)$
23	22	imp	$⊢ (n ∥ N \land \neg (μ (n) \neq 0 \land n ∥ N)) \to μ (n) = 0$
24	23	a1i	$⊢ n \in ℕ \to ((n ∥ N \land \neg (μ (n) \neq 0 \land n ∥ N)) \to μ (n) = 0)$
25	24	ss2rabi	$⊢ \{n \in ℕ \| (n ∥ N \land \neg (μ (n) \neq 0 \land n ∥ N))\} \subseteq \{n \in ℕ \| μ (n) = 0\}$
26	20 25	eqsstri	$⊢ \{n \in ℕ \| n ∥ N\} ∖ \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} \subseteq \{n \in ℕ \| μ (n) = 0\}$
27	26	sseli	$⊢ k \in (\{n \in ℕ \| n ∥ N\} ∖ \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}) \to k \in \{n \in ℕ \| μ (n) = 0\}$
28		fveqeq2	$⊢ n = k \to (μ (n) = 0 \leftrightarrow μ (k) = 0)$
29	28	elrab	$⊢ k \in \{n \in ℕ \| μ (n) = 0\} \leftrightarrow (k \in ℕ \land μ (k) = 0)$
30	29	simprbi	$⊢ k \in \{n \in ℕ \| μ (n) = 0\} \to μ (k) = 0$
31	27 30	syl	$⊢ k \in (\{n \in ℕ \| n ∥ N\} ∖ \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}) \to μ (k) = 0$
32	31	adantl	$⊢ (N \in ℕ \land k \in (\{n \in ℕ \| n ∥ N\} ∖ \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\})) \to μ (k) = 0$
33		dvdsfi	$⊢ N \in ℕ \to \{n \in ℕ \| n ∥ N\} \in Fin$
34	13 19 32 33	fsumss	$⊢ N \in ℕ \to \sum_{k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}} μ (k) = \sum_{k \in \{n \in ℕ \| n ∥ N\}} μ (k)$
35		fveq2	$⊢ x = \{p \in ℙ \| p ∥ k\} \to \|x\| = \|\{p \in ℙ \| p ∥ k\}\|$
36	35	oveq2d	$⊢ x = \{p \in ℙ \| p ∥ k\} \to {(- 1)}^{\|x\|} = {(- 1)}^{\|\{p \in ℙ \| p ∥ k\}\|}$
37	33 13	ssfid	$⊢ N \in ℕ \to \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} \in Fin$
38		eqid	$⊢ \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} = \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}$
39		eqid	$⊢ (m \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} ⟼ \{p \in ℙ \| p ∥ m\}) = (m \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} ⟼ \{p \in ℙ \| p ∥ m\})$
40		oveq1	$⊢ q = p \to q pCnt x = p pCnt x$
41	40	cbvmptv	$⊢ (q \in ℙ ⟼ q pCnt x) = (p \in ℙ ⟼ p pCnt x)$
42		oveq2	$⊢ x = m \to p pCnt x = p pCnt m$
43	42	mpteq2dv	$⊢ x = m \to (p \in ℙ ⟼ p pCnt x) = (p \in ℙ ⟼ p pCnt m)$
44	41 43	eqtrid	$⊢ x = m \to (q \in ℙ ⟼ q pCnt x) = (p \in ℙ ⟼ p pCnt m)$
45	44	cbvmptv	$⊢ (x \in ℕ ⟼ (q \in ℙ ⟼ q pCnt x)) = (m \in ℕ ⟼ (p \in ℙ ⟼ p pCnt m))$
46	38 39 45	sqff1o	$⊢ N \in ℕ \to (m \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} ⟼ \{p \in ℙ \| p ∥ m\}) : \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} \underset{1-1 onto}{⟶} 𝒫 \{p \in ℙ \| p ∥ N\}$
47		breq2	$⊢ m = k \to (p ∥ m \leftrightarrow p ∥ k)$
48	47	rabbidv	$⊢ m = k \to \{p \in ℙ \| p ∥ m\} = \{p \in ℙ \| p ∥ k\}$
49		prmex	$⊢ ℙ \in V$
50	49	rabex	$⊢ \{p \in ℙ \| p ∥ k\} \in V$
51	48 39 50	fvmpt	$⊢ k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} \to (m \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} ⟼ \{p \in ℙ \| p ∥ m\}) (k) = \{p \in ℙ \| p ∥ k\}$
52	51	adantl	$⊢ (N \in ℕ \land k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}) \to (m \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} ⟼ \{p \in ℙ \| p ∥ m\}) (k) = \{p \in ℙ \| p ∥ k\}$
53		neg1cn	$⊢ - 1 \in ℂ$
54		prmdvdsfi	$⊢ N \in ℕ \to \{p \in ℙ \| p ∥ N\} \in Fin$
55		elpwi	$⊢ x \in 𝒫 \{p \in ℙ \| p ∥ N\} \to x \subseteq \{p \in ℙ \| p ∥ N\}$
56		ssfi	$⊢ (\{p \in ℙ \| p ∥ N\} \in Fin \land x \subseteq \{p \in ℙ \| p ∥ N\}) \to x \in Fin$
57	54 55 56	syl2an	$⊢ (N \in ℕ \land x \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to x \in Fin$
58		hashcl	$⊢ x \in Fin \to \|x\| \in ℕ_{0}$
59	57 58	syl	$⊢ (N \in ℕ \land x \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|x\| \in ℕ_{0}$
60		expcl	$⊢ (- 1 \in ℂ \land \|x\| \in ℕ_{0}) \to {(- 1)}^{\|x\|} \in ℂ$
61	53 59 60	sylancr	$⊢ (N \in ℕ \land x \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to {(- 1)}^{\|x\|} \in ℂ$
62	36 37 46 52 61	fsumf1o	$⊢ N \in ℕ \to \sum_{x \in 𝒫 \{p \in ℙ \| p ∥ N\}} {(- 1)}^{\|x\|} = \sum_{k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}} {(- 1)}^{\|\{p \in ℙ \| p ∥ k\}\|}$
63		fzfid	$⊢ N \in ℕ \to (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \in Fin$
64	54	adantr	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to \{p \in ℙ \| p ∥ N\} \in Fin$
65		pwfi	$⊢ \{p \in ℙ \| p ∥ N\} \in Fin \leftrightarrow 𝒫 \{p \in ℙ \| p ∥ N\} \in Fin$
66	64 65	sylib	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to 𝒫 \{p \in ℙ \| p ∥ N\} \in Fin$
67		ssrab2	$⊢ \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \subseteq 𝒫 \{p \in ℙ \| p ∥ N\}$
68		ssfi	$⊢ (𝒫 \{p \in ℙ \| p ∥ N\} \in Fin \land \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \subseteq 𝒫 \{p \in ℙ \| p ∥ N\}) \to \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \in Fin$
69	66 67 68	sylancl	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \in Fin$
70		simprr	$⊢ (N \in ℕ \land (z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \land x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\})) \to x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}$
71		fveqeq2	$⊢ s = x \to (\|s\| = z \leftrightarrow \|x\| = z)$
72	71	elrab	$⊢ x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \leftrightarrow (x \in 𝒫 \{p \in ℙ \| p ∥ N\} \land \|x\| = z)$
73	72	simprbi	$⊢ x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \to \|x\| = z$
74	70 73	syl	$⊢ (N \in ℕ \land (z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \land x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\})) \to \|x\| = z$
75	74	ralrimivva	$⊢ N \in ℕ \to \forall z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \forall x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \|x\| = z$
76		invdisj	$⊢ \forall z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \forall x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \|x\| = z \to {Disj}_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}$
77	75 76	syl	$⊢ N \in ℕ \to {Disj}_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}$
78	54	adantr	$⊢ (N \in ℕ \land (z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \land x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\})) \to \{p \in ℙ \| p ∥ N\} \in Fin$
79	67 70	sselid	$⊢ (N \in ℕ \land (z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \land x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\})) \to x \in 𝒫 \{p \in ℙ \| p ∥ N\}$
80	79 55	syl	$⊢ (N \in ℕ \land (z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \land x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\})) \to x \subseteq \{p \in ℙ \| p ∥ N\}$
81	78 80	ssfid	$⊢ (N \in ℕ \land (z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \land x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\})) \to x \in Fin$
82	81 58	syl	$⊢ (N \in ℕ \land (z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \land x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\})) \to \|x\| \in ℕ_{0}$
83	53 82 60	sylancr	$⊢ (N \in ℕ \land (z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \land x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\})) \to {(- 1)}^{\|x\|} \in ℂ$
84	63 69 77 83	fsumiun	$⊢ N \in ℕ \to \sum_{x \in ⋃_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}} {(- 1)}^{\|x\|} = \sum_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \sum_{x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}} {(- 1)}^{\|x\|}$
85		iunrab	$⊢ ⋃_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} = \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \exists z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \|s\| = z\}$
86	54	adantr	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \{p \in ℙ \| p ∥ N\} \in Fin$
87		elpwi	$⊢ s \in 𝒫 \{p \in ℙ \| p ∥ N\} \to s \subseteq \{p \in ℙ \| p ∥ N\}$
88	87	adantl	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to s \subseteq \{p \in ℙ \| p ∥ N\}$
89		ssdomg	$⊢ \{p \in ℙ \| p ∥ N\} \in Fin \to (s \subseteq \{p \in ℙ \| p ∥ N\} \to s ≼ \{p \in ℙ \| p ∥ N\})$
90	86 88 89	sylc	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to s ≼ \{p \in ℙ \| p ∥ N\}$
91		ssfi	$⊢ (\{p \in ℙ \| p ∥ N\} \in Fin \land s \subseteq \{p \in ℙ \| p ∥ N\}) \to s \in Fin$
92	54 87 91	syl2an	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to s \in Fin$
93		hashdom	$⊢ (s \in Fin \land \{p \in ℙ \| p ∥ N\} \in Fin) \to (\|s\| \leq \|\{p \in ℙ \| p ∥ N\}\| \leftrightarrow s ≼ \{p \in ℙ \| p ∥ N\})$
94	92 86 93	syl2anc	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to (\|s\| \leq \|\{p \in ℙ \| p ∥ N\}\| \leftrightarrow s ≼ \{p \in ℙ \| p ∥ N\})$
95	90 94	mpbird	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|s\| \leq \|\{p \in ℙ \| p ∥ N\}\|$
96		hashcl	$⊢ s \in Fin \to \|s\| \in ℕ_{0}$
97	92 96	syl	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|s\| \in ℕ_{0}$
98		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
99	97 98	eleqtrdi	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|s\| \in ℤ_{\geq 0}$
100		hashcl	$⊢ \{p \in ℙ \| p ∥ N\} \in Fin \to \|\{p \in ℙ \| p ∥ N\}\| \in ℕ_{0}$
101	54 100	syl	$⊢ N \in ℕ \to \|\{p \in ℙ \| p ∥ N\}\| \in ℕ_{0}$
102	101	adantr	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|\{p \in ℙ \| p ∥ N\}\| \in ℕ_{0}$
103	102	nn0zd	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|\{p \in ℙ \| p ∥ N\}\| \in ℤ$
104		elfz5	$⊢ (\|s\| \in ℤ_{\geq 0} \land \|\{p \in ℙ \| p ∥ N\}\| \in ℤ) \to (\|s\| \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \leftrightarrow \|s\| \leq \|\{p \in ℙ \| p ∥ N\}\|)$
105	99 103 104	syl2anc	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to (\|s\| \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \leftrightarrow \|s\| \leq \|\{p \in ℙ \| p ∥ N\}\|)$
106	95 105	mpbird	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|s\| \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)$
107		eqidd	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|s\| = \|s\|$
108		eqeq2	$⊢ z = \|s\| \to (\|s\| = z \leftrightarrow \|s\| = \|s\|)$
109	108	rspcev	$⊢ (\|s\| \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \land \|s\| = \|s\|) \to \exists z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \|s\| = z$
110	106 107 109	syl2anc	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \exists z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \|s\| = z$
111	110	ralrimiva	$⊢ N \in ℕ \to \forall s \in 𝒫 \{p \in ℙ \| p ∥ N\} \exists z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \|s\| = z$
112		rabid2	$⊢ 𝒫 \{p \in ℙ \| p ∥ N\} = \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \exists z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \|s\| = z\} \leftrightarrow \forall s \in 𝒫 \{p \in ℙ \| p ∥ N\} \exists z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \|s\| = z$
113	111 112	sylibr	$⊢ N \in ℕ \to 𝒫 \{p \in ℙ \| p ∥ N\} = \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \exists z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \|s\| = z\}$
114	85 113	eqtr4id	$⊢ N \in ℕ \to ⋃_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} = 𝒫 \{p \in ℙ \| p ∥ N\}$
115	114	sumeq1d	$⊢ N \in ℕ \to \sum_{x \in ⋃_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}} {(- 1)}^{\|x\|} = \sum_{x \in 𝒫 \{p \in ℙ \| p ∥ N\}} {(- 1)}^{\|x\|}$
116		elfznn0	$⊢ z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \to z \in ℕ_{0}$
117	116	adantl	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to z \in ℕ_{0}$
118		expcl	$⊢ (- 1 \in ℂ \land z \in ℕ_{0}) \to {(- 1)}^{z} \in ℂ$
119	53 117 118	sylancr	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to {(- 1)}^{z} \in ℂ$
120		fsumconst	$⊢ (\{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \in Fin \land {(- 1)}^{z} \in ℂ) \to \sum_{x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}} {(- 1)}^{z} = \|\{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}\| {(- 1)}^{z}$
121	69 119 120	syl2anc	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to \sum_{x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}} {(- 1)}^{z} = \|\{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}\| {(- 1)}^{z}$
122	73	adantl	$⊢ ((N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \land x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}) \to \|x\| = z$
123	122	oveq2d	$⊢ ((N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \land x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}) \to {(- 1)}^{\|x\|} = {(- 1)}^{z}$
124	123	sumeq2dv	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to \sum_{x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}} {(- 1)}^{\|x\|} = \sum_{x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}} {(- 1)}^{z}$
125		elfzelz	$⊢ z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \to z \in ℤ$
126		hashbc	$⊢ (\{p \in ℙ \| p ∥ N\} \in Fin \land z \in ℤ) \to (\binom{\|\{p \in ℙ \| p ∥ N\}\|}{z}) = \|\{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}\|$
127	54 125 126	syl2an	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to (\binom{\|\{p \in ℙ \| p ∥ N\}\|}{z}) = \|\{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}\|$
128	127	oveq1d	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to (\binom{\|\{p \in ℙ \| p ∥ N\}\|}{z}) {(- 1)}^{z} = \|\{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}\| {(- 1)}^{z}$
129	121 124 128	3eqtr4d	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to \sum_{x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}} {(- 1)}^{\|x\|} = (\binom{\|\{p \in ℙ \| p ∥ N\}\|}{z}) {(- 1)}^{z}$
130	129	sumeq2dv	$⊢ N \in ℕ \to \sum_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \sum_{x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}} {(- 1)}^{\|x\|} = \sum_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} (\binom{\|\{p \in ℙ \| p ∥ N\}\|}{z}) {(- 1)}^{z}$
131		1pneg1e0	$⊢ 1 + -1 = 0$
132	131	oveq1i	$⊢ {(1 + -1)}^{\|\{p \in ℙ \| p ∥ N\}\|} = 0^{\|\{p \in ℙ \| p ∥ N\}\|}$
133		binom1p	$⊢ (- 1 \in ℂ \land \|\{p \in ℙ \| p ∥ N\}\| \in ℕ_{0}) \to {(1 + -1)}^{\|\{p \in ℙ \| p ∥ N\}\|} = \sum_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} (\binom{\|\{p \in ℙ \| p ∥ N\}\|}{z}) {(- 1)}^{z}$
134	53 101 133	sylancr	$⊢ N \in ℕ \to {(1 + -1)}^{\|\{p \in ℙ \| p ∥ N\}\|} = \sum_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} (\binom{\|\{p \in ℙ \| p ∥ N\}\|}{z}) {(- 1)}^{z}$
135	132 134	eqtr3id	$⊢ N \in ℕ \to 0^{\|\{p \in ℙ \| p ∥ N\}\|} = \sum_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} (\binom{\|\{p \in ℙ \| p ∥ N\}\|}{z}) {(- 1)}^{z}$
136		eqeq2	$⊢ 1 = if (N = 1, 1, 0) \to (0^{\|\{p \in ℙ \| p ∥ N\}\|} = 1 \leftrightarrow 0^{\|\{p \in ℙ \| p ∥ N\}\|} = if (N = 1, 1, 0))$
137		eqeq2	$⊢ 0 = if (N = 1, 1, 0) \to (0^{\|\{p \in ℙ \| p ∥ N\}\|} = 0 \leftrightarrow 0^{\|\{p \in ℙ \| p ∥ N\}\|} = if (N = 1, 1, 0))$
138		nprmdvds1	$⊢ p \in ℙ \to \neg p ∥ 1$
139		simpr	$⊢ (N \in ℕ \land N = 1) \to N = 1$
140	139	breq2d	$⊢ (N \in ℕ \land N = 1) \to (p ∥ N \leftrightarrow p ∥ 1)$
141	140	notbid	$⊢ (N \in ℕ \land N = 1) \to (\neg p ∥ N \leftrightarrow \neg p ∥ 1)$
142	138 141	imbitrrid	$⊢ (N \in ℕ \land N = 1) \to (p \in ℙ \to \neg p ∥ N)$
143	142	ralrimiv	$⊢ (N \in ℕ \land N = 1) \to \forall p \in ℙ \neg p ∥ N$
144		rabeq0	$⊢ \{p \in ℙ \| p ∥ N\} = \emptyset \leftrightarrow \forall p \in ℙ \neg p ∥ N$
145	143 144	sylibr	$⊢ (N \in ℕ \land N = 1) \to \{p \in ℙ \| p ∥ N\} = \emptyset$
146	145	fveq2d	$⊢ (N \in ℕ \land N = 1) \to \|\{p \in ℙ \| p ∥ N\}\| = \|\emptyset\|$
147		hash0	$⊢ \|\emptyset\| = 0$
148	146 147	eqtrdi	$⊢ (N \in ℕ \land N = 1) \to \|\{p \in ℙ \| p ∥ N\}\| = 0$
149	148	oveq2d	$⊢ (N \in ℕ \land N = 1) \to 0^{\|\{p \in ℙ \| p ∥ N\}\|} = 0^{0}$
150		0exp0e1	$⊢ 0^{0} = 1$
151	149 150	eqtrdi	$⊢ (N \in ℕ \land N = 1) \to 0^{\|\{p \in ℙ \| p ∥ N\}\|} = 1$
152		df-ne	$⊢ N \neq 1 \leftrightarrow \neg N = 1$
153		eluz2b3	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land N \neq 1)$
154	153	biimpri	$⊢ (N \in ℕ \land N \neq 1) \to N \in ℤ_{\geq 2}$
155	152 154	sylan2br	$⊢ (N \in ℕ \land \neg N = 1) \to N \in ℤ_{\geq 2}$
156		exprmfct	$⊢ N \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ N$
157	155 156	syl	$⊢ (N \in ℕ \land \neg N = 1) \to \exists p \in ℙ p ∥ N$
158		rabn0	$⊢ \{p \in ℙ \| p ∥ N\} \neq \emptyset \leftrightarrow \exists p \in ℙ p ∥ N$
159	157 158	sylibr	$⊢ (N \in ℕ \land \neg N = 1) \to \{p \in ℙ \| p ∥ N\} \neq \emptyset$
160	54	adantr	$⊢ (N \in ℕ \land \neg N = 1) \to \{p \in ℙ \| p ∥ N\} \in Fin$
161		hashnncl	$⊢ \{p \in ℙ \| p ∥ N\} \in Fin \to (\|\{p \in ℙ \| p ∥ N\}\| \in ℕ \leftrightarrow \{p \in ℙ \| p ∥ N\} \neq \emptyset)$
162	160 161	syl	$⊢ (N \in ℕ \land \neg N = 1) \to (\|\{p \in ℙ \| p ∥ N\}\| \in ℕ \leftrightarrow \{p \in ℙ \| p ∥ N\} \neq \emptyset)$
163	159 162	mpbird	$⊢ (N \in ℕ \land \neg N = 1) \to \|\{p \in ℙ \| p ∥ N\}\| \in ℕ$
164	163	0expd	$⊢ (N \in ℕ \land \neg N = 1) \to 0^{\|\{p \in ℙ \| p ∥ N\}\|} = 0$
165	136 137 151 164	ifbothda	$⊢ N \in ℕ \to 0^{\|\{p \in ℙ \| p ∥ N\}\|} = if (N = 1, 1, 0)$
166	130 135 165	3eqtr2d	$⊢ N \in ℕ \to \sum_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \sum_{x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}} {(- 1)}^{\|x\|} = if (N = 1, 1, 0)$
167	84 115 166	3eqtr3d	$⊢ N \in ℕ \to \sum_{x \in 𝒫 \{p \in ℙ \| p ∥ N\}} {(- 1)}^{\|x\|} = if (N = 1, 1, 0)$
168	62 167	eqtr3d	$⊢ N \in ℕ \to \sum_{k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}} {(- 1)}^{\|\{p \in ℙ \| p ∥ k\}\|} = if (N = 1, 1, 0)$
169	10 34 168	3eqtr3d	$⊢ N \in ℕ \to \sum_{k \in \{n \in ℕ \| n ∥ N\}} μ (k) = if (N = 1, 1, 0)$

Metamath Proof Explorer

Theorem musum

Proof