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 ) )