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 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ P pCnt A ≤ P pCnt B → P pCnt A gcd B = P pCnt A

Proof

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