Metamath Proof Explorer

Theorem aks6d1c6lem4

Description: Claim 6 of Theorem 6.1 of https://www3.nd.edu/%7eandyp/notes/AKS.pdf Add hypothesis on coprimality, lift function to the integers so that group operations may be applied. Inline definition. (Contributed by metakunt, 14-May-2025)

Ref Expression
Hypotheses aks6d1c6lem4.1 
|- .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
aks6d1c6lem4.2 
|- P = ( chr ` K )
aks6d1c6lem4.3 
|- ( ph -> K e. Field )
aks6d1c6lem4.4 
|- ( ph -> P e. Prime )
aks6d1c6lem4.5 
|- ( ph -> R e. NN )
aks6d1c6lem4.6 
|- ( ph -> N e. NN )
aks6d1c6lem4.7 
|- ( ph -> P || N )
aks6d1c6lem4.8 
|- ( ph -> ( N gcd R ) = 1 )
aks6d1c6lem4.9 
|- ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
aks6d1c6lem4.10 
|- G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
aks6d1c6lem4.11 
|- A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
aksaks6dlem4.12 
|- E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
aks6d1c6lem4.13 
|- L = ( ZRHom ` ( Z/nZ ` R ) )
aks6d1c6lem4.14 
|- ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
aks6d1c6lem4.15 
|- ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
aks6d1c6lem4.16 
|- ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
aks6d1c6lem4.17 
|- H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
aks6d1c6lem4.18 
|- D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
aks6d1c6lem4.19 
|- S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) }
aks6d1c6lem4.20 
|- J = ( j e. ZZ |-> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
aks6d1c6lem4.21 
|- ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( J " ( E " ( NN0 X. NN0 ) ) ) ) )
aks6d1c6lem4.22 
|- U = { m e. ( Base ` ( mulGrp ` K ) ) | E. n e. ( Base ` ( mulGrp ` K ) ) ( n ( +g ` ( mulGrp ` K ) ) m ) = ( 0g ` ( mulGrp ` K ) ) }
Assertion aks6d1c6lem4 
|- ( ph -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) )

Proof

Step Hyp Ref Expression
1 aks6d1c6lem4.1 
 |-  .~ = { <. e , f >. | ( e e. NN /\ f e. ( Base ` ( Poly1 ` K ) ) /\ A. y e. ( ( mulGrp ` K ) PrimRoots R ) ( e ( .g ` ( mulGrp ` K ) ) ( ( ( eval1 ` K ) ` f ) ` y ) ) = ( ( ( eval1 ` K ) ` f ) ` ( e ( .g ` ( mulGrp ` K ) ) y ) ) ) }
2 aks6d1c6lem4.2 
 |-  P = ( chr ` K )
3 aks6d1c6lem4.3 
 |-  ( ph -> K e. Field )
4 aks6d1c6lem4.4 
 |-  ( ph -> P e. Prime )
5 aks6d1c6lem4.5 
 |-  ( ph -> R e. NN )
6 aks6d1c6lem4.6 
 |-  ( ph -> N e. NN )
7 aks6d1c6lem4.7 
 |-  ( ph -> P || N )
8 aks6d1c6lem4.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks6d1c6lem4.9 
 |-  ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
10 aks6d1c6lem4.10 
 |-  G = ( g e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( mulGrp ` ( Poly1 ` K ) ) gsum ( i e. ( 0 ... A ) |-> ( ( g ` i ) ( .g ` ( mulGrp ` ( Poly1 ` K ) ) ) ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` i ) ) ) ) ) ) )
11 aks6d1c6lem4.11 
 |-  A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
12 aksaks6dlem4.12 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
13 aks6d1c6lem4.13 
 |-  L = ( ZRHom ` ( Z/nZ ` R ) )
14 aks6d1c6lem4.14 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
15 aks6d1c6lem4.15 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
16 aks6d1c6lem4.16 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
17 aks6d1c6lem4.17 
 |-  H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
18 aks6d1c6lem4.18 
 |-  D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
19 aks6d1c6lem4.19 
 |-  S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) }
