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 eqtr2id 
 |-  ( ( 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 153 elfzelzd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> z e. ZZ )
203 24 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P e. NN )
204 fzm1ndvds 
 |-  ( ( P e. NN /\ z e. ( 1 ... ( P - 1 ) ) ) -> -. P || z )
205 203 153 204 syl2anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. P || z )
206 eqid 
 |-  ( ( z ^ ( P - 2 ) ) mod P ) = ( ( z ^ ( P - 2 ) ) mod P )
207 206 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 ) ) )
208 152 202 205 207 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 ) ) )
209 208 simprd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P || ( ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) - 1 ) )
210 elfznn 
 |-  ( z e. ( 1 ... ( P - 1 ) ) -> z e. NN )
211 153 210 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> z e. NN )
212 129 96 sseldd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( z ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) )
213 elfznn 
 |-  ( ( ( z ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) -> ( ( z ^ ( P - 2 ) ) mod P ) e. NN )
214 212 213 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( z ^ ( P - 2 ) ) mod P ) e. NN )
215 211 214 nnmulcld 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) e. NN )
216 215 nnzd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) e. ZZ )
217 1zzd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> 1 e. ZZ )
218 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 ) ) )
219 203 216 217 218 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 ) ) )
220 209 219 mpbird 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) mod P ) = ( 1 mod P ) )
221 220 adantr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ z =/= 1 ) -> ( ( z x. ( ( z ^ ( P - 2 ) ) mod P ) ) mod P ) = ( 1 mod P ) )
222 201 221 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 ) )
223 165 222 pm2.61dane 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( T gsum ( _I |` { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) mod P ) = ( 1 mod P ) )
224 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 ) )
225 127 128 140 141 223 224 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 ) )
226 140 zcnd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) e. CC )
227 226 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 ) } ) ) ) )
228 227 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 ) )
229 sseqin2 
 |-  ( { z , ( ( z ^ ( P - 2 ) ) mod P ) } C_ S <-> ( S i^i { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) = { z , ( ( z ^ ( P - 2 ) ) mod P ) } )
230 97 229 sylib 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S i^i { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) = { z , ( ( z ^ ( P - 2 ) ) mod P ) } )
231 vex 
 |-  z e. _V
232 231 prnz 
 |-  { z , ( ( z ^ ( P - 2 ) ) mod P ) } =/= (/)
233 232 a1i 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> { z , ( ( z ^ ( P - 2 ) ) mod P ) } =/= (/) )
234 230 233 eqnetrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S i^i { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) =/= (/) )
235 disj4 
 |-  ( ( S i^i { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) = (/) <-> -. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C. S )
236 235 necon2abii 
 |-  ( ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C. S <-> ( S i^i { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) =/= (/) )
237 234 236 sylibr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C. S )
238 psseq1 
 |-  ( s = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( s C. S <-> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C. S ) )
239 reseq2 
 |-  ( s = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( _I |` s ) = ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) )
240 239 oveq2d 
 |-  ( s = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( T gsum ( _I |` s ) ) = ( T gsum ( _I |` ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) ) )
241 240 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 ) )
242 241 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 ) ) )
243 238 242 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 ) ) ) )
244 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 ) ) )
245 ovex 
 |-  ( 1 ... ( P - 1 ) ) e. _V
246 245 elpw2 
 |-  ( ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) e. ~P ( 1 ... ( P - 1 ) ) <-> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) C_ ( 1 ... ( P - 1 ) ) )
247 130 246 sylibr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) e. ~P ( 1 ... ( P - 1 ) ) )
248 14 adantr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. S )
249 eqcom 
 |-  ( z = ( P - 1 ) <-> ( P - 1 ) = z )
250 182 249 bitri 
 |-  ( z e. { ( P - 1 ) } <-> ( P - 1 ) = z )
251 181 250 sylnib 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. ( P - 1 ) = z )
252 oveq1 
 |-  ( ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) -> ( ( P - 1 ) ^ ( P - 2 ) ) = ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) )
253 252 oveq1d 
 |-  ( ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) -> ( ( ( P - 1 ) ^ ( P - 2 ) ) mod P ) = ( ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
254 203 36 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. NN0 )
255 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
256 254 255 eleqtrdi 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. ( ZZ>= ` 0 ) )
257 eluzfz2 
 |-  ( ( P - 1 ) e. ( ZZ>= ` 0 ) -> ( P - 1 ) e. ( 0 ... ( P - 1 ) ) )
258 256 257 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. ( 0 ... ( P - 1 ) ) )
259 prmz 
 |-  ( P e. Prime -> P e. ZZ )
