Metamath Proof Explorer

Theorem pcgcd

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

Proof

Step Hyp Ref Expression
1 pcgcd1 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ P pCnt A ≤ P pCnt B → P pCnt A gcd B = P pCnt A
2 iftrue ⊢ P pCnt A ≤ P pCnt B → if P pCnt A ≤ P pCnt B P pCnt A P pCnt B = P pCnt A
3 2 adantl ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ P pCnt A ≤ P pCnt B → if P pCnt A ≤ P pCnt B P pCnt A P pCnt B = P pCnt A
4 1 3 eqtr4d ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ P pCnt A ≤ P pCnt B → P pCnt A gcd B = if P pCnt A ≤ P pCnt B P pCnt A P pCnt B
5 gcdcom ⊢ A ∈ ℤ ∧ B ∈ ℤ → A gcd B = B gcd A
6 5 3adant1 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ → A gcd B = B gcd A
7 6 adantr ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ P pCnt A ≤ P pCnt B → A gcd B = B gcd A
8 7 oveq2d ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ P pCnt A ≤ P pCnt B → P pCnt A gcd B = P pCnt B gcd A
9 iffalse ⊢ ¬ P pCnt A ≤ P pCnt B → if P pCnt A ≤ P pCnt B P pCnt A P pCnt B = P pCnt B
10 9 adantl ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ P pCnt A ≤ P pCnt B → if P pCnt A ≤ P pCnt B P pCnt A P pCnt B = P pCnt B
11 zq ⊢ A ∈ ℤ → A ∈ ℚ
12 pcxcl ⊢ P ∈ ℙ ∧ A ∈ ℚ → P pCnt A ∈ ℝ *
13 11 12 sylan2 ⊢ P ∈ ℙ ∧ A ∈ ℤ → P pCnt A ∈ ℝ *
14 13 3adant3 ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ → P pCnt A ∈ ℝ *
15 zq ⊢ B ∈ ℤ → B ∈ ℚ
16 pcxcl ⊢ P ∈ ℙ ∧ B ∈ ℚ → P pCnt B ∈ ℝ *
17 15 16 sylan2 ⊢ P ∈ ℙ ∧ B ∈ ℤ → P pCnt B ∈ ℝ *
18 xrletri ⊢ P pCnt A ∈ ℝ * ∧ P pCnt B ∈ ℝ * → P pCnt A ≤ P pCnt B ∨ P pCnt B ≤ P pCnt A
19 14 17 18 3imp3i2an ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ → P pCnt A ≤ P pCnt B ∨ P pCnt B ≤ P pCnt A
20 19 orcanai ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ P pCnt A ≤ P pCnt B → P pCnt B ≤ P pCnt A
21 3ancomb ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ↔ P ∈ ℙ ∧ B ∈ ℤ ∧ A ∈ ℤ
22 pcgcd1 ⊢ P ∈ ℙ ∧ B ∈ ℤ ∧ A ∈ ℤ ∧ P pCnt B ≤ P pCnt A → P pCnt B gcd A = P pCnt B
23 21 22 sylanb ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ P pCnt B ≤ P pCnt A → P pCnt B gcd A = P pCnt B
24 20 23 syldan ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ P pCnt A ≤ P pCnt B → P pCnt B gcd A = P pCnt B
25 10 24 eqtr4d ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ P pCnt A ≤ P pCnt B → if P pCnt A ≤ P pCnt B P pCnt A P pCnt B = P pCnt B gcd A
26 8 25 eqtr4d ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ ∧ ¬ P pCnt A ≤ P pCnt B → P pCnt A gcd B = if P pCnt A ≤ P pCnt B P pCnt A P pCnt B
27 4 26 pm2.61dan ⊢ P ∈ ℙ ∧ A ∈ ℤ ∧ B ∈ ℤ → P pCnt A gcd B = if P pCnt A ≤ P pCnt B P pCnt A P pCnt B