Metamath Proof Explorer

Theorem primrootspoweq0

Description: The power of a R -th primitive root is zero if and only if it divides R . (Contributed by metakunt, 15-May-2025)

Ref Expression
Hypotheses primrootspoweq0.1 
|- ( ph -> R e. CMnd )
primrootspoweq0.2 
|- ( ph -> K e. NN )
primrootspoweq0.3 
|- ( ph -> M e. ( R PrimRoots K ) )
primrootspoweq0.4 
|- U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
primrootspoweq0.5 
|- ( ph -> N e. ZZ )
Assertion primrootspoweq0 
|- ( ph -> ( ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) <-> K || N ) )

Proof

Step Hyp Ref Expression
1 primrootspoweq0.1 
 |-  ( ph -> R e. CMnd )
2 primrootspoweq0.2 
 |-  ( ph -> K e. NN )
3 primrootspoweq0.3 
 |-  ( ph -> M e. ( R PrimRoots K ) )
4 primrootspoweq0.4 
 |-  U = { a e. ( Base ` R ) | E. i e. ( Base ` R ) ( i ( +g ` R ) a ) = ( 0g ` R ) }
5 primrootspoweq0.5 
 |-  ( ph -> N e. ZZ )
6 simplr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> N = ( ( x x. K ) + y ) )
7 6 oveq1d 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( N ( .g ` ( R |`s U ) ) M ) = ( ( ( x x. K ) + y ) ( .g ` ( R |`s U ) ) M ) )
8 1 2 4 primrootsunit 
 |-  ( ph -> ( ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) /\ ( R |`s U ) e. Abel ) )
9 8 simprd 
 |-  ( ph -> ( R |`s U ) e. Abel )
10 9 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( R |`s U ) e. Abel )
11 10 ablgrpd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( R |`s U ) e. Grp )
12 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> x e. ZZ )
13 2 nnzd 
 |-  ( ph -> K e. ZZ )
14 13 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> K e. ZZ )
15 12 14 zmulcld 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( x x. K ) e. ZZ )
16 simpllr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> y e. ( 0 ... ( K - 1 ) ) )
17 16 elfzelzd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> y e. ZZ )
18 8 simpld 
 |-  ( ph -> ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) )
19 3 18 eleqtrd 
 |-  ( ph -> M e. ( ( R |`s U ) PrimRoots K ) )
20 ablcmn 
 |-  ( ( R |`s U ) e. Abel -> ( R |`s U ) e. CMnd )
21 9 20 syl 
 |-  ( ph -> ( R |`s U ) e. CMnd )
22 2 nnnn0d 
 |-  ( ph -> K e. NN0 )
23 eqid 
 |-  ( .g ` ( R |`s U ) ) = ( .g ` ( R |`s U ) )
24 21 22 23 isprimroot 
 |-  ( ph -> ( M e. ( ( R |`s U ) PrimRoots K ) <-> ( M e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
25 24 biimpd 
 |-  ( ph -> ( M e. ( ( R |`s U ) PrimRoots K ) -> ( M e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) ) )
26 19 25 mpd 
 |-  ( ph -> ( M e. ( Base ` ( R |`s U ) ) /\ ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) /\ A. l e. NN0 ( ( l ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || l ) ) )
27 26 simp1d 
 |-  ( ph -> M e. ( Base ` ( R |`s U ) ) )
28 27 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> M e. ( Base ` ( R |`s U ) ) )
29 15 17 28 3jca 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( x x. K ) e. ZZ /\ y e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) )
30 eqid 
 |-  ( Base ` ( R |`s U ) ) = ( Base ` ( R |`s U ) )
31 eqid 
 |-  ( +g ` ( R |`s U ) ) = ( +g ` ( R |`s U ) )
32 30 23 31 mulgdir 
 |-  ( ( ( R |`s U ) e. Grp /\ ( ( x x. K ) e. ZZ /\ y e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) ) -> ( ( ( x x. K ) + y ) ( .g ` ( R |`s U ) ) M ) = ( ( ( x x. K ) ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( y ( .g ` ( R |`s U ) ) M ) ) )
33 11 29 32 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( ( x x. K ) + y ) ( .g ` ( R |`s U ) ) M ) = ( ( ( x x. K ) ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( y ( .g ` ( R |`s U ) ) M ) ) )
34 12 14 28 3jca 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( x e. ZZ /\ K e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) )
35 30 23 mulgass 
 |-  ( ( ( R |`s U ) e. Grp /\ ( x e. ZZ /\ K e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) ) -> ( ( x x. K ) ( .g ` ( R |`s U ) ) M ) = ( x ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) )
36 11 34 35 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( x x. K ) ( .g ` ( R |`s U ) ) M ) = ( x ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) )
37 26 simp2d 
 |-  ( ph -> ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
38 37 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
39 38 oveq2d 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( x ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) = ( x ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) )
40 eqid 
 |-  ( 0g ` ( R |`s U ) ) = ( 0g ` ( R |`s U ) )
