Metamath Proof Explorer

Theorem wilthlem3

Description: Lemma for wilth . Here we round out the argument of wilthlem2 with the final step of the induction. The induction argument shows that every subset of 1 ... ( P - 1 ) that is closed under inverse and contains P - 1 multiplies to -u 1 mod P , and clearly 1 ... ( P - 1 ) itself is such a set. Thus, the product of all the elements is -u 1 , and all that is left is to translate the group sum notation (which we used for its unordered summing capabilities) into an ordered sequence to match the definition of the factorial. (Contributed by Mario Carneiro, 24-Jan-2015) (Proof shortened by AV, 27-Jul-2019)

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 ) }
Assertion wilthlem3 
|- ( P e. Prime -> P || ( ( ! ` ( P - 1 ) ) + 1 ) )

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 prmuz2 
 |-  ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
4 uz2m1nn 
 |-  ( P e. ( ZZ>= ` 2 ) -> ( P - 1 ) e. NN )
5 3 4 syl 
 |-  ( P e. Prime -> ( P - 1 ) e. NN )
6 nnuz 
 |-  NN = ( ZZ>= ` 1 )
7 5 6 eleqtrdi 
 |-  ( P e. Prime -> ( P - 1 ) e. ( ZZ>= ` 1 ) )
8 eluzfz2 
 |-  ( ( P - 1 ) e. ( ZZ>= ` 1 ) -> ( P - 1 ) e. ( 1 ... ( P - 1 ) ) )
9 7 8 syl 
 |-  ( P e. Prime -> ( P - 1 ) e. ( 1 ... ( P - 1 ) ) )
10 simpl 
 |-  ( ( P e. Prime /\ y e. ( 1 ... ( P - 1 ) ) ) -> P e. Prime )
11 elfzelz 
 |-  ( y e. ( 1 ... ( P - 1 ) ) -> y e. ZZ )
12 11 adantl 
 |-  ( ( P e. Prime /\ y e. ( 1 ... ( P - 1 ) ) ) -> y e. ZZ )
13 prmnn 
 |-  ( P e. Prime -> P e. NN )
14 fzm1ndvds 
 |-  ( ( P e. NN /\ y e. ( 1 ... ( P - 1 ) ) ) -> -. P || y )
15 13 14 sylan 
 |-  ( ( P e. Prime /\ y e. ( 1 ... ( P - 1 ) ) ) -> -. P || y )
16 eqid 
 |-  ( ( y ^ ( P - 2 ) ) mod P ) = ( ( y ^ ( P - 2 ) ) mod P )
17 16 prmdiv 
 |-  ( ( P e. Prime /\ y e. ZZ /\ -. P || y ) -> ( ( ( y ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) /\ P || ( ( y x. ( ( y ^ ( P - 2 ) ) mod P ) ) - 1 ) ) )
18 10 12 15 17 syl3anc 
 |-  ( ( P e. Prime /\ y e. ( 1 ... ( P - 1 ) ) ) -> ( ( ( y ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) /\ P || ( ( y x. ( ( y ^ ( P - 2 ) ) mod P ) ) - 1 ) ) )
19 18 simpld 
 |-  ( ( P e. Prime /\ y e. ( 1 ... ( P - 1 ) ) ) -> ( ( y ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) )
20 19 ralrimiva 
 |-  ( P e. Prime -> A. y e. ( 1 ... ( P - 1 ) ) ( ( y ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) )
21 ovex 
 |-  ( 1 ... ( P - 1 ) ) e. _V
22 21 pwid 
 |-  ( 1 ... ( P - 1 ) ) e. ~P ( 1 ... ( P - 1 ) )
23 eleq2 
 |-  ( x = ( 1 ... ( P - 1 ) ) -> ( ( P - 1 ) e. x <-> ( P - 1 ) e. ( 1 ... ( P - 1 ) ) ) )
24 eleq2 
 |-  ( x = ( 1 ... ( P - 1 ) ) -> ( ( ( y ^ ( P - 2 ) ) mod P ) e. x <-> ( ( y ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) ) )
25 24 raleqbi1dv 
 |-  ( x = ( 1 ... ( P - 1 ) ) -> ( A. y e. x ( ( y ^ ( P - 2 ) ) mod P ) e. x <-> A. y e. ( 1 ... ( P - 1 ) ) ( ( y ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) ) )
26 23 25 anbi12d 
 |-  ( x = ( 1 ... ( P - 1 ) ) -> ( ( ( P - 1 ) e. x /\ A. y e. x ( ( y ^ ( P - 2 ) ) mod P ) e. x ) <-> ( ( P - 1 ) e. ( 1 ... ( P - 1 ) ) /\ A. y e. ( 1 ... ( P - 1 ) ) ( ( y ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) ) ) )
27 26 2 elrab2 
 |-  ( ( 1 ... ( P - 1 ) ) e. A <-> ( ( 1 ... ( P - 1 ) ) e. ~P ( 1 ... ( P - 1 ) ) /\ ( ( P - 1 ) e. ( 1 ... ( P - 1 ) ) /\ A. y e. ( 1 ... ( P - 1 ) ) ( ( y ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) ) ) )
28 22 27 mpbiran 
 |-  ( ( 1 ... ( P - 1 ) ) e. A <-> ( ( P - 1 ) e. ( 1 ... ( P - 1 ) ) /\ A. y e. ( 1 ... ( P - 1 ) ) ( ( y ^ ( P - 2 ) ) mod P ) e. ( 1 ... ( P - 1 ) ) ) )
29 9 20 28 sylanbrc 
 |-  ( P e. Prime -> ( 1 ... ( P - 1 ) ) e. A )
30 fzfi 
 |-  ( 1 ... ( P - 1 ) ) e. Fin
31 eleq1 
 |-  ( s = t -> ( s e. A <-> t e. A ) )
32 reseq2 
 |-  ( s = t -> ( _I |` s ) = ( _I |` t ) )
33 32 oveq2d 
 |-  ( s = t -> ( T gsum ( _I |` s ) ) = ( T gsum ( _I |` t ) ) )
34 33 oveq1d 
 |-  ( s = t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( ( T gsum ( _I |` t ) ) mod P ) )
