Metamath Proof Explorer

Theorem wilthlem2

Description: Lemma for wilth : 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 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) (Proof shortened by AV, 27-Jul-2019)

Ref Expression
Hypotheses wilthlem.t 
|- T = ( mulGrp ` CCfld )
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 gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) )
Assertion wilthlem2 
|- ( ph -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) )

Proof

Step Hyp Ref Expression
1 wilthlem.t 
 |-  T = ( mulGrp ` CCfld )
2 wilthlem.a 
 |-  A = { x e. ~P ( 1 ... ( P - 1 ) ) | ( ( P - 1 ) e. x /\ A. y e. x ( ( y ^ ( P - 2 ) ) mod P ) e. x ) }
3 wilthlem2.p 
 |-  ( ph -> P e. Prime )
4 wilthlem2.s 
 |-  ( ph -> S e. A )
5 wilthlem2.r 
 |-  ( ph -> A. s e. A ( s C. S -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) )
6 simpr 
 |-  ( ( ph /\ S C_ { ( P - 1 ) } ) -> S C_ { ( P - 1 ) } )
7 eleq2 
 |-  ( x = S -> ( ( P - 1 ) e. x <-> ( P - 1 ) e. S ) )
8 eleq2 
 |-  ( x = S -> ( ( ( y ^ ( P - 2 ) ) mod P ) e. x <-> ( ( y ^ ( P - 2 ) ) mod P ) e. S ) )
9 8 raleqbi1dv 
 |-  ( x = S -> ( A. y e. x ( ( y ^ ( P - 2 ) ) mod P ) e. x <-> A. y e. S ( ( y ^ ( P - 2 ) ) mod P ) e. S ) )
10 7 9 anbi12d 
 |-  ( 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 ) ) )
11 10 2 elrab2 
 |-  ( S e. A <-> ( S e. ~P ( 1 ... ( P - 1 ) ) /\ ( ( P - 1 ) e. S /\ A. y e. S ( ( y ^ ( P - 2 ) ) mod P ) e. S ) ) )
12 4 11 sylib 
 |-  ( ph -> ( S e. ~P ( 1 ... ( P - 1 ) ) /\ ( ( P - 1 ) e. S /\ A. y e. S ( ( y ^ ( P - 2 ) ) mod P ) e. S ) ) )
13 12 simprd 
 |-  ( ph -> ( ( P - 1 ) e. S /\ A. y e. S ( ( y ^ ( P - 2 ) ) mod P ) e. S ) )
14 13 simpld 
 |-  ( ph -> ( P - 1 ) e. S )
15 14 snssd 
 |-  ( ph -> { ( P - 1 ) } C_ S )
16 15 adantr 
 |-  ( ( ph /\ S C_ { ( P - 1 ) } ) -> { ( P - 1 ) } C_ S )
17 6 16 eqssd 
 |-  ( ( ph /\ S C_ { ( P - 1 ) } ) -> S = { ( P - 1 ) } )
18 17 reseq2d 
 |-  ( ( ph /\ S C_ { ( P - 1 ) } ) -> ( _I |` S ) = ( _I |` { ( P - 1 ) } ) )
19 mptresid 
 |-  ( _I |` { ( P - 1 ) } ) = ( z e. { ( P - 1 ) } |-> z )
20 18 19 eqtrdi 
 |-  ( ( ph /\ S C_ { ( P - 1 ) } ) -> ( _I |` S ) = ( z e. { ( P - 1 ) } |-> z ) )
21 20 oveq2d 
 |-  ( ( ph /\ S C_ { ( P - 1 ) } ) -> ( T gsum ( _I |` S ) ) = ( T gsum ( z e. { ( P - 1 ) } |-> z ) ) )
22 21 oveq1d 
 |-  ( ( ph /\ S C_ { ( P - 1 ) } ) -> ( ( T gsum ( _I |` S ) ) mod P ) = ( ( T gsum ( z e. { ( P - 1 ) } |-> z ) ) mod P ) )
23 prmnn 
 |-  ( P e. Prime -> P e. NN )
24 3 23 syl 
 |-  ( ph -> P e. NN )
25 24 nncnd 
 |-  ( ph -> P e. CC )
26 ax-1cn 
 |-  1 e. CC
27 negsub 
 |-  ( ( P e. CC /\ 1 e. CC ) -> ( P + -u 1 ) = ( P - 1 ) )
28 25 26 27 sylancl 
 |-  ( ph -> ( P + -u 1 ) = ( P - 1 ) )
29 neg1cn 
 |-  -u 1 e. CC
30 addcom 
 |-  ( ( P e. CC /\ -u 1 e. CC ) -> ( P + -u 1 ) = ( -u 1 + P ) )
