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 𝑇 = ( mulGrp ‘ ℂfld )
wilthlem.a 𝐴 = { 𝑥 ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ∣ ( ( 𝑃 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ) }
Assertion wilthlem3 ( 𝑃 ∈ ℙ → 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 wilthlem.t 𝑇 = ( mulGrp ‘ ℂfld )
2 wilthlem.a 𝐴 = { 𝑥 ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ∣ ( ( 𝑃 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ) }
3 prmuz2 ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ ‘ 2 ) )
4 uz2m1nn ( 𝑃 ∈ ( ℤ ‘ 2 ) → ( 𝑃 − 1 ) ∈ ℕ )
5 3 4 syl ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) ∈ ℕ )
6 nnuz ℕ = ( ℤ ‘ 1 )
7 5 6 eleqtrdi ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) ∈ ( ℤ ‘ 1 ) )
8 eluzfz2 ( ( 𝑃 − 1 ) ∈ ( ℤ ‘ 1 ) → ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
9 7 8 syl ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
10 simpl ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℙ )
11 elfzelz ( 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑦 ∈ ℤ )
12 11 adantl ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑦 ∈ ℤ )
13 prmnn ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
14 fzm1ndvds ( ( 𝑃 ∈ ℕ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃𝑦 )
15 13 14 sylan ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃𝑦 )
16 eqid ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 )
17 16 prmdiv ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ ¬ 𝑃𝑦 ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝑦 · ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) − 1 ) ) )
18 10 12 15 17 syl3anc ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝑦 · ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) − 1 ) ) )
19 18 simpld ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
20 19 ralrimiva ( 𝑃 ∈ ℙ → ∀ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) )
21 ovex ( 1 ... ( 𝑃 − 1 ) ) ∈ V
22 21 pwid ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) )
23 eleq2 ( 𝑥 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( 𝑃 − 1 ) ∈ 𝑥 ↔ ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) )
24 eleq2 ( 𝑥 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ↔ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) )
25 24 raleqbi1dv ( 𝑥 = ( 1 ... ( 𝑃 − 1 ) ) → ( ∀ 𝑦𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) )
26 23 25 anbi12d ( 𝑥 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( ( 𝑃 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ) ↔ ( ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) ) )
27 26 2 elrab2 ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 ↔ ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) ) )
28 22 27 mpbiran ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 ↔ ( ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) )
29 9 20 28 sylanbrc ( 𝑃 ∈ ℙ → ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 )
30 fzfi ( 1 ... ( 𝑃 − 1 ) ) ∈ Fin
31 eleq1 ( 𝑠 = 𝑡 → ( 𝑠𝐴𝑡𝐴 ) )
32 reseq2 ( 𝑠 = 𝑡 → ( I ↾ 𝑠 ) = ( I ↾ 𝑡 ) )
33 32 oveq2d ( 𝑠 = 𝑡 → ( 𝑇 Σg ( I ↾ 𝑠 ) ) = ( 𝑇 Σg ( I ↾ 𝑡 ) ) )
34 33 oveq1d ( 𝑠 = 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) )
35 34 eqeq1d ( 𝑠 = 𝑡 → ( ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
36 31 35 imbi12d ( 𝑠 = 𝑡 → ( ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ↔ ( 𝑡𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) )
37 36 imbi2d ( 𝑠 = 𝑡 → ( ( 𝑃 ∈ ℙ → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ↔ ( 𝑃 ∈ ℙ → ( 𝑡𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) )
38 eleq1 ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( 𝑠𝐴 ↔ ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 ) )
39 reseq2 ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( I ↾ 𝑠 ) = ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) )
40 39 oveq2d ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( 𝑇 Σg ( I ↾ 𝑠 ) ) = ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) )
41 40 oveq1d ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) )
42 41 eqeq1d ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
43 38 42 imbi12d ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ↔ ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) )
44 43 imbi2d ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( 𝑃 ∈ ℙ → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ↔ ( 𝑃 ∈ ℙ → ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) )
45 bi2.04 ( ( 𝑠𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) ↔ ( 𝑃 ∈ ℙ → ( 𝑠𝑡 → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) )
46 pm2.27 ( 𝑃 ∈ ℙ → ( ( 𝑃 ∈ ℙ → ( 𝑠𝑡 → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ( 𝑠𝑡 → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) )
47 46 com34 ( 𝑃 ∈ ℙ → ( ( 𝑃 ∈ ℙ → ( 𝑠𝑡 → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ( 𝑠𝐴 → ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) )
48 45 47 syl5bi ( 𝑃 ∈ ℙ → ( ( 𝑠𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ( 𝑠𝐴 → ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) )
49 48 alimdv ( 𝑃 ∈ ℙ → ( ∀ 𝑠 ( 𝑠𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ∀ 𝑠 ( 𝑠𝐴 → ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) )
50 df-ral ( ∀ 𝑠𝐴 ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ↔ ∀ 𝑠 ( 𝑠𝐴 → ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) )
51 49 50 syl6ibr ( 𝑃 ∈ ℙ → ( ∀ 𝑠 ( 𝑠𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ∀ 𝑠𝐴 ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) )
52 simp1 ( ( 𝑃 ∈ ℙ ∧ ∀ 𝑠𝐴 ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ∧ 𝑡𝐴 ) → 𝑃 ∈ ℙ )
53 simp3 ( ( 𝑃 ∈ ℙ ∧ ∀ 𝑠𝐴 ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ∧ 𝑡𝐴 ) → 𝑡𝐴 )
54 simp2 ( ( 𝑃 ∈ ℙ ∧ ∀ 𝑠𝐴 ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ∧ 𝑡𝐴 ) → ∀ 𝑠𝐴 ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
55 1 2 52 53 54 wilthlem2 ( ( 𝑃 ∈ ℙ ∧ ∀ 𝑠𝐴 ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ∧ 𝑡𝐴 ) → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
56 55 3exp ( 𝑃 ∈ ℙ → ( ∀ 𝑠𝐴 ( 𝑠𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( 𝑡𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) )
57 51 56 syldc ( ∀ 𝑠 ( 𝑠𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ( 𝑃 ∈ ℙ → ( 𝑡𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) )
58 57 a1i ( 𝑡 ∈ Fin → ( ∀ 𝑠 ( 𝑠𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ( 𝑃 ∈ ℙ → ( 𝑡𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) )
59 37 44 58 findcard3 ( ( 1 ... ( 𝑃 − 1 ) ) ∈ Fin → ( 𝑃 ∈ ℙ → ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) )
60 30 59 ax-mp ( 𝑃 ∈ ℙ → ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) )
61 29 60 mpd ( 𝑃 ∈ ℙ → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) )
62 cnfld1 1 = ( 1r ‘ ℂfld )
63 1 62 ringidval 1 = ( 0g𝑇 )
64 cncrng fld ∈ CRing
65 1 crngmgp ( ℂfld ∈ CRing → 𝑇 ∈ CMnd )
66 64 65 mp1i ( 𝑃 ∈ ℙ → 𝑇 ∈ CMnd )
67 30 a1i ( 𝑃 ∈ ℙ → ( 1 ... ( 𝑃 − 1 ) ) ∈ Fin )
68 zsubrg ℤ ∈ ( SubRing ‘ ℂfld )
69 1 subrgsubm ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubMnd ‘ 𝑇 ) )
70 68 69 mp1i ( 𝑃 ∈ ℙ → ℤ ∈ ( SubMnd ‘ 𝑇 ) )
71 f1oi ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) –1-1-onto→ ( 1 ... ( 𝑃 − 1 ) )
72 f1of ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) –1-1-onto→ ( 1 ... ( 𝑃 − 1 ) ) → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ( 1 ... ( 𝑃 − 1 ) ) )
73 71 72 ax-mp ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ( 1 ... ( 𝑃 − 1 ) )
74 fzssz ( 1 ... ( 𝑃 − 1 ) ) ⊆ ℤ
75 fss ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ( 1 ... ( 𝑃 − 1 ) ) ∧ ( 1 ... ( 𝑃 − 1 ) ) ⊆ ℤ ) → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℤ )
76 73 74 75 mp2an ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℤ
77 76 a1i ( 𝑃 ∈ ℙ → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℤ )
78 1ex 1 ∈ V
79 78 a1i ( 𝑃 ∈ ℙ → 1 ∈ V )
80 77 67 79 fdmfifsupp ( 𝑃 ∈ ℙ → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) finSupp 1 )
81 63 66 67 70 77 80 gsumsubmcl ( 𝑃 ∈ ℙ → ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ∈ ℤ )
82 1z 1 ∈ ℤ
83 znegcl ( 1 ∈ ℤ → - 1 ∈ ℤ )
84 82 83 mp1i ( 𝑃 ∈ ℙ → - 1 ∈ ℤ )
85 moddvds ( ( 𝑃 ∈ ℕ ∧ ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ∈ ℤ ∧ - 1 ∈ ℤ ) → ( ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) − - 1 ) ) )
86 13 81 84 85 syl3anc ( 𝑃 ∈ ℙ → ( ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) − - 1 ) ) )
87 61 86 mpbid ( 𝑃 ∈ ℙ → 𝑃 ∥ ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) − - 1 ) )
88 fcoi1 ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ( 1 ... ( 𝑃 − 1 ) ) → ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) = ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) )
89 73 88 ax-mp ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) = ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) )
90 89 fveq1i ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ‘ 𝑘 ) = ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ‘ 𝑘 )
91 fvres ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) → ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ‘ 𝑘 ) = ( I ‘ 𝑘 ) )
92 90 91 syl5eq ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) → ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ‘ 𝑘 ) = ( I ‘ 𝑘 ) )
93 92 adantl ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ‘ 𝑘 ) = ( I ‘ 𝑘 ) )
94 7 93 seqfveq ( 𝑃 ∈ ℙ → ( seq 1 ( · , ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ) ‘ ( 𝑃 − 1 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑃 − 1 ) ) )
95 cnfldbas ℂ = ( Base ‘ ℂfld )
96 1 95 mgpbas ℂ = ( Base ‘ 𝑇 )
97 cnfldmul · = ( .r ‘ ℂfld )
98 1 97 mgpplusg · = ( +g𝑇 )
99 eqid ( Cntz ‘ 𝑇 ) = ( Cntz ‘ 𝑇 )
100 cnring fld ∈ Ring
101 1 ringmgp ( ℂfld ∈ Ring → 𝑇 ∈ Mnd )
102 100 101 mp1i ( 𝑃 ∈ ℙ → 𝑇 ∈ Mnd )
103 zsscn ℤ ⊆ ℂ
104 fss ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℤ ∧ ℤ ⊆ ℂ ) → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℂ )
105 76 103 104 mp2an ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℂ
106 105 a1i ( 𝑃 ∈ ℙ → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℂ )
107 96 99 66 106 cntzcmnf ( 𝑃 ∈ ℙ → ran ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ⊆ ( ( Cntz ‘ 𝑇 ) ‘ ran ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) )
108 f1of1 ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) –1-1-onto→ ( 1 ... ( 𝑃 − 1 ) ) → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) –1-1→ ( 1 ... ( 𝑃 − 1 ) ) )
109 71 108 mp1i ( 𝑃 ∈ ℙ → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) –1-1→ ( 1 ... ( 𝑃 − 1 ) ) )
110 suppssdm ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) supp 1 ) ⊆ dom ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) )
111 dmresi dom ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) = ( 1 ... ( 𝑃 − 1 ) )
112 110 111 sseqtri ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) supp 1 ) ⊆ ( 1 ... ( 𝑃 − 1 ) )
113 rnresi ran ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) = ( 1 ... ( 𝑃 − 1 ) )
114 112 113 sseqtrri ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) supp 1 ) ⊆ ran ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) )
115 114 a1i ( 𝑃 ∈ ℙ → ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) supp 1 ) ⊆ ran ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) )
116 eqid ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) supp 1 ) = ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) supp 1 )
117 96 63 98 99 102 67 106 107 5 109 115 116 gsumval3 ( 𝑃 ∈ ℙ → ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) = ( seq 1 ( · , ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ) ‘ ( 𝑃 − 1 ) ) )
118 facnn ( ( 𝑃 − 1 ) ∈ ℕ → ( ! ‘ ( 𝑃 − 1 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑃 − 1 ) ) )
119 5 118 syl ( 𝑃 ∈ ℙ → ( ! ‘ ( 𝑃 − 1 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑃 − 1 ) ) )
120 94 117 119 3eqtr4d ( 𝑃 ∈ ℙ → ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
121 120 oveq1d ( 𝑃 ∈ ℙ → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) − - 1 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) )
122 nnm1nn0 ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
123 13 122 syl ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) ∈ ℕ0 )
124 123 faccld ( 𝑃 ∈ ℙ → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ )
125 124 nncnd ( 𝑃 ∈ ℙ → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ )
126 ax-1cn 1 ∈ ℂ
127 subneg ( ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) )
128 125 126 127 sylancl ( 𝑃 ∈ ℙ → ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) )
129 121 128 eqtrd ( 𝑃 ∈ ℙ → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) − - 1 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) )
130 87 129 breqtrd ( 𝑃 ∈ ℙ → 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) )