Theorem 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	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 ∥ 𝐵 ↔ ∀ 𝑝 ∈ ℙ ( 𝑝 pCnt 𝐴 ) ≤ ( 𝑝 pCnt 𝐵 ) ) )

Proof

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