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

Theorem wilthlem2 20309
Description: Lemma for wilth 20311: induction step. The "hand proof" version of this theorem works by writing out the list of all numbers from  1 to  P  -  1 in pairs such that a number is paired with its inverse. Every number has a unique inverse different from itself except  1 and  P  -  1, and so each pair multiplies to  1, and  1 and  P  -  1  ==  -u 1 multiply to  -u 1, so the full product is equal to  -u 1. Here we make this precise by doing the product pair by pair.

The induction hypothesis says that every subset  S of  1 ... ( P  -  1 ) that is closed under inverse (i.e. all pairs are matched up) and contains 
P  -  1 multiplies to  -u 1  mod  P. Given such a set, we take out one element  z  =/=  P  -  1. If there are no such elements, then 
S  =  { P  -  1 } which forms the base case. Otherwise,  S  \  { z ,  z ^ -u 1 } is also closed under inverse and contains  P  -  1, so the induction hypothesis says that this equals  -u 1; and the remaining two elements are either equal to each other, in which case wilthlem1 20308 gives that  z  =  1 or  P  -  1, and we've already excluded the second case, so the product gives  1; or  z  =/=  z ^ -u 1 and their product is  1. In either case the accumulated product is unaffected. (Contributed by Mario Carneiro, 24-Jan-2015.)

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 ) }
wilthlem2.p  |-  ( ph  ->  P  e.  Prime )
wilthlem2.s  |-  ( ph  ->  S  e.  A )
wilthlem2.r  |-  ( ph  ->  A. s  e.  A  ( s  C.  S  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) )
Assertion
Ref Expression
wilthlem2  |-  ( ph  ->  ( ( T  gsumg  (  _I  |`  S ) )  mod 
P )  =  (
-u 1  mod  P
) )
Distinct variable groups:    x, s,
y, A    P, s, x, y    ph, x, y    S, s, x, y    T, s, x, y
Allowed substitution hint:    ph( s)

Proof of Theorem wilthlem2
Dummy variables  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 447 . . . . . . . . 9  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  S  C_ 
{ ( P  - 
1 ) } )
2 wilthlem2.s . . . . . . . . . . . . . 14  |-  ( ph  ->  S  e.  A )
3 eleq2 2346 . . . . . . . . . . . . . . . 16  |-  ( x  =  S  ->  (
( P  -  1 )  e.  x  <->  ( P  -  1 )  e.  S ) )
4 eleq2 2346 . . . . . . . . . . . . . . . . 17  |-  ( x  =  S  ->  (
( ( y ^
( P  -  2 ) )  mod  P
)  e.  x  <->  ( (
y ^ ( P  -  2 ) )  mod  P )  e.  S ) )
54raleqbi1dv 2746 . . . . . . . . . . . . . . . 16  |-  ( x  =  S  ->  ( A. y  e.  x  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  x  <->  A. y  e.  S  ( (
y ^ ( P  -  2 ) )  mod  P )  e.  S ) )
63, 5anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( x  =  S  ->  (
( ( P  - 
1 )  e.  x  /\  A. y  e.  x  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  x )  <-> 
( ( P  - 
1 )  e.  S  /\  A. y  e.  S  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  S ) ) )
7 wilthlem.a . . . . . . . . . . . . . . 15  |-  A  =  { x  e.  ~P ( 1 ... ( P  -  1 ) )  |  ( ( P  -  1 )  e.  x  /\  A. y  e.  x  (
( y ^ ( P  -  2 ) )  mod  P )  e.  x ) }
86, 7elrab2 2927 . . . . . . . . . . . . . 14  |-  ( S  e.  A  <->  ( S  e.  ~P ( 1 ... ( P  -  1 ) )  /\  (
( P  -  1 )  e.  S  /\  A. y  e.  S  ( ( y ^ ( P  -  2 ) )  mod  P )  e.  S ) ) )
92, 8sylib 188 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  e.  ~P ( 1 ... ( P  -  1 ) )  /\  ( ( P  -  1 )  e.  S  /\  A. y  e.  S  (
( y ^ ( P  -  2 ) )  mod  P )  e.  S ) ) )
109simprd 449 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( P  - 
1 )  e.  S  /\  A. y  e.  S  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  S ) )
1110simpld 445 . . . . . . . . . . 11  |-  ( ph  ->  ( P  -  1 )  e.  S )
1211snssd 3762 . . . . . . . . . 10  |-  ( ph  ->  { ( P  - 
1 ) }  C_  S )
1312adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  { ( P  -  1 ) }  C_  S )
141, 13eqssd 3198 . . . . . . . 8  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  S  =  { ( P  - 
1 ) } )
1514reseq2d 4957 . . . . . . 7  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  (  _I  |`  S )  =  (  _I  |`  { ( P  -  1 ) } ) )
16 mptresid 5006 . . . . . . 7  |-  ( z  e.  { ( P  -  1 ) } 
|->  z )  =  (  _I  |`  { ( P  -  1 ) } )
1715, 16syl6eqr 2335 . . . . . 6  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  (  _I  |`  S )  =  ( z  e.  {
( P  -  1 ) }  |->  z ) )
1817oveq2d 5876 . . . . 5  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  ( T  gsumg  (  _I  |`  S ) )  =  ( T 
gsumg  ( z  e.  {
( P  -  1 ) }  |->  z ) ) )
1918oveq1d 5875 . . . 4  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  (
( T  gsumg  (  _I  |`  S ) )  mod  P )  =  ( ( T 
gsumg  ( z  e.  {
( P  -  1 ) }  |->  z ) )  mod  P ) )
20 wilthlem2.p . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  Prime )
21 prmnn 12763 . . . . . . . . . . . 12  |-  ( P  e.  Prime  ->  P  e.  NN )
2220, 21syl 15 . . . . . . . . . . 11  |-  ( ph  ->  P  e.  NN )
2322nncnd 9764 . . . . . . . . . 10  |-  ( ph  ->  P  e.  CC )
24 ax-1cn 8797 . . . . . . . . . 10  |-  1  e.  CC
25 negsub 9097 . . . . . . . . . 10  |-  ( ( P  e.  CC  /\  1  e.  CC )  ->  ( P  +  -u
1 )  =  ( P  -  1 ) )
2623, 24, 25sylancl 643 . . . . . . . . 9  |-  ( ph  ->  ( P  +  -u
1 )  =  ( P  -  1 ) )
27 neg1cn 9815 . . . . . . . . . 10  |-  -u 1  e.  CC
28 addcom 9000 . . . . . . . . . 10  |-  ( ( P  e.  CC  /\  -u 1  e.  CC )  ->  ( P  +  -u 1 )  =  (
-u 1  +  P
) )
2923, 27, 28sylancl 643 . . . . . . . . 9  |-  ( ph  ->  ( P  +  -u
1 )  =  (
-u 1  +  P
) )
3026, 29eqtr3d 2319 . . . . . . . 8  |-  ( ph  ->  ( P  -  1 )  =  ( -u
1  +  P ) )
31 cnrng 16398 . . . . . . . . . 10  |-fld  e.  Ring
32 wilthlem.t . . . . . . . . . . 11  |-  T  =  (mulGrp ` fld )
3332rngmgp 15349 . . . . . . . . . 10  |-  (fld  e.  Ring  ->  T  e.  Mnd )
3431, 33mp1i 11 . . . . . . . . 9  |-  ( ph  ->  T  e.  Mnd )
35 nnm1nn0 10007 . . . . . . . . . . 11  |-  ( P  e.  NN  ->  ( P  -  1 )  e.  NN0 )
3622, 35syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( P  -  1 )  e.  NN0 )
3736nn0cnd 10022 . . . . . . . . 9  |-  ( ph  ->  ( P  -  1 )  e.  CC )
38 cnfldbas 16385 . . . . . . . . . . 11  |-  CC  =  ( Base ` fld )
3932, 38mgpbas 15333 . . . . . . . . . 10  |-  CC  =  ( Base `  T )
40 id 19 . . . . . . . . . 10  |-  ( z  =  ( P  - 
1 )  ->  z  =  ( P  - 
1 ) )
4139, 40gsumsn 15222 . . . . . . . . 9  |-  ( ( T  e.  Mnd  /\  ( P  -  1
)  e.  CC  /\  ( P  -  1
)  e.  CC )  ->  ( T  gsumg  ( z  e.  { ( P  -  1 ) } 
|->  z ) )  =  ( P  -  1 ) )
4234, 37, 37, 41syl3anc 1182 . . . . . . . 8  |-  ( ph  ->  ( T  gsumg  ( z  e.  {
( P  -  1 ) }  |->  z ) )  =  ( P  -  1 ) )
4323mulid2d 8855 . . . . . . . . 9  |-  ( ph  ->  ( 1  x.  P
)  =  P )
4443oveq2d 5876 . . . . . . . 8  |-  ( ph  ->  ( -u 1  +  ( 1  x.  P
) )  =  (
-u 1  +  P
) )
4530, 42, 443eqtr4d 2327 . . . . . . 7  |-  ( ph  ->  ( T  gsumg  ( z  e.  {
( P  -  1 ) }  |->  z ) )  =  ( -u
1  +  ( 1  x.  P ) ) )
4645oveq1d 5875 . . . . . 6  |-  ( ph  ->  ( ( T  gsumg  ( z  e.  { ( P  -  1 ) } 
|->  z ) )  mod 
P )  =  ( ( -u 1  +  ( 1  x.  P
) )  mod  P
) )
47 1re 8839 . . . . . . . . 9  |-  1  e.  RR
4847renegcli 9110 . . . . . . . 8  |-  -u 1  e.  RR
4948a1i 10 . . . . . . 7  |-  ( ph  -> 
-u 1  e.  RR )
5022nnrpd 10391 . . . . . . 7  |-  ( ph  ->  P  e.  RR+ )
51 1z 10055 . . . . . . . 8  |-  1  e.  ZZ
5251a1i 10 . . . . . . 7  |-  ( ph  ->  1  e.  ZZ )
53 modcyc 11001 . . . . . . 7  |-  ( (
-u 1  e.  RR  /\  P  e.  RR+  /\  1  e.  ZZ )  ->  (
( -u 1  +  ( 1  x.  P ) )  mod  P )  =  ( -u 1  mod  P ) )
5449, 50, 52, 53syl3anc 1182 . . . . . 6  |-  ( ph  ->  ( ( -u 1  +  ( 1  x.  P ) )  mod 
P )  =  (
-u 1  mod  P
) )
5546, 54eqtrd 2317 . . . . 5  |-  ( ph  ->  ( ( T  gsumg  ( z  e.  { ( P  -  1 ) } 
|->  z ) )  mod 
P )  =  (
-u 1  mod  P
) )
5655adantr 451 . . . 4  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  (
( T  gsumg  ( z  e.  {
( P  -  1 ) }  |->  z ) )  mod  P )  =  ( -u 1  mod  P ) )
5719, 56eqtrd 2317 . . 3  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  (
( T  gsumg  (  _I  |`  S ) )  mod  P )  =  ( -u 1  mod  P ) )
5857ex 423 . 2  |-  ( ph  ->  ( S  C_  { ( P  -  1 ) }  ->  ( ( T  gsumg  (  _I  |`  S ) )  mod  P )  =  ( -u 1  mod  P ) ) )
59 nss 3238 . . 3  |-  ( -.  S  C_  { ( P  -  1 ) }  <->  E. z ( z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )
60 cnfld1 16401 . . . . . . . . . 10  |-  1  =  ( 1r ` fld )
6132, 60rngidval 15345 . . . . . . . . 9  |-  1  =  ( 0g `  T )
62 cnfldmul 16387 . . . . . . . . . 10  |-  x.  =  ( .r ` fld )
6332, 62mgpplusg 15331 . . . . . . . . 9  |-  x.  =  ( +g  `  T )
64 cncrng 16397 . . . . . . . . . . 11  |-fld  e.  CRing
6532crngmgp 15351 . . . . . . . . . . 11  |-  (fld  e.  CRing  ->  T  e. CMnd )
6664, 65ax-mp 8 . . . . . . . . . 10  |-  T  e. CMnd
6766a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  T  e. CMnd )
682adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  S  e.  A )
69 f1oi 5513 . . . . . . . . . . . 12  |-  (  _I  |`  S ) : S -1-1-onto-> S
70 f1of 5474 . . . . . . . . . . . 12  |-  ( (  _I  |`  S ) : S -1-1-onto-> S  ->  (  _I  |`  S ) : S --> S )
7169, 70ax-mp 8 . . . . . . . . . . 11  |-  (  _I  |`  S ) : S --> S
729simpld 445 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  e.  ~P (
1 ... ( P  - 
1 ) ) )
73 elpwi 3635 . . . . . . . . . . . . . 14  |-  ( S  e.  ~P ( 1 ... ( P  - 
1 ) )  ->  S  C_  ( 1 ... ( P  -  1 ) ) )
7472, 73syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  S  C_  ( 1 ... ( P  - 
1 ) ) )
75 elfzelz 10800 . . . . . . . . . . . . . 14  |-  ( z  e.  ( 1 ... ( P  -  1 ) )  ->  z  e.  ZZ )
7675ssriv 3186 . . . . . . . . . . . . 13  |-  ( 1 ... ( P  - 
1 ) )  C_  ZZ
7774, 76syl6ss 3193 . . . . . . . . . . . 12  |-  ( ph  ->  S  C_  ZZ )
78 zsscn 10034 . . . . . . . . . . . 12  |-  ZZ  C_  CC
7977, 78syl6ss 3193 . . . . . . . . . . 11  |-  ( ph  ->  S  C_  CC )
80 fss 5399 . . . . . . . . . . 11  |-  ( ( (  _I  |`  S ) : S --> S  /\  S  C_  CC )  -> 
(  _I  |`  S ) : S --> CC )
8171, 79, 80sylancr 644 . . . . . . . . . 10  |-  ( ph  ->  (  _I  |`  S ) : S --> CC )
8281adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  (  _I  |`  S ) : S --> CC )
83 fzfi 11036 . . . . . . . . . . . 12  |-  ( 1 ... ( P  - 
1 ) )  e. 
Fin
84 ssfi 7085 . . . . . . . . . . . 12  |-  ( ( ( 1 ... ( P  -  1 ) )  e.  Fin  /\  S  C_  ( 1 ... ( P  -  1 ) ) )  ->  S  e.  Fin )
8583, 74, 84sylancr 644 . . . . . . . . . . 11  |-  ( ph  ->  S  e.  Fin )
86 cnvimass 5035 . . . . . . . . . . . 12  |-  ( `' (  _I  |`  S )
" ( _V  \  { 1 } ) )  C_  dom  (  _I  |`  S )
87 dmresi 5007 . . . . . . . . . . . 12  |-  dom  (  _I  |`  S )  =  S
8886, 87sseqtri 3212 . . . . . . . . . . 11  |-  ( `' (  _I  |`  S )
" ( _V  \  { 1 } ) )  C_  S
89 ssfi 7085 . . . . . . . . . . 11  |-  ( ( S  e.  Fin  /\  ( `' (  _I  |`  S )
" ( _V  \  { 1 } ) )  C_  S )  ->  ( `' (  _I  |`  S ) " ( _V  \  { 1 } ) )  e.  Fin )
9085, 88, 89sylancl 643 . . . . . . . . . 10  |-  ( ph  ->  ( `' (  _I  |`  S ) " ( _V  \  { 1 } ) )  e.  Fin )
9190adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( `' (  _I  |`  S )
" ( _V  \  { 1 } ) )  e.  Fin )
92 disjdif 3528 . . . . . . . . . 10  |-  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  i^i  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  (/)
9392a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  i^i  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  (/) )
94 undif2 3532 . . . . . . . . . 10  |-  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  u.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  ( { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  u.  S
)
95 simprl 732 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  e.  S )
9610simprd 449 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. y  e.  S  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  S )
9796adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  A. y  e.  S  ( (
y ^ ( P  -  2 ) )  mod  P )  e.  S )
98 oveq1 5867 . . . . . . . . . . . . . . . 16  |-  ( y  =  z  ->  (
y ^ ( P  -  2 ) )  =  ( z ^
( P  -  2 ) ) )
9998oveq1d 5875 . . . . . . . . . . . . . . 15  |-  ( y  =  z  ->  (
( y ^ ( P  -  2 ) )  mod  P )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )
10099eleq1d 2351 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  (
( ( y ^
( P  -  2 ) )  mod  P
)  e.  S  <->  ( (
z ^ ( P  -  2 ) )  mod  P )  e.  S ) )
101100rspcv 2882 . . . . . . . . . . . . 13  |-  ( z  e.  S  ->  ( A. y  e.  S  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  S  -> 
( ( z ^
( P  -  2 ) )  mod  P
)  e.  S ) )
10295, 97, 101sylc 56 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
z ^ ( P  -  2 ) )  mod  P )  e.  S )
103 prssi 3773 . . . . . . . . . . . 12  |-  ( ( z  e.  S  /\  ( ( z ^
( P  -  2 ) )  mod  P
)  e.  S )  ->  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  C_  S
)
10495, 102, 103syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  C_  S )
105 ssequn1 3347 . . . . . . . . . . 11  |-  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } 
C_  S  <->  ( {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  u.  S )  =  S )
106104, 105sylib 188 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  u.  S )  =  S )
10794, 106syl5req 2330 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  S  =  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  u.  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )
10839, 61, 63, 67, 68, 82, 91, 93, 107gsumsplit 15209 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  (  _I  |`  S )
)  =  ( ( T  gsumg  ( (  _I  |`  S )  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  x.  ( T  gsumg  ( (  _I  |`  S )  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) ) ) )
109 resabs1 4986 . . . . . . . . . . 11  |-  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } 
C_  S  ->  (
(  _I  |`  S )  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )
110104, 109syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (  _I  |`  S )  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )
111110oveq2d 5876 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  ( (  _I  |`  S )  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) ) )
112 difss 3305 . . . . . . . . . . . 12  |-  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } )  C_  S
113 resabs1 4986 . . . . . . . . . . . 12  |-  ( ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) 
C_  S  ->  (
(  _I  |`  S )  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  (  _I  |`  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )
114112, 113ax-mp 8 . . . . . . . . . . 11  |-  ( (  _I  |`  S )  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  (  _I  |`  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )
115114oveq2i 5871 . . . . . . . . . 10  |-  ( T 
gsumg  ( (  _I  |`  S )  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )  =  ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )
116115a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  ( (  _I  |`  S )  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )  =  ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) )
117111, 116oveq12d 5878 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( T  gsumg  ( (  _I  |`  S )  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  x.  ( T  gsumg  ( (  _I  |`  S )  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) ) )  =  ( ( T 
gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  x.  ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) ) )
118108, 117eqtrd 2317 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  (  _I  |`  S )
)  =  ( ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  x.  ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) ) )
119118oveq1d 5875 . . . . . 6  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( T  gsumg  (  _I  |`  S ) )  mod  P )  =  ( ( ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  x.  ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) )  mod  P
) )
120 prfi 7133 . . . . . . . . . 10  |-  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  e.  Fin
121120a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  e.  Fin )
122 zsubrg 16427 . . . . . . . . . 10  |-  ZZ  e.  (SubRing ` fld )
12332subrgsubm 15560 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubMnd `  T ) )
124122, 123mp1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ZZ  e.  (SubMnd `  T ) )
125 f1oi 5513 . . . . . . . . . . 11  |-  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) : {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } -1-1-onto-> { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }
126 f1of 5474 . . . . . . . . . . 11  |-  ( (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) : { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } -1-1-onto-> { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  ->  (  _I  |` 
{ z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) : {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } --> { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )
127125, 126ax-mp 8 . . . . . . . . . 10  |-  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) : {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } --> { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }
12877adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  S  C_  ZZ )
129104, 128sstrd 3191 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  C_  ZZ )
130 fss 5399 . . . . . . . . . 10  |-  ( ( (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) : { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } --> { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  /\  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } 
C_  ZZ )  -> 
(  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) : { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } --> ZZ )
131127, 129, 130sylancr 644 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  (  _I  |` 
{ z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) : {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } --> ZZ )
132121, 131fisuppfi 14452 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( `' (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )
" ( _V  \  { 1 } ) )  e.  Fin )
13361, 67, 121, 124, 131, 132gsumsubmcl 15203 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  e.  ZZ )
134133zred 10119 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  e.  RR )
13547a1i 10 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  1  e.  RR )
13674adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  S  C_  (
1 ... ( P  - 
1 ) ) )
137112, 136syl5ss 3192 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C_  (
1 ... ( P  - 
1 ) ) )
138 ssfi 7085 . . . . . . . . 9  |-  ( ( ( 1 ... ( P  -  1 ) )  e.  Fin  /\  ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) 
C_  ( 1 ... ( P  -  1 ) ) )  -> 
( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  e.  Fin )
13983, 137, 138sylancr 644 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  e.  Fin )
140 f1oi 5513 . . . . . . . . . 10  |-  (  _I  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) : ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) -1-1-onto-> ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )
141 f1of 5474 . . . . . . . . . 10  |-  ( (  _I  |`  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) : ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) -1-1-onto-> ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (  _I  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) : ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) --> ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )
142140, 141ax-mp 8 . . . . . . . . 9  |-  (  _I  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) : ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) --> ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )
143112, 128syl5ss 3192 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C_  ZZ )
144 fss 5399 . . . . . . . . 9  |-  ( ( (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) : ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) --> ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } )  /\  ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) 
C_  ZZ )  -> 
(  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) : ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) --> ZZ )
145142, 143, 144sylancr 644 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  (  _I  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) : ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) --> ZZ )
146139, 145fisuppfi 14452 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( `' (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) )
" ( _V  \  { 1 } ) )  e.  Fin )
14761, 67, 139, 124, 145, 146gsumsubmcl 15203 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )  e.  ZZ )
14850adantr 451 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  e.  RR+ )
14934adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  T  e.  Mnd )
15079adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  S  C_  CC )
151150, 95sseldd 3183 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  e.  CC )
152 id 19 . . . . . . . . . . . . 13  |-  ( w  =  z  ->  w  =  z )
15339, 152gsumsn 15222 . . . . . . . . . . . 12  |-  ( ( T  e.  Mnd  /\  z  e.  CC  /\  z  e.  CC )  ->  ( T  gsumg  ( w  e.  {
z }  |->  w ) )  =  z )
154149, 151, 151, 153syl3anc 1182 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  ( w  e.  { z }  |->  w ) )  =  z )
155154adantr 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  ( T  gsumg  ( w  e.  { z } 
|->  w ) )  =  z )
156 mptresid 5006 . . . . . . . . . . . 12  |-  ( w  e.  { z } 
|->  w )  =  (  _I  |`  { z } )
157 dfsn2 3656 . . . . . . . . . . . . . 14  |-  { z }  =  { z ,  z }
158 simpr 447 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  z  =  1 )
159158orcd 381 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  ( z  =  1  \/  z  =  ( P  -  1 ) ) )
16020adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  e.  Prime )
161136, 95sseldd 3183 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  e.  ( 1 ... ( P  -  1 ) ) )
162 wilthlem1 20308 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  e.  Prime  /\  z  e.  ( 1 ... ( P  -  1 ) ) )  ->  (
z  =  ( ( z ^ ( P  -  2 ) )  mod  P )  <->  ( z  =  1  \/  z  =  ( P  - 
1 ) ) ) )
163160, 161, 162syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  <->  ( z  =  1  \/  z  =  ( P  - 
1 ) ) ) )
164163biimpar 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  ( z  =  1  \/  z  =  ( P  -  1 ) ) )  ->  z  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )
165159, 164syldan 456 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  z  =  ( ( z ^ ( P  -  2 ) )  mod  P ) )
166165preq2d 3715 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  { z ,  z }  =  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )
167157, 166syl5eq 2329 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  { z }  =  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } )
168167reseq2d 4957 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  (  _I  |`  { z } )  =  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )
169156, 168syl5eq 2329 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  ( w  e. 
{ z }  |->  w )  =  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )
170169oveq2d 5876 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  ( T  gsumg  ( w  e.  { z } 
|->  w ) )  =  ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) ) )
171155, 170, 1583eqtr3d 2325 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  1 )
172171oveq1d 5875 . . . . . . . 8  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  ( ( T 
gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  mod  P )  =  ( 1  mod 
P ) )
173 df-pr 3649 . . . . . . . . . . . . . . 15  |-  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  =  ( { z }  u.  { ( ( z ^
( P  -  2 ) )  mod  P
) } )
174173reseq2i 4954 . . . . . . . . . . . . . 14  |-  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  (  _I  |`  ( {
z }  u.  {
( ( z ^
( P  -  2 ) )  mod  P
) } ) )
175 mptresid 5006 . . . . . . . . . . . . . 14  |-  ( w  e.  ( { z }  u.  { ( ( z ^ ( P  -  2 ) )  mod  P ) } )  |->  w )  =  (  _I  |`  ( { z }  u.  { ( ( z ^
( P  -  2 ) )  mod  P
) } ) )
176174, 175eqtr4i 2308 . . . . . . . . . . . . 13  |-  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  ( w  e.  ( { z }  u.  {
( ( z ^
( P  -  2 ) )  mod  P
) } )  |->  w )
177176oveq2i 5871 . . . . . . . . . . . 12  |-  ( T 
gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  =  ( T 
gsumg  ( w  e.  ( { z }  u.  { ( ( z ^
( P  -  2 ) )  mod  P
) } )  |->  w ) )
17866a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  ->  T  e. CMnd )
179 snfi 6943 . . . . . . . . . . . . . 14  |-  { z }  e.  Fin
180179a1i 10 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  ->  { z }  e.  Fin )
181 elsni 3666 . . . . . . . . . . . . . . . 16  |-  ( w  e.  { z }  ->  w  =  z )
182181adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  w  e.  { z } )  ->  w  =  z )
183151adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  w  e.  { z } )  ->  z  e.  CC )
184182, 183eqeltrd 2359 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  w  e.  { z } )  ->  w  e.  CC )
185184adantlr 695 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( z  e.  S  /\  -.  z  e.  {
( P  -  1 ) } ) )  /\  z  =/=  1
)  /\  w  e.  { z } )  ->  w  e.  CC )
186150, 102sseldd 3183 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
z ^ ( P  -  2 ) )  mod  P )  e.  CC )
187186adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( ( z ^
( P  -  2 ) )  mod  P
)  e.  CC )
188 simprr 733 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  z  e.  { ( P  - 
1 ) } )
189 elsn 3657 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  { ( P  -  1 ) }  <-> 
z  =  ( P  -  1 ) )
190188, 189sylnib 295 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  z  =  ( P  - 
1 ) )
191 biorf 394 . . . . . . . . . . . . . . . . 17  |-  ( -.  z  =  ( P  -  1 )  -> 
( z  =  1  <-> 
( z  =  ( P  -  1 )  \/  z  =  1 ) ) )
192190, 191syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  =  1  <->  ( z  =  ( P  - 
1 )  \/  z  =  1 ) ) )
193 ovex 5885 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z ^ ( P  -  2 ) )  mod  P )  e. 
_V
194193elsnc 3665 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( z ^ ( P  -  2 ) )  mod  P )  e.  { z }  <-> 
( ( z ^
( P  -  2 ) )  mod  P
)  =  z )
195 eqcom 2287 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( z ^ ( P  -  2 ) )  mod  P )  =  z  <->  z  =  ( ( z ^
( P  -  2 ) )  mod  P
) )
196194, 195bitri 240 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z ^ ( P  -  2 ) )  mod  P )  e.  { z }  <-> 
z  =  ( ( z ^ ( P  -  2 ) )  mod  P ) )
197 orcom 376 . . . . . . . . . . . . . . . . 17  |-  ( ( z  =  ( P  -  1 )  \/  z  =  1 )  <-> 
( z  =  1  \/  z  =  ( P  -  1 ) ) )
198163, 196, 1973bitr4g 279 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( z ^ ( P  -  2 ) )  mod  P )  e.  { z }  <-> 
( z  =  ( P  -  1 )  \/  z  =  1 ) ) )
199192, 198bitr4d 247 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  =  1  <->  ( (
z ^ ( P  -  2 ) )  mod  P )  e. 
{ z } ) )
200199necon3abid 2481 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  =/=  1  <->  -.  ( (
z ^ ( P  -  2 ) )  mod  P )  e. 
{ z } ) )
201200biimpa 470 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  ->  -.  ( ( z ^
( P  -  2 ) )  mod  P
)  e.  { z } )
202 id 19 . . . . . . . . . . . . 13  |-  ( w  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  ->  w  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )
20339, 63, 178, 180, 185, 187, 201, 187, 202gsumunsn 15223 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( T  gsumg  ( w  e.  ( { z }  u.  { ( ( z ^
( P  -  2 ) )  mod  P
) } )  |->  w ) )  =  ( ( T  gsumg  ( w  e.  {
z }  |->  w ) )  x.  ( ( z ^ ( P  -  2 ) )  mod  P ) ) )
204177, 203syl5eq 2329 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  =  ( ( T  gsumg  ( w  e.  {
z }  |->  w ) )  x.  ( ( z ^ ( P  -  2 ) )  mod  P ) ) )
205154adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( T  gsumg  ( w  e.  {
z }  |->  w ) )  =  z )
206205oveq1d 5875 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( ( T  gsumg  ( w  e.  { z } 
|->  w ) )  x.  ( ( z ^
( P  -  2 ) )  mod  P
) )  =  ( z  x.  ( ( z ^ ( P  -  2 ) )  mod  P ) ) )
207204, 206eqtrd 2317 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  =  ( z  x.  ( ( z ^ ( P  - 
2 ) )  mod 
P ) ) )
208207oveq1d 5875 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  mod 
P )  =  ( ( z  x.  (
( z ^ ( P  -  2 ) )  mod  P ) )  mod  P ) )
209161, 75syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  e.  ZZ )
21022adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  e.  NN )
211 fzm1ndvds 12582 . . . . . . . . . . . . . 14  |-  ( ( P  e.  NN  /\  z  e.  ( 1 ... ( P  - 
1 ) ) )  ->  -.  P  ||  z
)
212210, 161, 211syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  P  ||  z )
213 eqid 2285 . . . . . . . . . . . . . 14  |-  ( ( z ^ ( P  -  2 ) )  mod  P )  =  ( ( z ^
( P  -  2 ) )  mod  P
)
214213prmdiv 12855 . . . . . . . . . . . . 13  |-  ( ( P  e.  Prime  /\  z  e.  ZZ  /\  -.  P  ||  z )  ->  (
( ( z ^
( P  -  2 ) )  mod  P
)  e.  ( 1 ... ( P  - 
1 ) )  /\  P  ||  ( ( z  x.  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )  - 
1 ) ) )
215160, 209, 212, 214syl3anc 1182 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( z ^ ( P  -  2 ) )  mod  P )  e.  ( 1 ... ( P  -  1 ) )  /\  P  ||  ( ( z  x.  ( ( z ^
( P  -  2 ) )  mod  P
) )  -  1 ) ) )
216215simprd 449 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  ||  (
( z  x.  (
( z ^ ( P  -  2 ) )  mod  P ) )  -  1 ) )
217 elfznn 10821 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( 1 ... ( P  -  1 ) )  ->  z  e.  NN )
218161, 217syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  e.  NN )
219136, 102sseldd 3183 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
z ^ ( P  -  2 ) )  mod  P )  e.  ( 1 ... ( P  -  1 ) ) )
220 elfznn 10821 . . . . . . . . . . . . . . 15  |-  ( ( ( z ^ ( P  -  2 ) )  mod  P )  e.  ( 1 ... ( P  -  1 ) )  ->  (
( z ^ ( P  -  2 ) )  mod  P )  e.  NN )
221219, 220syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
z ^ ( P  -  2 ) )  mod  P )  e.  NN )
222218, 221nnmulcld 9795 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  x.  ( ( z ^
( P  -  2 ) )  mod  P
) )  e.  NN )
223222nnzd 10118 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  x.  ( ( z ^
( P  -  2 ) )  mod  P
) )  e.  ZZ )
22451a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  1  e.  ZZ )
225 moddvds 12540 . . . . . . . . . . . 12  |-  ( ( P  e.  NN  /\  ( z  x.  (
( z ^ ( P  -  2 ) )  mod  P ) )  e.  ZZ  /\  1  e.  ZZ )  ->  ( ( ( z  x.  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )  mod 
P )  =  ( 1  mod  P )  <-> 
P  ||  ( (
z  x.  ( ( z ^ ( P  -  2 ) )  mod  P ) )  -  1 ) ) )
226210, 223, 224, 225syl3anc 1182 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( z  x.  (
( z ^ ( P  -  2 ) )  mod  P ) )  mod  P )  =  ( 1  mod 
P )  <->  P  ||  (
( z  x.  (
( z ^ ( P  -  2 ) )  mod  P ) )  -  1 ) ) )
227216, 226mpbird 223 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
z  x.  ( ( z ^ ( P  -  2 ) )  mod  P ) )  mod  P )  =  ( 1  mod  P
) )
228227adantr 451 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( ( z  x.  ( ( z ^
( P  -  2 ) )  mod  P
) )  mod  P
)  =  ( 1  mod  P ) )
229208, 228eqtrd 2317 . . . . . . . 8  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  mod 
P )  =  ( 1  mod  P ) )
230172, 229pm2.61dane 2526 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  mod  P )  =  ( 1  mod 
P ) )
231 modmul1 11004 . . . . . . 7  |-  ( ( ( ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  e.  RR  /\  1  e.  RR )  /\  (
( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )  e.  ZZ  /\  P  e.  RR+ )  /\  ( ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  mod 
P )  =  ( 1  mod  P ) )  ->  ( (
( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  x.  ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) )  mod  P
)  =  ( ( 1  x.  ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) )  mod  P
) )
232134, 135, 147, 148, 230, 231syl221anc 1193 . . . . . 6  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  x.  ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) )  mod  P
)  =  ( ( 1  x.  ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) )  mod  P
) )
233147zcnd 10120 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )  e.  CC )
234233mulid2d 8855 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( 1  x.  ( T  gsumg  (  _I  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) ) )  =  ( T  gsumg  (  _I  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) ) )
235234oveq1d 5875 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
1  x.  ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) )  mod  P
)  =  ( ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )  mod  P ) )
236 ovex 5885 . . . . . . . . . . 11  |-  ( 1 ... ( P  - 
1 ) )  e. 
_V
237236elpw2 4177 . . . . . . . . . 10  |-  ( ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )  e.  ~P ( 1 ... ( P  - 
1 ) )  <->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C_  (
1 ... ( P  - 
1 ) ) )
238137, 237sylibr 203 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  e.  ~P ( 1 ... ( P  -  1 ) ) )
23911adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  S )
240 eqcom 2287 . . . . . . . . . . . . . . 15  |-  ( z  =  ( P  - 
1 )  <->  ( P  -  1 )  =  z )
241189, 240bitri 240 . . . . . . . . . . . . . 14  |-  ( z  e.  { ( P  -  1 ) }  <-> 
( P  -  1 )  =  z )
242188, 241sylnib 295 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  ( P  -  1 )  =  z )
243 oveq1 5867 . . . . . . . . . . . . . . . 16  |-  ( ( P  -  1 )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  ->  (
( P  -  1 ) ^ ( P  -  2 ) )  =  ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^
( P  -  2 ) ) )
244243oveq1d 5875 . . . . . . . . . . . . . . 15  |-  ( ( P  -  1 )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  ->  (
( ( P  - 
1 ) ^ ( P  -  2 ) )  mod  P )  =  ( ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^ ( P  - 
2 ) )  mod 
P ) )
245210, 35syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e. 
NN0 )
246 nn0uz 10264 . . . . . . . . . . . . . . . . . . 19  |-  NN0  =  ( ZZ>= `  0 )
247245, 246syl6eleq 2375 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  ( ZZ>= `  0 )
)
248 eluzfz2 10806 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  -  1 )  e.  ( ZZ>= `  0
)  ->  ( P  -  1 )  e.  ( 0 ... ( P  -  1 ) ) )
249247, 248syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  ( 0 ... ( P  -  1 ) ) )
250 prmz 12764 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e.  Prime  ->  P  e.  ZZ )
251160, 250syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  e.  ZZ )
252128, 239sseldd 3183 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  ZZ )
253 zsubcl 10063 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( P  -  1 )  e.  ZZ  /\  1  e.  ZZ )  ->  ( ( P  - 
1 )  -  1 )  e.  ZZ )
254252, 51, 253sylancl 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  -  1 )  e.  ZZ )
255 dvdsmul1 12552 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  ZZ  /\  ( ( P  - 
1 )  -  1 )  e.  ZZ )  ->  P  ||  ( P  x.  ( ( P  -  1 )  -  1 ) ) )
256251, 254, 255syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  ||  ( P  x.  ( ( P  -  1 )  -  1 ) ) )
257210nncnd 9764 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  e.  CC )
25824a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  1  e.  CC )
259245nn0cnd 10022 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  CC )
260257, 258, 259subdird 9238 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  x.  ( P  - 
1 ) )  =  ( ( P  x.  ( P  -  1
) )  -  (
1  x.  ( P  -  1 ) ) ) )
261257, 259mulcld 8857 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  x.  ( P  -  1 ) )  e.  CC )
262261, 257, 258subsubd 9187 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  x.  ( P  -  1 ) )  -  ( P  - 
1 ) )  =  ( ( ( P  x.  ( P  - 
1 ) )  -  P )  +  1 ) )
263259mulid2d 8855 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( 1  x.  ( P  - 
1 ) )  =  ( P  -  1 ) )
264263oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  x.  ( P  -  1 ) )  -  ( 1  x.  ( P  -  1 ) ) )  =  ( ( P  x.  ( P  -  1
) )  -  ( P  -  1 ) ) )
265257, 259, 258subdid 9237 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  x.  ( ( P  - 
1 )  -  1 ) )  =  ( ( P  x.  ( P  -  1 ) )  -  ( P  x.  1 ) ) )
266257mulid1d 8854 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  x.  1 )  =  P )
267266oveq2d 5876 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  x.  ( P  -  1 ) )  -  ( P  x.  1 ) )  =  ( ( P  x.  ( P  -  1
) )  -  P
) )
268265, 267eqtrd 2317 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  x.  ( ( P  - 
1 )  -  1 ) )  =  ( ( P  x.  ( P  -  1 ) )  -  P ) )
269268oveq1d 5875 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  x.  ( ( P  -  1 )  -  1 ) )  +  1 )  =  ( ( ( P  x.  ( P  - 
1 ) )  -  P )  +  1 ) )
270262, 264, 2693eqtr4d 2327 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  x.  ( P  -  1 ) )  -  ( 1  x.  ( P  -  1 ) ) )  =  ( ( P  x.  ( ( P  - 
1 )  -  1 ) )  +  1 ) )
271260, 270eqtrd 2317 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  x.  ( P  - 
1 ) )  =  ( ( P  x.  ( ( P  - 
1 )  -  1 ) )  +  1 ) )
272271oveq1d 5875 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( P  -  1 )  x.  ( P  -  1 ) )  -  1 )  =  ( ( ( P  x.  ( ( P  -  1 )  - 
1 ) )  +  1 )  -  1 ) )
273254zcnd 10120 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  -  1 )  e.  CC )
274257, 273mulcld 8857 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  x.  ( ( P  - 
1 )  -  1 ) )  e.  CC )
275 pncan 9059 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( P  x.  (
( P  -  1 )  -  1 ) )  e.  CC  /\  1  e.  CC )  ->  ( ( ( P  x.  ( ( P  -  1 )  - 
1 ) )  +  1 )  -  1 )  =  ( P  x.  ( ( P  -  1 )  - 
1 ) ) )
276274, 24, 275sylancl 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( P  x.  (
( P  -  1 )  -  1 ) )  +  1 )  -  1 )  =  ( P  x.  (
( P  -  1 )  -  1 ) ) )
277272, 276eqtrd 2317 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( P  -  1 )  x.  ( P  -  1 ) )  -  1 )  =  ( P  x.  (
( P  -  1 )  -  1 ) ) )
278256, 277breqtrrd 4051 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  ||  (
( ( P  - 
1 )  x.  ( P  -  1 ) )  -  1 ) )
279136, 239sseldd 3183 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  ( 1 ... ( P  -  1 ) ) )
280 fzm1ndvds 12582 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  NN  /\  ( P  -  1
)  e.  ( 1 ... ( P  - 
1 ) ) )  ->  -.  P  ||  ( P  -  1 ) )
281210, 279, 280syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  P  ||  ( P  -  1 ) )
282 eqid 2285 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( P  -  1 ) ^ ( P  -  2 ) )  mod  P )  =  ( ( ( P  -  1 ) ^
( P  -  2 ) )  mod  P
)
283282prmdiveq 12856 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  e.  Prime  /\  ( P  -  1 )  e.  ZZ  /\  -.  P  ||  ( P  - 
1 ) )  -> 
( ( ( P  -  1 )  e.  ( 0 ... ( P  -  1 ) )  /\  P  ||  ( ( ( P  -  1 )  x.  ( P  -  1 ) )  -  1 ) )  <->  ( P  -  1 )  =  ( ( ( P  -  1 ) ^
( P  -  2 ) )  mod  P
) ) )
284160, 252, 281, 283syl3anc 1182 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( P  -  1 )  e.  ( 0 ... ( P  - 
1 ) )  /\  P  ||  ( ( ( P  -  1 )  x.  ( P  - 
1 ) )  - 
1 ) )  <->  ( P  -  1 )  =  ( ( ( P  -  1 ) ^
( P  -  2 ) )  mod  P
) ) )
285249, 278, 284mpbi2and 887 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  =  ( ( ( P  -  1 ) ^
( P  -  2 ) )  mod  P
) )
286213prmdivdiv 12857 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e.  Prime  /\  z  e.  ( 1 ... ( P  -  1 ) ) )  ->  z  =  ( ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^ ( P  - 
2 ) )  mod 
P ) )
287160, 161, 286syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  =  ( ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^
( P  -  2 ) )  mod  P
) )
288285, 287eqeq12d 2299 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  =  z  <->  ( (
( P  -  1 ) ^ ( P  -  2 ) )  mod  P )  =  ( ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^
( P  -  2 ) )  mod  P
) ) )
289244, 288syl5ibr 212 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  ->  ( P  -  1 )  =  z ) )
290242, 289mtod 168 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  ( P  -  1 )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )
291 ioran 476 . . . . . . . . . . . . 13  |-  ( -.  ( ( P  - 
1 )  =  z  \/  ( P  - 
1 )  =  ( ( z ^ ( P  -  2 ) )  mod  P ) )  <->  ( -.  ( P  -  1 )  =  z  /\  -.  ( P  -  1
)  =  ( ( z ^ ( P  -  2 ) )  mod  P ) ) )
292242, 290, 291sylanbrc 645 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  (
( P  -  1 )  =  z  \/  ( P  -  1 )  =  ( ( z ^ ( P  -  2 ) )  mod  P ) ) )
293 ovex 5885 . . . . . . . . . . . . 13  |-  ( P  -  1 )  e. 
_V
294293elpr 3660 . . . . . . . . . . . 12  |-  ( ( P  -  1 )  e.  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  <->  ( ( P  -  1 )  =  z  \/  ( P  -  1 )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) ) )
295292, 294sylnibr 296 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  ( P  -  1 )  e.  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } )
296 eldif 3164 . . . . . . . . . . 11  |-  ( ( P  -  1 )  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  <->  ( ( P  -  1 )  e.  S  /\  -.  ( P  -  1
)  e.  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )
297239, 295, 296sylanbrc 645 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )
298 eldifi 3300 . . . . . . . . . . . . 13  |-  ( y  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  y  e.  S )
29997r19.21bi 2643 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  S )
300298, 299sylan2 460 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  -> 
( ( y ^
( P  -  2 ) )  mod  P
)  e.  S )
301 eldif 3164 . . . . . . . . . . . . 13  |-  ( y  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  <->  ( y  e.  S  /\  -.  y  e.  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )
302160adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  P  e.  Prime )
303136sselda 3182 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  y  e.  ( 1 ... ( P  - 
1 ) ) )
304 eqid 2285 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y ^ ( P  -  2 ) )  mod  P )  =  ( ( y ^
( P  -  2 ) )  mod  P
)
305304prmdivdiv 12857 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  Prime  /\  y  e.  ( 1 ... ( P  -  1 ) ) )  ->  y  =  ( ( ( ( y ^ ( P  -  2 ) )  mod  P ) ^ ( P  - 
2 ) )  mod 
P ) )
306302, 303, 305syl2anc 642 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  y  =  ( ( ( ( y ^
( P  -  2 ) )  mod  P
) ^ ( P  -  2 ) )  mod  P ) )
307 oveq1 5867 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y ^ ( P  -  2 ) )  mod  P )  =  z  ->  (
( ( y ^
( P  -  2 ) )  mod  P
) ^ ( P  -  2 ) )  =  ( z ^
( P  -  2 ) ) )
308307oveq1d 5875 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y ^ ( P  -  2 ) )  mod  P )  =  z  ->  (
( ( ( y ^ ( P  - 
2 ) )  mod 
P ) ^ ( P  -  2 ) )  mod  P )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )
309308eqeq2d 2296 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y ^ ( P  -  2 ) )  mod  P )  =  z  ->  (
y  =  ( ( ( ( y ^
( P  -  2 ) )  mod  P
) ^ ( P  -  2 ) )  mod  P )  <->  y  =  ( ( z ^
( P  -  2 ) )  mod  P
) ) )
310306, 309syl5ibcom 211 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  ( ( ( y ^ ( P  - 
2 ) )  mod 
P )  =  z  ->  y  =  ( ( z ^ ( P  -  2 ) )  mod  P ) ) )
311 oveq1 5867 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y ^ ( P  -  2 ) )  mod  P )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  ->  (
( ( y ^
( P  -  2 ) )  mod  P
) ^ ( P  -  2 ) )  =  ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^
( P  -  2 ) ) )
312311oveq1d 5875 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y ^ ( P  -  2 ) )  mod  P )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  ->  (
( ( ( y ^ ( P  - 
2 ) )  mod 
P ) ^ ( P  -  2 ) )  mod  P )  =  ( ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^ ( P  - 
2 ) )  mod 
P ) )
313287adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  z  =  ( ( ( ( z ^
( P  -  2 ) )  mod  P
) ^ ( P  -  2 ) )  mod  P ) )
314306, 313eqeq12d 2299 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  ( y  =  z  <-> 
( ( ( ( y ^ ( P  -  2 ) )  mod  P ) ^
( P  -  2 ) )  mod  P
)  =  ( ( ( ( z ^
( P  -  2 ) )  mod  P
) ^ ( P  -  2 ) )  mod  P ) ) )
315312, 314syl5ibr 212 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  ( ( ( y ^ ( P  - 
2 ) )  mod 
P )  =  ( ( z ^ ( P  -  2 ) )  mod  P )  ->  y  =  z ) )
316310, 315orim12d 811 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  ( ( ( ( y ^ ( P  -  2 ) )  mod  P )  =  z  \/  ( ( y ^ ( P  -  2 ) )  mod  P )  =  ( ( z ^
( P  -  2 ) )  mod  P
) )  ->  (
y  =  ( ( z ^ ( P  -  2 ) )  mod  P )  \/  y  =  z ) ) )
317 ovex 5885 . . . . . . . . . . . . . . . . 17  |-  ( ( y ^ ( P  -  2 ) )  mod  P )  e. 
_V
318317elpr 3660 . . . . . . . . . . . . . . . 16  |-  ( ( ( y ^ ( P  -  2 ) )  mod  P )  e.  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  <->  ( (
( y ^ ( P  -  2 ) )  mod  P )  =  z  \/  (
( y ^ ( P  -  2 ) )  mod  P )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) ) )
319 vex 2793 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
320319elpr 3660 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  <->  ( y  =  z  \/  y  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) ) )
321 orcom 376 . . . . . . . . . . . . . . . . 17  |-  ( ( y  =  z  \/  y  =  ( ( z ^ ( P  -  2 ) )  mod  P ) )  <-> 
( y  =  ( ( z ^ ( P  -  2 ) )  mod  P )  \/  y  =  z ) )
322320, 321bitri 240 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  <->  ( y  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  \/  y  =  z ) )
323316, 318, 3223imtr4g 261 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  ( ( ( y ^ ( P  - 
2 ) )  mod 
P )  e.  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  ->  y  e.  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )
324323con3d 125 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  ( -.  y  e. 
{ z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  ->  -.  (
( y ^ ( P  -  2 ) )  mod  P )  e.  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) )
325324impr 602 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  ( y  e.  S  /\  -.  y  e.  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  ->  -.  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )
326301, 325sylan2b 461 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  ->  -.  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )
327 eldif 3164 . . . . . . . . . . . 12  |-  ( ( ( y ^ ( P  -  2 ) )  mod  P )  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  <->  ( (
( y ^ ( P  -  2 ) )  mod  P )  e.  S  /\  -.  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )
328300, 326, 327sylanbrc 645 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  -> 
( ( y ^
( P  -  2 ) )  mod  P
)  e.  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) )
329328ralrimiva 2628 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  A. y  e.  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ( ( y ^ ( P  - 
2 ) )  mod 
P )  e.  ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )
330297, 329jca 518 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  /\  A. y  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ( ( y ^ ( P  -  2 ) )  mod  P )  e.  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )
331 eleq2 2346 . . . . . . . . . . 11  |-  ( x  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (
( P  -  1 )  e.  x  <->  ( P  -  1 )  e.  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )
332 eleq2 2346 . . . . . . . . . . . 12  |-  ( x  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (
( ( y ^
( P  -  2 ) )  mod  P
)  e.  x  <->  ( (
y ^ ( P  -  2 ) )  mod  P )  e.  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )
333332raleqbi1dv 2746 . . . . . . . . . . 11  |-  ( x  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  ( A. y  e.  x  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  x  <->  A. y  e.  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ( ( y ^ ( P  - 
2 ) )  mod 
P )  e.  ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) ) )
334331, 333anbi12d 691 . . . . . . . . . 10  |-  ( x  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (
( ( P  - 
1 )  e.  x  /\  A. y  e.  x  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  x )  <-> 
( ( P  - 
1 )  e.  ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )  /\  A. y  e.  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ( ( y ^ ( P  - 
2 ) )  mod 
P )  e.  ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) ) ) )
335334, 7elrab2 2927 . . . . . . . . 9  |-  ( ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )  e.  A  <->  ( ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } )  e. 
~P ( 1 ... ( P  -  1 ) )  /\  (
( P  -  1 )  e.  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } )  /\  A. y  e.  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ( ( y ^ ( P  -  2 ) )  mod  P )  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) ) )
336238, 330, 335sylanbrc 645 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  e.  A
)
337 wilthlem2.r . . . . . . . . 9  |-  ( ph  ->  A. s  e.  A  ( s  C.  S  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) )
338337adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  A. s  e.  A  ( s  C.  S  ->  ( ( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( -u
1  mod  P )
) )
339 dfss1 3375 . . . . . . . . . . 11  |-  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } 
C_  S  <->  ( S  i^i  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )
340104, 339sylib 188 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  i^i  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )
341 vex 2793 . . . . . . . . . . . 12  |-  z  e. 
_V
342341prnz 3747 . . . . . . . . . . 11  |-  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  =/=  (/)
343342a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  =/=  (/) )
344340, 343eqnetrd 2466 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  i^i  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =/=  (/) )
345 disj4 3505 . . . . . . . . . 10  |-  ( ( S  i^i  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )  =  (/)  <->  -.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C.  S
)
346345necon2abii 2503 . . . . . . . . 9  |-  ( ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) 
C.  S  <->  ( S  i^i  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =/=  (/) )
347344, 346sylibr 203 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C.  S
)
348 psseq1 3265 . . . . . . . . . 10  |-  ( s  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (
s  C.  S  <->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C.  S
) )
349 reseq2 4952 . . . . . . . . . . . . 13  |-  ( s  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (  _I  |`  s )  =  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )
350349oveq2d 5876 . . . . . . . . . . . 12  |-  ( s  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  ( T  gsumg  (  _I  |`  s
) )  =  ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) )
351350oveq1d 5875 . . . . . . . . . . 11  |-  ( s  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (
( T  gsumg  (  _I  |`  s
) )  mod  P
)  =  ( ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )  mod  P ) )
352351eqeq1d 2293 . . . . . . . . . 10  |-  ( s  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (
( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
)  <->  ( ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )  mod  P )  =  ( -u 1  mod  P ) ) )
353348, 352imbi12d 311 . . . . . . . . 9  |-  ( s  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (
( s  C.  S  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) )  <->  ( ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } )  C.  S  ->  ( ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )  mod  P )  =  ( -u 1  mod  P ) ) ) )
354353rspcv 2882 . . . . . . . 8  |-  ( ( S  \  { z ,  ( (