This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) ) )