31 25 29 30 sylancl 
 |-  ( ph -> ( P + -u 1 ) = ( -u 1 + P ) )
32 28 31 eqtr3d 
 |-  ( ph -> ( P - 1 ) = ( -u 1 + P ) )
33 cnring 
 |-  CCfld e. Ring
34 1 ringmgp 
 |-  ( CCfld e. Ring -> T e. Mnd )
35 33 34 mp1i 
 |-  ( ph -> T e. Mnd )
36 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
37 24 36 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
38 37 nn0cnd 
 |-  ( ph -> ( P - 1 ) e. CC )
39 cnfldbas 
 |-  CC = ( Base ` CCfld )
40 1 39 mgpbas 
 |-  CC = ( Base ` T )
41 id 
 |-  ( z = ( P - 1 ) -> z = ( P - 1 ) )
42 40 41 gsumsn 
 |-  ( ( T e. Mnd /\ ( P - 1 ) e. CC /\ ( P - 1 ) e. CC ) -> ( T gsum ( z e. { ( P - 1 ) } |-> z ) ) = ( P - 1 ) )
43 35 38 38 42 syl3anc 
 |-  ( ph -> ( T gsum ( z e. { ( P - 1 ) } |-> z ) ) = ( P - 1 ) )
44 25 mulid2d 
 |-  ( ph -> ( 1 x. P ) = P )
45 44 oveq2d 
 |-  ( ph -> ( -u 1 + ( 1 x. P ) ) = ( -u 1 + P ) )
46 32 43 45 3eqtr4d 
 |-  ( ph -> ( T gsum ( z e. { ( P - 1 ) } |-> z ) ) = ( -u 1 + ( 1 x. P ) ) )
47 46 oveq1d 
 |-  ( ph -> ( ( T gsum ( z e. { ( P - 1 ) } |-> z ) ) mod P ) = ( ( -u 1 + ( 1 x. P ) ) mod P ) )
48 neg1rr 
 |-  -u 1 e. RR
49 48 a1i 
 |-  ( ph -> -u 1 e. RR )
50 24 nnrpd 
 |-  ( ph -> P e. RR+ )
51 1zzd 
 |-  ( ph -> 1 e. ZZ )
52 modcyc 
 |-  ( ( -u 1 e. RR /\ P e. RR+ /\ 1 e. ZZ ) -> ( ( -u 1 + ( 1 x. P ) ) mod P ) = ( -u 1 mod P ) )
53 49 50 51 52 syl3anc 
 |-  ( ph -> ( ( -u 1 + ( 1 x. P ) ) mod P ) = ( -u 1 mod P ) )
54 47 53 eqtrd 
 |-  ( ph -> ( ( T gsum ( z e. { ( P - 1 ) } |-> z ) ) mod P ) = ( -u 1 mod P ) )
55 54 adantr 
 |-  ( ( ph /\ S C_ { ( P - 1 ) } ) -> ( ( T gsum ( z e. { ( P - 1 ) } |-> z ) ) mod P ) = ( -u 1 mod P ) )
56 22 55 eqtrd 
 |-  ( ( ph /\ S C_ { ( P - 1 ) } ) -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) )
57 56 ex 
 |-  ( ph -> ( S C_ { ( P - 1 ) } -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) ) )
58 nss 
 |-  ( -. S C_ { ( P - 1 ) } <-> E. z ( z e. S /\ -. z e. { ( P - 1 ) } ) )
59 cnfld1 
 |-  1 = ( 1r ` CCfld )
60 1 59 ringidval 
 |-  1 = ( 0g ` T )
61 cnfldmul 
 |-  x. = ( .r ` CCfld )
62 1 61 mgpplusg 
 |-  x. = ( +g ` T )
63 cncrng 
 |-  CCfld e. CRing
64 1 crngmgp 
 |-  ( CCfld e. CRing -> T e. CMnd )
65 63 64 ax-mp 
 |-  T e. CMnd
66 65 a1i 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> T e. CMnd )
67 4 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> S e. A )
68 f1oi 
 |-  ( _I |` S ) : S -1-1-onto-> S
69 f1of 
 |-  ( ( _I |` S ) : S -1-1-onto-> S -> ( _I |` S ) : S --> S )
70 68 69 ax-mp 
 |-  ( _I |` S ) : S --> S
71 12 simpld 
 |-  ( ph -> S e. ~P ( 1 ... ( P - 1 ) ) )
72 71 elpwid 
 |-  ( ph -> S C_ ( 1 ... ( P - 1 ) ) )
73 fzssz 
 |-  ( 1 ... ( P - 1 ) ) C_ ZZ
74 72 73 sstrdi 
 |-  ( ph -> S C_ ZZ )
75 zsscn 
 |-  ZZ C_ CC
