pc2dvds

Description: A characterization of divisibility in terms of prime count. (Contributed by Mario Carneiro, 23-Feb-2014) (Revised by Mario Carneiro, 3-Oct-2014)

		Ref	Expression
	Assertion	pc2dvds	$⊢ (A \in ℤ \land B \in ℤ) \to (A ∥ B \leftrightarrow \forall p \in ℙ p pCnt A \leq p pCnt B)$

Proof

Step	Hyp	Ref	Expression
1		pcdvdstr	$⊢ (p \in ℙ \land (A \in ℤ \land B \in ℤ \land A ∥ B)) \to p pCnt A \leq p pCnt B$
2	1	ancoms	$⊢ ((A \in ℤ \land B \in ℤ \land A ∥ B) \land p \in ℙ) \to p pCnt A \leq p pCnt B$
3	2	ralrimiva	$⊢ (A \in ℤ \land B \in ℤ \land A ∥ B) \to \forall p \in ℙ p pCnt A \leq p pCnt B$
4	3	3expia	$⊢ (A \in ℤ \land B \in ℤ) \to (A ∥ B \to \forall p \in ℙ p pCnt A \leq p pCnt B)$
5		oveq2	$⊢ A = 0 \to p pCnt A = p pCnt 0$
6	5	breq1d	$⊢ A = 0 \to (p pCnt A \leq p pCnt B \leftrightarrow p pCnt 0 \leq p pCnt B)$
7	6	ralbidv	$⊢ A = 0 \to (\forall p \in ℙ p pCnt A \leq p pCnt B \leftrightarrow \forall p \in ℙ p pCnt 0 \leq p pCnt B)$
8		breq1	$⊢ A = 0 \to (A ∥ B \leftrightarrow 0 ∥ B)$
9	7 8	imbi12d	$⊢ A = 0 \to ((\forall p \in ℙ p pCnt A \leq p pCnt B \to A ∥ B) \leftrightarrow (\forall p \in ℙ p pCnt 0 \leq p pCnt B \to 0 ∥ B))$
10		gcddvds	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \land (A \gcd B) ∥ B)$
11	10	simpld	$⊢ (A \in ℤ \land B \in ℤ) \to (A \gcd B) ∥ A$
12		gcdcl	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B \in ℕ_{0}$
13	12	nn0zd	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B \in ℤ$
14		simpl	$⊢ (A \in ℤ \land B \in ℤ) \to A \in ℤ$
15		dvdsabsb	$⊢ (A \gcd B \in ℤ \land A \in ℤ) \to ((A \gcd B) ∥ A \leftrightarrow (A \gcd B) ∥ \|A\|)$
16	13 14 15	syl2anc	$⊢ (A \in ℤ \land B \in ℤ) \to ((A \gcd B) ∥ A \leftrightarrow (A \gcd B) ∥ \|A\|)$
17	11 16	mpbid	$⊢ (A \in ℤ \land B \in ℤ) \to (A \gcd B) ∥ \|A\|$
18	17	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (A \gcd B) ∥ \|A\|$
19		simpl	$⊢ (A = 0 \land B = 0) \to A = 0$
20	19	necon3ai	$⊢ A \neq 0 \to \neg (A = 0 \land B = 0)$
21		gcdn0cl	$⊢ ((A \in ℤ \land B \in ℤ) \land \neg (A = 0 \land B = 0)) \to A \gcd B \in ℕ$
22	20 21	sylan2	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to A \gcd B \in ℕ$
23	22	nnzd	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to A \gcd B \in ℤ$
24	22	nnne0d	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to A \gcd B \neq 0$
25		nnabscl	$⊢ (A \in ℤ \land A \neq 0) \to \|A\| \in ℕ$
26	25	adantlr	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to \|A\| \in ℕ$
27	26	nnzd	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to \|A\| \in ℤ$
28		dvdsval2	$⊢ (A \gcd B \in ℤ \land A \gcd B \neq 0 \land \|A\| \in ℤ) \to ((A \gcd B) ∥ \|A\| \leftrightarrow \frac{\|A\|}{A \gcd B} \in ℤ)$
29	23 24 27 28	syl3anc	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to ((A \gcd B) ∥ \|A\| \leftrightarrow \frac{\|A\|}{A \gcd B} \in ℤ)$
30	18 29	mpbid	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to \frac{\|A\|}{A \gcd B} \in ℤ$
31		nnre	$⊢ \|A\| \in ℕ \to \|A\| \in ℝ$
32		nngt0	$⊢ \|A\| \in ℕ \to 0 < \|A\|$
33	31 32	jca	$⊢ \|A\| \in ℕ \to (\|A\| \in ℝ \land 0 < \|A\|)$
34		nnre	$⊢ A \gcd B \in ℕ \to A \gcd B \in ℝ$
35		nngt0	$⊢ A \gcd B \in ℕ \to 0 < A \gcd B$
36	34 35	jca	$⊢ A \gcd B \in ℕ \to (A \gcd B \in ℝ \land 0 < A \gcd B)$
37		divgt0	$⊢ ((\|A\| \in ℝ \land 0 < \|A\|) \land (A \gcd B \in ℝ \land 0 < A \gcd B)) \to 0 < \frac{\|A\|}{A \gcd B}$
38	33 36 37	syl2an	$⊢ (\|A\| \in ℕ \land A \gcd B \in ℕ) \to 0 < \frac{\|A\|}{A \gcd B}$
39	26 22 38	syl2anc	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to 0 < \frac{\|A\|}{A \gcd B}$
40		elnnz	$⊢ \frac{\|A\|}{A \gcd B} \in ℕ \leftrightarrow (\frac{\|A\|}{A \gcd B} \in ℤ \land 0 < \frac{\|A\|}{A \gcd B})$
41	30 39 40	sylanbrc	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to \frac{\|A\|}{A \gcd B} \in ℕ$
42		elnn1uz2	$⊢ \frac{\|A\|}{A \gcd B} \in ℕ \leftrightarrow (\frac{\|A\|}{A \gcd B} = 1 \lor \frac{\|A\|}{A \gcd B} \in ℤ_{\geq 2})$
43	41 42	sylib	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (\frac{\|A\|}{A \gcd B} = 1 \lor \frac{\|A\|}{A \gcd B} \in ℤ_{\geq 2})$
44	10	simprd	$⊢ (A \in ℤ \land B \in ℤ) \to (A \gcd B) ∥ B$
45	44	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (A \gcd B) ∥ B$
46		breq1	$⊢ A \gcd B = \|A\| \to ((A \gcd B) ∥ B \leftrightarrow \|A\| ∥ B)$
47	45 46	syl5ibcom	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (A \gcd B = \|A\| \to \|A\| ∥ B)$
48	26	nncnd	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to \|A\| \in ℂ$
49	22	nncnd	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to A \gcd B \in ℂ$
50		1cnd	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to 1 \in ℂ$
51	48 49 50 24	divmuld	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (\frac{\|A\|}{A \gcd B} = 1 \leftrightarrow (A \gcd B) \cdot 1 = \|A\|)$
52	49	mulridd	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (A \gcd B) \cdot 1 = A \gcd B$
53	52	eqeq1d	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to ((A \gcd B) \cdot 1 = \|A\| \leftrightarrow A \gcd B = \|A\|)$
54	51 53	bitrd	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (\frac{\|A\|}{A \gcd B} = 1 \leftrightarrow A \gcd B = \|A\|)$
55		absdvdsb	$⊢ (A \in ℤ \land B \in ℤ) \to (A ∥ B \leftrightarrow \|A\| ∥ B)$
56	55	adantr	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (A ∥ B \leftrightarrow \|A\| ∥ B)$
57	47 54 56	3imtr4d	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (\frac{\|A\|}{A \gcd B} = 1 \to A ∥ B)$
58		exprmfct	$⊢ \frac{\|A\|}{A \gcd B} \in ℤ_{\geq 2} \to \exists p \in ℙ p ∥ (\frac{\|A\|}{A \gcd B})$
59		simprl	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p \in ℙ$
60	26	adantr	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \|A\| \in ℕ$
61	60	nnzd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \|A\| \in ℤ$
62	60	nnne0d	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \|A\| \neq 0$
63	22	adantr	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to A \gcd B \in ℕ$
64		pcdiv	$⊢ (p \in ℙ \land (\|A\| \in ℤ \land \|A\| \neq 0) \land A \gcd B \in ℕ) \to p pCnt (\frac{\|A\|}{A \gcd B}) = (p pCnt \|A\|) - (p pCnt (A \gcd B))$
65	59 61 62 63 64	syl121anc	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt (\frac{\|A\|}{A \gcd B}) = (p pCnt \|A\|) - (p pCnt (A \gcd B))$
66		simplll	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to A \in ℤ$
67		zq	$⊢ A \in ℤ \to A \in ℚ$
68	66 67	syl	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to A \in ℚ$
69		pcabs	$⊢ (p \in ℙ \land A \in ℚ) \to p pCnt \|A\| = p pCnt A$
70	59 68 69	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt \|A\| = p pCnt A$
71	70	oveq1d	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (p pCnt \|A\|) - (p pCnt (A \gcd B)) = (p pCnt A) - (p pCnt (A \gcd B))$
72	65 71	eqtrd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt (\frac{\|A\|}{A \gcd B}) = (p pCnt A) - (p pCnt (A \gcd B))$
73		simprr	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p ∥ (\frac{\|A\|}{A \gcd B})$
74	41	adantr	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \frac{\|A\|}{A \gcd B} \in ℕ$
75		pcelnn	$⊢ (p \in ℙ \land \frac{\|A\|}{A \gcd B} \in ℕ) \to (p pCnt (\frac{\|A\|}{A \gcd B}) \in ℕ \leftrightarrow p ∥ (\frac{\|A\|}{A \gcd B}))$
76	59 74 75	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (p pCnt (\frac{\|A\|}{A \gcd B}) \in ℕ \leftrightarrow p ∥ (\frac{\|A\|}{A \gcd B}))$
77	73 76	mpbird	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt (\frac{\|A\|}{A \gcd B}) \in ℕ$
78	72 77	eqeltrrd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (p pCnt A) - (p pCnt (A \gcd B)) \in ℕ$
79	59 63	pccld	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt (A \gcd B) \in ℕ_{0}$
80	79	nn0zd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt (A \gcd B) \in ℤ$
81		simplr	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to A \neq 0$
82		pczcl	$⊢ (p \in ℙ \land (A \in ℤ \land A \neq 0)) \to p pCnt A \in ℕ_{0}$
83	59 66 81 82	syl12anc	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt A \in ℕ_{0}$
84	83	nn0zd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt A \in ℤ$
85		znnsub	$⊢ (p pCnt (A \gcd B) \in ℤ \land p pCnt A \in ℤ) \to (p pCnt (A \gcd B) < p pCnt A \leftrightarrow (p pCnt A) - (p pCnt (A \gcd B)) \in ℕ)$
86	80 84 85	syl2anc	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (p pCnt (A \gcd B) < p pCnt A \leftrightarrow (p pCnt A) - (p pCnt (A \gcd B)) \in ℕ)$
87	78 86	mpbird	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt (A \gcd B) < p pCnt A$
88	79	nn0red	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt (A \gcd B) \in ℝ$
89	83	nn0red	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt A \in ℝ$
90	88 89	ltnled	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (p pCnt (A \gcd B) < p pCnt A \leftrightarrow \neg p pCnt A \leq p pCnt (A \gcd B))$
91	87 90	mpbid	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \neg p pCnt A \leq p pCnt (A \gcd B)$
92		simpllr	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to B \in ℤ$
93		nprmdvds1	$⊢ p \in ℙ \to \neg p ∥ 1$
94	93	ad2antrl	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \neg p ∥ 1$
95		gcdid0	$⊢ A \in ℤ \to A \gcd 0 = \|A\|$
96	66 95	syl	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to A \gcd 0 = \|A\|$
97	96	oveq2d	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \frac{\|A\|}{A \gcd 0} = \frac{\|A\|}{\|A\|}$
98	48	adantr	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \|A\| \in ℂ$
99	98 62	dividd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \frac{\|A\|}{\|A\|} = 1$
100	97 99	eqtrd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \frac{\|A\|}{A \gcd 0} = 1$
101	100	breq2d	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (p ∥ (\frac{\|A\|}{A \gcd 0}) \leftrightarrow p ∥ 1)$
102	94 101	mtbird	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \neg p ∥ (\frac{\|A\|}{A \gcd 0})$
103		oveq2	$⊢ B = 0 \to A \gcd B = A \gcd 0$
104	103	oveq2d	$⊢ B = 0 \to \frac{\|A\|}{A \gcd B} = \frac{\|A\|}{A \gcd 0}$
105	104	breq2d	$⊢ B = 0 \to (p ∥ (\frac{\|A\|}{A \gcd B}) \leftrightarrow p ∥ (\frac{\|A\|}{A \gcd 0}))$
106	73 105	syl5ibcom	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (B = 0 \to p ∥ (\frac{\|A\|}{A \gcd 0}))$
107	106	necon3bd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (\neg p ∥ (\frac{\|A\|}{A \gcd 0}) \to B \neq 0)$
108	102 107	mpd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to B \neq 0$
109		pczcl	$⊢ (p \in ℙ \land (B \in ℤ \land B \neq 0)) \to p pCnt B \in ℕ_{0}$
110	59 92 108 109	syl12anc	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt B \in ℕ_{0}$
111	110	nn0red	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt B \in ℝ$
112		lemin	$⊢ (p pCnt A \in ℝ \land p pCnt A \in ℝ \land p pCnt B \in ℝ) \to (p pCnt A \leq if (p pCnt A \leq p pCnt B, p pCnt A, p pCnt B) \leftrightarrow (p pCnt A \leq p pCnt A \land p pCnt A \leq p pCnt B))$
113	89 89 111 112	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (p pCnt A \leq if (p pCnt A \leq p pCnt B, p pCnt A, p pCnt B) \leftrightarrow (p pCnt A \leq p pCnt A \land p pCnt A \leq p pCnt B))$
114		pcgcd	$⊢ (p \in ℙ \land A \in ℤ \land B \in ℤ) \to p pCnt (A \gcd B) = if (p pCnt A \leq p pCnt B, p pCnt A, p pCnt B)$
115	59 66 92 114	syl3anc	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt (A \gcd B) = if (p pCnt A \leq p pCnt B, p pCnt A, p pCnt B)$
116	115	breq2d	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (p pCnt A \leq p pCnt (A \gcd B) \leftrightarrow p pCnt A \leq if (p pCnt A \leq p pCnt B, p pCnt A, p pCnt B))$
117	89	leidd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to p pCnt A \leq p pCnt A$
118	117	biantrurd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (p pCnt A \leq p pCnt B \leftrightarrow (p pCnt A \leq p pCnt A \land p pCnt A \leq p pCnt B))$
119	113 116 118	3bitr4rd	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to (p pCnt A \leq p pCnt B \leftrightarrow p pCnt A \leq p pCnt (A \gcd B))$
120	91 119	mtbird	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land (p \in ℙ \land p ∥ (\frac{\|A\|}{A \gcd B}))) \to \neg p pCnt A \leq p pCnt B$
121	120	expr	$⊢ (((A \in ℤ \land B \in ℤ) \land A \neq 0) \land p \in ℙ) \to (p ∥ (\frac{\|A\|}{A \gcd B}) \to \neg p pCnt A \leq p pCnt B)$
122	121	reximdva	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (\exists p \in ℙ p ∥ (\frac{\|A\|}{A \gcd B}) \to \exists p \in ℙ \neg p pCnt A \leq p pCnt B)$
123		rexnal	$⊢ \exists p \in ℙ \neg p pCnt A \leq p pCnt B \leftrightarrow \neg \forall p \in ℙ p pCnt A \leq p pCnt B$
124	122 123	imbitrdi	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (\exists p \in ℙ p ∥ (\frac{\|A\|}{A \gcd B}) \to \neg \forall p \in ℙ p pCnt A \leq p pCnt B)$
125	58 124	syl5	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (\frac{\|A\|}{A \gcd B} \in ℤ_{\geq 2} \to \neg \forall p \in ℙ p pCnt A \leq p pCnt B)$
126	57 125	orim12d	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to ((\frac{\|A\|}{A \gcd B} = 1 \lor \frac{\|A\|}{A \gcd B} \in ℤ_{\geq 2}) \to (A ∥ B \lor \neg \forall p \in ℙ p pCnt A \leq p pCnt B))$
127	43 126	mpd	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (A ∥ B \lor \neg \forall p \in ℙ p pCnt A \leq p pCnt B)$
128	127	ord	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (\neg A ∥ B \to \neg \forall p \in ℙ p pCnt A \leq p pCnt B)$
129	128	con4d	$⊢ ((A \in ℤ \land B \in ℤ) \land A \neq 0) \to (\forall p \in ℙ p pCnt A \leq p pCnt B \to A ∥ B)$
130		2prm	$⊢ 2 \in ℙ$
131	130	ne0ii	$⊢ ℙ \neq \emptyset$
132		r19.2z	$⊢ (ℙ \neq \emptyset \land \forall p \in ℙ p pCnt 0 \leq p pCnt B) \to \exists p \in ℙ p pCnt 0 \leq p pCnt B$
133	131 132	mpan	$⊢ \forall p \in ℙ p pCnt 0 \leq p pCnt B \to \exists p \in ℙ p pCnt 0 \leq p pCnt B$
134		id	$⊢ p \in ℙ \to p \in ℙ$
135		zq	$⊢ B \in ℤ \to B \in ℚ$
136	135	adantl	$⊢ (A \in ℤ \land B \in ℤ) \to B \in ℚ$
137		pcxcl	$⊢ (p \in ℙ \land B \in ℚ) \to p pCnt B \in ℝ^{*}$
138	134 136 137	syl2anr	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to p pCnt B \in ℝ^{*}$
139		pnfge	$⊢ p pCnt B \in ℝ^{*} \to p pCnt B \leq +∞$
140	138 139	syl	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to p pCnt B \leq +∞$
141	140	biantrurd	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to (+∞ \leq p pCnt B \leftrightarrow (p pCnt B \leq +∞ \land +∞ \leq p pCnt B))$
142		pc0	$⊢ p \in ℙ \to p pCnt 0 = +∞$
143	142	adantl	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to p pCnt 0 = +∞$
144	143	breq1d	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to (p pCnt 0 \leq p pCnt B \leftrightarrow +∞ \leq p pCnt B)$
145		pnfxr	$⊢ +∞ \in ℝ^{*}$
146		xrletri3	$⊢ (p pCnt B \in ℝ^{} \land +∞ \in ℝ^{}) \to (p pCnt B = +∞ \leftrightarrow (p pCnt B \leq +∞ \land +∞ \leq p pCnt B))$
147	138 145 146	sylancl	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to (p pCnt B = +∞ \leftrightarrow (p pCnt B \leq +∞ \land +∞ \leq p pCnt B))$
148	141 144 147	3bitr4d	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to (p pCnt 0 \leq p pCnt B \leftrightarrow p pCnt B = +∞)$
149		pnfnre	$⊢ +∞ \notin ℝ$
150	149	neli	$⊢ \neg +∞ \in ℝ$
151		eleq1	$⊢ p pCnt B = +∞ \to (p pCnt B \in ℝ \leftrightarrow +∞ \in ℝ)$
152	150 151	mtbiri	$⊢ p pCnt B = +∞ \to \neg p pCnt B \in ℝ$
153	109	nn0red	$⊢ (p \in ℙ \land (B \in ℤ \land B \neq 0)) \to p pCnt B \in ℝ$
154	153	adantll	$⊢ ((A \in ℤ \land p \in ℙ) \land (B \in ℤ \land B \neq 0)) \to p pCnt B \in ℝ$
155	154	an4s	$⊢ ((A \in ℤ \land B \in ℤ) \land (p \in ℙ \land B \neq 0)) \to p pCnt B \in ℝ$
156	155	expr	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to (B \neq 0 \to p pCnt B \in ℝ)$
157	156	necon1bd	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to (\neg p pCnt B \in ℝ \to B = 0)$
158	152 157	syl5	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to (p pCnt B = +∞ \to B = 0)$
159	148 158	sylbid	$⊢ ((A \in ℤ \land B \in ℤ) \land p \in ℙ) \to (p pCnt 0 \leq p pCnt B \to B = 0)$
160	159	rexlimdva	$⊢ (A \in ℤ \land B \in ℤ) \to (\exists p \in ℙ p pCnt 0 \leq p pCnt B \to B = 0)$
161		0dvds	$⊢ B \in ℤ \to (0 ∥ B \leftrightarrow B = 0)$
162	161	adantl	$⊢ (A \in ℤ \land B \in ℤ) \to (0 ∥ B \leftrightarrow B = 0)$
163	160 162	sylibrd	$⊢ (A \in ℤ \land B \in ℤ) \to (\exists p \in ℙ p pCnt 0 \leq p pCnt B \to 0 ∥ B)$
164	133 163	syl5	$⊢ (A \in ℤ \land B \in ℤ) \to (\forall p \in ℙ p pCnt 0 \leq p pCnt B \to 0 ∥ B)$
165	9 129 164	pm2.61ne	$⊢ (A \in ℤ \land B \in ℤ) \to (\forall p \in ℙ p pCnt A \leq p pCnt B \to A ∥ B)$
166	4 165	impbid	$⊢ (A \in ℤ \land B \in ℤ) \to (A ∥ B \leftrightarrow \forall p \in ℙ p pCnt A \leq p pCnt B)$

Metamath Proof Explorer

Theorem pc2dvds

Proof