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)

		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		nncn	$⊢ A \in ℕ \to A \in ℂ$
19		nncn	$⊢ B \in ℕ \to B \in ℂ$
20		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
21	18 19 20	syl2an	$⊢ (A \in ℕ \land B \in ℕ) \to A B = B A$
22	21	fveq2d	$⊢ (A \in ℕ \land B \in ℕ) \to μ (A B) = μ (B A)$
23	22	adantr	$⊢ ((A \in ℕ \land B \in ℕ) \land μ (B) = 0) \to μ (A B) = μ (B A)$
24		mumullem1	$⊢ ((B \in ℕ \land A \in ℕ) \land μ (B) = 0) \to μ (B A) = 0$
25	24	ancom1s	$⊢ ((A \in ℕ \land B \in ℕ) \land μ (B) = 0) \to μ (B A) = 0$
26	23 25	eqtrd	$⊢ ((A \in ℕ \land B \in ℕ) \land μ (B) = 0) \to μ (A B) = 0$
27	26	3adantl3	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (B) = 0) \to μ (A B) = 0$
28	15 17 27	3eqtr4rd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land μ (B) = 0) \to μ (A B) = μ (A) μ (B)$
29		simpl1	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to A \in ℕ$
30		simpl2	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to B \in ℕ$
31	29 30	nnmulcld	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to A B \in ℕ$
32		mumullem2	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (A B) \neq 0$
33		muval2	$⊢ (A B \in ℕ \land μ (A B) \neq 0) \to μ (A B) = {(- 1)}^{\|\{p \in ℙ \| p ∥ A B\}\|}$
34	31 32 33	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\}\|}$
35		neg1cn	$⊢ - 1 \in ℂ$
36	35	a1i	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to - 1 \in ℂ$
37		fzfi	$⊢ (1 \dots B) \in Fin$
38		prmssnn	$⊢ ℙ \subseteq ℕ$
39		rabss2	$⊢ ℙ \subseteq ℕ \to \{p \in ℙ \| p ∥ B\} \subseteq \{p \in ℕ \| p ∥ B\}$
40	38 39	ax-mp	$⊢ \{p \in ℙ \| p ∥ B\} \subseteq \{p \in ℕ \| p ∥ B\}$
41		dvdsssfz1	$⊢ B \in ℕ \to \{p \in ℕ \| p ∥ B\} \subseteq (1 \dots B)$
42	30 41	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)$
43	40 42	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)$
44		ssfi	$⊢ ((1 \dots B) \in Fin \land \{p \in ℙ \| p ∥ B\} \subseteq (1 \dots B)) \to \{p \in ℙ \| p ∥ B\} \in Fin$
45	37 43 44	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$
46		hashcl	$⊢ \{p \in ℙ \| p ∥ B\} \in Fin \to \|\{p \in ℙ \| p ∥ B\}\| \in ℕ_{0}$
47	45 46	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}$
48		fzfi	$⊢ (1 \dots A) \in Fin$
49		rabss2	$⊢ ℙ \subseteq ℕ \to \{p \in ℙ \| p ∥ A\} \subseteq \{p \in ℕ \| p ∥ A\}$
50	38 49	ax-mp	$⊢ \{p \in ℙ \| p ∥ A\} \subseteq \{p \in ℕ \| p ∥ A\}$
51		dvdsssfz1	$⊢ A \in ℕ \to \{p \in ℕ \| p ∥ A\} \subseteq (1 \dots A)$
52	29 51	syl	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \{p \in ℕ \| p ∥ A\} \subseteq (1 \dots A)$
53	50 52	sstrid	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to \{p \in ℙ \| p ∥ A\} \subseteq (1 \dots A)$
54		ssfi	$⊢ ((1 \dots A) \in Fin \land \{p \in ℙ \| p ∥ A\} \subseteq (1 \dots A)) \to \{p \in ℙ \| p ∥ A\} \in Fin$
55	48 53 54	sylancr	$⊢ ((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$
56		hashcl	$⊢ \{p \in ℙ \| p ∥ A\} \in Fin \to \|\{p \in ℙ \| p ∥ A\}\| \in ℕ_{0}$
57	55 56	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}$
58	36 47 57	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\}\|}$
59		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 ℙ$
60		simpl1	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land p \in ℙ) \to A \in ℕ$
61	60	nnzd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land p \in ℙ) \to A \in ℤ$
62	61	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 ℤ$
63		simpl2	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land p \in ℙ) \to B \in ℕ$
64	63	nnzd	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land p \in ℙ) \to B \in ℤ$
65	64	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 ℤ$
66		euclemma	$⊢ (p \in ℙ \land A \in ℤ \land B \in ℤ) \to (p ∥ A B \leftrightarrow (p ∥ A \lor p ∥ B))$
67	59 62 65 66	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))$
68	67	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)\}$
69		unrab	$⊢ \{p \in ℙ \| p ∥ A\} \cup \{p \in ℙ \| p ∥ B\} = \{p \in ℙ \| (p ∥ A \lor p ∥ B)\}$
70	68 69	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\}$
71	70	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\}\|$
72		inrab	$⊢ \{p \in ℙ \| p ∥ A\} \cap \{p \in ℙ \| p ∥ B\} = \{p \in ℙ \| (p ∥ A \land p ∥ B)\}$
73		nprmdvds1	$⊢ p \in ℙ \to \neg p ∥ 1$
74	73	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$
75		prmz	$⊢ p \in ℙ \to p \in ℤ$
76	75	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 ℤ$
77		dvdsgcd	$⊢ (p \in ℤ \land A \in ℤ \land B \in ℤ) \to ((p ∥ A \land p ∥ B) \to p ∥ (A \gcd B))$
78	76 62 65 77	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))$
79		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$
80	79	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)$
81	78 80	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)$
82	74 81	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)$
83	82	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)$
84		rabeq0	$⊢ \{p \in ℙ \| (p ∥ A \land p ∥ B)\} = \emptyset \leftrightarrow \forall p \in ℙ \neg (p ∥ A \land p ∥ B)$
85	83 84	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$
86	72 85	syl5eq	$⊢ ((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$
87		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\}\|$
88	55 45 86 87	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\}\|$
89	71 88	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\}\|$
90	89	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\}\|}$
91		simprl	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (A) \neq 0$
92		muval2	$⊢ (A \in ℕ \land μ (A) \neq 0) \to μ (A) = {(- 1)}^{\|\{p \in ℙ \| p ∥ A\}\|}$
93	29 91 92	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\}\|}$
94		simprr	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (B) \neq 0$
95		muval2	$⊢ (B \in ℕ \land μ (B) \neq 0) \to μ (B) = {(- 1)}^{\|\{p \in ℙ \| p ∥ B\}\|}$
96	30 94 95	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\}\|}$
97	93 96	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\}\|}$
98	58 90 97	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\}\|}$
99	34 98	eqtr4d	$⊢ ((A \in ℕ \land B \in ℕ \land A \gcd B = 1) \land (μ (A) \neq 0 \land μ (B) \neq 0)) \to μ (A B) = μ (A) μ (B)$
100	10 28 99	pm2.61da2ne	$⊢ (A \in ℕ \land B \in ℕ \land A \gcd B = 1) \to μ (A B) = μ (A) μ (B)$

Metamath Proof Explorer

Theorem mumul

Proof