MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrfi Structured version   Unicode version

Theorem dchrfi 22553
Description: The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.)
Hypotheses
Ref Expression
dchrabl.g  |-  G  =  (DChr `  N )
dchrfi.b  |-  D  =  ( Base `  G
)
Assertion
Ref Expression
dchrfi  |-  ( N  e.  NN  ->  D  e.  Fin )

Proof of Theorem dchrfi
Dummy variables  x  f  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snfi 7386 . . . 4  |-  { 0 }  e.  Fin
2 cnex 9359 . . . . . . . . 9  |-  CC  e.  _V
32a1i 11 . . . . . . . 8  |-  ( N  e.  NN  ->  CC  e.  _V )
4 ovex 6115 . . . . . . . . 9  |-  ( z ^ ( phi `  N ) )  e. 
_V
54a1i 11 . . . . . . . 8  |-  ( ( N  e.  NN  /\  z  e.  CC )  ->  ( z ^ ( phi `  N ) )  e.  _V )
6 1cnd 9398 . . . . . . . 8  |-  ( ( N  e.  NN  /\  z  e.  CC )  ->  1  e.  CC )
7 eqidd 2442 . . . . . . . 8  |-  ( N  e.  NN  ->  (
z  e.  CC  |->  ( z ^ ( phi `  N ) ) )  =  ( z  e.  CC  |->  ( z ^
( phi `  N
) ) ) )
8 fconstmpt 4878 . . . . . . . . 9  |-  ( CC 
X.  { 1 } )  =  ( z  e.  CC  |->  1 )
98a1i 11 . . . . . . . 8  |-  ( N  e.  NN  ->  ( CC  X.  { 1 } )  =  ( z  e.  CC  |->  1 ) )
103, 5, 6, 7, 9offval2 6335 . . . . . . 7  |-  ( N  e.  NN  ->  (
( z  e.  CC  |->  ( z ^ ( phi `  N ) ) )  oF  -  ( CC  X.  { 1 } ) )  =  ( z  e.  CC  |->  ( ( z ^
( phi `  N
) )  -  1 ) ) )
11 ssid 3372 . . . . . . . . . 10  |-  CC  C_  CC
1211a1i 11 . . . . . . . . 9  |-  ( N  e.  NN  ->  CC  C_  CC )
13 1cnd 9398 . . . . . . . . 9  |-  ( N  e.  NN  ->  1  e.  CC )
14 phicl 13840 . . . . . . . . . 10  |-  ( N  e.  NN  ->  ( phi `  N )  e.  NN )
1514nnnn0d 10632 . . . . . . . . 9  |-  ( N  e.  NN  ->  ( phi `  N )  e. 
NN0 )
16 plypow 21632 . . . . . . . . 9  |-  ( ( CC  C_  CC  /\  1  e.  CC  /\  ( phi `  N )  e.  NN0 )  ->  ( z  e.  CC  |->  ( z ^
( phi `  N
) ) )  e.  (Poly `  CC )
)
1712, 13, 15, 16syl3anc 1213 . . . . . . . 8  |-  ( N  e.  NN  ->  (
z  e.  CC  |->  ( z ^ ( phi `  N ) ) )  e.  (Poly `  CC ) )
18 ax-1cn 9336 . . . . . . . . 9  |-  1  e.  CC
19 plyconst 21633 . . . . . . . . 9  |-  ( ( CC  C_  CC  /\  1  e.  CC )  ->  ( CC  X.  { 1 } )  e.  (Poly `  CC ) )
2011, 18, 19mp2an 667 . . . . . . . 8  |-  ( CC 
X.  { 1 } )  e.  (Poly `  CC )
21 plysubcl 21649 . . . . . . . 8  |-  ( ( ( z  e.  CC  |->  ( z ^ ( phi `  N ) ) )  e.  (Poly `  CC )  /\  ( CC  X.  { 1 } )  e.  (Poly `  CC ) )  ->  (
( z  e.  CC  |->  ( z ^ ( phi `  N ) ) )  oF  -  ( CC  X.  { 1 } ) )  e.  (Poly `  CC )
)
2217, 20, 21sylancl 657 . . . . . . 7  |-  ( N  e.  NN  ->  (
( z  e.  CC  |->  ( z ^ ( phi `  N ) ) )  oF  -  ( CC  X.  { 1 } ) )  e.  (Poly `  CC )
)
2310, 22eqeltrrd 2516 . . . . . 6  |-  ( N  e.  NN  ->  (
z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  -  1 ) )  e.  (Poly `  CC ) )
24 0cn 9374 . . . . . . 7  |-  0  e.  CC
25 neg1ne0 10423 . . . . . . . 8  |-  -u 1  =/=  0
26140expd 12020 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  (
0 ^ ( phi `  N ) )  =  0 )
2726oveq1d 6105 . . . . . . . . . 10  |-  ( N  e.  NN  ->  (
( 0 ^ ( phi `  N ) )  -  1 )  =  ( 0  -  1 ) )
28 oveq1 6097 . . . . . . . . . . . . 13  |-  ( z  =  0  ->  (
z ^ ( phi `  N ) )  =  ( 0 ^ ( phi `  N ) ) )
2928oveq1d 6105 . . . . . . . . . . . 12  |-  ( z  =  0  ->  (
( z ^ ( phi `  N ) )  -  1 )  =  ( ( 0 ^ ( phi `  N
) )  -  1 ) )
30 eqid 2441 . . . . . . . . . . . 12  |-  ( z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  - 
1 ) )  =  ( z  e.  CC  |->  ( ( z ^
( phi `  N
) )  -  1 ) )
31 ovex 6115 . . . . . . . . . . . 12  |-  ( ( 0 ^ ( phi `  N ) )  - 
1 )  e.  _V
3229, 30, 31fvmpt 5771 . . . . . . . . . . 11  |-  ( 0  e.  CC  ->  (
( z  e.  CC  |->  ( ( z ^
( phi `  N
) )  -  1 ) ) `  0
)  =  ( ( 0 ^ ( phi `  N ) )  - 
1 ) )
3324, 32ax-mp 5 . . . . . . . . . 10  |-  ( ( z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  -  1 ) ) `
 0 )  =  ( ( 0 ^ ( phi `  N
) )  -  1 )
34 df-neg 9594 . . . . . . . . . 10  |-  -u 1  =  ( 0  -  1 )
3527, 33, 343eqtr4g 2498 . . . . . . . . 9  |-  ( N  e.  NN  ->  (
( z  e.  CC  |->  ( ( z ^
( phi `  N
) )  -  1 ) ) `  0
)  =  -u 1
)
3635neeq1d 2619 . . . . . . . 8  |-  ( N  e.  NN  ->  (
( ( z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  - 
1 ) ) ` 
0 )  =/=  0  <->  -u 1  =/=  0 ) )
3725, 36mpbiri 233 . . . . . . 7  |-  ( N  e.  NN  ->  (
( z  e.  CC  |->  ( ( z ^
( phi `  N
) )  -  1 ) ) `  0
)  =/=  0 )
38 ne0p 21634 . . . . . . 7  |-  ( ( 0  e.  CC  /\  ( ( z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  - 
1 ) ) ` 
0 )  =/=  0
)  ->  ( z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  - 
1 ) )  =/=  0p )
3924, 37, 38sylancr 658 . . . . . 6  |-  ( N  e.  NN  ->  (
z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  -  1 ) )  =/=  0p )
4030mptiniseg 5329 . . . . . . . . 9  |-  ( 0  e.  CC  ->  ( `' ( z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  - 
1 ) ) " { 0 } )  =  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  - 
1 )  =  0 } )
4124, 40ax-mp 5 . . . . . . . 8  |-  ( `' ( z  e.  CC  |->  ( ( z ^
( phi `  N
) )  -  1 ) ) " {
0 } )  =  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  - 
1 )  =  0 }
4241eqcomi 2445 . . . . . . 7  |-  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 }  =  ( `' ( z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  - 
1 ) ) " { 0 } )
4342fta1 21733 . . . . . 6  |-  ( ( ( z  e.  CC  |->  ( ( z ^
( phi `  N
) )  -  1 ) )  e.  (Poly `  CC )  /\  (
z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  -  1 ) )  =/=  0p )  ->  ( { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 }  e.  Fin  /\  ( # `  {
z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } )  <_  (deg `  (
z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  -  1 ) ) ) ) )
4423, 39, 43syl2anc 656 . . . . 5  |-  ( N  e.  NN  ->  ( { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  - 
1 )  =  0 }  e.  Fin  /\  ( # `  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } )  <_ 
(deg `  ( z  e.  CC  |->  ( ( z ^ ( phi `  N ) )  - 
1 ) ) ) ) )
4544simpld 456 . . . 4  |-  ( N  e.  NN  ->  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 }  e.  Fin )
46 unfi 7575 . . . 4  |-  ( ( { 0 }  e.  Fin  /\  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  - 
1 )  =  0 }  e.  Fin )  ->  ( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  - 
1 )  =  0 } )  e.  Fin )
471, 45, 46sylancr 658 . . 3  |-  ( N  e.  NN  ->  ( { 0 }  u.  { z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } )  e.  Fin )
48 eqid 2441 . . . 4  |-  (ℤ/n `  N
)  =  (ℤ/n `  N
)
49 eqid 2441 . . . 4  |-  ( Base `  (ℤ/n `  N ) )  =  ( Base `  (ℤ/n `  N
) )
5048, 49znfi 17951 . . 3  |-  ( N  e.  NN  ->  ( Base `  (ℤ/n `  N ) )  e. 
Fin )
51 mapfi 7603 . . 3  |-  ( ( ( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  - 
1 )  =  0 } )  e.  Fin  /\  ( Base `  (ℤ/n `  N
) )  e.  Fin )  ->  ( ( { 0 }  u.  {
z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } )  ^m  ( Base `  (ℤ/n `  N ) ) )  e.  Fin )
5247, 50, 51syl2anc 656 . 2  |-  ( N  e.  NN  ->  (
( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  - 
1 )  =  0 } )  ^m  ( Base `  (ℤ/n `  N ) ) )  e.  Fin )
53 dchrabl.g . . . . . . . 8  |-  G  =  (DChr `  N )
54 dchrfi.b . . . . . . . 8  |-  D  =  ( Base `  G
)
55 simpr 458 . . . . . . . 8  |-  ( ( N  e.  NN  /\  f  e.  D )  ->  f  e.  D )
5653, 48, 54, 49, 55dchrf 22540 . . . . . . 7  |-  ( ( N  e.  NN  /\  f  e.  D )  ->  f : ( Base `  (ℤ/n `  N ) ) --> CC )
57 ffn 5556 . . . . . . 7  |-  ( f : ( Base `  (ℤ/n `  N
) ) --> CC  ->  f  Fn  ( Base `  (ℤ/n `  N
) ) )
5856, 57syl 16 . . . . . 6  |-  ( ( N  e.  NN  /\  f  e.  D )  ->  f  Fn  ( Base `  (ℤ/n `  N ) ) )
59 df-ne 2606 . . . . . . . . . . 11  |-  ( ( f `  x )  =/=  0  <->  -.  (
f `  x )  =  0 )
60 fvex 5698 . . . . . . . . . . . 12  |-  ( f `
 x )  e. 
_V
6160elsnc 3898 . . . . . . . . . . 11  |-  ( ( f `  x )  e.  { 0 }  <-> 
( f `  x
)  =  0 )
6259, 61xchbinxr 311 . . . . . . . . . 10  |-  ( ( f `  x )  =/=  0  <->  -.  (
f `  x )  e.  { 0 } )
63 simpl 454 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( Base `  (ℤ/n `  N ) )  /\  ( f `  x
)  =/=  0 )  ->  x  e.  (
Base `  (ℤ/n `  N ) ) )
64 ffvelrn 5838 . . . . . . . . . . . . 13  |-  ( ( f : ( Base `  (ℤ/n `  N ) ) --> CC 
/\  x  e.  (
Base `  (ℤ/n `  N ) ) )  ->  ( f `  x )  e.  CC )
6556, 63, 64syl2an 474 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( f `  x
)  e.  CC )
6653, 48, 54dchrmhm 22539 . . . . . . . . . . . . . . . . . 18  |-  D  C_  ( (mulGrp `  (ℤ/n `  N ) ) MndHom  (mulGrp ` fld ) )
67 simplr 749 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
f  e.  D )
6866, 67sseldi 3351 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
f  e.  ( (mulGrp `  (ℤ/n `  N ) ) MndHom  (mulGrp ` fld ) ) )
6915ad2antrr 720 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( phi `  N
)  e.  NN0 )
70 simprl 750 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  ->  x  e.  ( Base `  (ℤ/n `  N ) ) )
71 eqid 2441 . . . . . . . . . . . . . . . . . . 19  |-  (mulGrp `  (ℤ/n `  N ) )  =  (mulGrp `  (ℤ/n `  N ) )
7271, 49mgpbas 16587 . . . . . . . . . . . . . . . . . 18  |-  ( Base `  (ℤ/n `  N ) )  =  ( Base `  (mulGrp `  (ℤ/n `  N ) ) )
73 eqid 2441 . . . . . . . . . . . . . . . . . 18  |-  (.g `  (mulGrp `  (ℤ/n `  N ) ) )  =  (.g `  (mulGrp `  (ℤ/n `  N
) ) )
74 eqid 2441 . . . . . . . . . . . . . . . . . 18  |-  (.g `  (mulGrp ` fld ) )  =  (.g `  (mulGrp ` fld ) )
7572, 73, 74mhmmulg 15652 . . . . . . . . . . . . . . . . 17  |-  ( ( f  e.  ( (mulGrp `  (ℤ/n `  N ) ) MndHom  (mulGrp ` fld ) )  /\  ( phi `  N )  e.  NN0  /\  x  e.  ( Base `  (ℤ/n `  N ) ) )  ->  ( f `  ( ( phi `  N ) (.g `  (mulGrp `  (ℤ/n `  N ) ) ) x ) )  =  ( ( phi `  N ) (.g `  (mulGrp ` fld ) ) ( f `  x ) ) )
7668, 69, 70, 75syl3anc 1213 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( f `  (
( phi `  N
) (.g `  (mulGrp `  (ℤ/n `  N
) ) ) x ) )  =  ( ( phi `  N
) (.g `  (mulGrp ` fld ) ) ( f `
 x ) ) )
