Metamath Proof Explorer

Theorem aks6d1c7lem2

Description: Contradiction to Claim 2 and Claim 7. We assumed in Claim 2 that there are two different prime numbers P and Q . (Contributed by metakunt, 16-May-2025)

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

Proof

Step Hyp Ref Expression
1 aks6d1c7lem2.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 aks6d1c7lem2.2 
 |-  P = ( chr ` K )
3 aks6d1c7lem2.3 
 |-  ( ph -> K e. Field )
4 aks6d1c7lem2.4 
 |-  ( ph -> P e. Prime )
5 aks6d1c7lem2.5 
 |-  ( ph -> R e. NN )
6 aks6d1c7lem2.6 
 |-  ( ph -> N e. ( ZZ>= ` 3 ) )
7 aks6d1c7lem2.7 
 |-  ( ph -> P || N )
8 aks6d1c7lem2.8 
 |-  ( ph -> ( N gcd R ) = 1 )
9 aks6d1c7lem2.9 
 |-  E = ( k e. NN0 , l e. NN0 |-> ( ( P ^ k ) x. ( ( N / P ) ^ l ) ) )
10 aks6d1c7lem2.10 
 |-  L = ( ZRHom ` ( Z/nZ ` R ) )
11 aks6d1c7lem2.11 
 |-  D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) )
12 aks6d1c7lem2.12 
 |-  A = ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
13 aks6d1c7lem2.13 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
14 aks6d1c7lem2.14 
 |-  ( ph -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
15 aks6d1c7lem2.15 
 |-  ( ph -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
16 aks6d1c7lem2.16 
 |-  H = ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) )
17 aks6d1c7lem2.17 
 |-  B = ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
18 aks6d1c7lem2.18 
 |-  C = ( E " ( ( 0 ... B ) X. ( 0 ... B ) ) )
19 aks6d1c7lem2.19 
 |-  ( ph -> ( Q e. Prime /\ Q || N ) )
20 aks6d1c7lem2.20 
 |-  ( ph -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
21 aks6d1c7lem2.21 
 |-  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 ) ) ) ) ) ) )
22 aks6d1c7lem2.22 
 |-  ( ph -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
23 aks6d1c7lem2.23 
 |-  S = { s e. ( NN0 ^m ( 0 ... A ) ) | sum_ t e. ( 0 ... A ) ( s ` t ) <_ ( D - 1 ) }
24 simpr 
 |-  ( ( ph /\ P = Q ) -> P = Q )
25 3 adantr 
 |-  ( ( ph /\ P =/= Q ) -> K e. Field )
26 4 adantr 
 |-  ( ( ph /\ P =/= Q ) -> P e. Prime )
27 5 adantr 
 |-  ( ( ph /\ P =/= Q ) -> R e. NN )
28 eluzelz 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. ZZ )
29 6 28 syl 
 |-  ( ph -> N e. ZZ )
30 0red 
 |-  ( ph -> 0 e. RR )
31 3re 
 |-  3 e. RR
32 31 a1i 
 |-  ( ph -> 3 e. RR )
33 29 zred 
 |-  ( ph -> N e. RR )
34 3pos 
 |-  0 < 3
35 34 a1i 
 |-  ( ph -> 0 < 3 )
36 eluzle 
 |-  ( N e. ( ZZ>= ` 3 ) -> 3 <_ N )
37 6 36 syl 
 |-  ( ph -> 3 <_ N )
38 30 32 33 35 37 ltletrd 
 |-  ( ph -> 0 < N )
39 29 38 jca 
 |-  ( ph -> ( N e. ZZ /\ 0 < N ) )
40 elnnz 
 |-  ( N e. NN <-> ( N e. ZZ /\ 0 < N ) )
41 39 40 sylibr 
 |-  ( ph -> N e. NN )
42 41 adantr 
 |-  ( ( ph /\ P =/= Q ) -> N e. NN )
43 7 adantr 
 |-  ( ( ph /\ P =/= Q ) -> P || N )
44 8 adantr 
 |-  ( ( ph /\ P =/= Q ) -> ( N gcd R ) = 1 )
45 5 phicld 
 |-  ( ph -> ( phi ` R ) e. NN )
46 45 nnred 
 |-  ( ph -> ( phi ` R ) e. RR )
47 1red 
 |-  ( ph -> 1 e. RR )
48 0le1 
 |-  0 <_ 1
49 48 a1i 
 |-  ( ph -> 0 <_ 1 )
50 45 nnge1d 
 |-  ( ph -> 1 <_ ( phi ` R ) )
51 30 47 46 49 50 letrd 
 |-  ( ph -> 0 <_ ( phi ` R ) )
52 46 51 resqrtcld 
 |-  ( ph -> ( sqrt ` ( phi ` R ) ) e. RR )