20 aks6d1c6lem4.20 
 |-  J = ( j e. ZZ |-> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
21 aks6d1c6lem4.21 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( J " ( E " ( NN0 X. NN0 ) ) ) ) )
22 aks6d1c6lem4.22 
 |-  U = { m e. ( Base ` ( mulGrp ` K ) ) | E. n e. ( Base ` ( mulGrp ` K ) ) ( n ( +g ` ( mulGrp ` K ) ) m ) = ( 0g ` ( mulGrp ` K ) ) }
23 simpr 
 |-  ( ( ph /\ A < P ) -> A < P )
24 prmnn 
 |-  ( P e. Prime -> P e. NN )
25 4 24 syl 
 |-  ( ph -> P e. NN )
26 25 nnred 
 |-  ( ph -> P e. RR )
27 5 phicld 
 |-  ( ph -> ( phi ` R ) e. NN )
28 27 nnred 
 |-  ( ph -> ( phi ` R ) e. RR )
29 27 nnnn0d 
 |-  ( ph -> ( phi ` R ) e. NN0 )
30 29 nn0ge0d 
 |-  ( ph -> 0 <_ ( phi ` R ) )
31 28 30 resqrtcld 
 |-  ( ph -> ( sqrt ` ( phi ` R ) ) e. RR )
32 2re 
 |-  2 e. RR
33 32 a1i 
 |-  ( ph -> 2 e. RR )
34 2pos 
 |-  0 < 2
35 34 a1i 
 |-  ( ph -> 0 < 2 )
36 6 nnred 
 |-  ( ph -> N e. RR )
37 6 nngt0d 
 |-  ( ph -> 0 < N )
38 1red 
 |-  ( ph -> 1 e. RR )
39 1lt2 
 |-  1 < 2
40 39 a1i 
 |-  ( ph -> 1 < 2 )
41 38 40 ltned 
 |-  ( ph -> 1 =/= 2 )
42 41 necomd 
 |-  ( ph -> 2 =/= 1 )
43 33 35 36 37 42 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
44 31 43 remulcld 
 |-  ( ph -> ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) e. RR )
