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

Theorem wilthlem3 22297
Description: Lemma for wilth 22298. Here we round out the argument of wilthlem2 22296 with the final step of the induction. The induction argument shows that every subset of  1 ... ( P  -  1 ) that is closed under inverse and contains  P  -  1 multiplies to  -u 1  mod  P, and clearly  1 ... ( P  -  1 ) itself is such a set. Thus, the product of all the elements is  -u 1, and all that is left is to translate the group sum notation (which we used for its unordered summing capabilities) into an ordered sequence to match the definition of the factorial. (Contributed by Mario Carneiro, 24-Jan-2015.) (Proof shortened by AV, 27-Jul-2019.)
Hypotheses
Ref Expression
wilthlem.t  |-  T  =  (mulGrp ` fld )
wilthlem.a  |-  A  =  { x  e.  ~P ( 1 ... ( P  -  1 ) )  |  ( ( P  -  1 )  e.  x  /\  A. y  e.  x  (
( y ^ ( P  -  2 ) )  mod  P )  e.  x ) }
Assertion
Ref Expression
wilthlem3  |-  ( P  e.  Prime  ->  P  ||  ( ( ! `  ( P  -  1
) )  +  1 ) )
Distinct variable groups:    x, y, A    x, P, y    x, T, y

Proof of Theorem wilthlem3
Dummy variables  t 
s  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prmuz2 13768 . . . . . . . 8  |-  ( P  e.  Prime  ->  P  e.  ( ZZ>= `  2 )
)
2 uz2m1nn 10921 . . . . . . . 8  |-  ( P  e.  ( ZZ>= `  2
)  ->  ( P  -  1 )  e.  NN )
31, 2syl 16 . . . . . . 7  |-  ( P  e.  Prime  ->  ( P  -  1 )  e.  NN )
4 nnuz 10888 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
53, 4syl6eleq 2527 . . . . . 6  |-  ( P  e.  Prime  ->  ( P  -  1 )  e.  ( ZZ>= `  1 )
)
6 eluzfz2 11450 . . . . . 6  |-  ( ( P  -  1 )  e.  ( ZZ>= `  1
)  ->  ( P  -  1 )  e.  ( 1 ... ( P  -  1 ) ) )
75, 6syl 16 . . . . 5  |-  ( P  e.  Prime  ->  ( P  -  1 )  e.  ( 1 ... ( P  -  1 ) ) )
8 simpl 454 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  y  e.  ( 1 ... ( P  -  1 ) ) )  ->  P  e.  Prime )
9 elfzelz 11444 . . . . . . . . 9  |-  ( y  e.  ( 1 ... ( P  -  1 ) )  ->  y  e.  ZZ )
109adantl 463 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  y  e.  ( 1 ... ( P  -  1 ) ) )  ->  y  e.  ZZ )
11 prmnn 13753 . . . . . . . . 9  |-  ( P  e.  Prime  ->  P  e.  NN )
12 fzm1ndvds 13572 . . . . . . . . 9  |-  ( ( P  e.  NN  /\  y  e.  ( 1 ... ( P  - 
1 ) ) )  ->  -.  P  ||  y
)
1311, 12sylan 468 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  y  e.  ( 1 ... ( P  -  1 ) ) )  ->  -.  P  ||  y )
14 eqid 2437 . . . . . . . . 9  |-  ( ( y ^ ( P  -  2 ) )  mod  P )  =  ( ( y ^
( P  -  2 ) )  mod  P
)
1514prmdiv 13847 . . . . . . . 8  |-  ( ( P  e.  Prime  /\  y  e.  ZZ  /\  -.  P  ||  y )  ->  (
( ( y ^
( P  -  2 ) )  mod  P
)  e.  ( 1 ... ( P  - 
1 ) )  /\  P  ||  ( ( y  x.  ( ( y ^ ( P  - 
2 ) )  mod 
P ) )  - 
1 ) ) )
168, 10, 13, 15syl3anc 1213 . . . . . . 7  |-  ( ( P  e.  Prime  /\  y  e.  ( 1 ... ( P  -  1 ) ) )  ->  (
( ( y ^
( P  -  2 ) )  mod  P
)  e.  ( 1 ... ( P  - 
1 ) )  /\  P  ||  ( ( y  x.  ( ( y ^ ( P  - 
2 ) )  mod 
P ) )  - 
1 ) ) )
1716simpld 456 . . . . . 6  |-  ( ( P  e.  Prime  /\  y  e.  ( 1 ... ( P  -  1 ) ) )  ->  (
( y ^ ( P  -  2 ) )  mod  P )  e.  ( 1 ... ( P  -  1 ) ) )
1817ralrimiva 2793 . . . . 5  |-  ( P  e.  Prime  ->  A. y  e.  ( 1 ... ( P  -  1 ) ) ( ( y ^ ( P  - 
2 ) )  mod 
P )  e.  ( 1 ... ( P  -  1 ) ) )
19 ovex 6109 . . . . . . 7  |-  ( 1 ... ( P  - 
1 ) )  e. 
_V
2019pwid 3866 . . . . . 6  |-  ( 1 ... ( P  - 
1 ) )  e. 
~P ( 1 ... ( P  -  1 ) )
21 eleq2 2498 . . . . . . . 8  |-  ( x  =  ( 1 ... ( P  -  1 ) )  ->  (
( P  -  1 )  e.  x  <->  ( P  -  1 )  e.  ( 1 ... ( P  -  1 ) ) ) )
22 eleq2 2498 . . . . . . . . 9  |-  ( x  =  ( 1 ... ( P  -  1 ) )  ->  (
( ( y ^
( P  -  2 ) )  mod  P
)  e.  x  <->  ( (
y ^ ( P  -  2 ) )  mod  P )  e.  ( 1 ... ( P  -  1 ) ) ) )
2322raleqbi1dv 2919 . . . . . . . 8  |-  ( x  =  ( 1 ... ( P  -  1 ) )  ->  ( A. y  e.  x  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  x  <->  A. y  e.  ( 1 ... ( P  -  1 ) ) ( ( y ^ ( P  - 
2 ) )  mod 
P )  e.  ( 1 ... ( P  -  1 ) ) ) )
2421, 23anbi12d 705 . . . . . . 7  |-  ( x  =  ( 1 ... ( P  -  1 ) )  ->  (
( ( P  - 
1 )  e.  x  /\  A. y  e.  x  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  x )  <-> 
( ( P  - 
1 )  e.  ( 1 ... ( P  -  1 ) )  /\  A. y  e.  ( 1 ... ( P  -  1 ) ) ( ( y ^ ( P  - 
2 ) )  mod 
P )  e.  ( 1 ... ( P  -  1 ) ) ) ) )
25 wilthlem.a . . . . . . 7  |-  A  =  { x  e.  ~P ( 1 ... ( P  -  1 ) )  |  ( ( P  -  1 )  e.  x  /\  A. y  e.  x  (
( y ^ ( P  -  2 ) )  mod  P )  e.  x ) }
2624, 25elrab2 3112 . . . . . 6  |-  ( ( 1 ... ( P  -  1 ) )  e.  A  <->  ( (
1 ... ( P  - 
1 ) )  e. 
~P ( 1 ... ( P  -  1 ) )  /\  (
( P  -  1 )  e.  ( 1 ... ( P  - 
1 ) )  /\  A. y  e.  ( 1 ... ( P  - 
1 ) ) ( ( y ^ ( P  -  2 ) )  mod  P )  e.  ( 1 ... ( P  -  1 ) ) ) ) )
2720, 26mpbiran 904 . . . . 5  |-  ( ( 1 ... ( P  -  1 ) )  e.  A  <->  ( ( P  -  1 )  e.  ( 1 ... ( P  -  1 ) )  /\  A. y  e.  ( 1 ... ( P  - 
1 ) ) ( ( y ^ ( P  -  2 ) )  mod  P )  e.  ( 1 ... ( P  -  1 ) ) ) )
287, 18, 27sylanbrc 659 . . . 4  |-  ( P  e.  Prime  ->  ( 1 ... ( P  - 
1 ) )  e.  A )
29 fzfi 11782 . . . . 5  |-  ( 1 ... ( P  - 
1 ) )  e. 
Fin
30 eleq1 2497 . . . . . . . 8  |-  ( s  =  t  ->  (
s  e.  A  <->  t  e.  A ) )
31 reseq2 5096 . . . . . . . . . . 11  |-  ( s  =  t  ->  (  _I  |`  s )  =  (  _I  |`  t
) )
3231oveq2d 6100 . . . . . . . . . 10  |-  ( s  =  t  ->  ( T  gsumg  (  _I  |`  s
) )  =  ( T  gsumg  (  _I  |`  t
) ) )
3332oveq1d 6099 . . . . . . . . 9  |-  ( s  =  t  ->  (
( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( ( T  gsumg  (  _I  |`  t
) )  mod  P
) )
3433eqeq1d 2445 . . . . . . . 8  |-  ( s  =  t  ->  (
( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
)  <->  ( ( T 
gsumg  (  _I  |`  t ) )  mod  P )  =  ( -u 1  mod  P ) ) )
3530, 34imbi12d 320 . . . . . . 7  |-  ( s  =  t  ->  (
( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) )  <->  ( t  e.  A  ->  ( ( T  gsumg  (  _I  |`  t
) )  mod  P
)  =  ( -u
1  mod  P )
) ) )
3635imbi2d 316 . . . . . 6  |-  ( s  =  t  ->  (
( P  e.  Prime  -> 
( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) )  <->  ( P  e.  Prime  ->  ( t  e.  A  ->  ( ( T  gsumg  (  _I  |`  t
) )  mod  P
)  =  ( -u
1  mod  P )
) ) ) )
37 eleq1 2497 . . . . . . . 8  |-  ( s  =  ( 1 ... ( P  -  1 ) )  ->  (
s  e.  A  <->  ( 1 ... ( P  - 
1 ) )  e.  A ) )
38 reseq2 5096 . . . . . . . . . . 11  |-  ( s  =  ( 1 ... ( P  -  1 ) )  ->  (  _I  |`  s )  =  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )
3938oveq2d 6100 . . . . . . . . . 10  |-  ( s  =  ( 1 ... ( P  -  1 ) )  ->  ( T  gsumg  (  _I  |`  s
) )  =  ( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) ) )
4039oveq1d 6099 . . . . . . . . 9  |-  ( s  =  ( 1 ... ( P  -  1 ) )  ->  (
( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( ( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  mod  P ) )
4140eqeq1d 2445 . . . . . . . 8  |-  ( s  =  ( 1 ... ( P  -  1 ) )  ->  (
( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
)  <->  ( ( T 
gsumg  (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) )  mod  P )  =  ( -u 1  mod  P ) ) )
4237, 41imbi12d 320 . . . . . . 7  |-  ( s  =  ( 1 ... ( P  -  1 ) )  ->  (
( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) )  <->  ( (
1 ... ( P  - 
1 ) )  e.  A  ->  ( ( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  mod  P )  =  ( -u 1  mod  P ) ) ) )
4342imbi2d 316 . . . . . 6  |-  ( s  =  ( 1 ... ( P  -  1 ) )  ->  (
( P  e.  Prime  -> 
( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) )  <->  ( P  e.  Prime  ->  ( (
1 ... ( P  - 
1 ) )  e.  A  ->  ( ( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  mod  P )  =  ( -u 1  mod  P ) ) ) ) )
44 bi2.04 361 . . . . . . . . . . . 12  |-  ( ( s  C.  t  ->  ( P  e.  Prime  ->  ( s  e.  A  -> 
( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) ) )  <-> 
( P  e.  Prime  -> 
( s  C.  t  ->  ( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) ) ) )
45 pm2.27 39 . . . . . . . . . . . . 13  |-  ( P  e.  Prime  ->  ( ( P  e.  Prime  ->  ( s  C.  t  ->  ( s  e.  A  -> 
( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) ) )  ->  ( s  C.  t  ->  ( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) ) ) )
4645com34 83 . . . . . . . . . . . 12  |-  ( P  e.  Prime  ->  ( ( P  e.  Prime  ->  ( s  C.  t  ->  ( s  e.  A  -> 
( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) ) )  ->  ( s  e.  A  ->  ( s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) ) ) )
4744, 46syl5bi 217 . . . . . . . . . . 11  |-  ( P  e.  Prime  ->  ( ( s  C.  t  ->  ( P  e.  Prime  ->  ( s  e.  A  -> 
( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) ) )  ->  ( s  e.  A  ->  ( s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) ) ) )
4847alimdv 1676 . . . . . . . . . 10  |-  ( P  e.  Prime  ->  ( A. s ( s  C.  t  ->  ( P  e. 
Prime  ->  ( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) ) )  ->  A. s ( s  e.  A  ->  ( s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) ) ) )
49 df-ral 2714 . . . . . . . . . 10  |-  ( A. s  e.  A  (
s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
)  <->  A. s ( s  e.  A  ->  (
s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) ) )
5048, 49syl6ibr 227 . . . . . . . . 9  |-  ( P  e.  Prime  ->  ( A. s ( s  C.  t  ->  ( P  e. 
Prime  ->  ( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) ) )  ->  A. s  e.  A  ( s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) ) )
5150com12 31 . . . . . . . 8  |-  ( A. s ( s  C.  t  ->  ( P  e. 
Prime  ->  ( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) ) )  -> 
( P  e.  Prime  ->  A. s  e.  A  ( s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) ) )
52 wilthlem.t . . . . . . . . . 10  |-  T  =  (mulGrp ` fld )
53 simp1 983 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  A. s  e.  A  (
s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
)  /\  t  e.  A )  ->  P  e.  Prime )
54 simp3 985 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  A. s  e.  A  (
s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
)  /\  t  e.  A )  ->  t  e.  A )
55 simp2 984 . . . . . . . . . 10  |-  ( ( P  e.  Prime  /\  A. s  e.  A  (
s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
)  /\  t  e.  A )  ->  A. s  e.  A  ( s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) )
5652, 25, 53, 54, 55wilthlem2 22296 . . . . . . . . 9  |-  ( ( P  e.  Prime  /\  A. s  e.  A  (
s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
)  /\  t  e.  A )  ->  (
( T  gsumg  (  _I  |`  t
) )  mod  P
)  =  ( -u
1  mod  P )
)
57563exp 1181 . . . . . . . 8  |-  ( P  e.  Prime  ->  ( A. s  e.  A  (
s  C.  t  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
)  ->  ( t  e.  A  ->  ( ( T  gsumg  (  _I  |`  t
) )  mod  P
)  =  ( -u
1  mod  P )
) ) )
5851, 57sylcom 29 . . . . . . 7  |-  ( A. s ( s  C.  t  ->  ( P  e. 
Prime  ->  ( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) ) )  -> 
( P  e.  Prime  -> 
( t  e.  A  ->  ( ( T  gsumg  (  _I  |`  t ) )  mod 
P )  =  (
-u 1  mod  P
) ) ) )
5958a1i 11 . . . . . 6  |-  ( t  e.  Fin  ->  ( A. s ( s  C.  t  ->  ( P  e. 
Prime  ->  ( s  e.  A  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) ) )  -> 
( P  e.  Prime  -> 
( t  e.  A  ->  ( ( T  gsumg  (  _I  |`  t ) )  mod 
P )  =  (
-u 1  mod  P
) ) ) ) )
6036, 43, 59findcard3 7547 . . . . 5  |-  ( ( 1 ... ( P  -  1 ) )  e.  Fin  ->  ( P  e.  Prime  ->  (
( 1 ... ( P  -  1 ) )  e.  A  -> 
( ( T  gsumg  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) )  mod 
P )  =  (
-u 1  mod  P
) ) ) )
6129, 60ax-mp 5 . . . 4  |-  ( P  e.  Prime  ->  ( ( 1 ... ( P  -  1 ) )  e.  A  ->  (
( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  mod  P )  =  ( -u 1  mod  P ) ) )
6228, 61mpd 15 . . 3  |-  ( P  e.  Prime  ->  ( ( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  mod  P )  =  ( -u 1  mod  P ) )
63 cnfld1 17689 . . . . . 6  |-  1  =  ( 1r ` fld )
6452, 63rngidval 16587 . . . . 5  |-  1  =  ( 0g `  T )
65 cncrng 17685 . . . . . 6  |-fld  e.  CRing
6652crngmgp 16593 . . . . . 6  |-  (fld  e.  CRing  ->  T  e. CMnd )
6765, 66mp1i 12 . . . . 5  |-  ( P  e.  Prime  ->  T  e. CMnd
)
6829a1i 11 . . . . 5  |-  ( P  e.  Prime  ->  ( 1 ... ( P  - 
1 ) )  e. 
Fin )
69 zsubrg 17714 . . . . . 6  |-  ZZ  e.  (SubRing ` fld )
7052subrgsubm 16806 . . . . . 6  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubMnd `  T ) )
7169, 70mp1i 12 . . . . 5  |-  ( P  e.  Prime  ->  ZZ  e.  (SubMnd `  T ) )
72 f1oi 5668 . . . . . . . 8  |-  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) : ( 1 ... ( P  -  1 ) ) -1-1-onto-> ( 1 ... ( P  -  1 ) )
73 f1of 5633 . . . . . . . 8  |-  ( (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) : ( 1 ... ( P  -  1 ) ) -1-1-onto-> ( 1 ... ( P  -  1 ) )  ->  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> ( 1 ... ( P  -  1 ) ) )
7472, 73ax-mp 5 . . . . . . 7  |-  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> ( 1 ... ( P  -  1 ) )
759ssriv 3352 . . . . . . 7  |-  ( 1 ... ( P  - 
1 ) )  C_  ZZ
76 fss 5559 . . . . . . 7  |-  ( ( (  _I  |`  (
1 ... ( P  - 
1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> ( 1 ... ( P  - 
1 ) )  /\  ( 1 ... ( P  -  1 ) )  C_  ZZ )  ->  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> ZZ )
7774, 75, 76mp2an 667 . . . . . 6  |-  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> ZZ
7877a1i 11 . . . . 5  |-  ( P  e.  Prime  ->  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> ZZ )
79 1ex 9373 . . . . . . 7  |-  1  e.  _V
8079a1i 11 . . . . . 6  |-  ( P  e.  Prime  ->  1  e. 
_V )
8178, 68, 80fdmfifsupp 7622 . . . . 5  |-  ( P  e.  Prime  ->  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) finSupp  1 )
8264, 67, 68, 71, 78, 81gsumsubmcl 16388 . . . 4  |-  ( P  e.  Prime  ->  ( T 
gsumg  (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) )  e.  ZZ )
83 1z 10668 . . . . 5  |-  1  e.  ZZ
84 znegcl 10672 . . . . 5  |-  ( 1  e.  ZZ  ->  -u 1  e.  ZZ )
8583, 84mp1i 12 . . . 4  |-  ( P  e.  Prime  ->  -u 1  e.  ZZ )
86 moddvds 13529 . . . 4  |-  ( ( P  e.  NN  /\  ( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  e.  ZZ  /\  -u 1  e.  ZZ )  ->  ( ( ( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  mod  P )  =  ( -u 1  mod  P )  <->  P  ||  (
( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  -  -u 1
) ) )
8711, 82, 85, 86syl3anc 1213 . . 3  |-  ( P  e.  Prime  ->  ( ( ( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  mod  P )  =  ( -u 1  mod  P )  <->  P  ||  (
( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  -  -u 1
) ) )
8862, 87mpbid 210 . 2  |-  ( P  e.  Prime  ->  P  ||  ( ( T  gsumg  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) )  -  -u 1 ) )
89 fcoi1 5577 . . . . . . . . . 10  |-  ( (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> ( 1 ... ( P  - 
1 ) )  -> 
( (  _I  |`  (
1 ... ( P  - 
1 ) ) )  o.  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  =  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) )
9074, 89ax-mp 5 . . . . . . . . 9  |-  ( (  _I  |`  ( 1 ... ( P  - 
1 ) ) )  o.  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  =  (  _I  |`  ( 1 ... ( P  -  1 ) ) )
9190fveq1i 5684 . . . . . . . 8  |-  ( ( (  _I  |`  (
1 ... ( P  - 
1 ) ) )  o.  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) ) `  k )  =  ( (  _I  |`  ( 1 ... ( P  -  1 ) ) ) `  k
)
92 fvres 5696 . . . . . . . 8  |-  ( k  e.  ( 1 ... ( P  -  1 ) )  ->  (
(  _I  |`  (
1 ... ( P  - 
1 ) ) ) `
 k )  =  (  _I  `  k
) )
9391, 92syl5eq 2481 . . . . . . 7  |-  ( k  e.  ( 1 ... ( P  -  1 ) )  ->  (
( (  _I  |`  (
1 ... ( P  - 
1 ) ) )  o.  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) ) `  k )  =  (  _I  `  k ) )
9493adantl 463 . . . . . 6  |-  ( ( P  e.  Prime  /\  k  e.  ( 1 ... ( P  -  1 ) ) )  ->  (
( (  _I  |`  (
1 ... ( P  - 
1 ) ) )  o.  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) ) `  k )  =  (  _I  `  k ) )
955, 94seqfveq 11818 . . . . 5  |-  ( P  e.  Prime  ->  (  seq 1 (  x.  , 
( (  _I  |`  (
1 ... ( P  - 
1 ) ) )  o.  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) ) ) `  ( P  -  1 ) )  =  (  seq 1 (  x.  ,  _I  ) `  ( P  -  1 ) ) )
96 cnfldbas 17670 . . . . . . 7  |-  CC  =  ( Base ` fld )
9752, 96mgpbas 16575 . . . . . 6  |-  CC  =  ( Base `  T )
98 cnfldmul 17672 . . . . . . 7  |-  x.  =  ( .r ` fld )
9952, 98mgpplusg 16573 . . . . . 6  |-  x.  =  ( +g  `  T )
100 eqid 2437 . . . . . 6  |-  (Cntz `  T )  =  (Cntz `  T )
101 cnrng 17686 . . . . . . 7  |-fld  e.  Ring
10252rngmgp 16591 . . . . . . 7  |-  (fld  e.  Ring  ->  T  e.  Mnd )
103101, 102mp1i 12 . . . . . 6  |-  ( P  e.  Prime  ->  T  e. 
Mnd )
104 zsscn 10646 . . . . . . . 8  |-  ZZ  C_  CC
105 fss 5559 . . . . . . . 8  |-  ( ( (  _I  |`  (
1 ... ( P  - 
1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> ZZ  /\  ZZ  C_  CC )  -> 
(  _I  |`  (
1 ... ( P  - 
1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> CC )
10677, 104, 105mp2an 667 . . . . . . 7  |-  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> CC
107106a1i 11 . . . . . 6  |-  ( P  e.  Prime  ->  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) : ( 1 ... ( P  -  1 ) ) --> CC )
10897, 100, 67, 107cntzcmnf 16311 . . . . . 6  |-  ( P  e.  Prime  ->  ran  (  _I  |`  ( 1 ... ( P  -  1 ) ) )  C_  ( (Cntz `  T ) `  ran  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) ) )
109 f1of1 5632 . . . . . . 7  |-  ( (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) : ( 1 ... ( P  -  1 ) ) -1-1-onto-> ( 1 ... ( P  -  1 ) )  ->  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) : ( 1 ... ( P  -  1 ) )
-1-1-> ( 1 ... ( P  -  1 ) ) )
11072, 109mp1i 12 . . . . . 6  |-  ( P  e.  Prime  ->  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) : ( 1 ... ( P  -  1 ) )
-1-1-> ( 1 ... ( P  -  1 ) ) )
111 suppssdm 6696 . . . . . . . . 9  |-  ( (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) supp  1 )  C_  dom  (  _I  |`  ( 1 ... ( P  - 
1 ) ) )
112 dmresi 5153 . . . . . . . . 9  |-  dom  (  _I  |`  ( 1 ... ( P  -  1 ) ) )  =  ( 1 ... ( P  -  1 ) )
113111, 112sseqtri 3380 . . . . . . . 8  |-  ( (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) supp  1 )  C_  (
1 ... ( P  - 
1 ) )
114 rnresi 5174 . . . . . . . 8  |-  ran  (  _I  |`  ( 1 ... ( P  -  1 ) ) )  =  ( 1 ... ( P  -  1 ) )
115113, 114sseqtr4i 3381 . . . . . . 7  |-  ( (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) supp  1 )  C_  ran  (  _I  |`  ( 1 ... ( P  - 
1 ) ) )
116115a1i 11 . . . . . 6  |-  ( P  e.  Prime  ->  ( (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) supp  1 )  C_  ran  (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) )
117 eqid 2437 . . . . . 6  |-  ( ( (  _I  |`  (
1 ... ( P  - 
1 ) ) )  o.  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) ) supp  1 )  =  ( ( (  _I  |`  ( 1 ... ( P  -  1 ) ) )  o.  (  _I  |`  ( 1 ... ( P  -  1 ) ) ) ) supp  1 )
11897, 64, 99, 100, 103, 68, 107, 108, 3, 110, 116, 117gsumval3 16369 . . . . 5  |-  ( P  e.  Prime  ->  ( T 
gsumg  (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) )  =  (  seq 1 (  x.  , 
( (  _I  |`  (
1 ... ( P  - 
1 ) ) )  o.  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) ) ) `  ( P  -  1 ) ) )
119 facnn 12041 . . . . . 6  |-  ( ( P  -  1 )  e.  NN  ->  ( ! `  ( P  -  1 ) )  =  (  seq 1
(  x.  ,  _I  ) `  ( P  -  1 ) ) )
1203, 119syl 16 . . . . 5  |-  ( P  e.  Prime  ->  ( ! `
 ( P  - 
1 ) )  =  (  seq 1 (  x.  ,  _I  ) `  ( P  -  1 ) ) )
12195, 118, 1203eqtr4d 2479 . . . 4  |-  ( P  e.  Prime  ->  ( T 
gsumg  (  _I  |`  ( 1 ... ( P  - 
1 ) ) ) )  =  ( ! `
 ( P  - 
1 ) ) )
122121oveq1d 6099 . . 3  |-  ( P  e.  Prime  ->  ( ( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  -  -u 1
)  =  ( ( ! `  ( P  -  1 ) )  -  -u 1 ) )
123 nnm1nn0 10613 . . . . . . 7  |-  ( P  e.  NN  ->  ( P  -  1 )  e.  NN0 )
12411, 123syl 16 . . . . . 6  |-  ( P  e.  Prime  ->  ( P  -  1 )  e. 
NN0 )
125 faccl 12049 . . . . . 6  |-  ( ( P  -  1 )  e.  NN0  ->  ( ! `
 ( P  - 
1 ) )  e.  NN )
126124, 125syl 16 . . . . 5  |-  ( P  e.  Prime  ->  ( ! `
 ( P  - 
1 ) )  e.  NN )
127126nncnd 10330 . . . 4  |-  ( P  e.  Prime  ->  ( ! `
 ( P  - 
1 ) )  e.  CC )
128 ax-1cn 9332 . . . 4  |-  1  e.  CC
129 subneg 9650 . . . 4  |-  ( ( ( ! `  ( P  -  1 ) )  e.  CC  /\  1  e.  CC )  ->  ( ( ! `  ( P  -  1
) )  -  -u 1
)  =  ( ( ! `  ( P  -  1 ) )  +  1 ) )
130127, 128, 129sylancl 657 . . 3  |-  ( P  e.  Prime  ->  ( ( ! `  ( P  -  1 ) )  -  -u 1 )  =  ( ( ! `  ( P  -  1
) )  +  1 ) )
131122, 130eqtrd 2469 . 2  |-  ( P  e.  Prime  ->  ( ( T  gsumg  (  _I  |`  (
1 ... ( P  - 
1 ) ) ) )  -  -u 1
)  =  ( ( ! `  ( P  -  1 ) )  +  1 ) )
13288, 131breqtrd 4308 1  |-  ( P  e.  Prime  ->  P  ||  ( ( ! `  ( P  -  1
) )  +  1 ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 960   A.wal 1362    = wceq 1364    e. wcel 1757   A.wral 2709   {crab 2713   _Vcvv 2966    C_ wss 3320    C. wpss 3321   ~Pcpw 3852   class class class wbr 4284    _I cid 4622   dom cdm 4831   ran crn 4832    |` cres 4833    o. ccom 4835   -->wf 5406   -1-1->wf1 5407   -1-1-onto->wf1o 5409   ` cfv 5410  (class class class)co 6084   supp csupp 6683   Fincfn 7302   CCcc 9272   1c1 9275    + caddc 9277    x. cmul 9279    - cmin 9587   -ucneg 9588   NNcn 10314   2c2 10363   NN0cn0 10571   ZZcz 10638   ZZ>=cuz 10853   ...cfz 11428    mod cmo 11696    seqcseq 11794   ^cexp 11853   !cfa 12039    || cdivides 13522   Primecprime 13750    gsumg cgsu 14366   Mndcmnd 15396  SubMndcsubmnd 15450  Cntzccntz 15817  CMndccmn 16261  mulGrpcmgp 16569   Ringcrg 16581   CRingccrg 16582  SubRingcsubrg 16789  ℂfldccnfld 17666
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 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2418  ax-rep 4395  ax-sep 4405  ax-nul 4413  ax-pow 4462  ax-pr 4523  ax-un 6365  ax-inf2 7839  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352  ax-addf 9353  ax-mulf 9354
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3281  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3630  df-if 3784  df-pw 3854  df-sn 3870  df-pr 3872  df-tp 3874  df-op 3876  df-uni 4084  df-int 4121  df-iun 4165  df-iin 4166  df-br 4285  df-opab 4343  df-mpt 4344  df-tr 4378  df-eprel 4623  df-id 4627  df-po 4632  df-so 4633  df-fr 4670  df-se 4671  df-we 4672  df-ord 4713  df-on 4714  df-lim 4715  df-suc 4716  df-xp 4837  df-rel 4838  df-cnv 4839  df-co 4840  df-dm 4841  df-rn 4842  df-res 4843  df-ima 4844  df-iota 5373  df-fun 5412  df-fn 5413  df-f 5414  df-f1 5415  df-fo 5416  df-f1o 5417  df-fv 5418  df-isom 5419  df-riota 6043  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-of 6313  df-om 6470  df-1st 6570  df-2nd 6571  df-supp 6684  df-recs 6822  df-rdg 6856  df-1o 6912  df-2o 6913  df-oadd 6916  df-er 7093  df-map 7208  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-sup 7683  df-oi 7716  df-card 8101  df-cda 8329  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-rp 10984  df-fz 11429  df-fzo 11537  df-fl 11630  df-mod 11697  df-seq 11795  df-exp 11854  df-fac 12040  df-hash 12092  df-cj 12576  df-re 12577  df-im 12578  df-sqr 12712  df-abs 12713  df-dvds 13523  df-gcd 13678  df-prm 13751  df-phi 13828  df-struct 14163  df-ndx 14164  df-slot 14165  df-base 14166  df-sets 14167  df-ress 14168  df-plusg 14238  df-mulr 14239  df-starv 14240  df-tset 14244  df-ple 14245  df-ds 14247  df-unif 14248  df-0g 14367  df-gsum 14368  df-mre 14511  df-mrc 14512  df-acs 14514  df-mnd 15402  df-submnd 15452  df-grp 15529  df-minusg 15530  df-mulg 15532  df-subg 15662  df-cntz 15819  df-cmn 16263  df-mgp 16570  df-rng 16584  df-cring 16585  df-ur 16586  df-subrg 16791  df-cnfld 17667
This theorem is referenced by:  wilth  22298
  Copyright terms: Public domain W3C validator