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 )