Metamath Proof Explorer

Theorem aks4d1p8d3

Description: The remainder of a division with its maximal prime power is coprime with that prime power. (Contributed by metakunt, 13-Nov-2024)

Ref Expression
Hypotheses aks4d1p8d3.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
aks4d1p8d3.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
aks4d1p8d3.3 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
Assertion aks4d1p8d3 ( 𝜑 → ( ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) gcd ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = 1 )

Proof

Step Hyp Ref Expression
1 aks4d1p8d3.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2 aks4d1p8d3.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
3 aks4d1p8d3.3 ⊢ ( 𝜑 → 𝑃 ∥ 𝑁 )
4 pcdvds ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 )
5 2 1 4 syl2anc ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 )
6 prmnn ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
7 2 6 syl ⊢ ( 𝜑 → 𝑃 ∈ ℕ )
8 7 nnzd ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
9 2 1 pccld ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ0 )
10 8 9 zexpcld ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℤ )
11 8 zcnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
12 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
13 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
14 8 zred ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
15 0lt1 ⊢ 0 < 1
16 15 a1i ⊢ ( 𝜑 → 0 < 1 )
17 prmgt1 ⊢ ( 𝑃 ∈ ℙ → 1 < 𝑃 )
18 2 17 syl ⊢ ( 𝜑 → 1 < 𝑃 )
19 12 13 14 16 18 lttrd ⊢ ( 𝜑 → 0 < 𝑃 )
20 12 19 ltned ⊢ ( 𝜑 → 0 ≠ 𝑃 )
21 20 necomd ⊢ ( 𝜑 → 𝑃 ≠ 0 )
22 9 nn0zd ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℤ )
23 11 21 22 expne0d ⊢ ( 𝜑 → ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ≠ 0 )
24 1 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
25 dvdsval2 ⊢ ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∈ ℤ ∧ ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ≠ 0 ∧ 𝑁 ∈ ℤ ) → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ∈ ℤ ) )
26 10 23 24 25 syl3anc ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ∥ 𝑁 ↔ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ∈ ℤ ) )
27 5 26 mpbid ⊢ ( 𝜑 → ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ∈ ℤ )
28 27 10 gcdcomd ⊢ ( 𝜑 → ( ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) gcd ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) )
29 pcndvds2 ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
30 2 1 29 syl2anc ⊢ ( 𝜑 → ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) )
31 coprm ⊢ ( ( 𝑃 ∈ ℙ ∧ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ∈ ℤ ) → ( ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ↔ ( 𝑃 gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ) )
32 2 27 31 syl2anc ⊢ ( 𝜑 → ( ¬ 𝑃 ∥ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ↔ ( 𝑃 gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ) )
33 30 32 mpbid ⊢ ( 𝜑 → ( 𝑃 gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 )
34 pcelnn ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ ) → ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ ↔ 𝑃 ∥ 𝑁 ) )
35 2 1 34 syl2anc ⊢ ( 𝜑 → ( ( 𝑃 pCnt 𝑁 ) ∈ ℕ ↔ 𝑃 ∥ 𝑁 ) )
36 3 35 mpbird ⊢ ( 𝜑 → ( 𝑃 pCnt 𝑁 ) ∈ ℕ )
37 rpexp ⊢ ( ( 𝑃 ∈ ℤ ∧ ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ∈ ℤ ∧ ( 𝑃 pCnt 𝑁 ) ∈ ℕ ) → ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ↔ ( 𝑃 gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ) )
38 8 27 36 37 syl3anc ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ↔ ( 𝑃 gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 ) )
39 33 38 mpbird ⊢ ( 𝜑 → ( ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) gcd ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) ) = 1 )
40 28 39 eqtrd ⊢ ( 𝜑 → ( ( 𝑁 / ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) gcd ( 𝑃 ↑ ( 𝑃 pCnt 𝑁 ) ) ) = 1 )