76 74 75 sstrdi 
 |-  ( ph -> S C_ CC )
77 fss 
 |-  ( ( ( _I |` S ) : S --> S /\ S C_ CC ) -> ( _I |` S ) : S --> CC )
78 70 76 77 sylancr 
 |-  ( ph -> ( _I |` S ) : S --> CC )
79 78 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( _I |` S ) : S --> CC )
80 fzfi 
 |-  ( 1 ... ( P - 1 ) ) e. Fin
81 ssfi 
 |-  ( ( ( 1 ... ( P - 1 ) ) e. Fin /\ S C_ ( 1 ... ( P - 1 ) ) ) -> S e. Fin )
82 80 72 81 sylancr 
 |-  ( ph -> S e. Fin )
83 1ex 
 |-  1 e. _V
84 83 a1i 
 |-  ( ph -> 1 e. _V )
85 78 82 84 fdmfifsupp 
 |-  ( ph -> ( _I |` S ) finSupp 1 )
86 85 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( _I |` S ) finSupp 1 )
87 disjdif 
 |-  ( { z , ( ( z ^ ( P - 2 ) ) mod P ) } i^i ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) = (/)
88 87 a1i 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( { z , ( ( z ^ ( P - 2 ) ) mod P ) } i^i ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) = (/) )
89 undif2 
 |-  ( { z , ( ( z ^ ( P - 2 ) ) mod P ) } u. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) = ( { z , ( ( z ^ ( P - 2 ) ) mod P ) } u. S )
90 simprl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> z e. S )
91 oveq1 
 |-  ( y = z -> ( y ^ ( P - 2 ) ) = ( z ^ ( P - 2 ) ) )
92 91 oveq1d 
 |-  ( y = z -> ( ( y ^ ( P - 2 ) ) mod P ) = ( ( z ^ ( P - 2 ) ) mod P ) )
93 92 eleq1d 
 |-  ( y = z -> ( ( ( y ^ ( P - 2 ) ) mod P ) e. S <-> ( ( z ^ ( P - 2 ) ) mod P ) e. S ) )
94 13 simprd 
 |-  ( ph -> A. y e. S ( ( y ^ ( P - 2 ) ) mod P ) e. S )
95 94 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> A. y e. S ( ( y ^ ( P - 2 ) ) mod P ) e. S )
96 93 95 90 rspcdva 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( z ^ ( P - 2 ) ) mod P ) e. S )
97 90 96 prssd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> { z , ( ( z ^ ( P - 2 ) ) mod P ) } C_ S )
98 ssequn1 
 |-  ( { z , ( ( z ^ ( P - 2 ) ) mod P ) } C_ S <-> ( { z , ( ( z ^ ( P - 2 ) ) mod P ) } u. S ) = S )
99 97 98 sylib 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( { z , ( ( z ^ ( P - 2 ) ) mod P ) } u. S ) = S )
100 89 99 syl5req 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> S = ( { z , ( ( z ^ ( P - 2 ) ) mod P ) } u. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) )
101 40 60 62 66 67 79 86 88 100 gsumsplit 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( T gsum ( _I |` S ) ) = ( ( T gsum ( ( _I |` S ) |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) x. ( T gsum ( ( _I |` S ) |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) )
102 97 resabs1d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( _I |` S ) |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) = ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) )
103 102 oveq2d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( T gsum ( ( _I |` S ) |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) = ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) )
104 difss 
 |-  ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C_ S
105 resabs1 
 |-  ( ( 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 ) } ) ) )
106 104 105 ax-mp 
 |-  ( ( _I |` S ) |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) = ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) )
107 106 oveq2i 
 |-  ( T gsum ( ( _I |` S ) |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) = ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) )
108 107 a1i 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( T gsum ( ( _I |` S ) |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) = ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) )
109 103 108 oveq12d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( T gsum ( ( _I |` S ) |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) x. ( T gsum ( ( _I |` S ) |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) = ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) x. ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) )
110 101 109 eqtrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( T gsum ( _I |` S ) ) = ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) x. ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) )
111 110 oveq1d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( T gsum ( _I |` S ) ) mod P ) = ( ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) x. ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) mod P ) )
112 prfi 
 |-  { z , ( ( z ^ ( P - 2 ) ) mod P ) } e. Fin
113 112 a1i 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> { z , ( ( z ^ ( P - 2 ) ) mod P ) } e. Fin )
114 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
115 1 subrgsubm 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubMnd ` T ) )
116 114 115 mp1i 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ZZ e. ( SubMnd ` T ) )
117 f1oi 
 |-  ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) : { z , ( ( z ^ ( P - 2 ) ) mod P ) } -1-1-onto-> { z , ( ( z ^ ( P - 2 ) ) mod P ) }
118 f1of 
 |-  ( ( _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 ) } )
