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 ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝑃 pCnt ( 𝐴 gcd 𝐵 ) ) = if ( ( 𝑃 pCnt 𝐴 ) ≤ ( 𝑃 pCnt 𝐵 ) , ( 𝑃 pCnt 𝐴 ) , ( 𝑃 pCnt 𝐵 ) ) )

Proof

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