Metamath Proof Explorer

Theorem pcgcd1

Description: The prime count of a GCD is the minimum of the prime counts of the arguments. (Contributed by Mario Carneiro, 3-Oct-2014)

Ref Expression
Assertion pcgcd1 ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ) → ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) = ( 𝑃 pCnt 𝐴 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝐵 = 0 → ( 𝐴 gcd 𝐵 ) = ( 𝐴 gcd 0 ) )
2 1 oveq2d ⊢ ( 𝐵 = 0 → ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) = ( 𝑃 pCnt ( 𝐴 gcd 0 ) ) )
3 2 eqeq1d ⊢ ( 𝐵 = 0 → ( ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) = ( 𝑃 pCnt 𝐴 ) ↔ ( 𝑃 pCnt ( 𝐴 gcd 0 ) ) = ( 𝑃 pCnt 𝐴 ) ) )
4 simpl1 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → 𝑃 ∈ ℙ )
5 simp2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → 𝐴 ∈ ℤ )
6 5 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℤ )
7 simpl3 ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ℤ )
8 simprr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
9 simpr ⊢ ( ( 𝐴 = 0 ∧ 𝐵 = 0 ) → 𝐵 = 0 )
10 9 necon3ai ⊢ ( 𝐵 ≠ 0 → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
11 8 10 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) )
12 gcdn0cl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ¬ ( 𝐴 = 0 ∧ 𝐵 = 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
13 6 7 11 12 syl21anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ )
14 13 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 gcd 𝐵 ) ∈ ℤ )
15 gcddvds ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
16 6 7 15 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐵 ) )
17 16 simpld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 gcd 𝐵 ) ∥ 𝐴 )
18 pcdvdstr ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 𝐵 ) ∥ 𝐴 ) ) → ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) ≤ ( 𝑃 pCnt 𝐴 ) )
19 4 14 6 17 18 syl13anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) ≤ ( 𝑃 pCnt 𝐴 ) )
20 zq ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℚ )
21 6 20 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ ℚ )
22 pcxcl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( 𝑃 pCnt 𝐴 ) ∈ ℝ* )
23 4 21 22 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℝ* )
24 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐵 ) ∈ ℕ0 )
25 4 7 8 24 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐵 ) ∈ ℕ0 )
26 25 nn0red ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐵 ) ∈ ℝ )
27 pcge0 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → 0 ≤ ( 𝑃 pCnt 𝐴 ) )
28 4 6 27 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → 0 ≤ ( 𝑃 pCnt 𝐴 ) )
29 ge0gtmnf ⊢ ( ( ( 𝑃 pCnt 𝐴 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 pCnt 𝐴 ) ) → -∞ < ( 𝑃 pCnt 𝐴 ) )
30 23 28 29 syl2anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → -∞ < ( 𝑃 pCnt 𝐴 ) )
31 simprl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) )
32 xrre ⊢ ( ( ( ( 𝑃 pCnt 𝐴 ) ∈ ℝ* ∧ ( 𝑃 pCnt 𝐵 ) ∈ ℝ ) ∧ ( -∞ < ( 𝑃 pCnt 𝐴 ) ∧ ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℝ )
33 23 26 30 31 32 syl22anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℝ )
34 pnfnre ⊢ +∞ ∉ ℝ
35 34 neli ⊢ ¬ +∞ ∈ ℝ
36 pc0 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 pCnt 0 ) = +∞ )
37 4 36 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 0 ) = +∞ )
38 37 eleq1d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑃 pCnt 0 ) ∈ ℝ ↔ +∞ ∈ ℝ ) )
39 35 38 mtbiri ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ¬ ( 𝑃 pCnt 0 ) ∈ ℝ )
40 oveq2 ⊢ ( 𝐴 = 0 → ( 𝑃 pCnt 𝐴 ) = ( 𝑃 pCnt 0 ) )
41 40 eleq1d ⊢ ( 𝐴 = 0 → ( ( 𝑃 pCnt 𝐴 ) ∈ ℝ ↔ ( 𝑃 pCnt 0 ) ∈ ℝ ) )
42 41 notbid ⊢ ( 𝐴 = 0 → ( ¬ ( 𝑃 pCnt 𝐴 ) ∈ ℝ ↔ ¬ ( 𝑃 pCnt 0 ) ∈ ℝ ) )
43 39 42 syl5ibrcom ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 = 0 → ¬ ( 𝑃 pCnt 𝐴 ) ∈ ℝ ) )
44 43 necon2ad ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑃 pCnt 𝐴 ) ∈ ℝ → 𝐴 ≠ 0 ) )
45 33 44 mpd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → 𝐴 ≠ 0 )
46 pczdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
47 4 6 45 46 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 )
48 pczcl ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
49 4 6 45 48 syl12anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 )
50 pcdvdsb ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐵 ∈ ℤ ∧ ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 ) → ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 ) )
51 4 7 49 50 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 ) )
52 31 51 mpbid ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 )
53 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
54 4 53 syl ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → 𝑃 ∈ ℕ )
55 54 49 nnexpcld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℕ )
56 55 nnzd ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℤ )
57 dvdsgcd ⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝐴 gcd 𝐵 ) ) )
58 56 6 7 57 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐴 ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ 𝐵 ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝐴 gcd 𝐵 ) ) )
59 47 52 58 mp2and ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝐴 gcd 𝐵 ) )
60 pcdvdsb ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝐴 gcd 𝐵 ) ∈ ℤ ∧ ( 𝑃 pCnt 𝐴 ) ∈ ℕ0 ) → ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝐴 gcd 𝐵 ) ) )
61 4 14 49 60 syl3anc ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) ↔ ( 𝑃 ↑ ( 𝑃 pCnt 𝐴 ) ) ∥ ( 𝐴 gcd 𝐵 ) ) )
62 59 61 mpbird ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) )
63 4 13 pccld ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) ∈ ℕ0 )
64 63 nn0red ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) ∈ ℝ )
65 64 33 letri3d ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) = ( 𝑃 pCnt 𝐴 ) ↔ ( ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) ≤ ( 𝑃 pCnt 𝐴 ) ∧ ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) ) ) )
66 19 62 65 mpbir2and ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ∧ 𝐵 ≠ 0 ) ) → ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) = ( 𝑃 pCnt 𝐴 ) )
67 66 anassrs ⊢ ( ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ) ∧ 𝐵 ≠ 0 ) → ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) = ( 𝑃 pCnt 𝐴 ) )
68 gcdid0 ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 gcd 0 ) = ( abs ‘ 𝐴 ) )
69 5 68 syl ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 0 ) = ( abs ‘ 𝐴 ) )
70 69 oveq2d ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑃 pCnt ( 𝐴 gcd 0 ) ) = ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) )
71 pcabs ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ ) → ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) = ( 𝑃 pCnt 𝐴 ) )
72 20 71 sylan2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) = ( 𝑃 pCnt 𝐴 ) )
73 72 3adant3 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑃 pCnt ( abs ‘ 𝐴 ) ) = ( 𝑃 pCnt 𝐴 ) )
74 70 73 eqtrd ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑃 pCnt ( 𝐴 gcd 0 ) ) = ( 𝑃 pCnt 𝐴 ) )
75 74 adantr ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ) → ( 𝑃 pCnt ( 𝐴 gcd 0 ) ) = ( 𝑃 pCnt 𝐴 ) )
76 3 67 75 pm2.61ne ⊢ ( ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) ) → ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) = ( 𝑃 pCnt 𝐴 ) )