119 117 118 ax-mp 
 |-  ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) : { z , ( ( z ^ ( P - 2 ) ) mod P ) } --> { z , ( ( z ^ ( P - 2 ) ) mod P ) }
120 74 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> S C_ ZZ )
121 97 120 sstrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> { z , ( ( z ^ ( P - 2 ) ) mod P ) } C_ ZZ )
122 fss 
 |-  ( ( ( _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 )
123 119 121 122 sylancr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) : { z , ( ( z ^ ( P - 2 ) ) mod P ) } --> ZZ )
124 83 a1i 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> 1 e. _V )
125 123 113 124 fdmfifsupp 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) finSupp 1 )
126 60 66 113 116 123 125 gsumsubmcl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) e. ZZ )
127 126 zred 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) e. RR )
128 1red 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> 1 e. RR )
129 72 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> S C_ ( 1 ... ( P - 1 ) ) )
130 129 ssdifssd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C_ ( 1 ... ( P - 1 ) ) )
131 ssfi 
 |-  ( ( ( 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 )
132 80 130 131 sylancr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) e. Fin )
133 f1oi 
 |-  ( _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 ) } )
134 f1of 
 |-  ( ( _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 ) } ) )
135 133 134 ax-mp 
 |-  ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) : ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) --> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } )
136 120 ssdifssd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C_ ZZ )
137 fss 
 |-  ( ( ( _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 )
138 135 136 137 sylancr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) : ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) --> ZZ )
139 138 132 124 fdmfifsupp 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) finSupp 1 )
140 60 66 132 116 138 139 gsumsubmcl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) e. ZZ )
141 50 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P e. RR+ )
142 35 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> T e. Mnd )
143 76 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> S C_ CC )
144 143 90 sseldd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> z e. CC )
145 id 
 |-  ( w = z -> w = z )
146 40 145 gsumsn 
 |-  ( ( T e. Mnd /\ z e. CC /\ z e. CC ) -> ( T gsum ( w e. { z } |-> w ) ) = z )
147 142 144 144 146 syl3anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( T gsum ( w e. { z } |-> w ) ) = z )
148 147 adantr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> ( T gsum ( w e. { z } |-> w ) ) = z )
149 mptresid 
 |-  ( _I |` { z } ) = ( w e. { z } |-> w )
150 dfsn2 
 |-  { z } = { z , z }
151 animorrl 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> ( z = 1 \/ z = ( P - 1 ) ) )
152 3 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P e. Prime )
153 129 90 sseldd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> z e. ( 1 ... ( P - 1 ) ) )
154 wilthlem1 
 |-  ( ( P e. Prime /\ z e. ( 1 ... ( P - 1 ) ) ) -> ( z = ( ( z ^ ( P - 2 ) ) mod P ) <-> ( z = 1 \/ z = ( P - 1 ) ) ) )
155 152 153 154 syl2anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( z = ( ( z ^ ( P - 2 ) ) mod P ) <-> ( z = 1 \/ z = ( P - 1 ) ) ) )
156 155 biimpar 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ ( z = 1 \/ z = ( P - 1 ) ) ) -> z = ( ( z ^ ( P - 2 ) ) mod P ) )
157 151 156 syldan 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> z = ( ( z ^ ( P - 2 ) ) mod P ) )
158 157 preq2d 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> { z , z } = { z , ( ( z ^ ( P - 2 ) ) mod P ) } )
159 150 158 syl5eq 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> { z } = { z , ( ( z ^ ( P - 2 ) ) mod P ) } )
160 159 reseq2d 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> ( _I |` { z } ) = ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) )
161 149 160 eqtr3id 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> ( w e. { z } |-> w ) = ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) )
162 161 oveq2d 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> ( T gsum ( w e. { z } |-> w ) ) = ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) )
163 simpr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> z = 1 )
164 148 162 163 3eqtr3d 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) = 1 )
165 164 oveq1d 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z = 1 ) -> ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) mod P ) = ( 1 mod P ) )
166 df-pr 
 |-  { z , ( ( z ^ ( P - 2 ) ) mod P ) } = ( { z } u. { ( ( z ^ ( P - 2 ) ) mod P ) } )
167 166 reseq2i 
 |-  ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) = ( _I |` ( { z } u. { ( ( z ^ ( P - 2 ) ) mod P ) } ) )
168 mptresid 
 |-  ( _I |` ( { z } u. { ( ( z ^ ( P - 2 ) ) mod P ) } ) ) = ( w e. ( { z } u. { ( ( z ^ ( P - 2 ) ) mod P ) } ) |-> w )
169 167 168 eqtri 
 |-  ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) = ( w e. ( { z } u. { ( ( z ^ ( P - 2 ) ) mod P ) } ) |-> w )