45 44 flcld 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. ZZ )
46 28 30 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( phi ` R ) ) )
47 33 recnd 
 |-  ( ph -> 2 e. CC )
48 35 gt0ne0d 
 |-  ( ph -> 2 =/= 0 )
49 logb1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 1 ) = 0 )
50 47 48 42 49 syl3anc 
 |-  ( ph -> ( 2 logb 1 ) = 0 )
51 50 eqcomd 
 |-  ( ph -> 0 = ( 2 logb 1 ) )
52 2z 
 |-  2 e. ZZ
53 52 a1i 
 |-  ( ph -> 2 e. ZZ )
54 33 leidd 
 |-  ( ph -> 2 <_ 2 )
55 0lt1 
 |-  0 < 1
56 55 a1i 
 |-  ( ph -> 0 < 1 )
57 6 nnge1d 
 |-  ( ph -> 1 <_ N )
58 53 54 38 56 36 37 57 logblebd 
 |-  ( ph -> ( 2 logb 1 ) <_ ( 2 logb N ) )
59 51 58 eqbrtrd 
 |-  ( ph -> 0 <_ ( 2 logb N ) )
60 31 43 46 59 mulge0d 
 |-  ( ph -> 0 <_ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
61 0zd 
 |-  ( ph -> 0 e. ZZ )
62 flge 
 |-  ( ( ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) <-> 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
63 44 61 62 syl2anc 
 |-  ( ph -> ( 0 <_ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) <-> 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
64 60 63 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) )
65 45 64 jca 
 |-  ( ph -> ( ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
66 elnn0z 
 |-  ( ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. NN0 <-> ( ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
67 65 66 sylibr 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. NN0 )
68 11 67 eqeltrid 
 |-  ( ph -> A e. NN0 )
69 68 nn0red 
 |-  ( ph -> A e. RR )
70 26 69 lenltd 
 |-  ( ph -> ( P <_ A <-> -. A < P ) )
71 70 biimpar 
 |-  ( ( ph /\ -. A < P ) -> P <_ A )
72 oveq1 
 |-  ( b = P -> ( b gcd N ) = ( P gcd N ) )
73 72 eqeq1d 
 |-  ( b = P -> ( ( b gcd N ) = 1 <-> ( P gcd N ) = 1 ) )
74 9 adantr 
 |-  ( ( ph /\ P <_ A ) -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
75 1zzd 
 |-  ( ( ph /\ P <_ A ) -> 1 e. ZZ )
76 11 45 eqeltrid 
 |-  ( ph -> A e. ZZ )
77 76 adantr 
 |-  ( ( ph /\ P <_ A ) -> A e. ZZ )
78 25 nnzd 
 |-  ( ph -> P e. ZZ )
79 78 adantr 
 |-  ( ( ph /\ P <_ A ) -> P e. ZZ )
80 25 nnge1d 
 |-  ( ph -> 1 <_ P )
81 80 adantr 
 |-  ( ( ph /\ P <_ A ) -> 1 <_ P )
82 simpr 
 |-  ( ( ph /\ P <_ A ) -> P <_ A )
83 75 77 79 81 82 elfzd 
 |-  ( ( ph /\ P <_ A ) -> P e. ( 1 ... A ) )
84 73 74 83 rspcdva 
 |-  ( ( ph /\ P <_ A ) -> ( P gcd N ) = 1 )
85 84 ex 
 |-  ( ph -> ( P <_ A -> ( P gcd N ) = 1 ) )
86 85 adantr 
 |-  ( ( ph /\ -. A < P ) -> ( P <_ A -> ( P gcd N ) = 1 ) )
87 71 86 mpd 
 |-  ( ( ph /\ -. A < P ) -> ( P gcd N ) = 1 )
88 6 nnzd 
 |-  ( ph -> N e. ZZ )
89 coprm 
 |-  ( ( P e. Prime /\ N e. ZZ ) -> ( -. P || N <-> ( P gcd N ) = 1 ) )
90 4 88 89 syl2anc 
 |-  ( ph -> ( -. P || N <-> ( P gcd N ) = 1 ) )
91 90 con1bid 
 |-  ( ph -> ( -. ( P gcd N ) = 1 <-> P || N ) )
92 91 bicomd 
 |-  ( ph -> ( P || N <-> -. ( P gcd N ) = 1 ) )
93 92 biimpd 
 |-  ( ph -> ( P || N -> -. ( P gcd N ) = 1 ) )
94 7 93 mpd 
 |-  ( ph -> -. ( P gcd N ) = 1 )
95 94 neqned 
 |-  ( ph -> ( P gcd N ) =/= 1 )
96 95 adantr 
 |-  ( ( ph /\ -. A < P ) -> ( P gcd N ) =/= 1 )
97 96 neneqd 
 |-  ( ( ph /\ -. A < P ) -> -. ( P gcd N ) = 1 )
98 87 97 pm2.21dd 
 |-  ( ( ph /\ -. A < P ) -> A < P )
99 23 98 pm2.61dan 
 |-  ( ph -> A < P )
100 eqid 
 |-  ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) )
101 imaco 
 |-  ( ( J o. E ) " ( NN0 X. NN0 ) ) = ( J " ( E " ( NN0 X. NN0 ) ) )
102 101 eqcomi 
 |-  ( J " ( E " ( NN0 X. NN0 ) ) ) = ( ( J o. E ) " ( NN0 X. NN0 ) )
103 resima 
 |-  ( ( ( J o. E ) |` ( NN0 X. NN0 ) ) " ( NN0 X. NN0 ) ) = ( ( J o. E ) " ( NN0 X. NN0 ) )
104 103 eqcomi 
 |-  ( ( J o. E ) " ( NN0 X. NN0 ) ) = ( ( ( J o. E ) |` ( NN0 X. NN0 ) ) " ( NN0 X. NN0 ) )
105 104 a1i 
 |-  ( ph -> ( ( J o. E ) " ( NN0 X. NN0 ) ) = ( ( ( J o. E ) |` ( NN0 X. NN0 ) ) " ( NN0 X. NN0 ) ) )
106 78 adantr 
 |-  ( ( ph /\ v e. ( NN0 X. NN0 ) ) -> P e. ZZ )
107 xp1st 
 |-  ( v e. ( NN0 X. NN0 ) -> ( 1st ` v ) e. NN0 )
108 107 adantl 
 |-  ( ( ph /\ v e. ( NN0 X. NN0 ) ) -> ( 1st ` v ) e. NN0 )