260 152 259 syl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P e. ZZ )
261 120 248 sseldd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. ZZ )
262 1z 
 |-  1 e. ZZ
263 zsubcl 
 |-  ( ( ( P - 1 ) e. ZZ /\ 1 e. ZZ ) -> ( ( P - 1 ) - 1 ) e. ZZ )
264 261 262 263 sylancl 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P - 1 ) - 1 ) e. ZZ )
265 dvdsmul1 
 |-  ( ( P e. ZZ /\ ( ( P - 1 ) - 1 ) e. ZZ ) -> P || ( P x. ( ( P - 1 ) - 1 ) ) )
266 260 264 265 syl2anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P || ( P x. ( ( P - 1 ) - 1 ) ) )
267 203 nncnd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P e. CC )
268 264 zcnd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P - 1 ) - 1 ) e. CC )
269 267 268 mulcld 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P x. ( ( P - 1 ) - 1 ) ) e. CC )
270 1cnd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> 1 e. CC )
271 254 nn0cnd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. CC )
272 267 270 271 subdird 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P - 1 ) x. ( P - 1 ) ) = ( ( P x. ( P - 1 ) ) - ( 1 x. ( P - 1 ) ) ) )
273 267 271 mulcld 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P x. ( P - 1 ) ) e. CC )
274 273 267 270 subsubd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P x. ( P - 1 ) ) - ( P - 1 ) ) = ( ( ( P x. ( P - 1 ) ) - P ) + 1 ) )
275 271 mulid2d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( 1 x. ( P - 1 ) ) = ( P - 1 ) )
276 275 oveq2d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P x. ( P - 1 ) ) - ( 1 x. ( P - 1 ) ) ) = ( ( P x. ( P - 1 ) ) - ( P - 1 ) ) )
277 267 271 muls1d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P x. ( ( P - 1 ) - 1 ) ) = ( ( P x. ( P - 1 ) ) - P ) )
278 277 oveq1d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P x. ( ( P - 1 ) - 1 ) ) + 1 ) = ( ( ( P x. ( P - 1 ) ) - P ) + 1 ) )
279 274 276 278 3eqtr4d 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P x. ( P - 1 ) ) - ( 1 x. ( P - 1 ) ) ) = ( ( P x. ( ( P - 1 ) - 1 ) ) + 1 ) )
280 272 279 eqtrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P - 1 ) x. ( P - 1 ) ) = ( ( P x. ( ( P - 1 ) - 1 ) ) + 1 ) )
281 269 270 280 mvrraddd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( ( P - 1 ) x. ( P - 1 ) ) - 1 ) = ( P x. ( ( P - 1 ) - 1 ) ) )
282 266 281 breqtrrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> P || ( ( ( P - 1 ) x. ( P - 1 ) ) - 1 ) )
283 129 248 sseldd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. ( 1 ... ( P - 1 ) ) )
284 fzm1ndvds 
 |-  ( ( P e. NN /\ ( P - 1 ) e. ( 1 ... ( P - 1 ) ) ) -> -. P || ( P - 1 ) )
285 203 283 284 syl2anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. P || ( P - 1 ) )
286 eqid 
 |-  ( ( ( P - 1 ) ^ ( P - 2 ) ) mod P ) = ( ( ( P - 1 ) ^ ( P - 2 ) ) mod P )
287 286 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 ) ) )
288 152 261 285 287 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 ) ) )
289 258 282 288 mpbi2and 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) = ( ( ( P - 1 ) ^ ( P - 2 ) ) mod P ) )
290 206 prmdivdiv 
 |-  ( ( P e. Prime /\ z e. ( 1 ... ( P - 1 ) ) ) -> z = ( ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
291 152 153 290 syl2anc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> z = ( ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
292 289 291 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 ) ) )
293 253 292 syl5ibr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) -> ( P - 1 ) = z ) )
294 251 293 mtod 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) )
295 ioran 
 |-  ( -. ( ( P - 1 ) = z \/ ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) ) <-> ( -. ( P - 1 ) = z /\ -. ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) ) )
296 251 294 295 sylanbrc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. ( ( P - 1 ) = z \/ ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) ) )
297 ovex 
 |-  ( P - 1 ) e. _V
298 297 elpr 
 |-  ( ( P - 1 ) e. { z , ( ( z ^ ( P - 2 ) ) mod P ) } <-> ( ( P - 1 ) = z \/ ( P - 1 ) = ( ( z ^ ( P - 2 ) ) mod P ) ) )