53 2re 
 |-  2 e. RR
54 53 a1i 
 |-  ( ph -> 2 e. RR )
55 2pos 
 |-  0 < 2
56 55 a1i 
 |-  ( ph -> 0 < 2 )
57 1lt2 
 |-  1 < 2
58 57 a1i 
 |-  ( ph -> 1 < 2 )
59 47 58 ltned 
 |-  ( ph -> 1 =/= 2 )
60 59 necomd 
 |-  ( ph -> 2 =/= 1 )
61 54 56 33 38 60 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
62 52 61 remulcld 
 |-  ( ph -> ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) e. RR )
63 62 flcld 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. ZZ )
64 46 51 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( phi ` R ) ) )
65 54 recnd 
 |-  ( ph -> 2 e. CC )
66 30 56 gtned 
 |-  ( ph -> 2 =/= 0 )
67 logb1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 1 ) = 0 )
68 65 66 60 67 syl3anc 
 |-  ( ph -> ( 2 logb 1 ) = 0 )
69 68 eqcomd 
 |-  ( ph -> 0 = ( 2 logb 1 ) )
70 2z 
 |-  2 e. ZZ
71 70 a1i 
 |-  ( ph -> 2 e. ZZ )
72 54 leidd 
 |-  ( ph -> 2 <_ 2 )
73 0lt1 
 |-  0 < 1
74 73 a1i 
 |-  ( ph -> 0 < 1 )
75 41 nnge1d 
 |-  ( ph -> 1 <_ N )
76 71 72 47 74 33 38 75 logblebd 
 |-  ( ph -> ( 2 logb 1 ) <_ ( 2 logb N ) )
77 69 76 eqbrtrd 
 |-  ( ph -> 0 <_ ( 2 logb N ) )
78 52 61 64 77 mulge0d 
 |-  ( ph -> 0 <_ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) )
79 0zd 
 |-  ( ph -> 0 e. ZZ )
80 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 ) ) ) ) )
81 62 79 80 syl2anc 
 |-  ( ph -> ( 0 <_ ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) <-> 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
82 78 81 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) )
83 63 82 jca 
 |-  ( ph -> ( ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) ) )
84 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 ) ) ) ) )
85 83 84 sylibr 
 |-  ( ph -> ( |_ ` ( ( sqrt ` ( phi ` R ) ) x. ( 2 logb N ) ) ) e. NN0 )
86 12 85 eqeltrid 
 |-  ( ph -> A e. NN0 )
87 86 adantr 
 |-  ( ( ph /\ P =/= Q ) -> A e. NN0 )