170 169 oveq2i 
 |-  ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) = ( T gsum ( w e. ( { z } u. { ( ( z ^ ( P - 2 ) ) mod P ) } ) |-> w ) )
171 65 a1i 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> T e. CMnd )
172 snfi 
 |-  { z } e. Fin
173 172 a1i 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> { z } e. Fin )
174 elsni 
 |-  ( w e. { z } -> w = z )
175 174 adantl 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ w e. { z } ) -> w = z )
176 144 adantr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ w e. { z } ) -> z e. CC )
177 175 176 eqeltrd 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ w e. { z } ) -> w e. CC )
178 177 adantlr 
 |-  ( ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) /\ w e. { z } ) -> w e. CC )
179 143 96 sseldd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( z ^ ( P - 2 ) ) mod P ) e. CC )
180 179 adantr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> ( ( z ^ ( P - 2 ) ) mod P ) e. CC )
181 simprr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. z e. { ( P - 1 ) } )
182 velsn 
 |-  ( z e. { ( P - 1 ) } <-> z = ( P - 1 ) )
183 181 182 sylnib 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. z = ( P - 1 ) )
184 biorf 
 |-  ( -. z = ( P - 1 ) -> ( z = 1 <-> ( z = ( P - 1 ) \/ z = 1 ) ) )
185 183 184 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( z = 1 <-> ( z = ( P - 1 ) \/ z = 1 ) ) )
186 ovex 
 |-  ( ( z ^ ( P - 2 ) ) mod P ) e. _V
187 186 elsn 
 |-  ( ( ( z ^ ( P - 2 ) ) mod P ) e. { z } <-> ( ( z ^ ( P - 2 ) ) mod P ) = z )
188 eqcom 
 |-  ( ( ( z ^ ( P - 2 ) ) mod P ) = z <-> z = ( ( z ^ ( P - 2 ) ) mod P ) )
189 187 188 bitri 
 |-  ( ( ( z ^ ( P - 2 ) ) mod P ) e. { z } <-> z = ( ( z ^ ( P - 2 ) ) mod P ) )
190 orcom 
 |-  ( ( z = ( P - 1 ) \/ z = 1 ) <-> ( z = 1 \/ z = ( P - 1 ) ) )
191 155 189 190 3bitr4g 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( ( z ^ ( P - 2 ) ) mod P ) e. { z } <-> ( z = ( P - 1 ) \/ z = 1 ) ) )
192 185 191 bitr4d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( z = 1 <-> ( ( z ^ ( P - 2 ) ) mod P ) e. { z } ) )
193 192 necon3abid 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( z =/= 1 <-> -. ( ( z ^ ( P - 2 ) ) mod P ) e. { z } ) )
194 193 biimpa 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> -. ( ( z ^ ( P - 2 ) ) mod P ) e. { z } )
195 id 
 |-  ( w = ( ( z ^ ( P - 2 ) ) mod P ) -> w = ( ( z ^ ( P - 2 ) ) mod P ) )
196 40 62 171 173 178 180 194 180 195 gsumunsn 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> ( T gsum ( w e. ( { z } u. { ( ( z ^ ( P - 2 ) ) mod P ) } ) |-> w ) ) = ( ( T gsum ( w e. { z } |-> w ) ) x. ( ( z ^ ( P - 2 ) ) mod P ) ) )
197 170 196 syl5eq 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) = ( ( T gsum ( w e. { z } |-> w ) ) x. ( ( z ^ ( P - 2 ) ) mod P ) ) )
198 147 adantr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> ( T gsum ( w e. { z } |-> w ) ) = z )
199 198 oveq1d 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> ( ( T gsum ( w e. { z } |-> w ) ) x. ( ( z ^ ( P - 2 ) ) mod P ) ) = ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) )
200 197 199 eqtrd 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) = ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) )
201 200 oveq1d 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) mod P ) = ( ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) mod P ) )
202 elfzelz 
 |-  ( z e. ( 1 ... ( P - 1 ) ) -> z e. ZZ )
203 153 202 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> z e. ZZ )
204 24 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P e. NN )
205 fzm1ndvds 
 |-  ( ( P e. NN /\ z e. ( 1 ... ( P - 1 ) ) ) -> -. P || z )
206 204 153 205 syl2anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. P || z )
207 eqid 
 |-  ( ( z ^ ( P - 2 ) ) mod P ) = ( ( z ^ ( P - 2 ) ) mod P )
208 207 prmdiv 
 |-  ( ( 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 ) ) )
209 152 203 206 208 syl3anc 
 |-  ( ( 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 ) ) )
210 209 simprd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P || ( ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) - 1 ) )
211 elfznn 
 |-  ( z e. ( 1 ... ( P - 1 ) ) -> z e. NN )