109 106 108 zexpcld 
 |-  ( ( ph /\ v e. ( NN0 X. NN0 ) ) -> ( P ^ ( 1st ` v ) ) e. ZZ )
110 25 nnne0d 
 |-  ( ph -> P =/= 0 )
111 dvdsval2 
 |-  ( ( P e. ZZ /\ P =/= 0 /\ N e. ZZ ) -> ( P || N <-> ( N / P ) e. ZZ ) )
112 78 110 88 111 syl3anc 
 |-  ( ph -> ( P || N <-> ( N / P ) e. ZZ ) )
113 7 112 mpbid 
 |-  ( ph -> ( N / P ) e. ZZ )
114 113 adantr 
 |-  ( ( ph /\ v e. ( NN0 X. NN0 ) ) -> ( N / P ) e. ZZ )
115 xp2nd 
 |-  ( v e. ( NN0 X. NN0 ) -> ( 2nd ` v ) e. NN0 )
116 115 adantl 
 |-  ( ( ph /\ v e. ( NN0 X. NN0 ) ) -> ( 2nd ` v ) e. NN0 )
117 114 116 zexpcld 
 |-  ( ( ph /\ v e. ( NN0 X. NN0 ) ) -> ( ( N / P ) ^ ( 2nd ` v ) ) e. ZZ )
118 109 117 zmulcld 
 |-  ( ( ph /\ v e. ( NN0 X. NN0 ) ) -> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) e. ZZ )
119 vex 
 |-  k e. _V
120 vex 
 |-  l e. _V
121 119 120 op1std 
 |-  ( v = <. k , l >. -> ( 1st ` v ) = k )
122 121 oveq2d 
 |-  ( v = <. k , l >. -> ( P ^ ( 1st ` v ) ) = ( P ^ k ) )
123 119 120 op2ndd 
 |-  ( v = <. k , l >. -> ( 2nd ` v ) = l )
124 123 oveq2d 
 |-  ( v = <. k , l >. -> ( ( N / P ) ^ ( 2nd ` v ) ) = ( ( N / P ) ^ l ) )
125 122 124 oveq12d 
 |-  ( v = <. k , l >. -> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) = ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
126 125 mpompt 
 |-  ( v e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ) = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
127 12 126 eqtr4i 
 |-  E = ( v e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) )
128 127 a1i 
 |-  ( ph -> E = ( v e. ( NN0 X. NN0 ) |-> ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ) )
129 20 a1i 
 |-  ( ph -> J = ( j e. ZZ |-> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
130 oveq1 
 |-  ( j = ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) -> ( j ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
131 118 128 129 130 fmptco 
 |-  ( ph -> ( J o. E ) = ( v e. ( NN0 X. NN0 ) |-> ( ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
132 131 reseq1d 
 |-  ( ph -> ( ( J o. E ) |` ( NN0 X. NN0 ) ) = ( ( v e. ( NN0 X. NN0 ) |-> ( ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) |` ( NN0 X. NN0 ) ) )
133 ssidd 
 |-  ( ph -> ( NN0 X. NN0 ) C_ ( NN0 X. NN0 ) )
134 133 resmptd 
 |-  ( ph -> ( ( v e. ( NN0 X. NN0 ) |-> ( ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) |` ( NN0 X. NN0 ) ) = ( v e. ( NN0 X. NN0 ) |-> ( ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
135 128 118 fvmpt2d 
 |-  ( ( ph /\ v e. ( NN0 X. NN0 ) ) -> ( E ` v ) = ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) )
136 135 oveq1d 
 |-  ( ( ph /\ v e. ( NN0 X. NN0 ) ) -> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
137 136 mpteq2dva 
 |-  ( ph -> ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( v e. ( NN0 X. NN0 ) |-> ( ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
138 137 eqcomd 
 |-  ( ph -> ( v e. ( NN0 X. NN0 ) |-> ( ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
139 ovexd 
 |-  ( ( ph /\ v e. ( NN0 X. NN0 ) ) -> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) e. _V )
140 eqid 
 |-  ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
141 139 140 fmptd 
 |-  ( ph -> ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) : ( NN0 X. NN0 ) --> _V )
142 ffn 
 |-  ( ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) : ( NN0 X. NN0 ) --> _V -> ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) Fn ( NN0 X. NN0 ) )
143 141 142 syl 
 |-  ( ph -> ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) Fn ( NN0 X. NN0 ) )
144 ovexd 
 |-  ( ( ph /\ j e. ( NN0 X. NN0 ) ) -> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) e. _V )
145 144 100 fmptd 
 |-  ( ph -> ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) : ( NN0 X. NN0 ) --> _V )
146 ffn 
 |-  ( ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) : ( NN0 X. NN0 ) --> _V -> ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) Fn ( NN0 X. NN0 ) )
147 145 146 syl 
 |-  ( ph -> ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) Fn ( NN0 X. NN0 ) )
148 eqidd 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) )
149 simpr 
 |-  ( ( ( ph /\ c e. ( NN0 X. NN0 ) ) /\ v = c ) -> v = c )
150 149 fveq2d 
 |-  ( ( ( ph /\ c e. ( NN0 X. NN0 ) ) /\ v = c ) -> ( E ` v ) = ( E ` c ) )
151 150 oveq1d 
 |-  ( ( ( ph /\ c e. ( NN0 X. NN0 ) ) /\ v = c ) -> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( ( E ` c ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
152 simpr 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> c e. ( NN0 X. NN0 ) )
153 ovexd 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> ( ( E ` c ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) e. _V )
154 148 151 152 153 fvmptd 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> ( ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) ` c ) = ( ( E ` c ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) )
155 eqid 
 |-  ( ( mulGrp ` K ) |`s U ) = ( ( mulGrp ` K ) |`s U )
156 22 ssrab3 
 |-  U C_ ( Base ` ( mulGrp ` K ) )
157 156 a1i 
 |-  ( ph -> U C_ ( Base ` ( mulGrp ` K ) ) )