88 22 adantr 
 |-  ( ( ph /\ P =/= Q ) -> A. a e. ( 1 ... A ) N .~ ( ( var1 ` K ) ( +g ` ( Poly1 ` K ) ) ( ( algSc ` ( Poly1 ` K ) ) ` ( ( ZRHom ` K ) ` a ) ) ) )
89 14 adantr 
 |-  ( ( ph /\ P =/= Q ) -> ( x e. ( Base ` K ) |-> ( P ( .g ` ( mulGrp ` K ) ) x ) ) e. ( K RingIso K ) )
90 15 adantr 
 |-  ( ( ph /\ P =/= Q ) -> M e. ( ( mulGrp ` K ) PrimRoots R ) )
91 19 simpld 
 |-  ( ph -> Q e. Prime )
92 91 adantr 
 |-  ( ( ph /\ P =/= Q ) -> Q e. Prime )
93 19 simprd 
 |-  ( ph -> Q || N )
94 93 adantr 
 |-  ( ( ph /\ P =/= Q ) -> Q || N )
95 simpr 
 |-  ( ( ph /\ P =/= Q ) -> P =/= Q )
96 92 94 95 3jca 
 |-  ( ( ph /\ P =/= Q ) -> ( Q e. Prime /\ Q || N /\ P =/= Q ) )
97 1 2 25 26 27 42 43 44 21 87 9 10 88 89 90 16 17 18 96 aks6d1c2 
 |-  ( ( ph /\ P =/= Q ) -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) )
98 41 nnzd 
 |-  ( ph -> N e. ZZ )
99 eqid 
 |-  ( Z/nZ ` R ) = ( Z/nZ ` R )
100 41 4 7 5 8 9 10 99 hashscontpowcl 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
101 100 nn0red 
 |-  ( ph -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. RR )
102 100 nn0ge0d 
 |-  ( ph -> 0 <_ ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) )
103 101 102 resqrtcld 
 |-  ( ph -> ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR )
104 103 flcld 
 |-  ( ph -> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ )
105 101 102 sqrtge0d 
 |-  ( ph -> 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) )
106 flge 
 |-  ( ( ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) <-> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
107 103 79 106 syl2anc 
 |-  ( ph -> ( 0 <_ ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) <-> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
108 105 107 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) )
109 104 108 jca 
 |-  ( ph -> ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
110 elnn0z 
 |-  ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. NN0 <-> ( ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) ) )
111 109 110 sylibr 
 |-  ( ph -> ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) e. NN0 )
112 17 111 eqeltrid 
 |-  ( ph -> B e. NN0 )
113 98 112 zexpcld 
 |-  ( ph -> ( N ^ B ) e. ZZ )
114 113 zred 
 |-  ( ph -> ( N ^ B ) e. RR )
115 114 adantr 
 |-  ( ( ph /\ P =/= Q ) -> ( N ^ B ) e. RR )
116 115 rexrd 
 |-  ( ( ph /\ P =/= Q ) -> ( N ^ B ) e. RR* )
117 100 adantr 
 |-  ( ( ph /\ P =/= Q ) -> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) e. NN0 )
118 11 117 eqeltrid 
 |-  ( ( ph /\ P =/= Q ) -> D e. NN0 )
119 118 87 nn0addcld 
 |-  ( ( ph /\ P =/= Q ) -> ( D + A ) e. NN0 )
120 118 nn0zd 
 |-  ( ( ph /\ P =/= Q ) -> D e. ZZ )
121 1zzd 
 |-  ( ( ph /\ P =/= Q ) -> 1 e. ZZ )
122 120 121 zsubcld 
 |-  ( ( ph /\ P =/= Q ) -> ( D - 1 ) e. ZZ )
123 bccl 
 |-  ( ( ( D + A ) e. NN0 /\ ( D - 1 ) e. ZZ ) -> ( ( D + A ) _C ( D - 1 ) ) e. NN0 )
124 119 122 123 syl2anc 
 |-  ( ( ph /\ P =/= Q ) -> ( ( D + A ) _C ( D - 1 ) ) e. NN0 )
125 124 nn0red 
 |-  ( ( ph /\ P =/= Q ) -> ( ( D + A ) _C ( D - 1 ) ) e. RR )
126 125 rexrd 
 |-  ( ( ph /\ P =/= Q ) -> ( ( D + A ) _C ( D - 1 ) ) e. RR* )
127 ovexd 
 |-  ( ( ph /\ P =/= Q ) -> ( NN0 ^m ( 0 ... A ) ) e. _V )
128 127 mptexd 
 |-  ( ( ph /\ P =/= Q ) -> ( h e. ( NN0 ^m ( 0 ... A ) ) |-> ( ( ( eval1 ` K ) ` ( G ` h ) ) ` M ) ) e. _V )
129 16 128 eqeltrid 
 |-  ( ( ph /\ P =/= Q ) -> H e. _V )
130 129 imaexd 
 |-  ( ( ph /\ P =/= Q ) -> ( H " ( NN0 ^m ( 0 ... A ) ) ) e. _V )
131 hashxrcl 
 |-  ( ( H " ( NN0 ^m ( 0 ... A ) ) ) e. _V -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. RR* )
132 130 131 syl 
 |-  ( ( ph /\ P =/= Q ) -> ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. RR* )
133 eqcom 
 |-  ( D = ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) <-> ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) = D )
134 11 133 mpbi 
 |-  ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) = D
135 134 fveq2i 
 |-  ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) = ( sqrt ` D )
136 135 fveq2i 
 |-  ( |_ ` ( sqrt ` ( # ` ( L " ( E " ( NN0 X. NN0 ) ) ) ) ) ) = ( |_ ` ( sqrt ` D ) )
