sqf11

Description: A squarefree number is completely determined by the set of its prime divisors. (Contributed by Mario Carneiro, 1-Jul-2015)

		Ref	Expression
	Assertion	sqf11	$⊢ ((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \to (A = B \leftrightarrow \forall p \in ℙ (p ∥ A \leftrightarrow p ∥ B))$

Proof

Step	Hyp	Ref	Expression
1		nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$
2		nnnn0	$⊢ B \in ℕ \to B \in ℕ_{0}$
3		pc11	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to (A = B \leftrightarrow \forall p \in ℙ p pCnt A = p pCnt B)$
4	1 2 3	syl2an	$⊢ (A \in ℕ \land B \in ℕ) \to (A = B \leftrightarrow \forall p \in ℙ p pCnt A = p pCnt B)$
5	4	ad2ant2r	$⊢ ((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \to (A = B \leftrightarrow \forall p \in ℙ p pCnt A = p pCnt B)$
6		eleq1	$⊢ p pCnt A = p pCnt B \to (p pCnt A \in ℕ \leftrightarrow p pCnt B \in ℕ)$
7		dfbi3	$⊢ (p pCnt A \in ℕ \leftrightarrow p pCnt B \in ℕ) \leftrightarrow ((p pCnt A \in ℕ \land p pCnt B \in ℕ) \lor (\neg p pCnt A \in ℕ \land \neg p pCnt B \in ℕ))$
8		sqfpc	$⊢ (A \in ℕ \land μ (A) \neq 0 \land p \in ℙ) \to p pCnt A \leq 1$
9	8	ad4ant124	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to p pCnt A \leq 1$
10		nnle1eq1	$⊢ p pCnt A \in ℕ \to (p pCnt A \leq 1 \leftrightarrow p pCnt A = 1)$
11	9 10	syl5ibcom	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (p pCnt A \in ℕ \to p pCnt A = 1)$
12		simprl	$⊢ ((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \to B \in ℕ$
13	12	adantr	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to B \in ℕ$
14		simplrr	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to μ (B) \neq 0$
15		simpr	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to p \in ℙ$
16		sqfpc	$⊢ (B \in ℕ \land μ (B) \neq 0 \land p \in ℙ) \to p pCnt B \leq 1$
17	13 14 15 16	syl3anc	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to p pCnt B \leq 1$
18		nnle1eq1	$⊢ p pCnt B \in ℕ \to (p pCnt B \leq 1 \leftrightarrow p pCnt B = 1)$
19	17 18	syl5ibcom	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (p pCnt B \in ℕ \to p pCnt B = 1)$
20	11 19	anim12d	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to ((p pCnt A \in ℕ \land p pCnt B \in ℕ) \to (p pCnt A = 1 \land p pCnt B = 1))$
21		eqtr3	$⊢ (p pCnt A = 1 \land p pCnt B = 1) \to p pCnt A = p pCnt B$
22	20 21	syl6	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to ((p pCnt A \in ℕ \land p pCnt B \in ℕ) \to p pCnt A = p pCnt B)$
23		id	$⊢ p \in ℙ \to p \in ℙ$
24		simpll	$⊢ ((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \to A \in ℕ$
25		pccl	$⊢ (p \in ℙ \land A \in ℕ) \to p pCnt A \in ℕ_{0}$
26	23 24 25	syl2anr	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to p pCnt A \in ℕ_{0}$
27		elnn0	$⊢ p pCnt A \in ℕ_{0} \leftrightarrow (p pCnt A \in ℕ \lor p pCnt A = 0)$
28	26 27	sylib	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (p pCnt A \in ℕ \lor p pCnt A = 0)$
29	28	ord	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (\neg p pCnt A \in ℕ \to p pCnt A = 0)$
30		pccl	$⊢ (p \in ℙ \land B \in ℕ) \to p pCnt B \in ℕ_{0}$
31	23 12 30	syl2anr	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to p pCnt B \in ℕ_{0}$
32		elnn0	$⊢ p pCnt B \in ℕ_{0} \leftrightarrow (p pCnt B \in ℕ \lor p pCnt B = 0)$
33	31 32	sylib	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (p pCnt B \in ℕ \lor p pCnt B = 0)$
34	33	ord	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (\neg p pCnt B \in ℕ \to p pCnt B = 0)$
35	29 34	anim12d	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to ((\neg p pCnt A \in ℕ \land \neg p pCnt B \in ℕ) \to (p pCnt A = 0 \land p pCnt B = 0))$
36		eqtr3	$⊢ (p pCnt A = 0 \land p pCnt B = 0) \to p pCnt A = p pCnt B$
37	35 36	syl6	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to ((\neg p pCnt A \in ℕ \land \neg p pCnt B \in ℕ) \to p pCnt A = p pCnt B)$
38	22 37	jaod	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (((p pCnt A \in ℕ \land p pCnt B \in ℕ) \lor (\neg p pCnt A \in ℕ \land \neg p pCnt B \in ℕ)) \to p pCnt A = p pCnt B)$
39	7 38	biimtrid	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to ((p pCnt A \in ℕ \leftrightarrow p pCnt B \in ℕ) \to p pCnt A = p pCnt B)$
40	6 39	impbid2	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (p pCnt A = p pCnt B \leftrightarrow (p pCnt A \in ℕ \leftrightarrow p pCnt B \in ℕ))$
41		pcelnn	$⊢ (p \in ℙ \land A \in ℕ) \to (p pCnt A \in ℕ \leftrightarrow p ∥ A)$
42	23 24 41	syl2anr	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (p pCnt A \in ℕ \leftrightarrow p ∥ A)$
43		pcelnn	$⊢ (p \in ℙ \land B \in ℕ) \to (p pCnt B \in ℕ \leftrightarrow p ∥ B)$
44	23 12 43	syl2anr	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (p pCnt B \in ℕ \leftrightarrow p ∥ B)$
45	42 44	bibi12d	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to ((p pCnt A \in ℕ \leftrightarrow p pCnt B \in ℕ) \leftrightarrow (p ∥ A \leftrightarrow p ∥ B))$
46	40 45	bitrd	$⊢ (((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \land p \in ℙ) \to (p pCnt A = p pCnt B \leftrightarrow (p ∥ A \leftrightarrow p ∥ B))$
47	46	ralbidva	$⊢ ((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \to (\forall p \in ℙ p pCnt A = p pCnt B \leftrightarrow \forall p \in ℙ (p ∥ A \leftrightarrow p ∥ B))$
48	5 47	bitrd	$⊢ ((A \in ℕ \land μ (A) \neq 0) \land (B \in ℕ \land μ (B) \neq 0)) \to (A = B \leftrightarrow \forall p \in ℙ (p ∥ A \leftrightarrow p ∥ B))$

Metamath Proof Explorer

Theorem sqf11

Proof