158 157 adantr 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> U C_ ( Base ` ( mulGrp ` K ) ) )
159 3 fldcrngd 
 |-  ( ph -> K e. CRing )
160 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
161 160 crngmgp 
 |-  ( K e. CRing -> ( mulGrp ` K ) e. CMnd )
162 159 161 syl 
 |-  ( ph -> ( mulGrp ` K ) e. CMnd )
163 162 5 22 primrootsunit 
 |-  ( ph -> ( ( ( mulGrp ` K ) PrimRoots R ) = ( ( ( mulGrp ` K ) |`s U ) PrimRoots R ) /\ ( ( mulGrp ` K ) |`s U ) e. Abel ) )
164 163 simpld 
 |-  ( ph -> ( ( mulGrp ` K ) PrimRoots R ) = ( ( ( mulGrp ` K ) |`s U ) PrimRoots R ) )
165 16 164 eleqtrd 
 |-  ( ph -> M e. ( ( ( mulGrp ` K ) |`s U ) PrimRoots R ) )
166 163 simprd 
 |-  ( ph -> ( ( mulGrp ` K ) |`s U ) e. Abel )
167 ablcmn 
 |-  ( ( ( mulGrp ` K ) |`s U ) e. Abel -> ( ( mulGrp ` K ) |`s U ) e. CMnd )
168 166 167 syl 
 |-  ( ph -> ( ( mulGrp ` K ) |`s U ) e. CMnd )
169 5 nnnn0d 
 |-  ( ph -> R e. NN0 )
170 eqid 
 |-  ( .g ` ( ( mulGrp ` K ) |`s U ) ) = ( .g ` ( ( mulGrp ` K ) |`s U ) )
171 168 169 170 isprimroot 
 |-  ( ph -> ( M e. ( ( ( mulGrp ` K ) |`s U ) PrimRoots R ) <-> ( M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) /\ ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) /\ A. w e. NN0 ( ( w ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) -> R || w ) ) ) )
172 171 biimpd 
 |-  ( ph -> ( M e. ( ( ( mulGrp ` K ) |`s U ) PrimRoots R ) -> ( M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) /\ ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) /\ A. w e. NN0 ( ( w ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) -> R || w ) ) ) )
173 165 172 mpd 
 |-  ( ph -> ( M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) /\ ( R ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) /\ A. w e. NN0 ( ( w ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( 0g ` ( ( mulGrp ` K ) |`s U ) ) -> R || w ) ) )
174 173 simp1d 
 |-  ( ph -> M e. ( Base ` ( ( mulGrp ` K ) |`s U ) ) )
175 eqid 
 |-  ( Base ` ( mulGrp ` K ) ) = ( Base ` ( mulGrp ` K ) )
176 155 175 ressbas2 
 |-  ( U C_ ( Base ` ( mulGrp ` K ) ) -> U = ( Base ` ( ( mulGrp ` K ) |`s U ) ) )
177 157 176 syl 
 |-  ( ph -> U = ( Base ` ( ( mulGrp ` K ) |`s U ) ) )
178 174 177 eleqtrrd 
 |-  ( ph -> M e. U )
179 178 adantr 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> M e. U )
180 6 4 7 12 aks6d1c2p1 
 |-  ( ph -> E : ( NN0 X. NN0 ) --> NN )
181 180 ffvelcdmda 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> ( E ` c ) e. NN )
182 155 158 179 181 ressmulgnnd 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> ( ( E ` c ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) = ( ( E ` c ) ( .g ` ( mulGrp ` K ) ) M ) )
183 eqidd 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) )
184 simpr 
 |-  ( ( ( ph /\ c e. ( NN0 X. NN0 ) ) /\ j = c ) -> j = c )
185 184 fveq2d 
 |-  ( ( ( ph /\ c e. ( NN0 X. NN0 ) ) /\ j = c ) -> ( E ` j ) = ( E ` c ) )
186 185 oveq1d 
 |-  ( ( ( ph /\ c e. ( NN0 X. NN0 ) ) /\ j = c ) -> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) = ( ( E ` c ) ( .g ` ( mulGrp ` K ) ) M ) )
