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 biimtrid ⊢ ( 𝑃 ∈ ℙ → ( ( 𝑠 ⊊ 𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σ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 imbitrrdi ⊢ ( 𝑃 ∈ ℙ → ( ∀ 𝑠 ( 𝑠 ⊊ 𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σ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 eqtrid ⊢ ( 𝑘 ∈ ( 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 ) )