mumul

Description: The Möbius function is a multiplicative function. This is one of the primary interests of the Möbius function as an arithmetic function. (Contributed by Mario Carneiro, 3-Oct-2014) (Proof shortened by Timothy J. O'Malley, 9-Oct-2026)

		Ref	Expression
	Assertion	mumul	$⊢ (A \in ℕ \land B \in ℕ \land A \gcd B = 1) \to μ (A B) = μ (A) μ (B)$

Proof

Step	Hyp	Ref	Expression
1		simpl2	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (A) = 0) \to B \in ℕ$
2		mucl	$⊢ B \in ℕ \to μ (B) \in ℤ$
3	1 2	syl	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (A) = 0) \to μ (B) \in ℤ$
4	3	zcnd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (A) = 0) \to μ (B) \in ℂ$
5	4	mul02d	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (A) = 0) \to 0 \cdot μ (B) = 0$
6		simpr	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (A) = 0) \to μ (A) = 0$
7	6	oveq1d	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (A) = 0) \to μ (A) μ (B) = 0 \cdot μ (B)$
8		mumullem1	$⊢ ((A \in ℕ \land B \in ℕ) \land μ (A) = 0) \to μ (A B) = 0$
9	8	3adantl3	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (A) = 0) \to μ (A B) = 0$
10	5 7 9	3eqtr4rd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (A) = 0) \to μ (A B) = μ (A) μ (B)$
11		simpl1	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (B) = 0) \to A \in ℕ$
12		mucl	$⊢ A \in ℕ \to μ (A) \in ℤ$
13	11 12	syl	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (B) = 0) \to μ (A) \in ℤ$
14	13	zcnd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (B) = 0) \to μ (A) \in ℂ$
15	14	mul01d	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (B) = 0) \to μ (A) \cdot 0 = 0$
16		simpr	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (B) = 0) \to μ (B) = 0$
17	16	oveq2d	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (B) = 0) \to μ (A) μ (B) = μ (A) \cdot 0$
18		nnmulcom	$⊢ (A \in ℕ \land B \in ℕ) \to A B = B A$
19	18	fveq2d	$⊢ (A \in ℕ \land B \in ℕ) \to μ (A B) = μ (B A)$
20	19	adantr	$⊢ ((A \in ℕ \land B \in ℕ) \land μ (B) = 0) \to μ (A B) = μ (B A)$
21		mumullem1	$⊢ ((B \in ℕ \land A \in ℕ) \land μ (B) = 0) \to μ (B A) = 0$
22	21	ancom1s	$⊢ ((A \in ℕ \land B \in ℕ) \land μ (B) = 0) \to μ (B A) = 0$
23	20 22	eqtrd	$⊢ ((A \in ℕ \land B \in ℕ) \land μ (B) = 0) \to μ (A B) = 0$
24	23	3adantl3	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (B) = 0) \to μ (A B) = 0$
25	15 17 24	3eqtr4rd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (B) = 0) \to μ (A B) = μ (A) μ (B)$
26		simpl1	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to A \in ℕ$
27		simpl2	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to B \in ℕ$
28	26 27	nnmulcld	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to A B \in ℕ$
29		mumullem2	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (A B) \neq 0$
30		muval2	$⊢ (A B \in ℕ \land μ (A B) \neq 0) \to μ (A B) = {(- 1)}^{\|\{p \in ℙ \| p ∥ A B\}\|}$
31	28 29 30	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (A B) = {(- 1)}^{\|\{p \in ℙ \| p ∥ A B\}\|}$
32		neg1cn	$⊢ - 1 \in ℂ$
33	32	a1i	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to - 1 \in ℂ$
34		fzfi	$⊢ (1 \dots B) \in Fin$
35		prmssnn	$⊢ ℙ \subseteq ℕ$
36		rabss2	$⊢ ℙ \subseteq ℕ \to \{p \in ℙ \| p ∥ B\} \subseteq \{p \in ℕ \| p ∥ B\}$
37	35 36	ax-mp	$⊢ \{p \in ℙ \| p ∥ B\} \subseteq \{p \in ℕ \| p ∥ B\}$
38		dvdsssfz1	$⊢ B \in ℕ \to \{p \in ℕ \| p ∥ B\} \subseteq (1 \dots B)$
39	27 38	syl	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \{p \in ℕ \| p ∥ B\} \subseteq (1 \dots B)$
40	37 39	sstrid	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \{p \in ℙ \| p ∥ B\} \subseteq (1 \dots B)$
41		ssfi	$⊢ ((1 \dots B) \in Fin \land \{p \in ℙ \| p ∥ B\} \subseteq (1 \dots B)) \to \{p \in ℙ \| p ∥ B\} \in Fin$
42	34 40 41	sylancr	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \{p \in ℙ \| p ∥ B\} \in Fin$
43		hashcl	$⊢ \{p \in ℙ \| p ∥ B\} \in Fin \to \|\{p \in ℙ \| p ∥ B\}\| \in ℕ_{0}$
44	42 43	syl	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \|\{p \in ℙ \| p ∥ B\}\| \in ℕ_{0}$
45		prmdvdsfi	$⊢ A \in ℕ \to \{p \in ℙ \| p ∥ A\} \in Fin$
46	26 45	syl	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \{p \in ℙ \| p ∥ A\} \in Fin$
47		hashcl	$⊢ \{p \in ℙ \| p ∥ A\} \in Fin \to \|\{p \in ℙ \| p ∥ A\}\| \in ℕ_{0}$
48	46 47	syl	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \|\{p \in ℙ \| p ∥ A\}\| \in ℕ_{0}$
49	33 44 48	expaddd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to {(- 1)}^{\|\{p \in ℙ \| p ∥ A\}\| + \|\{p \in ℙ \| p ∥ B\}\|} = {(- 1)}^{\|\{p \in ℙ \| p ∥ A\}\|} {(- 1)}^{\|\{p \in ℙ \| p ∥ B\}\|}$
50		simpr	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to p \in ℙ$
51		simpl1	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land p \in ℙ) \to A \in ℕ$
52	51	nnzd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land p \in ℙ) \to A \in ℤ$
53	52	adantlr	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to A \in ℤ$
54		simpl2	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land p \in ℙ) \to B \in ℕ$
55	54	nnzd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land p \in ℙ) \to B \in ℤ$
56	55	adantlr	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to B \in ℤ$
57		euclemma	$⊢ (p \in ℙ \land A \in ℤ \land B \in ℤ) \to (p ∥ A B \leftrightarrow (p ∥ A \lor p ∥ B))$
58	50 53 56 57	syl3anc	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to (p ∥ A B \leftrightarrow (p ∥ A \lor p ∥ B))$
59	58	rabbidva	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \{p \in ℙ \| p ∥ A B\} = \{p \in ℙ \| (p ∥ A \lor p ∥ B)\}$
60		unrab	$⊢ \{p \in ℙ \| p ∥ A\} \cup \{p \in ℙ \| p ∥ B\} = \{p \in ℙ \| (p ∥ A \lor p ∥ B)\}$
61	59 60	eqtr4di	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \{p \in ℙ \| p ∥ A B\} = \{p \in ℙ \| p ∥ A\} \cup \{p \in ℙ \| p ∥ B\}$
62	61	fveq2d	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \|\{p \in ℙ \| p ∥ A B\}\| = \|\{p \in ℙ \| p ∥ A\} \cup \{p \in ℙ \| p ∥ B\}\|$
63		inrab	$⊢ \{p \in ℙ \| p ∥ A\} \cap \{p \in ℙ \| p ∥ B\} = \{p \in ℙ \| (p ∥ A \land p ∥ B)\}$
64		nprmdvds1	$⊢ p \in ℙ \to \neg p ∥ 1$
65	64	adantl	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to \neg p ∥ 1$
66		prmz	$⊢ p \in ℙ \to p \in ℤ$
67	66	adantl	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to p \in ℤ$
68		dvdsgcd	$⊢ (p \in ℤ \land A \in ℤ \land B \in ℤ) \to ((p ∥ A \land p ∥ B) \to p ∥ (A \gcd B))$
69	67 53 56 68	syl3anc	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to ((p ∥ A \land p ∥ B) \to p ∥ (A \gcd B))$
70		simpll3	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to A \gcd B = 1$
71	70	breq2d	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to (p ∥ (A \gcd B) \leftrightarrow p ∥ 1)$
72	69 71	sylibd	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to ((p ∥ A \land p ∥ B) \to p ∥ 1)$
73	65 72	mtod	$⊢ (((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \land p \in ℙ) \to \neg (p ∥ A \land p ∥ B)$
74	73	ralrimiva	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \forall p \in ℙ \neg (p ∥ A \land p ∥ B)$
75		rabeq0	$⊢ \{p \in ℙ \| (p ∥ A \land p ∥ B)\} = \emptyset \leftrightarrow \forall p \in ℙ \neg (p ∥ A \land p ∥ B)$
76	74 75	sylibr	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \{p \in ℙ \| (p ∥ A \land p ∥ B)\} = \emptyset$
77	63 76	eqtrid	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \{p \in ℙ \| p ∥ A\} \cap \{p \in ℙ \| p ∥ B\} = \emptyset$
78		hashun	$⊢ (\{p \in ℙ \| p ∥ A\} \in Fin \land \{p \in ℙ \| p ∥ B\} \in Fin \land \{p \in ℙ \| p ∥ A\} \cap \{p \in ℙ \| p ∥ B\} = \emptyset) \to \|\{p \in ℙ \| p ∥ A\} \cup \{p \in ℙ \| p ∥ B\}\| = \|\{p \in ℙ \| p ∥ A\}\| + \|\{p \in ℙ \| p ∥ B\}\|$
79	46 42 77 78	syl3anc	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \|\{p \in ℙ \| p ∥ A\} \cup \{p \in ℙ \| p ∥ B\}\| = \|\{p \in ℙ \| p ∥ A\}\| + \|\{p \in ℙ \| p ∥ B\}\|$
80	62 79	eqtrd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \|\{p \in ℙ \| p ∥ A B\}\| = \|\{p \in ℙ \| p ∥ A\}\| + \|\{p \in ℙ \| p ∥ B\}\|$
81	80	oveq2d	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to {(- 1)}^{\|\{p \in ℙ \| p ∥ A B\}\|} = {(- 1)}^{\|\{p \in ℙ \| p ∥ A\}\| + \|\{p \in ℙ \| p ∥ B\}\|}$
82		simprl	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (A) \neq 0$
83		muval2	$⊢ (A \in ℕ \land μ (A) \neq 0) \to μ (A) = {(- 1)}^{\|\{p \in ℙ \| p ∥ A\}\|}$
84	26 82 83	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (A) = {(- 1)}^{\|\{p \in ℙ \| p ∥ A\}\|}$
85		simprr	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (B) \neq 0$
86		muval2	$⊢ (B \in ℕ \land μ (B) \neq 0) \to μ (B) = {(- 1)}^{\|\{p \in ℙ \| p ∥ B\}\|}$
87	27 85 86	syl2anc	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (B) = {(- 1)}^{\|\{p \in ℙ \| p ∥ B\}\|}$
88	84 87	oveq12d	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (A) μ (B) = {(- 1)}^{\|\{p \in ℙ \| p ∥ A\}\|} {(- 1)}^{\|\{p \in ℙ \| p ∥ B\}\|}$
89	49 81 88	3eqtr4rd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (A) μ (B) = {(- 1)}^{\|\{p \in ℙ \| p ∥ A B\}\|}$
90	31 89	eqtr4d	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (A B) = μ (A) μ (B)$
91	10 25 90	pm2.61da2ne	$⊢ (A \in ℕ \land B \in ℕ \land A \gcd B = 1) \to μ (A B) = μ (A) μ (B)$

Metamath Proof Explorer

Theorem mumul

Proof