187 ovexd 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> ( ( E ` c ) ( .g ` ( mulGrp ` K ) ) M ) e. _V )
188 183 186 152 187 fvmptd 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> ( ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) ` c ) = ( ( E ` c ) ( .g ` ( mulGrp ` K ) ) M ) )
189 188 eqcomd 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> ( ( E ` c ) ( .g ` ( mulGrp ` K ) ) M ) = ( ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) ` c ) )
190 154 182 189 3eqtrd 
 |-  ( ( ph /\ c e. ( NN0 X. NN0 ) ) -> ( ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) ` c ) = ( ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) ` c ) )
191 143 147 190 eqfnfvd 
 |-  ( ph -> ( v e. ( NN0 X. NN0 ) |-> ( ( E ` v ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) )
192 138 191 eqtrd 
 |-  ( ph -> ( v e. ( NN0 X. NN0 ) |-> ( ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) )
193 134 192 eqtrd 
 |-  ( ph -> ( ( v e. ( NN0 X. NN0 ) |-> ( ( ( P ^ ( 1st ` v ) ) x. ( ( N / P ) ^ ( 2nd ` v ) ) ) ( .g ` ( ( mulGrp ` K ) |`s U ) ) M ) ) |` ( NN0 X. NN0 ) ) = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) )
194 132 193 eqtrd 
 |-  ( ph -> ( ( J o. E ) |` ( NN0 X. NN0 ) ) = ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) )
195 194 imaeq1d 
 |-  ( ph -> ( ( ( J o. E ) |` ( NN0 X. NN0 ) ) " ( NN0 X. NN0 ) ) = ( ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) " ( NN0 X. NN0 ) ) )
196 105 195 eqtrd 
 |-  ( ph -> ( ( J o. E ) " ( NN0 X. NN0 ) ) = ( ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) " ( NN0 X. NN0 ) ) )
197 102 196 eqtrid 
 |-  ( ph -> ( J " ( E " ( NN0 X. NN0 ) ) ) = ( ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) " ( NN0 X. NN0 ) ) )
198 197 fveq2d 
 |-  ( ph -> ( # ` ( J " ( E " ( NN0 X. NN0 ) ) ) ) = ( # ` ( ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) " ( NN0 X. NN0 ) ) ) )
199 21 198 breqtrd 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <_ ( # ` ( ( j e. ( NN0 X. NN0 ) |-> ( ( E ` j ) ( .g ` ( mulGrp ` K ) ) M ) ) " ( NN0 X. NN0 ) ) ) )
200 1 2 3 4 5 6 7 8 99 10 68 12 13 14 15 16 17 18 19 100 199 aks6d1c6lem3 
 |-  ( ph -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) )