212 153 211 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> z e. NN )
213 129 96 sseldd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( z ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) )
214 elfznn 
 |-  ( ( ( z ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) -> ( ( z ^ ( P - 2 ) ) mod P ) e. NN )
215 213 214 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( z ^ ( P - 2 ) ) mod P ) e. NN )
216 212 215 nnmulcld 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) e. NN )
217 216 nnzd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) e. ZZ )
218 1zzd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> 1 e. ZZ )
219 moddvds 
 |-  ( ( 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 ) ) )
220 204 217 218 219 syl3anc 
 |-  ( ( 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 ) ) )
221 210 220 mpbird 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) mod P ) = ( 1 mod P ) )
222 221 adantr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> ( ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) mod P ) = ( 1 mod P ) )
223 201 222 eqtrd 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) mod P ) = ( 1 mod P ) )
224 165 223 pm2.61dane 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) mod P ) = ( 1 mod P ) )
225 modmul1 
 |-  ( ( ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) e. RR /\ 1 e. RR ) /\ ( ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) e. ZZ /\ P e. RR+ ) /\ ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) mod P ) = ( 1 mod P ) ) -> ( ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) x. ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) mod P ) = ( ( 1 x. ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) mod P ) )
226 127 128 140 141 224 225 syl221anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) x. ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) mod P ) = ( ( 1 x. ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) mod P ) )
227 140 zcnd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) e. CC )
228 227 mulid2d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( 1 x. ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) = ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) )
229 228 oveq1d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( 1 x. ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) mod P ) = ( ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) mod P ) )
230 sseqin2 
 |-  ( { z , ( ( z ^ ( P - 2 ) ) mod P ) } C_ S <-> ( S i^i { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) = { z , ( ( z ^ ( P - 2 ) ) mod P ) } )
231 97 230 sylib 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S i^i { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) = { z , ( ( z ^ ( P - 2 ) ) mod P ) } )
232 vex 
 |-  z e. _V
233 232 prnz 
 |-  { z , ( ( z ^ ( P - 2 ) ) mod P ) } =/= (/)
234 233 a1i 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> { z , ( ( z ^ ( P - 2 ) ) mod P ) } =/= (/) )
235 231 234 eqnetrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S i^i { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) =/= (/) )
236 disj4 
 |-  ( ( S i^i { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) = (/) <-> -. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C. S )
237 236 necon2abii 
 |-  ( ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C. S <-> ( S i^i { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) =/= (/) )
238 235 237 sylibr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C. S )
239 psseq1 
 |-  ( s = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( s C. S <-> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C. S ) )
240 reseq2 
 |-  ( s = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( _I |` s ) = ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) )
241 240 oveq2d 
 |-  ( s = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( T gsum ( _I |` s ) ) = ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) )
242 241 oveq1d 
 |-  ( s = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( ( T gsum ( _I |` s ) ) mod P ) = ( ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) mod P ) )
243 242 eqeq1d 
 |-  ( s = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) <-> ( ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) mod P ) = ( -u 1 mod P ) ) )
244 239 243 imbi12d 
 |-  ( s = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( ( s C. S -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) <-> ( ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C. S -> ( ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) mod P ) = ( -u 1 mod P ) ) ) )
245 5 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> A. s e. A ( s C. S -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) )
246 ovex 
 |-  ( 1 ... ( P - 1 ) ) e. _V
247 246 elpw2 
 |-  ( ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) e. ~P ( 1 ... ( P - 1 ) ) <-> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C_ ( 1 ... ( P - 1 ) ) )
248 130 247 sylibr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) e. ~P ( 1 ... ( P - 1 ) ) )
249 14 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. S )
250 eqcom 
 |-  ( z = ( P - 1 ) <-> ( P - 1 ) = z )
251 182 250 bitri 
 |-  ( z e. { ( P - 1 ) } <-> ( P - 1 ) = z )
252 181 251 sylnib 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. ( P - 1 ) = z )
253 oveq1 
 |-  ( ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) -> ( ( P - 1 ) ^ ( P - 2 ) ) = ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) )
254 253 oveq1d 
 |-  ( ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) -> ( ( ( P - 1 ) ^ ( P - 2 ) ) mod P ) = ( ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
255 204 36 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. NN0 )
256 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
257 255 256 eleqtrdi 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. ( ZZ>= ` 0 ) )
258 eluzfz2 
 |-  ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> ( P - 1 ) e. ( 0 ... ( P - 1 ) ) )
259 257 258 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. ( 0 ... ( P - 1 ) ) )
260 prmz 
 |-  ( P e. Prime -> P e. ZZ )
261 152 260 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P e. ZZ )
262 120 249 sseldd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. ZZ )
263 1z 
 |-  1 e. ZZ