299 296 298 sylnibr 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> -. ( P - 1 ) e. { z , ( ( z ^ ( P - 2 ) ) mod P ) } )
300 248 299 eldifd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( P - 1 ) e. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) )
301 eldifi 
 |-  ( y e. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> y e. S )
302 95 r19.21bi 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> ( ( y ^ ( P - 2 ) ) mod P ) e. S )
303 301 302 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 )
304 eldif 
 |-  ( y e. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) <-> ( y e. S /\ -. y e. { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) )
305 152 adantr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> P e. Prime )
306 129 sselda 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> y e. ( 1 ... ( P - 1 ) ) )
307 eqid 
 |-  ( ( y ^ ( P - 2 ) ) mod P ) = ( ( y ^ ( P - 2 ) ) mod P )
308 307 prmdivdiv 
 |-  ( ( P e. Prime /\ y e. ( 1 ... ( P - 1 ) ) ) -> y = ( ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
309 305 306 308 syl2anc 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> y = ( ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
310 oveq1 
 |-  ( ( ( y ^ ( P - 2 ) ) mod P ) = z -> ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) = ( z ^ ( P - 2 ) ) )
311 310 oveq1d 
 |-  ( ( ( y ^ ( P - 2 ) ) mod P ) = z -> ( ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) = ( ( z ^ ( P - 2 ) ) mod P ) )
312 311 eqeq2d 
 |-  ( ( ( y ^ ( P - 2 ) ) mod P ) = z -> ( y = ( ( ( ( y ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) <-> y = ( ( z ^ ( P - 2 ) ) mod P ) ) )
313 309 312 syl5ibcom 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> ( ( ( y ^ ( P - 2 ) ) mod P ) = z -> y = ( ( z ^ ( P - 2 ) ) mod P ) ) )
314 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 ) ) )
315 314 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 ) )
316 291 adantr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> z = ( ( ( ( z ^ ( P - 2 ) ) mod P ) ^ ( P - 2 ) ) mod P ) )
317 309 316 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 ) ) )
318 315 317 syl5ibr 
 |-  ( ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) /\ y e. S ) -> ( ( ( y ^ ( P - 2 ) ) mod P ) = ( ( z ^ ( P - 2 ) ) mod P ) -> y = z ) )
319 313 318 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 ) ) )
320 ovex 
 |-  ( ( y ^ ( P - 2 ) ) mod P ) e. _V
321 320 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 ) ) )
322 vex 
 |-  y e. _V
323 322 elpr 
 |-  ( y e. { z , ( ( z ^ ( P - 2 ) ) mod P ) } <-> ( y = z \/ y = ( ( z ^ ( P - 2 ) ) mod P ) ) )
324 orcom 
 |-  ( ( y = z \/ y = ( ( z ^ ( P - 2 ) ) mod P ) ) <-> ( y = ( ( z ^ ( P - 2 ) ) mod P ) \/ y = z ) )
325 323 324 bitri 
 |-  ( y e. { z , ( ( z ^ ( P - 2 ) ) mod P ) } <-> ( y = ( ( z ^ ( P - 2 ) ) mod P ) \/ y = z ) )
326 319 321 325 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 ) } ) )
327 326 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 ) } ) )
328 327 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 ) } )
329 304 328 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 ) } )
330 303 329 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 ) } ) )
331 330 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 ) } ) )
332 300 331 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 ) } ) ) )
333 eleq2 
 |-  ( x = ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) -> ( ( P - 1 ) e. x <-> ( P - 1 ) e. ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) ) )
334 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 ) } ) ) )
335 334 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 ) } ) ) )
336 333 335 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 ) } ) ) ) )
337 336 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 ) } ) ) ) )
338 247 332 337 sylanbrc 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( S \ { z , ( ( z ^ ( P - 2 ) ) mod P ) } ) e. A )
339 243 244 338 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 ) ) )
340 237 339 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 ) )
341 228 340 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 ) )
342 111 225 341 3eqtrd 
 |-  ( ( ph /\ ( z e. S /\ -. z e. { ( P - 1 ) } ) ) -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) )
343 342 ex 
 |-  ( ph -> ( ( z e. S /\ -. z e. { ( P - 1 ) } ) -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) ) )
344 343 exlimdv 
 |-  ( ph -> ( E. z ( z e. S /\ -. z e. { ( P - 1 ) } ) -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) ) )
345 58 344 syl5bi 
 |-  ( ph -> ( -. S C_ { ( P - 1 ) } -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) ) )
346 57 345 pm2.61d 
 |-  ( ph -> ( ( T gsum ( _I |` S ) ) mod P ) = ( -u 1 mod P ) )