137 17 136 eqtri 
 |-  B = ( |_ ` ( sqrt ` D ) )
138 137 a1i 
 |-  ( ( ph /\ P =/= Q ) -> B = ( |_ ` ( sqrt ` D ) ) )
139 138 oveq2d 
 |-  ( ( ph /\ P =/= Q ) -> ( N ^ B ) = ( N ^ ( |_ ` ( sqrt ` D ) ) ) )
140 6 adantr 
 |-  ( ( ph /\ P =/= Q ) -> N e. ( ZZ>= ` 3 ) )
141 13 adantr 
 |-  ( ( ph /\ P =/= Q ) -> ( ( 2 logb N ) ^ 2 ) < ( ( odZ ` R ) ` N ) )
142 26 27 140 43 44 9 10 11 12 141 aks6d1c7lem1 
 |-  ( ( ph /\ P =/= Q ) -> ( N ^ ( |_ ` ( sqrt ` D ) ) ) < ( ( D + A ) _C ( D - 1 ) ) )
143 139 142 eqbrtrd 
 |-  ( ( ph /\ P =/= Q ) -> ( N ^ B ) < ( ( D + A ) _C ( D - 1 ) ) )
144 20 adantr 
 |-  ( ( ph /\ P =/= Q ) -> A. b e. ( 1 ... A ) ( b gcd N ) = 1 )
145 eqid 
 |-  ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) = ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) )
146 eqid 
 |-  { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } = { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) }
147 nfcv 
 |-  F/_ b U. ( ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) " h )
148 nfcv 
 |-  F/_ h U. ( ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) " b )
149 imaeq2 
 |-  ( h = b -> ( ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) " h ) = ( ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) " b ) )
150 149 unieqd 
 |-  ( h = b -> U. ( ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) " h ) = U. ( ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) " b ) )
151 147 148 150 cbvmpt 
 |-  ( h e. ( Base ` ( ZZring /s ( ZZring ~QG ( `' ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) " { ( 0g ` ( ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) |`s ran ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) ) ) } ) ) ) ) |-> U. ( ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) " h ) ) = ( b e. ( Base ` ( ZZring /s ( ZZring ~QG ( `' ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) " { ( 0g ` ( ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) |`s ran ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) ) ) } ) ) ) ) |-> U. ( ( c e. ZZ |-> ( c ( .g ` ( ( mulGrp ` K ) |`s { j e. ( Base ` ( mulGrp ` K ) ) | E. m e. ( Base ` ( mulGrp ` K ) ) ( m ( +g ` ( mulGrp ` K ) ) j ) = ( 0g ` ( mulGrp ` K ) ) } ) ) M ) ) " b ) )
152 1 2 25 26 27 42 43 44 144 21 12 9 10 88 89 90 16 11 23 145 146 151 aks6d1c6lem5 
 |-  ( ( ph /\ P =/= Q ) -> ( ( D + A ) _C ( D - 1 ) ) <_ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) )
153 116 126 132 143 152 xrltletrd 
 |-  ( ( ph /\ P =/= Q ) -> ( N ^ B ) < ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) )
154 xrltnle 
 |-  ( ( ( N ^ B ) e. RR* /\ ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) e. RR* ) -> ( ( N ^ B ) < ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <-> -. ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) ) )
155 116 132 154 syl2anc 
 |-  ( ( ph /\ P =/= Q ) -> ( ( N ^ B ) < ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <-> -. ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) ) )
156 153 155 mpbid 
 |-  ( ( ph /\ P =/= Q ) -> -. ( # ` ( H " ( NN0 ^m ( 0 ... A ) ) ) ) <_ ( N ^ B ) )
157 97 156 pm2.21dd 
 |-  ( ( ph /\ P =/= Q ) -> P = Q )
158 24 157 pm2.61dane 
 |-  ( ph -> P = Q )