264 zsubcl 
 |-  ( ( ( P - 1 ) e. ZZ /\ 1 e. ZZ ) -> ( ( P - 1 ) - 1 ) e. ZZ )
265 262 263 264 sylancl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P - 1 ) - 1 ) e. ZZ )
266 dvdsmul1 
 |-  ( ( P e. ZZ /\ ( ( P - 1 ) - 1 ) e. ZZ ) -> P || ( P x. ( ( P - 1 ) - 1 ) ) )
267 261 265 266 syl2anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P || ( P x. ( ( P - 1 ) - 1 ) ) )
268 204 nncnd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P e. CC )
269 265 zcnd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P - 1 ) - 1 ) e. CC )
270 268 269 mulcld 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P x. ( ( P - 1 ) - 1 ) ) e. CC )
271 1cnd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> 1 e. CC )
272 255 nn0cnd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. CC )
273 268 271 272 subdird 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P - 1 ) x. ( P - 1 ) ) = ( ( P x. ( P - 1 ) ) - ( 1 x. ( P - 1 ) ) ) )
274 268 272 mulcld 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P x. ( P - 1 ) ) e. CC )
275 274 268 271 subsubd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P x. ( P - 1 ) ) - ( P - 1 ) ) = ( ( ( P x. ( P - 1 ) ) - P ) + 1 ) )
276 272 mulid2d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( 1 x. ( P - 1 ) ) = ( P - 1 ) )
277 276 oveq2d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P x. ( P - 1 ) ) - ( 1 x. ( P - 1 ) ) ) = ( ( P x. ( P - 1 ) ) - ( P - 1 ) ) )
278 268 272 muls1d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P x. ( ( P - 1 ) - 1 ) ) = ( ( P x. ( P - 1 ) ) - P ) )
279 278 oveq1d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P x. ( ( P - 1 ) - 1 ) ) + 1 ) = ( ( ( P x. ( P - 1 ) ) - P ) + 1 ) )
280 275 277 279 3eqtr4d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P x. ( P - 1 ) ) - ( 1 x. ( P - 1 ) ) ) = ( ( P x. ( ( P - 1 ) - 1 ) ) + 1 ) )
281 273 280 eqtrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P - 1 ) x. ( P - 1 ) ) = ( ( P x. ( ( P - 1 ) - 1 ) ) + 1 ) )
282 270 271 281 mvrraddd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( ( P - 1 ) x. ( P - 1 ) ) - 1 ) = ( P x. ( ( P - 1 ) - 1 ) ) )
283 267 282 breqtrrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P || ( ( ( P - 1 ) x. ( P - 1 ) ) - 1 ) )
284 129 249 sseldd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. ( 1 ... ( P - 1 ) ) )
285 fzm1ndvds 
 |-  ( ( P e. NN /\ ( P - 1 ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( P - 1 ) )
286 204 284 285 syl2anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. P || ( P - 1 ) )
287 eqid 
 |-  ( ( ( P - 1 ) ^ ( P - 2 ) ) mod P ) = ( ( ( P - 1 ) ^ ( P - 2 ) ) mod P )
288 287 prmdiveq 
 |-  ( ( 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 ) ) )
289 152 262 286 288 syl3anc 
 |-  ( ( 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 ) ) )
290 259 283 289 mpbi2and 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) = ( ( ( P - 1 ) ^ ( P - 2 ) ) mod P ) )
291 207 prmdivdiv 
 |-  ( ( P e. Prime /\ z e. ( 1 ... ( P - 1 ) ) ) -> z = ( ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
292 152 153 291 syl2anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> z = ( ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
293 290 292 eqeq12d 
 |-  ( ( 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 ) ) )
294 254 293 syl5ibr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) -> ( P - 1 ) = z ) )
295 252 294 mtod 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) )
296 ioran 
 |-  ( -. ( ( P - 1 ) = z \/ ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) ) <-> ( -. ( P - 1 ) = z /\ -. ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) ) )
297 252 295 296 sylanbrc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. ( ( P - 1 ) = z \/ ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) ) )
298 ovex 
 |-  ( P - 1 ) e. _V
299 298 elpr 
 |-  ( ( P - 1 ) e. { z , ( ( z ^ ( P - 2 ) ) mod P ) } <-> ( ( P - 1 ) = z \/ ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) ) )
300 297 299 sylnibr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. ( P - 1 ) e. { z , ( ( z ^ ( P - 2 ) ) mod P ) } )
301 249 300 eldifd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) )
302 eldifi 
 |-  ( y e. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> y e. S )
303 95 r19.21bi 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> ( ( y ^ ( P - 2 ) ) mod P ) e. S )
304 302 303 sylan2 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) -> ( ( y ^ ( P - 2 ) ) mod P ) e. S )
305 eldif 
 |-  ( y e. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) <-> ( y e. S /\ -. y e. { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) )
