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		fzfid	$⊢ N \in ℕ \to (1 \dots N) \in Fin$
34		dvdsssfz1	$⊢ N \in ℕ \to \{n \in ℕ \| n ∥ N\} \subseteq (1 \dots N)$
35	33 34	ssfid	$⊢ N \in ℕ \to \{n \in ℕ \| n ∥ N\} \in Fin$
36	13 19 32 35	fsumss	$⊢ N \in ℕ \to \sum_{k \in \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}} μ (k) = \sum_{k \in \{n \in ℕ \| n ∥ N\}} μ (k)$
37		fveq2	$⊢ x = \{p \in ℙ \| p ∥ k\} \to \|x\| = \|\{p \in ℙ \| p ∥ k\}\|$
38	37	oveq2d	$⊢ x = \{p \in ℙ \| p ∥ k\} \to {(- 1)}^{\|x\|} = {(- 1)}^{\|\{p \in ℙ \| p ∥ k\}\|}$
39	35 13	ssfid	$⊢ N \in ℕ \to \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} \in Fin$
40		eqid	$⊢ \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\} = \{n \in ℕ \| (μ (n) \neq 0 \land n ∥ N)\}$
41		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\})$
42		oveq1	$⊢ q = p \to q pCnt x = p pCnt x$
43	42	cbvmptv	$⊢ (q \in ℙ ⟼ q pCnt x) = (p \in ℙ ⟼ p pCnt x)$
44		oveq2	$⊢ x = m \to p pCnt x = p pCnt m$
45	44	mpteq2dv	$⊢ x = m \to (p \in ℙ ⟼ p pCnt x) = (p \in ℙ ⟼ p pCnt m)$
46	43 45	eqtrid	$⊢ x = m \to (q \in ℙ ⟼ q pCnt x) = (p \in ℙ ⟼ p pCnt m)$
47	46	cbvmptv	$⊢ (x \in ℕ ⟼ (q \in ℙ ⟼ q pCnt x)) = (m \in ℕ ⟼ (p \in ℙ ⟼ p pCnt m))$
48	40 41 47	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\}$
49		breq2	$⊢ m = k \to (p ∥ m \leftrightarrow p ∥ k)$
50	49	rabbidv	$⊢ m = k \to \{p \in ℙ \| p ∥ m\} = \{p \in ℙ \| p ∥ k\}$
51		prmex	$⊢ ℙ \in V$
52	51	rabex	$⊢ \{p \in ℙ \| p ∥ k\} \in V$
53	50 41 52	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\}$
54	53	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\}$
55		neg1cn	$⊢ - 1 \in ℂ$
56		prmdvdsfi	$⊢ N \in ℕ \to \{p \in ℙ \| p ∥ N\} \in Fin$
57		elpwi	$⊢ x \in 𝒫 \{p \in ℙ \| p ∥ N\} \to x \subseteq \{p \in ℙ \| p ∥ N\}$
58		ssfi	$⊢ (\{p \in ℙ \| p ∥ N\} \in Fin \land x \subseteq \{p \in ℙ \| p ∥ N\}) \to x \in Fin$
59	56 57 58	syl2an	$⊢ (N \in ℕ \land x \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to x \in Fin$
60		hashcl	$⊢ x \in Fin \to \|x\| \in ℕ_{0}$
61	59 60	syl	$⊢ (N \in ℕ \land x \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|x\| \in ℕ_{0}$
62		expcl	$⊢ (- 1 \in ℂ \land \|x\| \in ℕ_{0}) \to {(- 1)}^{\|x\|} \in ℂ$
63	55 61 62	sylancr	$⊢ (N \in ℕ \land x \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to {(- 1)}^{\|x\|} \in ℂ$
64	38 39 48 54 63	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\}\|}$
65		fzfid	$⊢ N \in ℕ \to (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \in Fin$
66	56	adantr	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to \{p \in ℙ \| p ∥ N\} \in Fin$
67		pwfi	$⊢ \{p \in ℙ \| p ∥ N\} \in Fin \leftrightarrow 𝒫 \{p \in ℙ \| p ∥ N\} \in Fin$
68	66 67	sylib	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to 𝒫 \{p \in ℙ \| p ∥ N\} \in Fin$
69		ssrab2	$⊢ \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \subseteq 𝒫 \{p \in ℙ \| p ∥ N\}$
70		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$
71	68 69 70	sylancl	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \in Fin$
72		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\}$
73		fveqeq2	$⊢ s = x \to (\|s\| = z \leftrightarrow \|x\| = z)$
74	73	elrab	$⊢ x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \leftrightarrow (x \in 𝒫 \{p \in ℙ \| p ∥ N\} \land \|x\| = z)$
75	74	simprbi	$⊢ x \in \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} \to \|x\| = z$
76	72 75	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$
77	76	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$
78		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\}$
79	77 78	syl	$⊢ N \in ℕ \to {Disj}_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\}$
80	56	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$
81	69 72	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\}$
82	81 57	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\}$
83	80 82	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$
84	83 60	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}$
85	55 84 62	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 ℂ$
86	65 71 79 85	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\|}$
87		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\}$
88	56	adantr	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \{p \in ℙ \| p ∥ N\} \in Fin$
89		elpwi	$⊢ s \in 𝒫 \{p \in ℙ \| p ∥ N\} \to s \subseteq \{p \in ℙ \| p ∥ N\}$
90	89	adantl	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to s \subseteq \{p \in ℙ \| p ∥ N\}$
91		ssdomg	$⊢ \{p \in ℙ \| p ∥ N\} \in Fin \to (s \subseteq \{p \in ℙ \| p ∥ N\} \to s ≼ \{p \in ℙ \| p ∥ N\})$
92	88 90 91	sylc	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to s ≼ \{p \in ℙ \| p ∥ N\}$
93		ssfi	$⊢ (\{p \in ℙ \| p ∥ N\} \in Fin \land s \subseteq \{p \in ℙ \| p ∥ N\}) \to s \in Fin$
94	56 89 93	syl2an	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to s \in Fin$
95		hashdom	$⊢ (s \in Fin \land \{p \in ℙ \| p ∥ N\} \in Fin) \to (\|s\| \leq \|\{p \in ℙ \| p ∥ N\}\| \leftrightarrow s ≼ \{p \in ℙ \| p ∥ N\})$
96	94 88 95	syl2anc	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to (\|s\| \leq \|\{p \in ℙ \| p ∥ N\}\| \leftrightarrow s ≼ \{p \in ℙ \| p ∥ N\})$
97	92 96	mpbird	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|s\| \leq \|\{p \in ℙ \| p ∥ N\}\|$
98		hashcl	$⊢ s \in Fin \to \|s\| \in ℕ_{0}$
99	94 98	syl	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|s\| \in ℕ_{0}$
100		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
101	99 100	eleqtrdi	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|s\| \in ℤ_{\geq 0}$
102		hashcl	$⊢ \{p \in ℙ \| p ∥ N\} \in Fin \to \|\{p \in ℙ \| p ∥ N\}\| \in ℕ_{0}$
103	56 102	syl	$⊢ N \in ℕ \to \|\{p \in ℙ \| p ∥ N\}\| \in ℕ_{0}$
104	103	adantr	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|\{p \in ℙ \| p ∥ N\}\| \in ℕ_{0}$
105	104	nn0zd	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|\{p \in ℙ \| p ∥ N\}\| \in ℤ$
106		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\}\|)$
107	101 105 106	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\}\|)$
108	97 107	mpbird	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|s\| \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)$
109		eqidd	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \|s\| = \|s\|$
110		eqeq2	$⊢ z = \|s\| \to (\|s\| = z \leftrightarrow \|s\| = \|s\|)$
111	110	rspcev	$⊢ (\|s\| \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \land \|s\| = \|s\|) \to \exists z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \|s\| = z$
112	108 109 111	syl2anc	$⊢ (N \in ℕ \land s \in 𝒫 \{p \in ℙ \| p ∥ N\}) \to \exists z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \|s\| = z$
113	112	ralrimiva	$⊢ N \in ℕ \to \forall s \in 𝒫 \{p \in ℙ \| p ∥ N\} \exists z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \|s\| = z$
114		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$
115	113 114	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\}$
116	87 115	eqtr4id	$⊢ N \in ℕ \to ⋃_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} \{s \in 𝒫 \{p \in ℙ \| p ∥ N\} \| \|s\| = z\} = 𝒫 \{p \in ℙ \| p ∥ N\}$
117	116	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\|}$
118		elfznn0	$⊢ z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \to z \in ℕ_{0}$
119	118	adantl	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to z \in ℕ_{0}$
120		expcl	$⊢ (- 1 \in ℂ \land z \in ℕ_{0}) \to {(- 1)}^{z} \in ℂ$
121	55 119 120	sylancr	$⊢ (N \in ℕ \land z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|)) \to {(- 1)}^{z} \in ℂ$
122		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}$
123	71 121 122	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}$
124	75	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$
125	124	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}$
126	125	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}$
127		elfzelz	$⊢ z \in (0 \dots \|\{p \in ℙ \| p ∥ N\}\|) \to z \in ℤ$
128		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\}\|$
129	56 127 128	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\}\|$
130	129	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}$
131	123 126 130	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}$
132	131	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}$
133		1pneg1e0	$⊢ 1 + -1 = 0$
134	133	oveq1i	$⊢ {(1 + -1)}^{\|\{p \in ℙ \| p ∥ N\}\|} = 0^{\|\{p \in ℙ \| p ∥ N\}\|}$
135		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}$
136	55 103 135	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}$
137	134 136	eqtr3id	$⊢ N \in ℕ \to 0^{\|\{p \in ℙ \| p ∥ N\}\|} = \sum_{z = 0}^{\|\{p \in ℙ \| p ∥ N\}\|} (\binom{\|\{p \in ℙ \| p ∥ N\}\|}{z}) {(- 1)}^{z}$
138		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))$
139		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))$
140		nprmdvds1	$⊢ p \in ℙ \to \neg p ∥ 1$
141		simpr	$⊢ (N \in ℕ \land N = 1) \to N = 1$
142	141	breq2d	$⊢ (N \in ℕ \land N = 1) \to (p ∥ N \leftrightarrow p ∥ 1)$
143	142	notbid	$⊢ (N \in ℕ \land N = 1) \to (\neg p ∥ N \leftrightarrow \neg p ∥ 1)$
144	140 143	imbitrrid	$⊢ (N \in ℕ \land N = 1) \to (p \in ℙ \to \neg p ∥ N)$
145	144	ralrimiv	$⊢ (N \in ℕ \land N = 1) \to \forall p \in ℙ \neg p ∥ N$
146		rabeq0	$⊢ \{p \in ℙ \| p ∥ N\} = \emptyset \leftrightarrow \forall p \in ℙ \neg p ∥ N$
147	145 146	sylibr	$⊢ (N \in ℕ \land N = 1) \to \{p \in ℙ \| p ∥ N\} = \emptyset$
148	147	fveq2d	$⊢ (N \in ℕ \land N = 1) \to \|\{p \in ℙ \| p ∥ N\}\| = \|\emptyset\|$
149		hash0	$⊢ \|\emptyset\| = 0$
150	148 149	eqtrdi	$⊢ (N \in ℕ \land N = 1) \to \|\{p \in ℙ \| p ∥ N\}\| = 0$
151	150	oveq2d	$⊢ (N \in ℕ \land N = 1) \to 0^{\|\{p \in ℙ \| p ∥ N\}\|} = 0^{0}$
152		0exp0e1	$⊢ 0^{0} = 1$
153	151 152	eqtrdi	$⊢ (N \in ℕ \land N = 1) \to 0^{\|\{p \in ℙ \| p ∥ N\}\|} = 1$
154		df-ne	$⊢ N \neq 1 \leftrightarrow \neg N = 1$
155		eluz2b3	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (N \in ℕ \land N \neq 1)$
156	155	biimpri	$⊢ (N \in ℕ \land N \neq 1) \to N \in ℤ_{\geq 2}$
157	154 156	sylan2br	$⊢ (N \in ℕ \land \neg N = 1) \to N \in ℤ_{\geq 2}$
158		exprmfct	$⊢ N \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ N$
159	157 158	syl	$⊢ (N \in ℕ \land \neg N = 1) \to \exists p \in ℙ p ∥ N$
160		rabn0	$⊢ \{p \in ℙ \| p ∥ N\} \neq \emptyset \leftrightarrow \exists p \in ℙ p ∥ N$
161	159 160	sylibr	$⊢ (N \in ℕ \land \neg N = 1) \to \{p \in ℙ \| p ∥ N\} \neq \emptyset$
162	56	adantr	$⊢ (N \in ℕ \land \neg N = 1) \to \{p \in ℙ \| p ∥ N\} \in Fin$
163		hashnncl	$⊢ \{p \in ℙ \| p ∥ N\} \in Fin \to (\|\{p \in ℙ \| p ∥ N\}\| \in ℕ \leftrightarrow \{p \in ℙ \| p ∥ N\} \neq \emptyset)$
164	162 163	syl	$⊢ (N \in ℕ \land \neg N = 1) \to (\|\{p \in ℙ \| p ∥ N\}\| \in ℕ \leftrightarrow \{p \in ℙ \| p ∥ N\} \neq \emptyset)$
165	161 164	mpbird	$⊢ (N \in ℕ \land \neg N = 1) \to \|\{p \in ℙ \| p ∥ N\}\| \in ℕ$
166	165	0expd	$⊢ (N \in ℕ \land \neg N = 1) \to 0^{\|\{p \in ℙ \| p ∥ N\}\|} = 0$
167	138 139 153 166	ifbothda	$⊢ N \in ℕ \to 0^{\|\{p \in ℙ \| p ∥ N\}\|} = if (N = 1, 1, 0)$
168	132 137 167	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)$
169	86 117 168	3eqtr3d	$⊢ N \in ℕ \to \sum_{x \in 𝒫 \{p \in ℙ \| p ∥ N\}} {(- 1)}^{\|x\|} = if (N = 1, 1, 0)$
170	64 169	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)$
171	10 36 170	3eqtr3d	$⊢ N \in ℕ \to \sum_{k \in \{n \in ℕ \| n ∥ N\}} μ (k) = if (N = 1, 1, 0)$

Metamath Proof Explorer

Theorem musum

Proof