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 
|- ( ph -> N e. NN )
aks4d1p8d3.2 
|- ( ph -> P e. Prime )
aks4d1p8d3.3 
|- ( ph -> P || N )
Assertion aks4d1p8d3 
|- ( ph -> ( ( N / ( P ^ ( P pCnt N ) ) ) gcd ( P ^ ( P pCnt N ) ) ) = 1 )

Proof

Step Hyp Ref Expression
1 aks4d1p8d3.1 
 |-  ( ph -> N e. NN )
2 aks4d1p8d3.2 
 |-  ( ph -> P e. Prime )
3 aks4d1p8d3.3 
 |-  ( ph -> P || N )
4 pcdvds 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( P ^ ( P pCnt N ) ) || N )
5 2 1 4 syl2anc 
 |-  ( ph -> ( P ^ ( P pCnt N ) ) || N )
6 prmnn 
 |-  ( P e. Prime -> P e. NN )
7 2 6 syl 
 |-  ( ph -> P e. NN )
8 7 nnzd 
 |-  ( ph -> P e. ZZ )
9 2 1 pccld 
 |-  ( ph -> ( P pCnt N ) e. NN0 )
10 8 9 zexpcld 
 |-  ( ph -> ( P ^ ( P pCnt N ) ) e. ZZ )
11 8 zcnd 
 |-  ( ph -> P e. CC )
12 0red 
 |-  ( ph -> 0 e. RR )
13 1red 
 |-  ( ph -> 1 e. RR )
14 8 zred 
 |-  ( ph -> P e. RR )
15 0lt1 
 |-  0 < 1
16 15 a1i 
 |-  ( ph -> 0 < 1 )
17 prmgt1 
 |-  ( P e. Prime -> 1 < P )
18 2 17 syl 
 |-  ( ph -> 1 < P )
19 12 13 14 16 18 lttrd 
 |-  ( ph -> 0 < P )
20 12 19 ltned 
 |-  ( ph -> 0 =/= P )
21 20 necomd 
 |-  ( ph -> P =/= 0 )
22 9 nn0zd 
 |-  ( ph -> ( P pCnt N ) e. ZZ )
23 11 21 22 expne0d 
 |-  ( ph -> ( P ^ ( P pCnt N ) ) =/= 0 )
24 1 nnzd 
 |-  ( ph -> N e. ZZ )
25 dvdsval2 
 |-  ( ( ( P ^ ( P pCnt N ) ) e. ZZ /\ ( P ^ ( P pCnt N ) ) =/= 0 /\ N e. ZZ ) -> ( ( P ^ ( P pCnt N ) ) || N <-> ( N / ( P ^ ( P pCnt N ) ) ) e. ZZ ) )
26 10 23 24 25 syl3anc 
 |-  ( ph -> ( ( P ^ ( P pCnt N ) ) || N <-> ( N / ( P ^ ( P pCnt N ) ) ) e. ZZ ) )
27 5 26 mpbid 
 |-  ( ph -> ( N / ( P ^ ( P pCnt N ) ) ) e. ZZ )
28 27 10 gcdcomd 
 |-  ( ph -> ( ( N / ( P ^ ( P pCnt N ) ) ) gcd ( P ^ ( P pCnt N ) ) ) = ( ( P ^ ( P pCnt N ) ) gcd ( N / ( P ^ ( P pCnt N ) ) ) ) )
29 pcndvds2 
 |-  ( ( P e. Prime /\ N e. NN ) -> -. P || ( N / ( P ^ ( P pCnt N ) ) ) )
30 2 1 29 syl2anc 
 |-  ( ph -> -. P || ( N / ( P ^ ( P pCnt N ) ) ) )
31 coprm 
 |-  ( ( P e. Prime /\ ( N / ( P ^ ( P pCnt N ) ) ) e. ZZ ) -> ( -. P || ( N / ( P ^ ( P pCnt N ) ) ) <-> ( P gcd ( N / ( P ^ ( P pCnt N ) ) ) ) = 1 ) )
32 2 27 31 syl2anc 
 |-  ( ph -> ( -. P || ( N / ( P ^ ( P pCnt N ) ) ) <-> ( P gcd ( N / ( P ^ ( P pCnt N ) ) ) ) = 1 ) )
33 30 32 mpbid 
 |-  ( ph -> ( P gcd ( N / ( P ^ ( P pCnt N ) ) ) ) = 1 )
34 pcelnn 
 |-  ( ( P e. Prime /\ N e. NN ) -> ( ( P pCnt N ) e. NN <-> P || N ) )
35 2 1 34 syl2anc 
 |-  ( ph -> ( ( P pCnt N ) e. NN <-> P || N ) )
36 3 35 mpbird 
 |-  ( ph -> ( P pCnt N ) e. NN )
37 rpexp 
 |-  ( ( P e. ZZ /\ ( N / ( P ^ ( P pCnt N ) ) ) e. ZZ /\ ( P pCnt N ) e. NN ) -> ( ( ( P ^ ( P pCnt N ) ) gcd ( N / ( P ^ ( P pCnt N ) ) ) ) = 1 <-> ( P gcd ( N / ( P ^ ( P pCnt N ) ) ) ) = 1 ) )
38 8 27 36 37 syl3anc 
 |-  ( ph -> ( ( ( P ^ ( P pCnt N ) ) gcd ( N / ( P ^ ( P pCnt N ) ) ) ) = 1 <-> ( P gcd ( N / ( P ^ ( P pCnt N ) ) ) ) = 1 ) )
39 33 38 mpbird 
 |-  ( ph -> ( ( P ^ ( P pCnt N ) ) gcd ( N / ( P ^ ( P pCnt N ) ) ) ) = 1 )
40 28 39 eqtrd 
 |-  ( ph -> ( ( N / ( P ^ ( P pCnt N ) ) ) gcd ( P ^ ( P pCnt N ) ) ) = 1 )