306 152 adantr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> P e. Prime )
307 129 sselda 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> y e. ( 1 ... ( P - 1 ) ) )
308 eqid 
 |-  ( ( y ^ ( P - 2 ) ) mod P ) = ( ( y ^ ( P - 2 ) ) mod P )
309 308 prmdivdiv 
 |-  ( ( P e. Prime /\ y e. ( 1 ... ( P - 1 ) ) ) -> y = ( ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
310 306 307 309 syl2anc 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> y = ( ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
311 oveq1 
 |-  ( ( ( y ^ ( P - 2 ) ) mod P ) = z -> ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) = ( z ^ ( P - 2 ) ) )
312 311 oveq1d 
 |-  ( ( ( y ^ ( P - 2 ) ) mod P ) = z -> ( ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) = ( ( z ^ ( P - 2 ) ) mod P ) )
313 312 eqeq2d 
 |-  ( ( ( y ^ ( P - 2 ) ) mod P ) = z -> ( y = ( ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) <-> y = ( ( z ^ ( P - 2 ) ) mod P ) ) )
314 310 313 syl5ibcom 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> ( ( ( y ^ ( P - 2 ) ) mod P ) = z -> y = ( ( z ^ ( P - 2 ) ) mod P ) ) )
315 oveq1 
 |-  ( ( ( y ^ ( P - 2 ) ) mod P ) = ( ( z ^ ( P - 2 ) ) mod P ) -> ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) = ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) )
316 315 oveq1d 
 |-  ( ( ( 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 ) )
317 292 adantr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> z = ( ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
318 310 317 eqeq12d 
 |-  ( ( ( 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 ) ) )
319 316 318 syl5ibr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> ( ( ( y ^ ( P - 2 ) ) mod P ) = ( ( z ^ ( P - 2 ) ) mod P ) -> y = z ) )
320 314 319 orim12d 
 |-  ( ( ( 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 ) ) )
321 ovex 
 |-  ( ( y ^ ( P - 2 ) ) mod P ) e. _V
322 321 elpr 
 |-  ( ( ( 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 ) ) )
323 vex 
 |-  y e. _V
324 323 elpr 
 |-  ( y e. { z , ( ( z ^ ( P - 2 ) ) mod P ) } <-> ( y = z \/ y = ( ( z ^ ( P - 2 ) ) mod P ) ) )
325 orcom 
 |-  ( ( y = z \/ y = ( ( z ^ ( P - 2 ) ) mod P ) ) <-> ( y = ( ( z ^ ( P - 2 ) ) mod P ) \/ y = z ) )
326 324 325 bitri 
 |-  ( y e. { z , ( ( z ^ ( P - 2 ) ) mod P ) } <-> ( y = ( ( z ^ ( P - 2 ) ) mod P ) \/ y = z ) )
327 320 322 326 3imtr4g 
 |-  ( ( ( 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 ) } ) )
328 327 con3d 
 |-  ( ( ( 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 ) } ) )
329 328 impr 
 |-  ( ( ( 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 ) } )
330 305 329 sylan2b 
 |-  ( ( ( 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 ) } )
331 304 330 eldifd 
 |-  ( ( ( 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 ) } ) )
332 331 ralrimiva 
 |-  ( ( 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 ) } ) )
333 301 332 jca 
 |-  ( ( 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 ) } ) ) )
334 eleq2 
 |-  ( x = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( ( P - 1 ) e. x <-> ( P - 1 ) e. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) )
335 eleq2 
 |-  ( 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 ) } ) ) )
336 335 raleqbi1dv 
 |-  ( 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 ) } ) ) )
337 334 336 anbi12d 
 |-  ( 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 ) } ) ) ) )
338 337 2 elrab2 
 |-  ( ( 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 ) } ) ) ) )
339 248 333 338 sylanbrc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) e. A )
340 244 245 339 rspcdva 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C. S -> ( ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) mod P ) = ( -u 1 mod P ) ) )
341 238 340 mpd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) mod P ) = ( -u 1 mod P ) )
342 229 341 eqtrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( 1 x. ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) ) mod P ) = ( -u 1 mod P ) )
343 111 226 342 3eqtrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) )
344 343 ex 
 |-  ( ph -> ( ( z e. S /\ -. z e. { ( P - 1 ) } ) -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) ) )
345 344 exlimdv 
 |-  ( ph -> ( E. z ( z e. S /\ -. z e. { ( P - 1 ) } ) -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) ) )
346 58 345 syl5bi 
 |-  ( ph -> ( -. S C_ { ( P - 1 ) } -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) ) )
347 57 346 pm2.61d 
 |-  ( ph -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) )