35 34 eqeq1d 
 |-  ( s = t -> ( ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) <-> ( ( T gsum ( _I |` t ) ) mod P ) = ( -u 1 mod P ) ) )
36 31 35 imbi12d 
 |-  ( s = t -> ( ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) <-> ( t e. A -> ( ( T gsum ( _I |` t ) ) mod P ) = ( -u 1 mod P ) ) ) )
37 36 imbi2d 
 |-  ( s = t -> ( ( P e. Prime -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) <-> ( P e. Prime -> ( t e. A -> ( ( T gsum ( _I |` t ) ) mod P ) = ( -u 1 mod P ) ) ) ) )
38 eleq1 
 |-  ( s = ( 1 ... ( P - 1 ) ) -> ( s e. A <-> ( 1 ... ( P - 1 ) ) e. A ) )
39 reseq2 
 |-  ( s = ( 1 ... ( P - 1 ) ) -> ( _I |` s ) = ( _I |` ( 1 ... ( P - 1 ) ) ) )
40 39 oveq2d 
 |-  ( s = ( 1 ... ( P - 1 ) ) -> ( T gsum ( _I |` s ) ) = ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) )
41 40 oveq1d 
 |-  ( s = ( 1 ... ( P - 1 ) ) -> ( ( T gsum ( _I |` s ) ) mod P ) = ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) mod P ) )
42 41 eqeq1d 
 |-  ( s = ( 1 ... ( P - 1 ) ) -> ( ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) <-> ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) mod P ) = ( -u 1 mod P ) ) )
43 38 42 imbi12d 
 |-  ( s = ( 1 ... ( P - 1 ) ) -> ( ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) <-> ( ( 1 ... ( P - 1 ) ) e. A -> ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) mod P ) = ( -u 1 mod P ) ) ) )
44 43 imbi2d 
 |-  ( s = ( 1 ... ( P - 1 ) ) -> ( ( P e. Prime -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) <-> ( P e. Prime -> ( ( 1 ... ( P - 1 ) ) e. A -> ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) mod P ) = ( -u 1 mod P ) ) ) ) )
45 bi2.04 
 |-  ( ( s C. t -> ( P e. Prime -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) <-> ( P e. Prime -> ( s C. t -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) )
46 pm2.27 
 |-  ( P e. Prime -> ( ( P e. Prime -> ( s C. t -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) -> ( s C. t -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) )
47 46 com34 
 |-  ( P e. Prime -> ( ( P e. Prime -> ( s C. t -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) -> ( s e. A -> ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) )
48 45 47 syl5bi 
 |-  ( P e. Prime -> ( ( s C. t -> ( P e. Prime -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) -> ( s e. A -> ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) )
49 48 alimdv 
 |-  ( P e. Prime -> ( A. s ( s C. t -> ( P e. Prime -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) -> A. s ( s e. A -> ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) )
50 df-ral 
 |-  ( A. s e. A ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) <-> A. s ( s e. A -> ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) )
51 49 50 syl6ibr 
 |-  ( P e. Prime -> ( A. s ( s C. t -> ( P e. Prime -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) -> A. s e. A ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) )
52 simp1 
 |-  ( ( P e. Prime /\ A. s e. A ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) /\ t e. A ) -> P e. Prime )
53 simp3 
 |-  ( ( P e. Prime /\ A. s e. A ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) /\ t e. A ) -> t e. A )
54 simp2 
 |-  ( ( P e. Prime /\ A. s e. A ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) /\ t e. A ) -> A. s e. A ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) )
55 1 2 52 53 54 wilthlem2 
 |-  ( ( P e. Prime /\ A. s e. A ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) /\ t e. A ) -> ( ( T gsum ( _I |` t ) ) mod P ) = ( -u 1 mod P ) )
56 55 3exp 
 |-  ( P e. Prime -> ( A. s e. A ( s C. t -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) -> ( t e. A -> ( ( T gsum ( _I |` t ) ) mod P ) = ( -u 1 mod P ) ) ) )
57 51 56 syldc 
 |-  ( A. s ( s C. t -> ( P e. Prime -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) -> ( P e. Prime -> ( t e. A -> ( ( T gsum ( _I |` t ) ) mod P ) = ( -u 1 mod P ) ) ) )
58 57 a1i 
 |-  ( t e. Fin -> ( A. s ( s C. t -> ( P e. Prime -> ( s e. A -> ( ( T gsum ( _I |` s ) ) mod P ) = ( -u 1 mod P ) ) ) ) -> ( P e. Prime -> ( t e. A -> ( ( T gsum ( _I |` t ) ) mod P ) = ( -u 1 mod P ) ) ) ) )
59 37 44 58 findcard3 
 |-  ( ( 1 ... ( P - 1 ) ) e. Fin -> ( P e. Prime -> ( ( 1 ... ( P - 1 ) ) e. A -> ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) mod P ) = ( -u 1 mod P ) ) ) )
60 30 59 ax-mp 
 |-  ( P e. Prime -> ( ( 1 ... ( P - 1 ) ) e. A -> ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) mod P ) = ( -u 1 mod P ) ) )
