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}_{ℂ_{fld}}$
	wilthlem.a	$⊢ A = \{x \in 𝒫 (1 \dots P - 1) \| (P - 1 \in x \land \forall y \in x y^{P - 2} \mod P \in x)\}$
Assertion	wilthlem3	$⊢ P \in ℙ \to P ∥ ((P - 1)! + 1)$

Proof

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

Metamath Proof Explorer

Theorem wilthlem3

Proof