muinv

Description: The Möbius inversion formula. If G ( n ) = sum_ k || n F ( k ) for every n e. NN , then F ( n ) = sum_ k || n mmu ( k ) G ( n / k ) = sum_ k || n mmu ( n / k ) G ( k ) , i.e. the Möbius function is the Dirichlet convolution inverse of the constant function 1 . Theorem 2.9 in ApostolNT p. 32. (Contributed by Mario Carneiro, 2-Jul-2015)

	Ref	Expression
Hypotheses	muinv.1	$⊢ φ \to F : ℕ ⟶ ℂ$
	muinv.2	$⊢ φ \to G = (n \in ℕ ⟼ \sum_{k \in \{x \in ℕ \| x ∥ n\}} F (k))$
Assertion	muinv	$⊢ φ \to F = (m \in ℕ ⟼ \sum_{j \in \{x \in ℕ \| x ∥ m\}} μ (j) G (\frac{m}{j}))$

Proof

Step	Hyp	Ref	Expression
1		muinv.1	$⊢ φ \to F : ℕ ⟶ ℂ$
2		muinv.2	$⊢ φ \to G = (n \in ℕ ⟼ \sum_{k \in \{x \in ℕ \| x ∥ n\}} F (k))$
3	1	feqmptd	$⊢ φ \to F = (m \in ℕ ⟼ F (m))$
4	2	ad2antrr	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to G = (n \in ℕ ⟼ \sum_{k \in \{x \in ℕ \| x ∥ n\}} F (k))$
5	4	fveq1d	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to G (\frac{m}{j}) = (n \in ℕ ⟼ \sum_{k \in \{x \in ℕ \| x ∥ n\}} F (k)) (\frac{m}{j})$
6		breq1	$⊢ x = j \to (x ∥ m \leftrightarrow j ∥ m)$
7	6	elrab	$⊢ j \in \{x \in ℕ \| x ∥ m\} \leftrightarrow (j \in ℕ \land j ∥ m)$
8	7	simprbi	$⊢ j \in \{x \in ℕ \| x ∥ m\} \to j ∥ m$
9	8	adantl	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to j ∥ m$
10		elrabi	$⊢ j \in \{x \in ℕ \| x ∥ m\} \to j \in ℕ$
11	10	adantl	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to j \in ℕ$
12	11	nnzd	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to j \in ℤ$
13	11	nnne0d	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to j \neq 0$
14		nnz	$⊢ m \in ℕ \to m \in ℤ$
15	14	ad2antlr	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to m \in ℤ$
16		dvdsval2	$⊢ (j \in ℤ \land j \neq 0 \land m \in ℤ) \to (j ∥ m \leftrightarrow \frac{m}{j} \in ℤ)$
17	12 13 15 16	syl3anc	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to (j ∥ m \leftrightarrow \frac{m}{j} \in ℤ)$
18	9 17	mpbid	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to \frac{m}{j} \in ℤ$
19		nnre	$⊢ m \in ℕ \to m \in ℝ$
20		nngt0	$⊢ m \in ℕ \to 0 < m$
21	19 20	jca	$⊢ m \in ℕ \to (m \in ℝ \land 0 < m)$
22	21	ad2antlr	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to (m \in ℝ \land 0 < m)$
23		nnre	$⊢ j \in ℕ \to j \in ℝ$
24		nngt0	$⊢ j \in ℕ \to 0 < j$
25	23 24	jca	$⊢ j \in ℕ \to (j \in ℝ \land 0 < j)$
26	11 25	syl	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to (j \in ℝ \land 0 < j)$
27		divgt0	$⊢ ((m \in ℝ \land 0 < m) \land (j \in ℝ \land 0 < j)) \to 0 < \frac{m}{j}$
28	22 26 27	syl2anc	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to 0 < \frac{m}{j}$
29		elnnz	$⊢ \frac{m}{j} \in ℕ \leftrightarrow (\frac{m}{j} \in ℤ \land 0 < \frac{m}{j})$
30	18 28 29	sylanbrc	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to \frac{m}{j} \in ℕ$
31		breq2	$⊢ n = \frac{m}{j} \to (x ∥ n \leftrightarrow x ∥ (\frac{m}{j}))$
32	31	rabbidv	$⊢ n = \frac{m}{j} \to \{x \in ℕ \| x ∥ n\} = \{x \in ℕ \| x ∥ (\frac{m}{j})\}$
33	32	sumeq1d	$⊢ n = \frac{m}{j} \to \sum_{k \in \{x \in ℕ \| x ∥ n\}} F (k) = \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} F (k)$
34		eqid	$⊢ (n \in ℕ ⟼ \sum_{k \in \{x \in ℕ \| x ∥ n\}} F (k)) = (n \in ℕ ⟼ \sum_{k \in \{x \in ℕ \| x ∥ n\}} F (k))$
35		sumex	$⊢ \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} F (k) \in V$
36	33 34 35	fvmpt	$⊢ \frac{m}{j} \in ℕ \to (n \in ℕ ⟼ \sum_{k \in \{x \in ℕ \| x ∥ n\}} F (k)) (\frac{m}{j}) = \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} F (k)$
37	30 36	syl	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to (n \in ℕ ⟼ \sum_{k \in \{x \in ℕ \| x ∥ n\}} F (k)) (\frac{m}{j}) = \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} F (k)$
38	5 37	eqtrd	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to G (\frac{m}{j}) = \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} F (k)$
39	38	oveq2d	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to μ (j) G (\frac{m}{j}) = μ (j) \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} F (k)$
40		fzfid	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to (1 \dots \frac{m}{j}) \in Fin$
41		dvdsssfz1	$⊢ \frac{m}{j} \in ℕ \to \{x \in ℕ \| x ∥ (\frac{m}{j})\} \subseteq (1 \dots \frac{m}{j})$
42	30 41	syl	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to \{x \in ℕ \| x ∥ (\frac{m}{j})\} \subseteq (1 \dots \frac{m}{j})$
43	40 42	ssfid	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to \{x \in ℕ \| x ∥ (\frac{m}{j})\} \in Fin$
44		mucl	$⊢ j \in ℕ \to μ (j) \in ℤ$
45	11 44	syl	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to μ (j) \in ℤ$
46	45	zcnd	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to μ (j) \in ℂ$
47	1	ad2antrr	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to F : ℕ ⟶ ℂ$
48		elrabi	$⊢ k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\} \to k \in ℕ$
49		ffvelrn	$⊢ (F : ℕ ⟶ ℂ \land k \in ℕ) \to F (k) \in ℂ$
50	47 48 49	syl2an	$⊢ (((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \land k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}) \to F (k) \in ℂ$
51	43 46 50	fsummulc2	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to μ (j) \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} F (k) = \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} μ (j) F (k)$
52	39 51	eqtrd	$⊢ ((φ \land m \in ℕ) \land j \in \{x \in ℕ \| x ∥ m\}) \to μ (j) G (\frac{m}{j}) = \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} μ (j) F (k)$
53	52	sumeq2dv	$⊢ (φ \land m \in ℕ) \to \sum_{j \in \{x \in ℕ \| x ∥ m\}} μ (j) G (\frac{m}{j}) = \sum_{j \in \{x \in ℕ \| x ∥ m\}} \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} μ (j) F (k)$
54		simpr	$⊢ (φ \land m \in ℕ) \to m \in ℕ$
55	46	adantrr	$⊢ ((φ \land m \in ℕ) \land (j \in \{x \in ℕ \| x ∥ m\} \land k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\})) \to μ (j) \in ℂ$
56	50	anasss	$⊢ ((φ \land m \in ℕ) \land (j \in \{x \in ℕ \| x ∥ m\} \land k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\})) \to F (k) \in ℂ$
57	55 56	mulcld	$⊢ ((φ \land m \in ℕ) \land (j \in \{x \in ℕ \| x ∥ m\} \land k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\})) \to μ (j) F (k) \in ℂ$
58	54 57	fsumdvdsdiag	$⊢ (φ \land m \in ℕ) \to \sum_{j \in \{x \in ℕ \| x ∥ m\}} \sum_{k \in \{x \in ℕ \| x ∥ (\frac{m}{j})\}} μ (j) F (k) = \sum_{k \in \{x \in ℕ \| x ∥ m\}} \sum_{j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}} μ (j) F (k)$
59		ssrab2	$⊢ \{x \in ℕ \| x ∥ m\} \subseteq ℕ$
60		dvdsdivcl	$⊢ (m \in ℕ \land k \in \{x \in ℕ \| x ∥ m\}) \to \frac{m}{k} \in \{x \in ℕ \| x ∥ m\}$
61	60	adantll	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to \frac{m}{k} \in \{x \in ℕ \| x ∥ m\}$
62	59 61	sselid	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to \frac{m}{k} \in ℕ$
63		musum	$⊢ \frac{m}{k} \in ℕ \to \sum_{j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}} μ (j) = if (\frac{m}{k} = 1, 1, 0)$
64	62 63	syl	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to \sum_{j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}} μ (j) = if (\frac{m}{k} = 1, 1, 0)$
65	64	oveq1d	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to \sum_{j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}} μ (j) F (k) = if (\frac{m}{k} = 1, 1, 0) F (k)$
66		fzfid	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to (1 \dots \frac{m}{k}) \in Fin$
67		dvdsssfz1	$⊢ \frac{m}{k} \in ℕ \to \{x \in ℕ \| x ∥ (\frac{m}{k})\} \subseteq (1 \dots \frac{m}{k})$
68	62 67	syl	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to \{x \in ℕ \| x ∥ (\frac{m}{k})\} \subseteq (1 \dots \frac{m}{k})$
69	66 68	ssfid	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to \{x \in ℕ \| x ∥ (\frac{m}{k})\} \in Fin$
70	1	adantr	$⊢ (φ \land m \in ℕ) \to F : ℕ ⟶ ℂ$
71		elrabi	$⊢ k \in \{x \in ℕ \| x ∥ m\} \to k \in ℕ$
72	70 71 49	syl2an	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to F (k) \in ℂ$
73		ssrab2	$⊢ \{x \in ℕ \| x ∥ (\frac{m}{k})\} \subseteq ℕ$
74		simpr	$⊢ (((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \land j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}) \to j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}$
75	73 74	sselid	$⊢ (((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \land j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}) \to j \in ℕ$
76	75 44	syl	$⊢ (((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \land j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}) \to μ (j) \in ℤ$
77	76	zcnd	$⊢ (((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \land j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}) \to μ (j) \in ℂ$
78	69 72 77	fsummulc1	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to \sum_{j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}} μ (j) F (k) = \sum_{j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}} μ (j) F (k)$
79		ovif	$⊢ if (\frac{m}{k} = 1, 1, 0) F (k) = if (\frac{m}{k} = 1, 1 F (k), 0 \cdot F (k))$
80		nncn	$⊢ m \in ℕ \to m \in ℂ$
81	80	ad2antlr	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to m \in ℂ$
82	71	adantl	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to k \in ℕ$
83	82	nncnd	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to k \in ℂ$
84		1cnd	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to 1 \in ℂ$
85	82	nnne0d	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to k \neq 0$
86	81 83 84 85	divmuld	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to (\frac{m}{k} = 1 \leftrightarrow k \cdot 1 = m)$
87	83	mulid1d	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to k \cdot 1 = k$
88	87	eqeq1d	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to (k \cdot 1 = m \leftrightarrow k = m)$
89	86 88	bitrd	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to (\frac{m}{k} = 1 \leftrightarrow k = m)$
90	72	mulid2d	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to 1 F (k) = F (k)$
91	72	mul02d	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to 0 \cdot F (k) = 0$
92	89 90 91	ifbieq12d	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to if (\frac{m}{k} = 1, 1 F (k), 0 \cdot F (k)) = if (k = m, F (k), 0)$
93	79 92	syl5eq	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to if (\frac{m}{k} = 1, 1, 0) F (k) = if (k = m, F (k), 0)$
94	65 78 93	3eqtr3d	$⊢ ((φ \land m \in ℕ) \land k \in \{x \in ℕ \| x ∥ m\}) \to \sum_{j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}} μ (j) F (k) = if (k = m, F (k), 0)$
95	94	sumeq2dv	$⊢ (φ \land m \in ℕ) \to \sum_{k \in \{x \in ℕ \| x ∥ m\}} \sum_{j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}} μ (j) F (k) = \sum_{k \in \{x \in ℕ \| x ∥ m\}} if (k = m, F (k), 0)$
96		breq1	$⊢ x = m \to (x ∥ m \leftrightarrow m ∥ m)$
97	54	nnzd	$⊢ (φ \land m \in ℕ) \to m \in ℤ$
98		iddvds	$⊢ m \in ℤ \to m ∥ m$
99	97 98	syl	$⊢ (φ \land m \in ℕ) \to m ∥ m$
100	96 54 99	elrabd	$⊢ (φ \land m \in ℕ) \to m \in \{x \in ℕ \| x ∥ m\}$
101	100	snssd	$⊢ (φ \land m \in ℕ) \to \{m\} \subseteq \{x \in ℕ \| x ∥ m\}$
102	101	sselda	$⊢ ((φ \land m \in ℕ) \land k \in \{m\}) \to k \in \{x \in ℕ \| x ∥ m\}$
103	102 72	syldan	$⊢ ((φ \land m \in ℕ) \land k \in \{m\}) \to F (k) \in ℂ$
104		0cn	$⊢ 0 \in ℂ$
105		ifcl	$⊢ (F (k) \in ℂ \land 0 \in ℂ) \to if (k = m, F (k), 0) \in ℂ$
106	103 104 105	sylancl	$⊢ ((φ \land m \in ℕ) \land k \in \{m\}) \to if (k = m, F (k), 0) \in ℂ$
107		eldifsni	$⊢ k \in (\{x \in ℕ \| x ∥ m\} ∖ \{m\}) \to k \neq m$
108	107	adantl	$⊢ ((φ \land m \in ℕ) \land k \in (\{x \in ℕ \| x ∥ m\} ∖ \{m\})) \to k \neq m$
109	108	neneqd	$⊢ ((φ \land m \in ℕ) \land k \in (\{x \in ℕ \| x ∥ m\} ∖ \{m\})) \to \neg k = m$
110	109	iffalsed	$⊢ ((φ \land m \in ℕ) \land k \in (\{x \in ℕ \| x ∥ m\} ∖ \{m\})) \to if (k = m, F (k), 0) = 0$
111		fzfid	$⊢ (φ \land m \in ℕ) \to (1 \dots m) \in Fin$
112		dvdsssfz1	$⊢ m \in ℕ \to \{x \in ℕ \| x ∥ m\} \subseteq (1 \dots m)$
113	112	adantl	$⊢ (φ \land m \in ℕ) \to \{x \in ℕ \| x ∥ m\} \subseteq (1 \dots m)$
114	111 113	ssfid	$⊢ (φ \land m \in ℕ) \to \{x \in ℕ \| x ∥ m\} \in Fin$
115	101 106 110 114	fsumss	$⊢ (φ \land m \in ℕ) \to \sum_{k \in \{m\}} if (k = m, F (k), 0) = \sum_{k \in \{x \in ℕ \| x ∥ m\}} if (k = m, F (k), 0)$
116	1	ffvelrnda	$⊢ (φ \land m \in ℕ) \to F (m) \in ℂ$
117		iftrue	$⊢ k = m \to if (k = m, F (k), 0) = F (k)$
118		fveq2	$⊢ k = m \to F (k) = F (m)$
119	117 118	eqtrd	$⊢ k = m \to if (k = m, F (k), 0) = F (m)$
120	119	sumsn	$⊢ (m \in ℕ \land F (m) \in ℂ) \to \sum_{k \in \{m\}} if (k = m, F (k), 0) = F (m)$
121	54 116 120	syl2anc	$⊢ (φ \land m \in ℕ) \to \sum_{k \in \{m\}} if (k = m, F (k), 0) = F (m)$
122	95 115 121	3eqtr2d	$⊢ (φ \land m \in ℕ) \to \sum_{k \in \{x \in ℕ \| x ∥ m\}} \sum_{j \in \{x \in ℕ \| x ∥ (\frac{m}{k})\}} μ (j) F (k) = F (m)$
123	53 58 122	3eqtrd	$⊢ (φ \land m \in ℕ) \to \sum_{j \in \{x \in ℕ \| x ∥ m\}} μ (j) G (\frac{m}{j}) = F (m)$
124	123	mpteq2dva	$⊢ φ \to (m \in ℕ ⟼ \sum_{j \in \{x \in ℕ \| x ∥ m\}} μ (j) G (\frac{m}{j})) = (m \in ℕ ⟼ F (m))$
125	3 124	eqtr4d	$⊢ φ \to F = (m \in ℕ ⟼ \sum_{j \in \{x \in ℕ \| x ∥ m\}} μ (j) G (\frac{m}{j}))$

Metamath Proof Explorer

Theorem muinv

Proof