77 nnnn0 10582 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  NN  ->  N  e.  NN0 )
7848zncrng 17936 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  NN0  ->  (ℤ/n `  N
)  e.  CRing )
7977, 78syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  NN  ->  (ℤ/n `  N
)  e.  CRing )
80 crngrng 16645 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (ℤ/n `  N )  e.  CRing  -> 
(ℤ/n `  N )  e.  Ring )
8179, 80syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  NN  ->  (ℤ/n `  N
)  e.  Ring )
8281ad2antrr 720 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
(ℤ/n `  N )  e.  Ring )
83 eqid 2441 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (Unit `  (ℤ/n `  N ) )  =  (Unit `  (ℤ/n `  N ) )
84 eqid 2441 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) )  =  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) )
8583, 84unitgrp 16749 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (ℤ/n `  N )  e.  Ring  -> 
( (mulGrp `  (ℤ/n `  N
) )s  (Unit `  (ℤ/n `  N ) ) )  e.  Grp )
8682, 85syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( (mulGrp `  (ℤ/n `  N
) )s  (Unit `  (ℤ/n `  N ) ) )  e.  Grp )
8748, 83znunithash 17956 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  NN  ->  ( # `
 (Unit `  (ℤ/n `  N
) ) )  =  ( phi `  N
) )
8887, 15eqeltrd 2515 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  NN  ->  ( # `
 (Unit `  (ℤ/n `  N
) ) )  e. 
NN0 )
89 fvex 5698 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (Unit `  (ℤ/n `  N ) )  e. 
_V
90 hashclb 12124 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (Unit `  (ℤ/n `  N ) )  e. 
_V  ->  ( (Unit `  (ℤ/n `  N ) )  e. 
Fin 
<->  ( # `  (Unit `  (ℤ/n `  N ) ) )  e.  NN0 ) )
9189, 90ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (Unit `  (ℤ/n `  N ) )  e. 
Fin 
<->  ( # `  (Unit `  (ℤ/n `  N ) ) )  e.  NN0 )
9288, 91sylibr 212 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN  ->  (Unit `  (ℤ/n `  N ) )  e. 
Fin )
9392ad2antrr 720 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
(Unit `  (ℤ/n `  N ) )  e. 
Fin )
94 simprr 751 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( f `  x
)  =/=  0 )
9553, 48, 54, 49, 83, 67, 70dchrn0 22548 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( f `  x )  =/=  0  <->  x  e.  (Unit `  (ℤ/n `  N
) ) ) )
9694, 95mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  ->  x  e.  (Unit `  (ℤ/n `  N
) ) )
9783, 84unitgrpbas 16748 . . . . . . . . . . . . . . . . . . . . . 22  |-  (Unit `  (ℤ/n `  N ) )  =  ( Base `  (
(mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) )
98 eqid 2441 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( od
`  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) )  =  ( od
`  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) )
9997, 98oddvds2 16060 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( (mulGrp `  (ℤ/n `  N
) )s  (Unit `  (ℤ/n `  N ) ) )  e.  Grp  /\  (Unit `  (ℤ/n `  N ) )  e. 
Fin  /\  x  e.  (Unit `  (ℤ/n `  N ) ) )  ->  ( ( od
`  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) `  x ) 
||  ( # `  (Unit `  (ℤ/n `  N ) ) ) )
10086, 93, 96, 99syl3anc 1213 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( od `  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) `  x ) 
||  ( # `  (Unit `  (ℤ/n `  N ) ) ) )
10187ad2antrr 720 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( # `  (Unit `  (ℤ/n `  N ) ) )  =  ( phi `  N ) )
102100, 101breqtrd 4313 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( od `  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) `  x ) 
||  ( phi `  N ) )
10314ad2antrr 720 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( phi `  N
)  e.  NN )
104103nnzd 10742 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( phi `  N
)  e.  ZZ )
105 eqid 2441 . . . . . . . . . . . . . . . . . . . . 21  |-  (.g `  (
(mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) )  =  (.g `  (
(mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) )
106 eqid 2441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 0g
`  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) )  =  ( 0g
`  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) )
10797, 98, 105, 106oddvds 16043 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( (mulGrp `  (ℤ/n `  N
) )s  (Unit `  (ℤ/n `  N ) ) )  e.  Grp  /\  x  e.  (Unit `  (ℤ/n `  N ) )  /\  ( phi `  N )  e.  ZZ )  -> 
( ( ( od
`  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) `  x ) 
||  ( phi `  N )  <->  ( ( phi `  N ) (.g `  ( (mulGrp `  (ℤ/n `  N
) )s  (Unit `  (ℤ/n `  N ) ) ) ) x )  =  ( 0g `  (
(mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) ) )
10886, 96, 104, 107syl3anc 1213 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( ( od
`  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) `  x ) 
||  ( phi `  N )  <->  ( ( phi `  N ) (.g `  ( (mulGrp `  (ℤ/n `  N
) )s  (Unit `  (ℤ/n `  N ) ) ) ) x )  =  ( 0g `  (
(mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) ) )
109102, 108mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( phi `  N ) (.g `  (
(mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) x )  =  ( 0g `  (
(mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) )
11083, 71unitsubm 16752 . . . . . . . . . . . . . . . . . . . 20  |-  ( (ℤ/n `  N )  e.  Ring  -> 
(Unit `  (ℤ/n `  N ) )  e.  (SubMnd `  (mulGrp `  (ℤ/n `  N
) ) ) )
11182, 110syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
(Unit `  (ℤ/n `  N ) )  e.  (SubMnd `  (mulGrp `  (ℤ/n `  N
) ) ) )
11273, 84, 105submmulg 15655 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (Unit `  (ℤ/n `  N ) )  e.  (SubMnd `  (mulGrp `  (ℤ/n `  N
) ) )  /\  ( phi `  N )  e.  NN0  /\  x  e.  (Unit `  (ℤ/n `  N ) ) )  ->  ( ( phi `  N ) (.g `  (mulGrp `  (ℤ/n `  N ) ) ) x )  =  ( ( phi `  N
) (.g `  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) x ) )
113111, 69, 96, 112syl3anc 1213 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( phi `  N ) (.g `  (mulGrp `  (ℤ/n `  N ) ) ) x )  =  ( ( phi `  N
) (.g `  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) x ) )
114 eqid 2441 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 1r
`  (ℤ/n `  N ) )  =  ( 1r `  (ℤ/n `  N
) )
11571, 114rngidval 16595 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1r
`  (ℤ/n `  N ) )  =  ( 0g `  (mulGrp `  (ℤ/n `  N ) ) )
11684, 115subm0 15479 . . . . . . . . . . . . . . . . . . 19  |-  ( (Unit `  (ℤ/n `  N ) )  e.  (SubMnd `  (mulGrp `  (ℤ/n `  N
) ) )  -> 
( 1r `  (ℤ/n `  N
) )  =  ( 0g `  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) )
117111, 116syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( 1r `  (ℤ/n `  N
) )  =  ( 0g `  ( (mulGrp `  (ℤ/n `  N ) )s  (Unit `  (ℤ/n `  N ) ) ) ) )
118109, 113, 1173eqtr4d 2483 . . . . . . . . . . . . . . . . 17  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( phi `  N ) (.g `  (mulGrp `  (ℤ/n `  N ) ) ) x )  =  ( 1r `  (ℤ/n `  N
) ) )
119118fveq2d 5692 . . . . . . . . . . . . . . . 16  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( f `  (
( phi `  N
) (.g `  (mulGrp `  (ℤ/n `  N
) ) ) x ) )  =  ( f `  ( 1r
`  (ℤ/n `  N ) ) ) )
12076, 119eqtr3d 2475 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( phi `  N ) (.g `  (mulGrp ` fld ) ) ( f `  x ) )  =  ( f `  ( 1r `  (ℤ/n `  N ) ) ) )
121 cnfldexp 17808 . . . . . . . . . . . . . . . 16  |-  ( ( ( f `  x
)  e.  CC  /\  ( phi `  N )  e.  NN0 )  -> 
( ( phi `  N ) (.g `  (mulGrp ` fld ) ) ( f `  x ) )  =  ( ( f `  x ) ^ ( phi `  N ) ) )
12265, 69, 121syl2anc 656 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( phi `  N ) (.g `  (mulGrp ` fld ) ) ( f `  x ) )  =  ( ( f `  x ) ^ ( phi `  N ) ) )
123 eqid 2441 . . . . . . . . . . . . . . . . . 18  |-  (mulGrp ` fld )  =  (mulGrp ` fld )
124 cnfld1 17800 . . . . . . . . . . . . . . . . . 18  |-  1  =  ( 1r ` fld )
125123, 124rngidval 16595 . . . . . . . . . . . . . . . . 17  |-  1  =  ( 0g `  (mulGrp ` fld ) )
126115, 125mhm0 15468 . . . . . . . . . . . . . . . 16  |-  ( f  e.  ( (mulGrp `  (ℤ/n `  N ) ) MndHom  (mulGrp ` fld ) )  ->  ( f `  ( 1r `  (ℤ/n `  N
) ) )  =  1 )
12768, 126syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( f `  ( 1r `  (ℤ/n `  N ) ) )  =  1 )
128120, 122, 1273eqtr3d 2481 . . . . . . . . . . . . . 14  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( f `  x ) ^ ( phi `  N ) )  =  1 )
129128oveq1d 6105 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( ( f `
 x ) ^
( phi `  N
) )  -  1 )  =  ( 1  -  1 ) )
130 1m1e0 10386 . . . . . . . . . . . . 13  |-  ( 1  -  1 )  =  0
131129, 130syl6eq 2489 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( ( ( f `
 x ) ^
( phi `  N
) )  -  1 )  =  0 )
132 oveq1 6097 . . . . . . . . . . . . . . 15  |-  ( z  =  ( f `  x )  ->  (
z ^ ( phi `  N ) )  =  ( ( f `  x ) ^ ( phi `  N ) ) )
133132oveq1d 6105 . . . . . . . . . . . . . 14  |-  ( z  =  ( f `  x )  ->  (
( z ^ ( phi `  N ) )  -  1 )  =  ( ( ( f `
 x ) ^
( phi `  N
) )  -  1 ) )
134133eqeq1d 2449 . . . . . . . . . . . . 13  |-  ( z  =  ( f `  x )  ->  (
( ( z ^
( phi `  N
) )  -  1 )  =  0  <->  (
( ( f `  x ) ^ ( phi `  N ) )  -  1 )  =  0 ) )
135134elrab 3114 . . . . . . . . . . . 12  |-  ( ( f `  x )  e.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  - 
1 )  =  0 }  <->  ( ( f `
 x )  e.  CC  /\  ( ( ( f `  x
) ^ ( phi `  N ) )  - 
1 )  =  0 ) )
13665, 131, 135sylanbrc 659 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  ( x  e.  ( Base `  (ℤ/n `  N
) )  /\  (
f `  x )  =/=  0 ) )  -> 
( f `  x
)  e.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } )
137136expr 612 . . . . . . . . . 10  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  x  e.  (
Base `  (ℤ/n `  N ) ) )  ->  ( ( f `
 x )  =/=  0  ->  ( f `  x )  e.  {
z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } ) )
13862, 137syl5bir 218 . . . . . . . . 9  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  x  e.  (
Base `  (ℤ/n `  N ) ) )  ->  ( -.  (
f `  x )  e.  { 0 }  ->  ( f `  x )  e.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  - 
1 )  =  0 } ) )
139138orrd 378 . . . . . . . 8  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  x  e.  (
Base `  (ℤ/n `  N ) ) )  ->  ( ( f `
 x )  e. 
{ 0 }  \/  ( f `  x
)  e.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } ) )
140 elun 3494 . . . . . . . 8  |-  ( ( f `  x )  e.  ( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } )  <->  ( (
f `  x )  e.  { 0 }  \/  ( f `  x
)  e.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } ) )
141139, 140sylibr 212 . . . . . . 7  |-  ( ( ( N  e.  NN  /\  f  e.  D )  /\  x  e.  (
Base `  (ℤ/n `  N ) ) )  ->  ( f `  x )  e.  ( { 0 }  u.  { z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } ) )
142141ralrimiva 2797 . . . . . 6  |-  ( ( N  e.  NN  /\  f  e.  D )  ->  A. x  e.  (
Base `  (ℤ/n `  N ) ) ( f `  x )  e.  ( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } ) )
143 ffnfv 5866 . . . . . 6  |-  ( f : ( Base `  (ℤ/n `  N
) ) --> ( { 0 }  u.  {
z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } )  <->  ( f  Fn  ( Base `  (ℤ/n `  N
) )  /\  A. x  e.  ( Base `  (ℤ/n `  N ) ) ( f `  x )  e.  ( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } ) ) )
14458, 142, 143sylanbrc 659 . . . . 5  |-  ( ( N  e.  NN  /\  f  e.  D )  ->  f : ( Base `  (ℤ/n `  N ) ) --> ( { 0 }  u.  { z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } ) )
145144ex 434 . . . 4  |-  ( N  e.  NN  ->  (
f  e.  D  -> 
f : ( Base `  (ℤ/n `  N ) ) --> ( { 0 }  u.  { z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } ) ) )
146 elmapg 7223 . . . . 5  |-  ( ( ( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  - 
1 )  =  0 } )  e.  Fin  /\  ( Base `  (ℤ/n `  N
) )  e.  Fin )  ->  ( f  e.  ( ( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } )  ^m  ( Base `  (ℤ/n `  N ) ) )  <-> 
f : ( Base `  (ℤ/n `  N ) ) --> ( { 0 }  u.  { z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } ) ) )
14747, 50, 146syl2anc 656 . . . 4  |-  ( N  e.  NN  ->  (
f  e.  ( ( { 0 }  u.  { z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } )  ^m  ( Base `  (ℤ/n `  N ) ) )  <-> 
f : ( Base `  (ℤ/n `  N ) ) --> ( { 0 }  u.  { z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } ) ) )
148145, 147sylibrd 234 . . 3  |-  ( N  e.  NN  ->  (
f  e.  D  -> 
f  e.  ( ( { 0 }  u.  { z  e.  CC  | 
( ( z ^
( phi `  N
) )  -  1 )  =  0 } )  ^m  ( Base `  (ℤ/n `  N ) ) ) ) )
149148ssrdv 3359 . 2  |-  ( N  e.  NN  ->  D  C_  ( ( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } )  ^m  ( Base `  (ℤ/n `  N ) ) ) )
150 ssfi 7529 . 2  |-  ( ( ( ( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } )  ^m  ( Base `  (ℤ/n `  N ) ) )  e.  Fin  /\  D  C_  ( ( { 0 }  u.  { z  e.  CC  |  ( ( z ^ ( phi `  N ) )  -  1 )  =  0 } )  ^m  ( Base `  (ℤ/n `  N ) ) ) )  ->  D  e.  Fin )
15152, 149, 150syl2anc 656 1  |-  ( N  e.  NN  ->  D  e.  Fin )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1364    e. wcel 1761    =/= wne 2604   A.wral 2713   {crab 2717   _Vcvv 2970    u. cun 3323    C_ wss 3325   {csn 3874   class class class wbr 4289    e. cmpt 4347    X. cxp 4834   `'ccnv 4835   "cima 4839    Fn wfn 5410   -->wf 5411   ` cfv 5415  (class class class)co 6090    oFcof 6317    ^m cmap 7210   Fincfn 7306   CCcc 9276   0cc0 9278   1c1 9279    <_ cle 9415    - cmin 9591   -ucneg 9592   NNcn 10318   NN0cn0 10575   ZZcz 10642   ^cexp 11861   #chash 12099    || cdivides 13531   phicphi 13835   Basecbs 14170   ↾s cress 14171   0gc0g 14374   Grpcgrp 15406  .gcmg 15410   MndHom cmhm 15458  SubMndcsubmnd 15459   odcod 16021  mulGrpcmgp 16581   1rcur 16593   Ringcrg 16635   CRingccrg 16636  Unitcui 16721  ℂfldccnfld 17777  ℤ/nczn 17893   0pc0p 21106  Polycply 21611  degcdgr 21614  DChrcdchr 22530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355  ax-pre-sup 9356  ax-addf 9357  ax-mulf 9358
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-disj 4260  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-of 6319  df-om 6476  df-1st 6576  df-2nd 6577  df-tpos 6744  df-recs 6828  df-rdg 6862  df-1o 6916  df-2o 6917  df-oadd 6920  df-omul 6921  df-er 7097  df-ec 7099  df-qs 7103  df-map 7212  df-pm 7213  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-sup 7687  df-oi 7720  df-card 8105  df-acn 8108  df-cda 8333  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-div 9990  df-nn 10319  df-2 10376  df-3 10377  df-4 10378  df-5 10379  df-6 10380  df-7 10381  df-8 10382  df-9 10383  df-10 10384  df-n0 10576  df-z 10643  df-dec 10752  df-uz 10858  df-rp 10988  df-fz 11434  df-fzo 11545  df-fl 11638  df-mod 11705  df-seq 11803  df-exp 11862  df-hash 12100  df-cj 12584  df-re 12585  df-im 12586  df-sqr 12720  df-abs 12721  df-clim 12962  df-rlim 12963  df-sum 13160  df-dvds 13532  df-gcd 13687  df-phi 13837  df-struct 14172  df-ndx 14173  df-slot 14174  df-base 14175  df-sets 14176  df-ress 14177  df-plusg 14247  df-mulr 14248  df-starv 14249  df-sca 14250  df-vsca 14251  df-ip 14252  df-tset 14253  df-ple 14254  df-ds 14256  df-unif 14257  df-0g 14376  df-imas 14442  df-divs 14443  df-mnd 15411  df-mhm 15460  df-submnd 15461  df-grp 15538  df-minusg 15539  df-sbg 15540  df-mulg 15541  df-subg 15671  df-nsg 15672  df-eqg 15673  df-ghm 15738  df-od 16025  df-cmn 16272  df-abl 16273  df-mgp 16582  df-ur 16594  df-rng 16637  df-cring 16638  df-oppr 16705  df-dvdsr 16723  df-unit 16724  df-invr 16754  df-rnghom 16796  df-subrg 16843  df-lmod 16930  df-lss 16992  df-lsp 17031  df-sra 17231  df-rgmod 17232  df-lidl 17233  df-rsp 17234  df-2idl 17292  df-cnfld 17778  df-zring 17843  df-zrh 17894  df-zn 17897  df-0p 21107  df-ply 21615  df-idp 21616  df-coe 21617  df-dgr 21618  df-quot 21716  df-dchr 22531
This theorem is referenced by:  sumdchr2  22568  dchrhash  22569  rpvmasum2  22720  dchrisum0re  22721
  Copyright terms: Public domain W3C validator