61 29 60 mpd 
 |-  ( P e. Prime -> ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) mod P ) = ( -u 1 mod P ) )
62 cnfld1 
 |-  1 = ( 1r ` CCfld )
63 1 62 ringidval 
 |-  1 = ( 0g ` T )
64 cncrng 
 |-  CCfld e. CRing
65 1 crngmgp 
 |-  ( CCfld e. CRing -> T e. CMnd )
66 64 65 mp1i 
 |-  ( P e. Prime -> T e. CMnd )
67 30 a1i 
 |-  ( P e. Prime -> ( 1 ... ( P - 1 ) ) e. Fin )
68 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
69 1 subrgsubm 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubMnd ` T ) )
70 68 69 mp1i 
 |-  ( P e. Prime -> ZZ e. ( SubMnd ` T ) )
71 f1oi 
 |-  ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) -1-1-onto-> ( 1 ... ( P - 1 ) )
72 f1of 
 |-  ( ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) -1-1-onto-> ( 1 ... ( P - 1 ) ) -> ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> ( 1 ... ( P - 1 ) ) )
73 71 72 ax-mp 
 |-  ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> ( 1 ... ( P - 1 ) )
74 fzssz 
 |-  ( 1 ... ( P - 1 ) ) C_ ZZ
75 fss 
 |-  ( ( ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> ( 1 ... ( P - 1 ) ) /\ ( 1 ... ( P - 1 ) ) C_ ZZ ) -> ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> ZZ )
76 73 74 75 mp2an 
 |-  ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> ZZ
77 76 a1i 
 |-  ( P e. Prime -> ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> ZZ )