41 30 23 40 mulgz 
 |-  ( ( ( R |`s U ) e. Grp /\ x e. ZZ ) -> ( x ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
42 11 12 41 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( x ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
43 39 42 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( x ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) = ( 0g ` ( R |`s U ) ) )
44 36 43 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( x x. K ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
45 44 oveq1d 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( ( x x. K ) ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( y ( .g ` ( R |`s U ) ) M ) ) = ( ( 0g ` ( R |`s U ) ) ( +g ` ( R |`s U ) ) ( y ( .g ` ( R |`s U ) ) M ) ) )
46 30 23 11 17 28 mulgcld 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( y ( .g ` ( R |`s U ) ) M ) e. ( Base ` ( R |`s U ) ) )
47 30 31 40 11 46 grplidd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( 0g ` ( R |`s U ) ) ( +g ` ( R |`s U ) ) ( y ( .g ` ( R |`s U ) ) M ) ) = ( y ( .g ` ( R |`s U ) ) M ) )
48 45 47 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( ( x x. K ) ( .g ` ( R |`s U ) ) M ) ( +g ` ( R |`s U ) ) ( y ( .g ` ( R |`s U ) ) M ) ) = ( y ( .g ` ( R |`s U ) ) M ) )
49 33 48 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( ( x x. K ) + y ) ( .g ` ( R |`s U ) ) M ) = ( y ( .g ` ( R |`s U ) ) M ) )
50 7 49 eqtrd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( N ( .g ` ( R |`s U ) ) M ) = ( y ( .g ` ( R |`s U ) ) M ) )
51 10 20 syl 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( R |`s U ) e. CMnd )
52 2 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> K e. NN )
53 3 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> M e. ( R PrimRoots K ) )
54 18 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( R PrimRoots K ) = ( ( R |`s U ) PrimRoots K ) )
55 53 54 eleqtrd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> M e. ( ( R |`s U ) PrimRoots K ) )
56 1cnd 
 |-  ( ph -> 1 e. CC )
57 56 addlidd 
 |-  ( ph -> ( 0 + 1 ) = 1 )
58 2 nnge1d 
 |-  ( ph -> 1 <_ K )
59 57 58 eqbrtrd 
 |-  ( ph -> ( 0 + 1 ) <_ K )
60 0red 
 |-  ( ph -> 0 e. RR )
61 1red 
 |-  ( ph -> 1 e. RR )
62 2 nnred 
 |-  ( ph -> K e. RR )
63 leaddsub 
 |-  ( ( 0 e. RR /\ 1 e. RR /\ K e. RR ) -> ( ( 0 + 1 ) <_ K <-> 0 <_ ( K - 1 ) ) )
64 60 61 62 63 syl3anc 
 |-  ( ph -> ( ( 0 + 1 ) <_ K <-> 0 <_ ( K - 1 ) ) )
65 59 64 mpbid 
 |-  ( ph -> 0 <_ ( K - 1 ) )
66 0zd 
 |-  ( ph -> 0 e. ZZ )
67 1zzd 
 |-  ( ph -> 1 e. ZZ )
68 13 67 zsubcld 
 |-  ( ph -> ( K - 1 ) e. ZZ )
69 eluz 
 |-  ( ( 0 e. ZZ /\ ( K - 1 ) e. ZZ ) -> ( ( K - 1 ) e. ( ZZ>= ` 0 ) <-> 0 <_ ( K - 1 ) ) )
70 66 68 69 syl2anc 
 |-  ( ph -> ( ( K - 1 ) e. ( ZZ>= ` 0 ) <-> 0 <_ ( K - 1 ) ) )
71 65 70 mpbird 
 |-  ( ph -> ( K - 1 ) e. ( ZZ>= ` 0 ) )
72 elfzp12 
 |-  ( ( K - 1 ) e. ( ZZ>= ` 0 ) -> ( y e. ( 0 ... ( K - 1 ) ) <-> ( y = 0 \/ y e. ( ( 0 + 1 ) ... ( K - 1 ) ) ) ) )
73 71 72 syl 
 |-  ( ph -> ( y e. ( 0 ... ( K - 1 ) ) <-> ( y = 0 \/ y e. ( ( 0 + 1 ) ... ( K - 1 ) ) ) ) )
74 73 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( y e. ( 0 ... ( K - 1 ) ) <-> ( y = 0 \/ y e. ( ( 0 + 1 ) ... ( K - 1 ) ) ) ) )
75 74 biimpd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( y e. ( 0 ... ( K - 1 ) ) -> ( y = 0 \/ y e. ( ( 0 + 1 ) ... ( K - 1 ) ) ) ) )
76 16 75 mpd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( y = 0 \/ y e. ( ( 0 + 1 ) ... ( K - 1 ) ) ) )
77 simp-5r 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> x e. ZZ )
78 52 adantr 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> K e. NN )
79 78 nnzd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> K e. ZZ )
80 dvdsmul2 
 |-  ( ( x e. ZZ /\ K e. ZZ ) -> K || ( x x. K ) )
81 77 79 80 syl2anc 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> K || ( x x. K ) )
82 77 zcnd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> x e. CC )
83 78 nncnd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> K e. CC )
84 82 83 mulcld 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> ( x x. K ) e. CC )
85 84 addridd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> ( ( x x. K ) + 0 ) = ( x x. K ) )
86 85 eqcomd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> ( x x. K ) = ( ( x x. K ) + 0 ) )
87 simpr 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> y = 0 )
88 87 eqcomd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> 0 = y )
89 88 oveq2d 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> ( ( x x. K ) + 0 ) = ( ( x x. K ) + y ) )
90 86 89 eqtrd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> ( x x. K ) = ( ( x x. K ) + y ) )
91 81 90 breqtrd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> K || ( ( x x. K ) + y ) )
92 6 adantr 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> N = ( ( x x. K ) + y ) )
93 92 eqcomd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> ( ( x x. K ) + y ) = N )
94 91 93 breqtrd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> K || N )
95 simplr 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> -. K || N )
96 94 95 pm2.21dd 
 |-  ( ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) /\ y = 0 ) -> y e. ( 1 ... ( K - 1 ) ) )
