muval1

Description: The value of the Möbius function at a non-squarefree number. (Contributed by Mario Carneiro, 21-Sep-2014)

		Ref	Expression
	Assertion	muval1	$⊢ (A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \to μ (A) = 0$

Proof

Step	Hyp	Ref	Expression
1		muval	$⊢ A \in ℕ \to μ (A) = if (\exists p \in ℙ p^{2} ∥ A, 0, {(- 1)}^{\|\{p \in ℙ \| p ∥ A\}\|})$
2	1	3ad2ant1	$⊢ (A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \to μ (A) = if (\exists p \in ℙ p^{2} ∥ A, 0, {(- 1)}^{\|\{p \in ℙ \| p ∥ A\}\|})$
3		exprmfct	$⊢ P \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ P$
4	3	3ad2ant2	$⊢ (A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \to \exists p \in ℙ p ∥ P$
5		prmnn	$⊢ p \in ℙ \to p \in ℕ$
6		simpl2	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to P \in ℤ_{\geq 2}$
7		eluz2b2	$⊢ P \in ℤ_{\geq 2} \leftrightarrow (P \in ℕ \land 1 < P)$
8	6 7	sylib	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to (P \in ℕ \land 1 < P)$
9	8	simpld	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to P \in ℕ$
10		dvdssqlem	$⊢ (p \in ℕ \land P \in ℕ) \to (p ∥ P \leftrightarrow p^{2} ∥ P^{2})$
11	5 9 10	syl2an2	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to (p ∥ P \leftrightarrow p^{2} ∥ P^{2})$
12		simpl3	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to P^{2} ∥ A$
13		prmz	$⊢ p \in ℙ \to p \in ℤ$
14	13	adantl	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to p \in ℤ$
15		zsqcl	$⊢ p \in ℤ \to p^{2} \in ℤ$
16	14 15	syl	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to p^{2} \in ℤ$
17		eluzelz	$⊢ P \in ℤ_{\geq 2} \to P \in ℤ$
18		zsqcl	$⊢ P \in ℤ \to P^{2} \in ℤ$
19	6 17 18	3syl	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to P^{2} \in ℤ$
20		simpl1	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to A \in ℕ$
21	20	nnzd	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to A \in ℤ$
22		dvdstr	$⊢ (p^{2} \in ℤ \land P^{2} \in ℤ \land A \in ℤ) \to ((p^{2} ∥ P^{2} \land P^{2} ∥ A) \to p^{2} ∥ A)$
23	16 19 21 22	syl3anc	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to ((p^{2} ∥ P^{2} \land P^{2} ∥ A) \to p^{2} ∥ A)$
24	12 23	mpan2d	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to (p^{2} ∥ P^{2} \to p^{2} ∥ A)$
25	11 24	sylbid	$⊢ ((A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \land p \in ℙ) \to (p ∥ P \to p^{2} ∥ A)$
26	25	reximdva	$⊢ (A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \to (\exists p \in ℙ p ∥ P \to \exists p \in ℙ p^{2} ∥ A)$
27	4 26	mpd	$⊢ (A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \to \exists p \in ℙ p^{2} ∥ A$
28	27	iftrued	$⊢ (A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \to if (\exists p \in ℙ p^{2} ∥ A, 0, {(- 1)}^{\|\{p \in ℙ \| p ∥ A\}\|}) = 0$
29	2 28	eqtrd	$⊢ (A \in ℕ \land P \in ℤ_{\geq 2} \land P^{2} ∥ A) \to μ (A) = 0$

Metamath Proof Explorer

Theorem muval1

Proof