78 1ex 
 |-  1 e. _V
79 78 a1i 
 |-  ( P e. Prime -> 1 e. _V )
80 77 67 79 fdmfifsupp 
 |-  ( P e. Prime -> ( _I |` ( 1 ... ( P - 1 ) ) ) finSupp 1 )
81 63 66 67 70 77 80 gsumsubmcl 
 |-  ( P e. Prime -> ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) e. ZZ )
82 1z 
 |-  1 e. ZZ
83 znegcl 
 |-  ( 1 e. ZZ -> -u 1 e. ZZ )
84 82 83 mp1i 
 |-  ( P e. Prime -> -u 1 e. ZZ )
85 moddvds 
 |-  ( ( P e. NN /\ ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) e. ZZ /\ -u 1 e. ZZ ) -> ( ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) mod P ) = ( -u 1 mod P ) <-> P || ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) - -u 1 ) ) )
86 13 81 84 85 syl3anc 
 |-  ( P e. Prime -> ( ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) mod P ) = ( -u 1 mod P ) <-> P || ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) - -u 1 ) ) )
87 61 86 mpbid 
 |-  ( P e. Prime -> P || ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) - -u 1 ) )
88 fcoi1 
 |-  ( ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> ( 1 ... ( P - 1 ) ) -> ( ( _I |` ( 1 ... ( P - 1 ) ) ) o. ( _I |` ( 1 ... ( P - 1 ) ) ) ) = ( _I |` ( 1 ... ( P - 1 ) ) ) )