97 96 ex 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( y = 0 -> y e. ( 1 ... ( K - 1 ) ) ) )
98 1cnd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> 1 e. CC )
99 98 addlidd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( 0 + 1 ) = 1 )
100 99 oveq1d 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( 0 + 1 ) ... ( K - 1 ) ) = ( 1 ... ( K - 1 ) ) )
101 ssidd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( 1 ... ( K - 1 ) ) C_ ( 1 ... ( K - 1 ) ) )
102 100 101 eqsstrd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( 0 + 1 ) ... ( K - 1 ) ) C_ ( 1 ... ( K - 1 ) ) )
103 102 sseld 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( y e. ( ( 0 + 1 ) ... ( K - 1 ) ) -> y e. ( 1 ... ( K - 1 ) ) ) )
104 97 103 jaod 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( ( y = 0 \/ y e. ( ( 0 + 1 ) ... ( K - 1 ) ) ) -> y e. ( 1 ... ( K - 1 ) ) ) )
105 76 104 mpd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> y e. ( 1 ... ( K - 1 ) ) )
106 51 52 55 105 primrootlekpowne0 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( y ( .g ` ( R |`s U ) ) M ) =/= ( 0g ` ( R |`s U ) ) )
107 50 106 eqnetrd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> ( N ( .g ` ( R |`s U ) ) M ) =/= ( 0g ` ( R |`s U ) ) )
108 107 neneqd 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ -. K || N ) -> -. ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
109 108 ex 
 |-  ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) -> ( -. K || N -> -. ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) ) )
110 109 con4d 
 |-  ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) -> ( ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) -> K || N ) )
111 simp-4l 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ K || N ) -> ph )
112 simpr 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ K || N ) -> K || N )
113 111 112 jca 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ K || N ) -> ( ph /\ K || N ) )
114 divides 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K || N <-> E. x e. ZZ ( x x. K ) = N ) )
115 13 5 114 syl2anc 
 |-  ( ph -> ( K || N <-> E. x e. ZZ ( x x. K ) = N ) )
