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

Theorem wilthlem2 20844
Description: Lemma for wilth 20846: 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 20843 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 448 . . . . . . . . 9  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  S  C_ 
{ ( P  - 
1 ) } )
2 wilthlem2.s . . . . . . . . . . . . . 14  |-  ( ph  ->  S  e.  A )
3 eleq2 2496 . . . . . . . . . . . . . . . 16  |-  ( x  =  S  ->  (
( P  -  1 )  e.  x  <->  ( P  -  1 )  e.  S ) )
4 eleq2 2496 . . . . . . . . . . . . . . . . 17  |-  ( x  =  S  ->  (
( ( y ^
( P  -  2 ) )  mod  P
)  e.  x  <->  ( (
y ^ ( P  -  2 ) )  mod  P )  e.  S ) )
54raleqbi1dv 2904 . . . . . . . . . . . . . . . 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 692 . . . . . . . . . . . . . . 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 3086 . . . . . . . . . . . . . 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 189 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  e.  ~P ( 1 ... ( P  -  1 ) )  /\  ( ( P  -  1 )  e.  S  /\  A. y  e.  S  (
( y ^ ( P  -  2 ) )  mod  P )  e.  S ) ) )
109simprd 450 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( P  - 
1 )  e.  S  /\  A. y  e.  S  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  S ) )
1110simpld 446 . . . . . . . . . . 11  |-  ( ph  ->  ( P  -  1 )  e.  S )
1211snssd 3935 . . . . . . . . . 10  |-  ( ph  ->  { ( P  - 
1 ) }  C_  S )
1312adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  { ( P  -  1 ) }  C_  S )
141, 13eqssd 3357 . . . . . . . 8  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  S  =  { ( P  - 
1 ) } )
1514reseq2d 5138 . . . . . . 7  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  (  _I  |`  S )  =  (  _I  |`  { ( P  -  1 ) } ) )
16 mptresid 5187 . . . . . . 7  |-  ( z  e.  { ( P  -  1 ) } 
|->  z )  =  (  _I  |`  { ( P  -  1 ) } )
1715, 16syl6eqr 2485 . . . . . 6  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  (  _I  |`  S )  =  ( z  e.  {
( P  -  1 ) }  |->  z ) )
1817oveq2d 6089 . . . . 5  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  ( T  gsumg  (  _I  |`  S ) )  =  ( T 
gsumg  ( z  e.  {
( P  -  1 ) }  |->  z ) ) )
1918oveq1d 6088 . . . 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 13074 . . . . . . . . . . . 12  |-  ( P  e.  Prime  ->  P  e.  NN )
2220, 21syl 16 . . . . . . . . . . 11  |-  ( ph  ->  P  e.  NN )
2322nncnd 10008 . . . . . . . . . 10  |-  ( ph  ->  P  e.  CC )
24 ax-1cn 9040 . . . . . . . . . 10  |-  1  e.  CC
25 negsub 9341 . . . . . . . . . 10  |-  ( ( P  e.  CC  /\  1  e.  CC )  ->  ( P  +  -u
1 )  =  ( P  -  1 ) )
2623, 24, 25sylancl 644 . . . . . . . . 9  |-  ( ph  ->  ( P  +  -u
1 )  =  ( P  -  1 ) )
27 neg1cn 10059 . . . . . . . . . 10  |-  -u 1  e.  CC
28 addcom 9244 . . . . . . . . . 10  |-  ( ( P  e.  CC  /\  -u 1  e.  CC )  ->  ( P  +  -u 1 )  =  (
-u 1  +  P
) )
2923, 27, 28sylancl 644 . . . . . . . . 9  |-  ( ph  ->  ( P  +  -u
1 )  =  (
-u 1  +  P
) )
3026, 29eqtr3d 2469 . . . . . . . 8  |-  ( ph  ->  ( P  -  1 )  =  ( -u
1  +  P ) )
31 cnrng 16715 . . . . . . . . . 10  |-fld  e.  Ring
32 wilthlem.t . . . . . . . . . . 11  |-  T  =  (mulGrp ` fld )
3332rngmgp 15662 . . . . . . . . . 10  |-  (fld  e.  Ring  ->  T  e.  Mnd )
3431, 33mp1i 12 . . . . . . . . 9  |-  ( ph  ->  T  e.  Mnd )
35 nnm1nn0 10253 . . . . . . . . . . 11  |-  ( P  e.  NN  ->  ( P  -  1 )  e.  NN0 )
3622, 35syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( P  -  1 )  e.  NN0 )
3736nn0cnd 10268 . . . . . . . . 9  |-  ( ph  ->  ( P  -  1 )  e.  CC )
38 cnfldbas 16699 . . . . . . . . . . 11  |-  CC  =  ( Base ` fld )
3932, 38mgpbas 15646 . . . . . . . . . 10  |-  CC  =  ( Base `  T )
40 id 20 . . . . . . . . . 10  |-  ( z  =  ( P  - 
1 )  ->  z  =  ( P  - 
1 ) )
4139, 40gsumsn 15535 . . . . . . . . 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 1184 . . . . . . . 8  |-  ( ph  ->  ( T  gsumg  ( z  e.  {
( P  -  1 ) }  |->  z ) )  =  ( P  -  1 ) )
4323mulid2d 9098 . . . . . . . . 9  |-  ( ph  ->  ( 1  x.  P
)  =  P )
4443oveq2d 6089 . . . . . . . 8  |-  ( ph  ->  ( -u 1  +  ( 1  x.  P
) )  =  (
-u 1  +  P
) )
4530, 42, 443eqtr4d 2477 . . . . . . 7  |-  ( ph  ->  ( T  gsumg  ( z  e.  {
( P  -  1 ) }  |->  z ) )  =  ( -u
1  +  ( 1  x.  P ) ) )
4645oveq1d 6088 . . . . . 6  |-  ( ph  ->  ( ( T  gsumg  ( z  e.  { ( P  -  1 ) } 
|->  z ) )  mod 
P )  =  ( ( -u 1  +  ( 1  x.  P
) )  mod  P
) )
47 1re 9082 . . . . . . . . 9  |-  1  e.  RR
4847renegcli 9354 . . . . . . . 8  |-  -u 1  e.  RR
4948a1i 11 . . . . . . 7  |-  ( ph  -> 
-u 1  e.  RR )
5022nnrpd 10639 . . . . . . 7  |-  ( ph  ->  P  e.  RR+ )
51 1z 10303 . . . . . . . 8  |-  1  e.  ZZ
5251a1i 11 . . . . . . 7  |-  ( ph  ->  1  e.  ZZ )
53 modcyc 11268 . . . . . . 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 1184 . . . . . 6  |-  ( ph  ->  ( ( -u 1  +  ( 1  x.  P ) )  mod 
P )  =  (
-u 1  mod  P
) )
5546, 54eqtrd 2467 . . . . 5  |-  ( ph  ->  ( ( T  gsumg  ( z  e.  { ( P  -  1 ) } 
|->  z ) )  mod 
P )  =  (
-u 1  mod  P
) )
5655adantr 452 . . . 4  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  (
( T  gsumg  ( z  e.  {
( P  -  1 ) }  |->  z ) )  mod  P )  =  ( -u 1  mod  P ) )
5719, 56eqtrd 2467 . . 3  |-  ( (
ph  /\  S  C_  { ( P  -  1 ) } )  ->  (
( T  gsumg  (  _I  |`  S ) )  mod  P )  =  ( -u 1  mod  P ) )
5857ex 424 . 2  |-  ( ph  ->  ( S  C_  { ( P  -  1 ) }  ->  ( ( T  gsumg  (  _I  |`  S ) )  mod  P )  =  ( -u 1  mod  P ) ) )
59 nss 3398 . . 3  |-  ( -.  S  C_  { ( P  -  1 ) }  <->  E. z ( z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )
60 cnfld1 16718 . . . . . . . . . 10  |-  1  =  ( 1r ` fld )
6132, 60rngidval 15658 . . . . . . . . 9  |-  1  =  ( 0g `  T )
62 cnfldmul 16701 . . . . . . . . . 10  |-  x.  =  ( .r ` fld )
6332, 62mgpplusg 15644 . . . . . . . . 9  |-  x.  =  ( +g  `  T )
64 cncrng 16714 . . . . . . . . . . 11  |-fld  e.  CRing
6532crngmgp 15664 . . . . . . . . . . 11  |-  (fld  e.  CRing  ->  T  e. CMnd )
6664, 65ax-mp 8 . . . . . . . . . 10  |-  T  e. CMnd
6766a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  T  e. CMnd )
682adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  S  e.  A )
69 f1oi 5705 . . . . . . . . . . . 12  |-  (  _I  |`  S ) : S -1-1-onto-> S
70 f1of 5666 . . . . . . . . . . . 12  |-  ( (  _I  |`  S ) : S -1-1-onto-> S  ->  (  _I  |`  S ) : S --> S )
7169, 70ax-mp 8 . . . . . . . . . . 11  |-  (  _I  |`  S ) : S --> S
729simpld 446 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  e.  ~P (
1 ... ( P  - 
1 ) ) )
7372elpwid 3800 . . . . . . . . . . . . 13  |-  ( ph  ->  S  C_  ( 1 ... ( P  - 
1 ) ) )
74 elfzelz 11051 . . . . . . . . . . . . . 14  |-  ( z  e.  ( 1 ... ( P  -  1 ) )  ->  z  e.  ZZ )
7574ssriv 3344 . . . . . . . . . . . . 13  |-  ( 1 ... ( P  - 
1 ) )  C_  ZZ
7673, 75syl6ss 3352 . . . . . . . . . . . 12  |-  ( ph  ->  S  C_  ZZ )
77 zsscn 10282 . . . . . . . . . . . 12  |-  ZZ  C_  CC
7876, 77syl6ss 3352 . . . . . . . . . . 11  |-  ( ph  ->  S  C_  CC )
79 fss 5591 . . . . . . . . . . 11  |-  ( ( (  _I  |`  S ) : S --> S  /\  S  C_  CC )  -> 
(  _I  |`  S ) : S --> CC )
8071, 78, 79sylancr 645 . . . . . . . . . 10  |-  ( ph  ->  (  _I  |`  S ) : S --> CC )
8180adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  (  _I  |`  S ) : S --> CC )
82 fzfi 11303 . . . . . . . . . . . 12  |-  ( 1 ... ( P  - 
1 ) )  e. 
Fin
83 ssfi 7321 . . . . . . . . . . . 12  |-  ( ( ( 1 ... ( P  -  1 ) )  e.  Fin  /\  S  C_  ( 1 ... ( P  -  1 ) ) )  ->  S  e.  Fin )
8482, 73, 83sylancr 645 . . . . . . . . . . 11  |-  ( ph  ->  S  e.  Fin )
85 cnvimass 5216 . . . . . . . . . . . 12  |-  ( `' (  _I  |`  S )
" ( _V  \  { 1 } ) )  C_  dom  (  _I  |`  S )
86 dmresi 5188 . . . . . . . . . . . 12  |-  dom  (  _I  |`  S )  =  S
8785, 86sseqtri 3372 . . . . . . . . . . 11  |-  ( `' (  _I  |`  S )
" ( _V  \  { 1 } ) )  C_  S
88 ssfi 7321 . . . . . . . . . . 11  |-  ( ( S  e.  Fin  /\  ( `' (  _I  |`  S )
" ( _V  \  { 1 } ) )  C_  S )  ->  ( `' (  _I  |`  S ) " ( _V  \  { 1 } ) )  e.  Fin )
8984, 87, 88sylancl 644 . . . . . . . . . 10  |-  ( ph  ->  ( `' (  _I  |`  S ) " ( _V  \  { 1 } ) )  e.  Fin )
9089adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( `' (  _I  |`  S )
" ( _V  \  { 1 } ) )  e.  Fin )
91 disjdif 3692 . . . . . . . . . 10  |-  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  i^i  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  (/)
9291a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  i^i  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  (/) )
93 undif2 3696 . . . . . . . . . 10  |-  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  u.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  ( { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  u.  S
)
94 simprl 733 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  e.  S )
9510simprd 450 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. y  e.  S  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  S )
9695adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  A. y  e.  S  ( (
y ^ ( P  -  2 ) )  mod  P )  e.  S )
97 oveq1 6080 . . . . . . . . . . . . . . . 16  |-  ( y  =  z  ->  (
y ^ ( P  -  2 ) )  =  ( z ^
( P  -  2 ) ) )
9897oveq1d 6088 . . . . . . . . . . . . . . 15  |-  ( y  =  z  ->  (
( y ^ ( P  -  2 ) )  mod  P )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )
9998eleq1d 2501 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  (
( ( y ^
( P  -  2 ) )  mod  P
)  e.  S  <->  ( (
z ^ ( P  -  2 ) )  mod  P )  e.  S ) )
10099rspcv 3040 . . . . . . . . . . . . 13  |-  ( z  e.  S  ->  ( A. y  e.  S  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  S  -> 
( ( z ^
( P  -  2 ) )  mod  P
)  e.  S ) )
10194, 96, 100sylc 58 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
z ^ ( P  -  2 ) )  mod  P )  e.  S )
102 prssi 3946 . . . . . . . . . . . 12  |-  ( ( z  e.  S  /\  ( ( z ^
( P  -  2 ) )  mod  P
)  e.  S )  ->  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  C_  S
)
10394, 101, 102syl2anc 643 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  C_  S )
104 ssequn1 3509 . . . . . . . . . . 11  |-  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } 
C_  S  <->  ( {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  u.  S )  =  S )
105103, 104sylib 189 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  u.  S )  =  S )
10693, 105syl5req 2480 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  S  =  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }  u.  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )
10739, 61, 63, 67, 68, 81, 90, 92, 106gsumsplit 15522 . . . . . . . 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 ) } ) ) ) ) )
108 resabs1 5167 . . . . . . . . . . 11  |-  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } 
C_  S  ->  (
(  _I  |`  S )  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )
109103, 108syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (  _I  |`  S )  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )
110109oveq2d 6089 . . . . . . . . 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 ) } ) ) )
111 difss 3466 . . . . . . . . . . . 12  |-  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } )  C_  S
112 resabs1 5167 . . . . . . . . . . . 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 ) } ) ) )
113111, 112ax-mp 8 . . . . . . . . . . 11  |-  ( (  _I  |`  S )  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  (  _I  |`  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )
114113oveq2i 6084 . . . . . . . . . 10  |-  ( T 
gsumg  ( (  _I  |`  S )  |`  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )  =  ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )
115114a1i 11 . . . . . . . . 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
) } ) ) ) )
116110, 115oveq12d 6091 . . . . . . . 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
) } ) ) ) ) )
117107, 116eqtrd 2467 . . . . . . 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
) } ) ) ) ) )
118117oveq1d 6088 . . . . . 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
) )
119 prfi 7373 . . . . . . . . . 10  |-  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  e.  Fin
120119a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  e.  Fin )
121 zsubrg 16744 . . . . . . . . . 10  |-  ZZ  e.  (SubRing ` fld )
12232subrgsubm 15873 . . . . . . . . . 10  |-  ( ZZ  e.  (SubRing ` fld )  ->  ZZ  e.  (SubMnd `  T ) )
123121, 122mp1i 12 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ZZ  e.  (SubMnd `  T ) )
124 f1oi 5705 . . . . . . . . . . 11  |-  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) : {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } -1-1-onto-> { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }
125 f1of 5666 . . . . . . . . . . 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 ) } )
126124, 125ax-mp 8 . . . . . . . . . 10  |-  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) : {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } --> { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) }
12776adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  S  C_  ZZ )
128103, 127sstrd 3350 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  C_  ZZ )
129 fss 5591 . . . . . . . . . 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 )
130126, 128, 129sylancr 645 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  (  _I  |` 
{ z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) : {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } --> ZZ )
131120, 130fisuppfi 14765 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( `' (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )
" ( _V  \  { 1 } ) )  e.  Fin )
13261, 67, 120, 123, 130, 131gsumsubmcl 15516 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  e.  ZZ )
133132zred 10367 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  e.  RR )
13447a1i 11 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  1  e.  RR )
13573adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  S  C_  (
1 ... ( P  - 
1 ) ) )
136135ssdifssd 3477 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C_  (
1 ... ( P  - 
1 ) ) )
137 ssfi 7321 . . . . . . . . 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 )
13882, 136, 137sylancr 645 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  e.  Fin )
139 f1oi 5705 . . . . . . . . . 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 ) } )
140 f1of 5666 . . . . . . . . . 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 ) } ) )
141139, 140ax-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 ) } )
142127ssdifssd 3477 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C_  ZZ )
143 fss 5591 . . . . . . . . 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 )
144141, 142, 143sylancr 645 . . . . . . . 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 )
145138, 144fisuppfi 14765 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( `' (  _I  |`  ( S 
\  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) )
" ( _V  \  { 1 } ) )  e.  Fin )
14661, 67, 138, 123, 144, 145gsumsubmcl 15516 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )  e.  ZZ )
14750adantr 452 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  e.  RR+ )
14834adantr 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  T  e.  Mnd )
14978adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  S  C_  CC )
150149, 94sseldd 3341 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  e.  CC )
151 id 20 . . . . . . . . . . . . 13  |-  ( w  =  z  ->  w  =  z )
15239, 151gsumsn 15535 . . . . . . . . . . . 12  |-  ( ( T  e.  Mnd  /\  z  e.  CC  /\  z  e.  CC )  ->  ( T  gsumg  ( w  e.  {
z }  |->  w ) )  =  z )
153148, 150, 150, 152syl3anc 1184 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  ( w  e.  { z }  |->  w ) )  =  z )
154153adantr 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  ( T  gsumg  ( w  e.  { z } 
|->  w ) )  =  z )
155 mptresid 5187 . . . . . . . . . . . 12  |-  ( w  e.  { z } 
|->  w )  =  (  _I  |`  { z } )
156 dfsn2 3820 . . . . . . . . . . . . . 14  |-  { z }  =  { z ,  z }
157 simpr 448 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  z  =  1 )
158157orcd 382 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  ( z  =  1  \/  z  =  ( P  -  1 ) ) )
15920adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  e.  Prime )
160135, 94sseldd 3341 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  e.  ( 1 ... ( P  -  1 ) ) )
161 wilthlem1 20843 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  e.  Prime  /\  z  e.  ( 1 ... ( P  -  1 ) ) )  ->  (
z  =  ( ( z ^ ( P  -  2 ) )  mod  P )  <->  ( z  =  1  \/  z  =  ( P  - 
1 ) ) ) )
162159, 160, 161syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  <->  ( z  =  1  \/  z  =  ( P  - 
1 ) ) ) )
163162biimpar 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  ( z  =  1  \/  z  =  ( P  -  1 ) ) )  ->  z  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )
164158, 163syldan 457 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  z  =  ( ( z ^ ( P  -  2 ) )  mod  P ) )
165164preq2d 3882 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  { z ,  z }  =  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )
166156, 165syl5eq 2479 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  { z }  =  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } )
167166reseq2d 5138 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  (  _I  |`  { z } )  =  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )
168155, 167syl5eq 2479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  ( w  e. 
{ z }  |->  w )  =  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )
169168oveq2d 6089 . . . . . . . . . 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 ) } ) ) )
170154, 169, 1573eqtr3d 2475 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =  1 )  ->  ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )  =  1 )
171170oveq1d 6088 . . . . . . . 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 ) )
172 df-pr 3813 . . . . . . . . . . . . . . 15  |-  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  =  ( { z }  u.  { ( ( z ^
( P  -  2 ) )  mod  P
) } )
173172reseq2i 5135 . . . . . . . . . . . . . 14  |-  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  (  _I  |`  ( {
z }  u.  {
( ( z ^
( P  -  2 ) )  mod  P
) } ) )
174 mptresid 5187 . . . . . . . . . . . . . 14  |-  ( w  e.  ( { z }  u.  { ( ( z ^ ( P  -  2 ) )  mod  P ) } )  |->  w )  =  (  _I  |`  ( { z }  u.  { ( ( z ^
( P  -  2 ) )  mod  P
) } ) )
175173, 174eqtr4i 2458 . . . . . . . . . . . . 13  |-  (  _I  |`  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  ( w  e.  ( { z }  u.  {
( ( z ^
( P  -  2 ) )  mod  P
) } )  |->  w )
176175oveq2i 6084 . . . . . . . . . . . 12  |-  ( T 
gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  =  ( T 
gsumg  ( w  e.  ( { z }  u.  { ( ( z ^
( P  -  2 ) )  mod  P
) } )  |->  w ) )
17766a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  ->  T  e. CMnd )
178 snfi 7179 . . . . . . . . . . . . . 14  |-  { z }  e.  Fin
179178a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  ->  { z }  e.  Fin )
180 elsni 3830 . . . . . . . . . . . . . . . 16  |-  ( w  e.  { z }  ->  w  =  z )
181180adantl 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  w  e.  { z } )  ->  w  =  z )
182150adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  w  e.  { z } )  ->  z  e.  CC )
183181, 182eqeltrd 2509 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  w  e.  { z } )  ->  w  e.  CC )
184183adantlr 696 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( z  e.  S  /\  -.  z  e.  {
( P  -  1 ) } ) )  /\  z  =/=  1
)  /\  w  e.  { z } )  ->  w  e.  CC )
185149, 101sseldd 3341 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
z ^ ( P  -  2 ) )  mod  P )  e.  CC )
186185adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( ( z ^
( P  -  2 ) )  mod  P
)  e.  CC )
187 simprr 734 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  z  e.  { ( P  - 
1 ) } )
188 elsn 3821 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  { ( P  -  1 ) }  <-> 
z  =  ( P  -  1 ) )
189187, 188sylnib 296 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  z  =  ( P  - 
1 ) )
190 biorf 395 . . . . . . . . . . . . . . . . 17  |-  ( -.  z  =  ( P  -  1 )  -> 
( z  =  1  <-> 
( z  =  ( P  -  1 )  \/  z  =  1 ) ) )
191189, 190syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  =  1  <->  ( z  =  ( P  - 
1 )  \/  z  =  1 ) ) )
192 ovex 6098 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z ^ ( P  -  2 ) )  mod  P )  e. 
_V
193192elsnc 3829 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( z ^ ( P  -  2 ) )  mod  P )  e.  { z }  <-> 
( ( z ^
( P  -  2 ) )  mod  P
)  =  z )
194 eqcom 2437 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( z ^ ( P  -  2 ) )  mod  P )  =  z  <->  z  =  ( ( z ^
( P  -  2 ) )  mod  P
) )
195193, 194bitri 241 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z ^ ( P  -  2 ) )  mod  P )  e.  { z }  <-> 
z  =  ( ( z ^ ( P  -  2 ) )  mod  P ) )
196 orcom 377 . . . . . . . . . . . . . . . . 17  |-  ( ( z  =  ( P  -  1 )  \/  z  =  1 )  <-> 
( z  =  1  \/  z  =  ( P  -  1 ) ) )
197162, 195, 1963bitr4g 280 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( z ^ ( P  -  2 ) )  mod  P )  e.  { z }  <-> 
( z  =  ( P  -  1 )  \/  z  =  1 ) ) )
198191, 197bitr4d 248 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  =  1  <->  ( (
z ^ ( P  -  2 ) )  mod  P )  e. 
{ z } ) )
199198necon3abid 2631 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  =/=  1  <->  -.  ( (
z ^ ( P  -  2 ) )  mod  P )  e. 
{ z } ) )
200199biimpa 471 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  ->  -.  ( ( z ^
( P  -  2 ) )  mod  P
)  e.  { z } )
201 id 20 . . . . . . . . . . . . 13  |-  ( w  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  ->  w  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )
20239, 63, 177, 179, 184, 186, 200, 186, 201gsumunsn 15536 . . . . . . . . . . . 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 ) ) )
203176, 202syl5eq 2479 . . . . . . . . . . 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 ) ) )
204153adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( T  gsumg  ( w  e.  {
z }  |->  w ) )  =  z )
205204oveq1d 6088 . . . . . . . . . . 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 ) ) )
206203, 205eqtrd 2467 . . . . . . . . . 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 ) ) )
207206oveq1d 6088 . . . . . . . . 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 ) )
208160, 74syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  e.  ZZ )
20922adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  e.  NN )
210 fzm1ndvds 12893 . . . . . . . . . . . . . 14  |-  ( ( P  e.  NN  /\  z  e.  ( 1 ... ( P  - 
1 ) ) )  ->  -.  P  ||  z
)
211209, 160, 210syl2anc 643 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  P  ||  z )
212 eqid 2435 . . . . . . . . . . . . . 14  |-  ( ( z ^ ( P  -  2 ) )  mod  P )  =  ( ( z ^
( P  -  2 ) )  mod  P
)
213212prmdiv 13166 . . . . . . . . . . . . 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 ) ) )
214159, 208, 211, 213syl3anc 1184 . . . . . . . . . . . 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 ) ) )
215214simprd 450 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  ||  (
( z  x.  (
( z ^ ( P  -  2 ) )  mod  P ) )  -  1 ) )
216 elfznn 11072 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( 1 ... ( P  -  1 ) )  ->  z  e.  NN )
217160, 216syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  e.  NN )
218135, 101sseldd 3341 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
z ^ ( P  -  2 ) )  mod  P )  e.  ( 1 ... ( P  -  1 ) ) )
219 elfznn 11072 . . . . . . . . . . . . . . 15  |-  ( ( ( z ^ ( P  -  2 ) )  mod  P )  e.  ( 1 ... ( P  -  1 ) )  ->  (
( z ^ ( P  -  2 ) )  mod  P )  e.  NN )
220218, 219syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
z ^ ( P  -  2 ) )  mod  P )  e.  NN )
221217, 220nnmulcld 10039 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  x.  ( ( z ^
( P  -  2 ) )  mod  P
) )  e.  NN )
222221nnzd 10366 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( z  x.  ( ( z ^
( P  -  2 ) )  mod  P
) )  e.  ZZ )
22351a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  1  e.  ZZ )
224 moddvds 12851 . . . . . . . . . . . 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 ) ) )
225209, 222, 223, 224syl3anc 1184 . . . . . . . . . . 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 ) ) )
226215, 225mpbird 224 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
z  x.  ( ( z ^ ( P  -  2 ) )  mod  P ) )  mod  P )  =  ( 1  mod  P
) )
227226adantr 452 . . . . . . . . 9  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  z  =/=  1 )  -> 
( ( z  x.  ( ( z ^
( P  -  2 ) )  mod  P
) )  mod  P
)  =  ( 1  mod  P ) )
228207, 227eqtrd 2467 . . . . . . . 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 ) )
229171, 228pm2.61dane 2676 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( T  gsumg  (  _I  |`  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) )  mod  P )  =  ( 1  mod 
P ) )
230 modmul1 11271 . . . . . . 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
) )
231133, 134, 146, 147, 229, 230syl221anc 1195 . . . . . 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
) )
232146zcnd 10368 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )  e.  CC )
233232mulid2d 9098 . . . . . . . 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 ) } ) ) ) )
234233oveq1d 6088 . . . . . . 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 ) )
235 ovex 6098 . . . . . . . . . . 11  |-  ( 1 ... ( P  - 
1 ) )  e. 
_V
236235elpw2 4356 . . . . . . . . . 10  |-  ( ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )  e.  ~P ( 1 ... ( P  - 
1 ) )  <->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C_  (
1 ... ( P  - 
1 ) ) )
237136, 236sylibr 204 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  e.  ~P ( 1 ... ( P  -  1 ) ) )
23811adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  S )
239 eqcom 2437 . . . . . . . . . . . . . . 15  |-  ( z  =  ( P  - 
1 )  <->  ( P  -  1 )  =  z )
240188, 239bitri 241 . . . . . . . . . . . . . 14  |-  ( z  e.  { ( P  -  1 ) }  <-> 
( P  -  1 )  =  z )
241187, 240sylnib 296 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  ( P  -  1 )  =  z )
242 oveq1 6080 . . . . . . . . . . . . . . . 16  |-  ( ( P  -  1 )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  ->  (
( P  -  1 ) ^ ( P  -  2 ) )  =  ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^
( P  -  2 ) ) )
243242oveq1d 6088 . . . . . . . . . . . . . . 15  |-  ( ( P  -  1 )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  ->  (
( ( P  - 
1 ) ^ ( P  -  2 ) )  mod  P )  =  ( ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^ ( P  - 
2 ) )  mod 
P ) )
244209, 35syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e. 
NN0 )
245 nn0uz 10512 . . . . . . . . . . . . . . . . . . 19  |-  NN0  =  ( ZZ>= `  0 )
246244, 245syl6eleq 2525 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  ( ZZ>= `  0 )
)
247 eluzfz2 11057 . . . . . . . . . . . . . . . . . 18  |-  ( ( P  -  1 )  e.  ( ZZ>= `  0
)  ->  ( P  -  1 )  e.  ( 0 ... ( P  -  1 ) ) )
248246, 247syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  ( 0 ... ( P  -  1 ) ) )
249 prmz 13075 . . . . . . . . . . . . . . . . . . . 20  |-  ( P  e.  Prime  ->  P  e.  ZZ )
250159, 249syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  e.  ZZ )
251127, 238sseldd 3341 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  ZZ )
252 zsubcl 10311 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( P  -  1 )  e.  ZZ  /\  1  e.  ZZ )  ->  ( ( P  - 
1 )  -  1 )  e.  ZZ )
253251, 51, 252sylancl 644 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  -  1 )  e.  ZZ )
254 dvdsmul1 12863 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  ZZ  /\  ( ( P  - 
1 )  -  1 )  e.  ZZ )  ->  P  ||  ( P  x.  ( ( P  -  1 )  -  1 ) ) )
255250, 253, 254syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  ||  ( P  x.  ( ( P  -  1 )  -  1 ) ) )
256209nncnd 10008 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  e.  CC )
25724a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  1  e.  CC )
258244nn0cnd 10268 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  CC )
259256, 257, 258subdird 9482 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  x.  ( P  - 
1 ) )  =  ( ( P  x.  ( P  -  1
) )  -  (
1  x.  ( P  -  1 ) ) ) )
260256, 258mulcld 9100 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  x.  ( P  -  1 ) )  e.  CC )
261260, 256, 257subsubd 9431 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  x.  ( P  -  1 ) )  -  ( P  - 
1 ) )  =  ( ( ( P  x.  ( P  - 
1 ) )  -  P )  +  1 ) )
262258mulid2d 9098 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( 1  x.  ( P  - 
1 ) )  =  ( P  -  1 ) )
263262oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  x.  ( P  -  1 ) )  -  ( 1  x.  ( P  -  1 ) ) )  =  ( ( P  x.  ( P  -  1
) )  -  ( P  -  1 ) ) )
264256, 258, 257subdid 9481 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  x.  ( ( P  - 
1 )  -  1 ) )  =  ( ( P  x.  ( P  -  1 ) )  -  ( P  x.  1 ) ) )
265256mulid1d 9097 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  x.  1 )  =  P )
266265oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  x.  ( P  -  1 ) )  -  ( P  x.  1 ) )  =  ( ( P  x.  ( P  -  1
) )  -  P
) )
267264, 266eqtrd 2467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  x.  ( ( P  - 
1 )  -  1 ) )  =  ( ( P  x.  ( P  -  1 ) )  -  P ) )
268267oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  x.  ( ( P  -  1 )  -  1 ) )  +  1 )  =  ( ( ( P  x.  ( P  - 
1 ) )  -  P )  +  1 ) )
269261, 263, 2683eqtr4d 2477 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  x.  ( P  -  1 ) )  -  ( 1  x.  ( P  -  1 ) ) )  =  ( ( P  x.  ( ( P  - 
1 )  -  1 ) )  +  1 ) )
270259, 269eqtrd 2467 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  x.  ( P  - 
1 ) )  =  ( ( P  x.  ( ( P  - 
1 )  -  1 ) )  +  1 ) )
271270oveq1d 6088 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( P  -  1 )  x.  ( P  -  1 ) )  -  1 )  =  ( ( ( P  x.  ( ( P  -  1 )  - 
1 ) )  +  1 )  -  1 ) )
272253zcnd 10368 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  -  1 )  e.  CC )
273256, 272mulcld 9100 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  x.  ( ( P  - 
1 )  -  1 ) )  e.  CC )
274 pncan 9303 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( P  x.  (
( P  -  1 )  -  1 ) )  e.  CC  /\  1  e.  CC )  ->  ( ( ( P  x.  ( ( P  -  1 )  - 
1 ) )  +  1 )  -  1 )  =  ( P  x.  ( ( P  -  1 )  - 
1 ) ) )
275273, 24, 274sylancl 644 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( P  x.  (
( P  -  1 )  -  1 ) )  +  1 )  -  1 )  =  ( P  x.  (
( P  -  1 )  -  1 ) ) )
276271, 275eqtrd 2467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
( P  -  1 )  x.  ( P  -  1 ) )  -  1 )  =  ( P  x.  (
( P  -  1 )  -  1 ) ) )
277255, 276breqtrrd 4230 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  P  ||  (
( ( P  - 
1 )  x.  ( P  -  1 ) )  -  1 ) )
278135, 238sseldd 3341 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  ( 1 ... ( P  -  1 ) ) )
279 fzm1ndvds 12893 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  NN  /\  ( P  -  1
)  e.  ( 1 ... ( P  - 
1 ) ) )  ->  -.  P  ||  ( P  -  1 ) )
280209, 278, 279syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  P  ||  ( P  -  1 ) )
281 eqid 2435 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( P  -  1 ) ^ ( P  -  2 ) )  mod  P )  =  ( ( ( P  -  1 ) ^
( P  -  2 ) )  mod  P
)
282281prmdiveq 13167 . . . . . . . . . . . . . . . . . 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
) ) )
283159, 251, 280, 282syl3anc 1184 . . . . . . . . . . . . . . . . 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
) ) )
284248, 277, 283mpbi2and 888 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  =  ( ( ( P  -  1 ) ^
( P  -  2 ) )  mod  P
) )
285212prmdivdiv 13168 . . . . . . . . . . . . . . . . 17  |-  ( ( P  e.  Prime  /\  z  e.  ( 1 ... ( P  -  1 ) ) )  ->  z  =  ( ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^ ( P  - 
2 ) )  mod 
P ) )
286159, 160, 285syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  z  =  ( ( ( ( z ^ ( P  -  2 ) )  mod  P ) ^
( P  -  2 ) )  mod  P
) )
287284, 286eqeq12d 2449 . . . . . . . . . . . . . . 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
) ) )
288243, 287syl5ibr 213 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( P  -  1 )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  ->  ( P  -  1 )  =  z ) )
289241, 288mtod 170 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  ( P  -  1 )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )
290 ioran 477 . . . . . . . . . . . . 13  |-  ( -.  ( ( P  - 
1 )  =  z  \/  ( P  - 
1 )  =  ( ( z ^ ( P  -  2 ) )  mod  P ) )  <->  ( -.  ( P  -  1 )  =  z  /\  -.  ( P  -  1
)  =  ( ( z ^ ( P  -  2 ) )  mod  P ) ) )
291241, 289, 290sylanbrc 646 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  (
( P  -  1 )  =  z  \/  ( P  -  1 )  =  ( ( z ^ ( P  -  2 ) )  mod  P ) ) )
292 ovex 6098 . . . . . . . . . . . . 13  |-  ( P  -  1 )  e. 
_V
293292elpr 3824 . . . . . . . . . . . 12  |-  ( ( P  -  1 )  e.  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  <->  ( ( P  -  1 )  =  z  \/  ( P  -  1 )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) ) )
294291, 293sylnibr 297 . . . . . . . . . . 11  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  -.  ( P  -  1 )  e.  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } )
295238, 294eldifd 3323 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( P  -  1 )  e.  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )
296 eldifi 3461 . . . . . . . . . . . . 13  |-  ( y  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  y  e.  S )
29796r19.21bi 2796 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  ( ( y ^
( P  -  2 ) )  mod  P
)  e.  S )
298296, 297sylan2 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.  S )
299 eldif 3322 . . . . . . . . . . . . 13  |-  ( y  e.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  <->  ( y  e.  S  /\  -.  y  e.  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) )
300159adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  P  e.  Prime )
301135sselda 3340 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  y  e.  ( 1 ... ( P  - 
1 ) ) )
302 eqid 2435 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( y ^ ( P  -  2 ) )  mod  P )  =  ( ( y ^
( P  -  2 ) )  mod  P
)
303302prmdivdiv 13168 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  e.  Prime  /\  y  e.  ( 1 ... ( P  -  1 ) ) )  ->  y  =  ( ( ( ( y ^ ( P  -  2 ) )  mod  P ) ^ ( P  - 
2 ) )  mod 
P ) )
304300, 301, 303syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  y  =  ( ( ( ( y ^
( P  -  2 ) )  mod  P
) ^ ( P  -  2 ) )  mod  P ) )
305 oveq1 6080 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( y ^ ( P  -  2 ) )  mod  P )  =  z  ->  (
( ( y ^
( P  -  2 ) )  mod  P
) ^ ( P  -  2 ) )  =  ( z ^
( P  -  2 ) ) )
306305oveq1d 6088 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( y ^ ( P  -  2 ) )  mod  P )  =  z  ->  (
( ( ( y ^ ( P  - 
2 ) )  mod 
P ) ^ ( P  -  2 ) )  mod  P )  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) )
307306eqeq2d 2446 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( y ^ ( P  -  2 ) )  mod  P )  =  z  ->  (
y  =  ( ( ( ( y ^
( P  -  2 ) )  mod  P
) ^ ( P  -  2 ) )  mod  P )  <->  y  =  ( ( z ^
( P  -  2 ) )  mod  P
) ) )
308304, 307syl5ibcom 212 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  ( ( ( y ^ ( P  - 
2 ) )  mod 
P )  =  z  ->  y  =  ( ( z ^ ( P  -  2 ) )  mod  P ) ) )
309 oveq1 6080 . . . . . . . . . . . . . . . . . . 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 ) ) )
310309oveq1d 6088 . . . . . . . . . . . . . . . . . 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 ) )
311286adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  z  =  ( ( ( ( z ^
( P  -  2 ) )  mod  P
) ^ ( P  -  2 ) )  mod  P ) )
312304, 311eqeq12d 2449 . . . . . . . . . . . . . . . . . 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 ) ) )
313310, 312syl5ibr 213 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
z  e.  S  /\  -.  z  e.  { ( P  -  1 ) } ) )  /\  y  e.  S )  ->  ( ( ( y ^ ( P  - 
2 ) )  mod 
P )  =  ( ( z ^ ( P  -  2 ) )  mod  P )  ->  y  =  z ) )
314308, 313orim12d 812 . . . . . . . . . . . . . . . 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 ) ) )
315 ovex 6098 . . . . . . . . . . . . . . . . 17  |-  ( ( y ^ ( P  -  2 ) )  mod  P )  e. 
_V
316315elpr 3824 . . . . . . . . . . . . . . . 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 ) ) )
317 vex 2951 . . . . . . . . . . . . . . . . . 18  |-  y  e. 
_V
318317elpr 3824 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  <->  ( y  =  z  \/  y  =  ( ( z ^ ( P  - 
2 ) )  mod 
P ) ) )
319 orcom 377 . . . . . . . . . . . . . . . . 17  |-  ( ( y  =  z  \/  y  =  ( ( z ^ ( P  -  2 ) )  mod  P ) )  <-> 
( y  =  ( ( z ^ ( P  -  2 ) )  mod  P )  \/  y  =  z ) )
320318, 319bitri 241 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) }  <->  ( y  =  ( ( z ^ ( P  - 
2 ) )  mod 
P )  \/  y  =  z ) )
321314, 316, 3203imtr4g 262 . . . . . . . . . . . . . . 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 ) } ) )
322321con3d 127 . . . . . . . . . . . . . 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
) } ) )
323322impr 603 . . . . . . . . . . . . 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 ) } )
324299, 323sylan2b 462 . . . . . . . . . . . 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 ) } )
325298, 324eldifd 3323 . . . . . . . . . . 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
) } ) )
326325ralrimiva 2781 . . . . . . . . . 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 ) } ) )
327295, 326jca 519 . . . . . . . . 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 ) } ) ) )
328 eleq2 2496 . . . . . . . . . . 11  |-  ( x  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (
( P  -  1 )  e.  x  <->  ( P  -  1 )  e.  ( S  \  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } ) ) )
329 eleq2 2496 . . . . . . . . . . . 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 ) } ) ) )
330329raleqbi1dv 2904 . . . . . . . . . . 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 ) } ) ) )
331328, 330anbi12d 692 . . . . . . . . . 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 ) } ) ) ) )
332331, 7elrab2 3086 . . . . . . . . 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 ) } ) ) ) )
333237, 327, 332sylanbrc 646 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  e.  A
)
334 wilthlem2.r . . . . . . . . 9  |-  ( ph  ->  A. s  e.  A  ( s  C.  S  ->  ( ( T  gsumg  (  _I  |`  s ) )  mod 
P )  =  (
-u 1  mod  P
) ) )
335334adantr 452 . . . . . . . 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 )
) )
336 dfss1 3537 . . . . . . . . . . 11  |-  ( { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } 
C_  S  <->  ( S  i^i  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )
337103, 336sylib 189 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  i^i  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =  {
z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )
338 vex 2951 . . . . . . . . . . . 12  |-  z  e. 
_V
339338prnz 3915 . . . . . . . . . . 11  |-  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  =/=  (/)
340339a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) }  =/=  (/) )
341337, 340eqnetrd 2616 . . . . . . . . 9  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  i^i  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =/=  (/) )
342 disj4 3668 . . . . . . . . . 10  |-  ( ( S  i^i  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )  =  (/)  <->  -.  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C.  S
)
343342necon2abii 2653 . . . . . . . . 9  |-  ( ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } ) 
C.  S  <->  ( S  i^i  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  =/=  (/) )
344341, 343sylibr 204 . . . . . . . 8  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C.  S
)
345 psseq1 3426 . . . . . . . . . 10  |-  ( s  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (
s  C.  S  <->  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  C.  S
) )
346 reseq2 5133 . . . . . . . . . . . . 13  |-  ( s  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  (  _I  |`  s )  =  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )
347346oveq2d 6089 . . . . . . . . . . . 12  |-  ( s  =  ( S  \  { z ,  ( ( z ^ ( P  -  2 ) )  mod  P ) } )  ->  ( T  gsumg  (  _I  |`  s
) )  =  ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) ) )
348347oveq1d 6088 . . . . . . . . . . 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 ) )
349348eqeq1d 2443 . . . . . . . . . 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 ) ) )
350345, 349imbi12d 312 . . . . . . . . 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 ) ) ) )
351350rspcv 3040 . . . . . . . 8  |-  ( ( S  \  { z ,  ( ( z ^ ( P  - 
2 ) )  mod 
P ) } )  e.  A  ->  ( A. s  e.  A  ( 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
) ) ) )
352333, 335, 344, 351syl3c 59 . . . . . . 7  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( ( T  gsumg  (  _I  |`  ( S  \  { z ,  ( ( z ^
( P  -  2 ) )  mod  P
) } ) ) )  mod  P )  =  ( -u 1  mod  P ) )
353234, 352eqtrd 2467 . . . . . 6  |-  ( (
ph  /\  ( z  e.  S  /\  -.  z  e.  { ( P  - 
1 ) } ) )  ->  ( (
1  x.  ( T 
gsumg  (  _I  |`  ( S 
\  { z ,  ( ( z