89 73 88 ax-mp 
 |-  ( ( _I |` ( 1 ... ( P - 1 ) ) ) o. ( _I |` ( 1 ... ( P - 1 ) ) ) ) = ( _I |` ( 1 ... ( P - 1 ) ) )
90 89 fveq1i 
 |-  ( ( ( _I |` ( 1 ... ( P - 1 ) ) ) o. ( _I |` ( 1 ... ( P - 1 ) ) ) ) ` k ) = ( ( _I |` ( 1 ... ( P - 1 ) ) ) ` k )
91 fvres 
 |-  ( k e. ( 1 ... ( P - 1 ) ) -> ( ( _I |` ( 1 ... ( P - 1 ) ) ) ` k ) = ( _I ` k ) )
92 90 91 syl5eq 
 |-  ( k e. ( 1 ... ( P - 1 ) ) -> ( ( ( _I |` ( 1 ... ( P - 1 ) ) ) o. ( _I |` ( 1 ... ( P - 1 ) ) ) ) ` k ) = ( _I ` k ) )
93 92 adantl 
 |-  ( ( P e. Prime /\ k e. ( 1 ... ( P - 1 ) ) ) -> ( ( ( _I |` ( 1 ... ( P - 1 ) ) ) o. ( _I |` ( 1 ... ( P - 1 ) ) ) ) ` k ) = ( _I ` k ) )
94 7 93 seqfveq 
 |-  ( P e. Prime -> ( seq 1 ( x. , ( ( _I |` ( 1 ... ( P - 1 ) ) ) o. ( _I |` ( 1 ... ( P - 1 ) ) ) ) ) ` ( P - 1 ) ) = ( seq 1 ( x. , _I ) ` ( P - 1 ) ) )
95 cnfldbas 
 |-  CC = ( Base ` CCfld )
96 1 95 mgpbas 
 |-  CC = ( Base ` T )
97 cnfldmul 
 |-  x. = ( .r ` CCfld )
98 1 97 mgpplusg 
 |-  x. = ( +g ` T )
99 eqid 
 |-  ( Cntz ` T ) = ( Cntz ` T )
100 cnring 
 |-  CCfld e. Ring
101 1 ringmgp 
 |-  ( CCfld e. Ring -> T e. Mnd )
102 100 101 mp1i 
 |-  ( P e. Prime -> T e. Mnd )
103 zsscn 
 |-  ZZ C_ CC
104 fss 
 |-  ( ( ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> ZZ /\ ZZ C_ CC ) -> ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> CC )
105 76 103 104 mp2an 
 |-  ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> CC
106 105 a1i 
 |-  ( P e. Prime -> ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) --> CC )
107 96 99 66 106 cntzcmnf 
 |-  ( P e. Prime -> ran ( _I |` ( 1 ... ( P - 1 ) ) ) C_ ( ( Cntz ` T ) ` ran ( _I |` ( 1 ... ( P - 1 ) ) ) ) )
108 f1of1 
 |-  ( ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) -1-1-onto-> ( 1 ... ( P - 1 ) ) -> ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) -1-1-> ( 1 ... ( P - 1 ) ) )
109 71 108 mp1i 
 |-  ( P e. Prime -> ( _I |` ( 1 ... ( P - 1 ) ) ) : ( 1 ... ( P - 1 ) ) -1-1-> ( 1 ... ( P - 1 ) ) )
110 suppssdm 
 |-  ( ( _I |` ( 1 ... ( P - 1 ) ) ) supp 1 ) C_ dom ( _I |` ( 1 ... ( P - 1 ) ) )
111 dmresi 
 |-  dom ( _I |` ( 1 ... ( P - 1 ) ) ) = ( 1 ... ( P - 1 ) )
112 110 111 sseqtri 
 |-  ( ( _I |` ( 1 ... ( P - 1 ) ) ) supp 1 ) C_ ( 1 ... ( P - 1 ) )
113 rnresi 
 |-  ran ( _I |` ( 1 ... ( P - 1 ) ) ) = ( 1 ... ( P - 1 ) )
114 112 113 sseqtrri 
 |-  ( ( _I |` ( 1 ... ( P - 1 ) ) ) supp 1 ) C_ ran ( _I |` ( 1 ... ( P - 1 ) ) )
115 114 a1i 
 |-  ( P e. Prime -> ( ( _I |` ( 1 ... ( P - 1 ) ) ) supp 1 ) C_ ran ( _I |` ( 1 ... ( P - 1 ) ) ) )
116 eqid 
 |-  ( ( ( _I |` ( 1 ... ( P - 1 ) ) ) o. ( _I |` ( 1 ... ( P - 1 ) ) ) ) supp 1 ) = ( ( ( _I |` ( 1 ... ( P - 1 ) ) ) o. ( _I |` ( 1 ... ( P - 1 ) ) ) ) supp 1 )
117 96 63 98 99 102 67 106 107 5 109 115 116 gsumval3 
 |-  ( P e. Prime -> ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) = ( seq 1 ( x. , ( ( _I |` ( 1 ... ( P - 1 ) ) ) o. ( _I |` ( 1 ... ( P - 1 ) ) ) ) ) ` ( P - 1 ) ) )
118 facnn 
 |-  ( ( P - 1 ) e. NN -> ( ! ` ( P - 1 ) ) = ( seq 1 ( x. , _I ) ` ( P - 1 ) ) )
119 5 118 syl 
 |-  ( P e. Prime -> ( ! ` ( P - 1 ) ) = ( seq 1 ( x. , _I ) ` ( P - 1 ) ) )
120 94 117 119 3eqtr4d 
 |-  ( P e. Prime -> ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) = ( ! ` ( P - 1 ) ) )
121 120 oveq1d 
 |-  ( P e. Prime -> ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) - -u 1 ) = ( ( ! ` ( P - 1 ) ) - -u 1 ) )
122 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
123 13 122 syl 
 |-  ( P e. Prime -> ( P - 1 ) e. NN0 )
124 123 faccld 
 |-  ( P e. Prime -> ( ! ` ( P - 1 ) ) e. NN )
125 124 nncnd 
 |-  ( P e. Prime -> ( ! ` ( P - 1 ) ) e. CC )
126 ax-1cn 
 |-  1 e. CC
127 subneg 
 |-  ( ( ( ! ` ( P - 1 ) ) e. CC /\ 1 e. CC ) -> ( ( ! ` ( P - 1 ) ) - -u 1 ) = ( ( ! ` ( P - 1 ) ) + 1 ) )
128 125 126 127 sylancl 
 |-  ( P e. Prime -> ( ( ! ` ( P - 1 ) ) - -u 1 ) = ( ( ! ` ( P - 1 ) ) + 1 ) )
129 121 128 eqtrd 
 |-  ( P e. Prime -> ( ( T gsum ( _I |` ( 1 ... ( P - 1 ) ) ) ) - -u 1 ) = ( ( ! ` ( P - 1 ) ) + 1 ) )
130 87 129 breqtrd 
 |-  ( P e. Prime -> P || ( ( ! ` ( P - 1 ) ) + 1 ) )