116 115 biimpd 
 |-  ( ph -> ( K || N -> E. x e. ZZ ( x x. K ) = N ) )
117 116 imp 
 |-  ( ( ph /\ K || N ) -> E. x e. ZZ ( x x. K ) = N )
118 simpr 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( y x. K ) = N )
119 118 eqcomd 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> N = ( y x. K ) )
120 119 oveq1d 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( N ( .g ` ( R |`s U ) ) M ) = ( ( y x. K ) ( .g ` ( R |`s U ) ) M ) )
121 9 ad3antrrr 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( R |`s U ) e. Abel )
122 ablgrp 
 |-  ( ( R |`s U ) e. Abel -> ( R |`s U ) e. Grp )
123 121 122 syl 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( R |`s U ) e. Grp )
124 simplr 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> y e. ZZ )
125 13 ad3antrrr 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> K e. ZZ )
126 27 ad3antrrr 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> M e. ( Base ` ( R |`s U ) ) )
127 124 125 126 3jca 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( y e. ZZ /\ K e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) )
128 30 23 mulgass 
 |-  ( ( ( R |`s U ) e. Grp /\ ( y e. ZZ /\ K e. ZZ /\ M e. ( Base ` ( R |`s U ) ) ) ) -> ( ( y x. K ) ( .g ` ( R |`s U ) ) M ) = ( y ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) )
129 123 127 128 syl2anc 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( ( y x. K ) ( .g ` ( R |`s U ) ) M ) = ( y ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) )
130 37 ad3antrrr 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( K ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
131 130 oveq2d 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( y ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) = ( y ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) )
132 30 23 40 mulgz 
 |-  ( ( ( R |`s U ) e. Grp /\ y e. ZZ ) -> ( y ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
133 123 124 132 syl2anc 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( y ( .g ` ( R |`s U ) ) ( 0g ` ( R |`s U ) ) ) = ( 0g ` ( R |`s U ) ) )
134 131 133 eqtrd 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( y ( .g ` ( R |`s U ) ) ( K ( .g ` ( R |`s U ) ) M ) ) = ( 0g ` ( R |`s U ) ) )
135 129 134 eqtrd 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( ( y x. K ) ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
136 120 135 eqtrd 
 |-  ( ( ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) /\ y e. ZZ ) /\ ( y x. K ) = N ) -> ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
137 nfv 
 |-  F/ y ( x x. K ) = N
138 nfv 
 |-  F/ x ( y x. K ) = N
139 oveq1 
 |-  ( x = y -> ( x x. K ) = ( y x. K ) )
140 139 eqeq1d 
 |-  ( x = y -> ( ( x x. K ) = N <-> ( y x. K ) = N ) )
141 137 138 140 cbvrexw 
 |-  ( E. x e. ZZ ( x x. K ) = N <-> E. y e. ZZ ( y x. K ) = N )
142 141 biimpi 
 |-  ( E. x e. ZZ ( x x. K ) = N -> E. y e. ZZ ( y x. K ) = N )
143 142 adantl 
 |-  ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) -> E. y e. ZZ ( y x. K ) = N )
144 136 143 r19.29a 
 |-  ( ( ph /\ E. x e. ZZ ( x x. K ) = N ) -> ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
145 144 ex 
 |-  ( ph -> ( E. x e. ZZ ( x x. K ) = N -> ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) ) )
146 145 adantr 
 |-  ( ( ph /\ K || N ) -> ( E. x e. ZZ ( x x. K ) = N -> ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) ) )
147 117 146 mpd 
 |-  ( ( ph /\ K || N ) -> ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
148 113 147 syl 
 |-  ( ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) /\ K || N ) -> ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) )
149 148 ex 
 |-  ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) -> ( K || N -> ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) ) )
150 110 149 impbid 
 |-  ( ( ( ( ph /\ x e. ZZ ) /\ y e. ( 0 ... ( K - 1 ) ) ) /\ N = ( ( x x. K ) + y ) ) -> ( ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) <-> K || N ) )
151 5 2 remexz 
 |-  ( ph -> E. x e. ZZ E. y e. ( 0 ... ( K - 1 ) ) N = ( ( x x. K ) + y ) )
152 150 151 r19.29vva 
 |-  ( ph -> ( ( N ( .g ` ( R |`s U ) ) M ) = ( 0g ` ( R |`s U ) ) <-> K || N ) )