wilthlem2

Description: Lemma for wilth : induction step. The "hand proof" version of this theorem works by writing out the list of all numbers from 1 to P - 1 in pairs such that a number is paired with its inverse. Every number has a unique inverse different from itself except 1 and P - 1 , and so each pair multiplies to 1 , and 1 and P - 1 == -u 1 multiply to -u 1 , so the full product is equal to -u 1 . Here we make this precise by doing the product pair by pair.

The induction hypothesis says that every subset S of 1 ... ( P - 1 ) that is closed under inverse (i.e. all pairs are matched up) and contains P - 1 multiplies to -u 1 mod P . Given such a set, we take out one element z =/= P - 1 . If there are no such elements, then S = { P - 1 } which forms the base case. Otherwise, S \ { z , z ^ -u 1 } is also closed under inverse and contains P - 1 , so the induction hypothesis says that this equals -u 1 ; and the remaining two elements are either equal to each other, in which case wilthlem1 gives that z = 1 or P - 1 , and we've already excluded the second case, so the product gives 1 ; or z =/= z ^ -u 1 and their product is 1 . In either case the accumulated product is unaffected. (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)\}$
	wilthlem2.p	$⊢ φ \to P \in ℙ$
	wilthlem2.s	$⊢ φ \to S \in A$
	wilthlem2.r	$⊢ φ \to \forall s \in A (s \subset S \to (\sum_{T}, ({I ↾}_{s})) \mod P = -1 \mod P)$
Assertion	wilthlem2	$⊢ φ \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P$

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		wilthlem2.p	$⊢ φ \to P \in ℙ$
4		wilthlem2.s	$⊢ φ \to S \in A$
5		wilthlem2.r	$⊢ φ \to \forall s \in A (s \subset S \to (\sum_{T}, ({I ↾}_{s})) \mod P = -1 \mod P)$
6		simpr	$⊢ (φ \land S \subseteq \{P - 1\}) \to S \subseteq \{P - 1\}$
7		eleq2	$⊢ x = S \to (P - 1 \in x \leftrightarrow P - 1 \in S)$
8		eleq2	$⊢ x = S \to (y^{P - 2} \mod P \in x \leftrightarrow y^{P - 2} \mod P \in S)$
9	8	raleqbi1dv	$⊢ x = S \to (\forall y \in x y^{P - 2} \mod P \in x \leftrightarrow \forall y \in S y^{P - 2} \mod P \in S)$
10	7 9	anbi12d	$⊢ x = S \to ((P - 1 \in x \land \forall y \in x y^{P - 2} \mod P \in x) \leftrightarrow (P - 1 \in S \land \forall y \in S y^{P - 2} \mod P \in S))$
11	10 2	elrab2	$⊢ S \in A \leftrightarrow (S \in 𝒫 (1 \dots P - 1) \land (P - 1 \in S \land \forall y \in S y^{P - 2} \mod P \in S))$
12	4 11	sylib	$⊢ φ \to (S \in 𝒫 (1 \dots P - 1) \land (P - 1 \in S \land \forall y \in S y^{P - 2} \mod P \in S))$
13	12	simprd	$⊢ φ \to (P - 1 \in S \land \forall y \in S y^{P - 2} \mod P \in S)$
14	13	simpld	$⊢ φ \to P - 1 \in S$
15	14	snssd	$⊢ φ \to \{P - 1\} \subseteq S$
16	15	adantr	$⊢ (φ \land S \subseteq \{P - 1\}) \to \{P - 1\} \subseteq S$
17	6 16	eqssd	$⊢ (φ \land S \subseteq \{P - 1\}) \to S = \{P - 1\}$
18	17	reseq2d	$⊢ (φ \land S \subseteq \{P - 1\}) \to {I ↾}_{S} = {I ↾}_{\{P - 1\}}$
19		mptresid	$⊢ {I ↾}_{\{P - 1\}} = (z \in \{P - 1\} ⟼ z)$
20	18 19	eqtrdi	$⊢ (φ \land S \subseteq \{P - 1\}) \to {I ↾}_{S} = (z \in \{P - 1\} ⟼ z)$
21	20	oveq2d	$⊢ (φ \land S \subseteq \{P - 1\}) \to \sum_{T} ({I ↾}_{S}) = \underset{z \in \{P - 1\}}{\sum_{T}} z$
22	21	oveq1d	$⊢ (φ \land S \subseteq \{P - 1\}) \to (\sum_{T}, ({I ↾}_{S})) \mod P = (\underset{z \in \{P - 1\}}{\sum_{T}}, z) \mod P$
23		prmnn	$⊢ P \in ℙ \to P \in ℕ$
24	3 23	syl	$⊢ φ \to P \in ℕ$
25	24	nncnd	$⊢ φ \to P \in ℂ$
26		ax-1cn	$⊢ 1 \in ℂ$
27		negsub	$⊢ (P \in ℂ \land 1 \in ℂ) \to P + -1 = P - 1$
28	25 26 27	sylancl	$⊢ φ \to P + -1 = P - 1$
29		neg1cn	$⊢ - 1 \in ℂ$
30		addcom	$⊢ (P \in ℂ \land - 1 \in ℂ) \to P + -1 = - 1 + P$
31	25 29 30	sylancl	$⊢ φ \to P + -1 = - 1 + P$
32	28 31	eqtr3d	$⊢ φ \to P - 1 = - 1 + P$
33		cnring	$⊢ ℂ_{fld} \in Ring$
34	1	ringmgp	$⊢ ℂ_{fld} \in Ring \to T \in Mnd$
35	33 34	mp1i	$⊢ φ \to T \in Mnd$
36		nnm1nn0	$⊢ P \in ℕ \to P - 1 \in ℕ_{0}$
37	24 36	syl	$⊢ φ \to P - 1 \in ℕ_{0}$
38	37	nn0cnd	$⊢ φ \to P - 1 \in ℂ$
39		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
40	1 39	mgpbas	$⊢ ℂ = {Base}_{T}$
41		id	$⊢ z = P - 1 \to z = P - 1$
42	40 41	gsumsn	$⊢ (T \in Mnd \land P - 1 \in ℂ \land P - 1 \in ℂ) \to \underset{z \in \{P - 1\}}{\sum_{T}} z = P - 1$
43	35 38 38 42	syl3anc	$⊢ φ \to \underset{z \in \{P - 1\}}{\sum_{T}} z = P - 1$
44	25	mulid2d	$⊢ φ \to 1 P = P$
45	44	oveq2d	$⊢ φ \to - 1 + 1 P = - 1 + P$
46	32 43 45	3eqtr4d	$⊢ φ \to \underset{z \in \{P - 1\}}{\sum_{T}} z = - 1 + 1 P$
47	46	oveq1d	$⊢ φ \to (\underset{z \in \{P - 1\}}{\sum_{T}}, z) \mod P = (- 1 + 1 P) \mod P$
48		neg1rr	$⊢ - 1 \in ℝ$
49	48	a1i	$⊢ φ \to - 1 \in ℝ$
50	24	nnrpd	$⊢ φ \to P \in ℝ^{+}$
51		1zzd	$⊢ φ \to 1 \in ℤ$
52		modcyc	$⊢ (- 1 \in ℝ \land P \in ℝ^{+} \land 1 \in ℤ) \to (- 1 + 1 P) \mod P = -1 \mod P$
53	49 50 51 52	syl3anc	$⊢ φ \to (- 1 + 1 P) \mod P = -1 \mod P$
54	47 53	eqtrd	$⊢ φ \to (\underset{z \in \{P - 1\}}{\sum_{T}}, z) \mod P = -1 \mod P$
55	54	adantr	$⊢ (φ \land S \subseteq \{P - 1\}) \to (\underset{z \in \{P - 1\}}{\sum_{T}}, z) \mod P = -1 \mod P$
56	22 55	eqtrd	$⊢ (φ \land S \subseteq \{P - 1\}) \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P$
57	56	ex	$⊢ φ \to (S \subseteq \{P - 1\} \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P)$
58		nss	$⊢ \neg S \subseteq \{P - 1\} \leftrightarrow \exists z (z \in S \land \neg z \in \{P - 1\})$
59		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
60	1 59	ringidval	$⊢ 1 = 0_{T}$
61		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
62	1 61	mgpplusg	$⊢ \times = +_{T}$
63		cncrng	$⊢ ℂ_{fld} \in CRing$
64	1	crngmgp	$⊢ ℂ_{fld} \in CRing \to T \in CMnd$
65	63 64	ax-mp	$⊢ T \in CMnd$
66	65	a1i	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to T \in CMnd$
67	4	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S \in A$
68		f1oi	$⊢ ({I ↾}_{S}) : S \underset{1-1 onto}{⟶} S$
69		f1of	$⊢ ({I ↾}_{S}) : S \underset{1-1 onto}{⟶} S \to ({I ↾}_{S}) : S ⟶ S$
70	68 69	ax-mp	$⊢ ({I ↾}_{S}) : S ⟶ S$
71	12	simpld	$⊢ φ \to S \in 𝒫 (1 \dots P - 1)$
72	71	elpwid	$⊢ φ \to S \subseteq (1 \dots P - 1)$
73		fzssz	$⊢ (1 \dots P - 1) \subseteq ℤ$
74	72 73	sstrdi	$⊢ φ \to S \subseteq ℤ$
75		zsscn	$⊢ ℤ \subseteq ℂ$
76	74 75	sstrdi	$⊢ φ \to S \subseteq ℂ$
77		fss	$⊢ (({I ↾}_{S}) : S ⟶ S \land S \subseteq ℂ) \to ({I ↾}_{S}) : S ⟶ ℂ$
78	70 76 77	sylancr	$⊢ φ \to ({I ↾}_{S}) : S ⟶ ℂ$
79	78	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to ({I ↾}_{S}) : S ⟶ ℂ$
80		fzfi	$⊢ (1 \dots P - 1) \in Fin$
81		ssfi	$⊢ ((1 \dots P - 1) \in Fin \land S \subseteq (1 \dots P - 1)) \to S \in Fin$
82	80 72 81	sylancr	$⊢ φ \to S \in Fin$
83		1ex	$⊢ 1 \in V$
84	83	a1i	$⊢ φ \to 1 \in V$
85	78 82 84	fdmfifsupp	$⊢ φ \to {finSupp}_{1} (({I ↾}_{S}))$
86	85	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to {finSupp}_{1} (({I ↾}_{S}))$
87		disjdif	$⊢ \{z, z^{P - 2} \mod P\} \cap (S ∖ \{z, z^{P - 2} \mod P\}) = \emptyset$
88	87	a1i	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \{z, z^{P - 2} \mod P\} \cap (S ∖ \{z, z^{P - 2} \mod P\}) = \emptyset$
89		undif2	$⊢ \{z, z^{P - 2} \mod P\} \cup (S ∖ \{z, z^{P - 2} \mod P\}) = \{z, z^{P - 2} \mod P\} \cup S$
90		simprl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z \in S$
91		oveq1	$⊢ y = z \to y^{P - 2} = z^{P - 2}$
92	91	oveq1d	$⊢ y = z \to y^{P - 2} \mod P = z^{P - 2} \mod P$
93	92	eleq1d	$⊢ y = z \to (y^{P - 2} \mod P \in S \leftrightarrow z^{P - 2} \mod P \in S)$
94	13	simprd	$⊢ φ \to \forall y \in S y^{P - 2} \mod P \in S$
95	94	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \forall y \in S y^{P - 2} \mod P \in S$
96	93 95 90	rspcdva	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z^{P - 2} \mod P \in S$
97	90 96	prssd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \{z, z^{P - 2} \mod P\} \subseteq S$
98		ssequn1	$⊢ \{z, z^{P - 2} \mod P\} \subseteq S \leftrightarrow \{z, z^{P - 2} \mod P\} \cup S = S$
99	97 98	sylib	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \{z, z^{P - 2} \mod P\} \cup S = S$
100	89 99	eqtr2id	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S = \{z, z^{P - 2} \mod P\} \cup (S ∖ \{z, z^{P - 2} \mod P\})$
101	40 60 62 66 67 79 86 88 100	gsumsplit	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \sum_{T} ({I ↾}_{S}) = (\sum_{T}, ({({I ↾}_{S}) ↾}_{\{z, z^{P - 2} \mod P\}})) (\sum_{T}, ({({I ↾}_{S}) ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}))$
102	97	resabs1d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to {({I ↾}_{S}) ↾}_{\{z, z^{P - 2} \mod P\}} = {I ↾}_{\{z, z^{P - 2} \mod P\}}$
103	102	oveq2d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \sum_{T} ({({I ↾}_{S}) ↾}_{\{z, z^{P - 2} \mod P\}}) = \sum_{T} ({I ↾}_{\{z, z^{P - 2} \mod P\}})$
104		difss	$⊢ S ∖ \{z, z^{P - 2} \mod P\} \subseteq S$
105		resabs1	$⊢ S ∖ \{z, z^{P - 2} \mod P\} \subseteq S \to {({I ↾}_{S}) ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})} = {I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}$
106	104 105	ax-mp	$⊢ {({I ↾}_{S}) ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})} = {I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}$
107	106	oveq2i	$⊢ \sum_{T} ({({I ↾}_{S}) ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) = \sum_{T} ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})$
108	107	a1i	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \sum_{T} ({({I ↾}_{S}) ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) = \sum_{T} ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})$
109	103 108	oveq12d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (\sum_{T}, ({({I ↾}_{S}) ↾}_{\{z, z^{P - 2} \mod P\}})) (\sum_{T}, ({({I ↾}_{S}) ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) = (\sum_{T}, ({I ↾}_{\{z, z^{P - 2} \mod P\}})) (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}))$
110	101 109	eqtrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \sum_{T} ({I ↾}_{S}) = (\sum_{T}, ({I ↾}_{\{z, z^{P - 2} \mod P\}})) (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}))$
111	110	oveq1d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (\sum_{T}, ({I ↾}_{S})) \mod P = (\sum_{T}, ({I ↾}_{\{z, z^{P - 2} \mod P\}})) (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P$
112		prfi	$⊢ \{z, z^{P - 2} \mod P\} \in Fin$
113	112	a1i	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \{z, z^{P - 2} \mod P\} \in Fin$
114		zsubrg	$⊢ ℤ \in SubRing (ℂ_{fld})$
115	1	subrgsubm	$⊢ ℤ \in SubRing (ℂ_{fld}) \to ℤ \in SubMnd (T)$
116	114 115	mp1i	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to ℤ \in SubMnd (T)$
117		f1oi	$⊢ ({I ↾}_{\{z, z^{P - 2} \mod P\}}) : \{z, z^{P - 2} \mod P\} \underset{1-1 onto}{⟶} \{z, z^{P - 2} \mod P\}$
118		f1of	$⊢ ({I ↾}_{\{z, z^{P - 2} \mod P\}}) : \{z, z^{P - 2} \mod P\} \underset{1-1 onto}{⟶} \{z, z^{P - 2} \mod P\} \to ({I ↾}_{\{z, z^{P - 2} \mod P\}}) : \{z, z^{P - 2} \mod P\} ⟶ \{z, z^{P - 2} \mod P\}$
119	117 118	ax-mp	$⊢ ({I ↾}_{\{z, z^{P - 2} \mod P\}}) : \{z, z^{P - 2} \mod P\} ⟶ \{z, z^{P - 2} \mod P\}$
120	74	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S \subseteq ℤ$
121	97 120	sstrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \{z, z^{P - 2} \mod P\} \subseteq ℤ$
122		fss	$⊢ (({I ↾}_{\{z, z^{P - 2} \mod P\}}) : \{z, z^{P - 2} \mod P\} ⟶ \{z, z^{P - 2} \mod P\} \land \{z, z^{P - 2} \mod P\} \subseteq ℤ) \to ({I ↾}_{\{z, z^{P - 2} \mod P\}}) : \{z, z^{P - 2} \mod P\} ⟶ ℤ$
123	119 121 122	sylancr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to ({I ↾}_{\{z, z^{P - 2} \mod P\}}) : \{z, z^{P - 2} \mod P\} ⟶ ℤ$
124	83	a1i	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 \in V$
125	123 113 124	fdmfifsupp	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to {finSupp}_{1} (({I ↾}_{\{z, z^{P - 2} \mod P\}}))$
126	60 66 113 116 123 125	gsumsubmcl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \sum_{T} ({I ↾}_{\{z, z^{P - 2} \mod P\}}) \in ℤ$
127	126	zred	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \sum_{T} ({I ↾}_{\{z, z^{P - 2} \mod P\}}) \in ℝ$
128		1red	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 \in ℝ$
129	72	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S \subseteq (1 \dots P - 1)$
130	129	ssdifssd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S ∖ \{z, z^{P - 2} \mod P\} \subseteq (1 \dots P - 1)$
131		ssfi	$⊢ ((1 \dots P - 1) \in Fin \land S ∖ \{z, z^{P - 2} \mod P\} \subseteq (1 \dots P - 1)) \to S ∖ \{z, z^{P - 2} \mod P\} \in Fin$
132	80 130 131	sylancr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S ∖ \{z, z^{P - 2} \mod P\} \in Fin$
133		f1oi	$⊢ ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) : S ∖ \{z, z^{P - 2} \mod P\} \underset{1-1 onto}{⟶} S ∖ \{z, z^{P - 2} \mod P\}$
134		f1of	$⊢ ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) : S ∖ \{z, z^{P - 2} \mod P\} \underset{1-1 onto}{⟶} S ∖ \{z, z^{P - 2} \mod P\} \to ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) : S ∖ \{z, z^{P - 2} \mod P\} ⟶ S ∖ \{z, z^{P - 2} \mod P\}$
135	133 134	ax-mp	$⊢ ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) : S ∖ \{z, z^{P - 2} \mod P\} ⟶ S ∖ \{z, z^{P - 2} \mod P\}$
136	120	ssdifssd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S ∖ \{z, z^{P - 2} \mod P\} \subseteq ℤ$
137		fss	$⊢ (({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) : S ∖ \{z, z^{P - 2} \mod P\} ⟶ S ∖ \{z, z^{P - 2} \mod P\} \land S ∖ \{z, z^{P - 2} \mod P\} \subseteq ℤ) \to ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) : S ∖ \{z, z^{P - 2} \mod P\} ⟶ ℤ$
138	135 136 137	sylancr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) : S ∖ \{z, z^{P - 2} \mod P\} ⟶ ℤ$
139	138 132 124	fdmfifsupp	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to {finSupp}_{1} (({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}))$
140	60 66 132 116 138 139	gsumsubmcl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \sum_{T} ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) \in ℤ$
141	50	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P \in ℝ^{+}$
142	35	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to T \in Mnd$
143	76	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S \subseteq ℂ$
144	143 90	sseldd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z \in ℂ$
145		id	$⊢ w = z \to w = z$
146	40 145	gsumsn	$⊢ (T \in Mnd \land z \in ℂ \land z \in ℂ) \to \underset{w \in \{z\}}{\sum_{T}} w = z$
147	142 144 144 146	syl3anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \underset{w \in \{z\}}{\sum_{T}} w = z$
148	147	adantr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to \underset{w \in \{z\}}{\sum_{T}} w = z$
149		mptresid	$⊢ {I ↾}_{\{z\}} = (w \in \{z\} ⟼ w)$
150		dfsn2	$⊢ \{z\} = \{z, z\}$
151		animorrl	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to (z = 1 \lor z = P - 1)$
152	3	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P \in ℙ$
153	129 90	sseldd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z \in (1 \dots P - 1)$
154		wilthlem1	$⊢ (P \in ℙ \land z \in (1 \dots P - 1)) \to (z = z^{P - 2} \mod P \leftrightarrow (z = 1 \lor z = P - 1))$
155	152 153 154	syl2anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (z = z^{P - 2} \mod P \leftrightarrow (z = 1 \lor z = P - 1))$
156	155	biimpar	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land (z = 1 \lor z = P - 1)) \to z = z^{P - 2} \mod P$
157	151 156	syldan	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to z = z^{P - 2} \mod P$
158	157	preq2d	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to \{z, z\} = \{z, z^{P - 2} \mod P\}$
159	150 158	syl5eq	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to \{z\} = \{z, z^{P - 2} \mod P\}$
160	159	reseq2d	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to {I ↾}_{\{z\}} = {I ↾}_{\{z, z^{P - 2} \mod P\}}$
161	149 160	eqtr3id	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to (w \in \{z\} ⟼ w) = {I ↾}_{\{z, z^{P - 2} \mod P\}}$
162	161	oveq2d	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to \underset{w \in \{z\}}{\sum_{T}} w = \sum_{T} ({I ↾}_{\{z, z^{P - 2} \mod P\}})$
163		simpr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to z = 1$
164	148 162 163	3eqtr3d	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to \sum_{T} ({I ↾}_{\{z, z^{P - 2} \mod P\}}) = 1$
165	164	oveq1d	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z = 1) \to (\sum_{T}, ({I ↾}_{\{z, z^{P - 2} \mod P\}})) \mod P = 1 \mod P$
166		df-pr	$⊢ \{z, z^{P - 2} \mod P\} = \{z\} \cup \{z^{P - 2} \mod P\}$
167	166	reseq2i	$⊢ {I ↾}_{\{z, z^{P - 2} \mod P\}} = {I ↾}_{(\{z\} \cup \{z^{P - 2} \mod P\})}$
168		mptresid	$⊢ {I ↾}_{(\{z\} \cup \{z^{P - 2} \mod P\})} = (w \in (\{z\} \cup \{z^{P - 2} \mod P\}) ⟼ w)$
169	167 168	eqtri	$⊢ {I ↾}_{\{z, z^{P - 2} \mod P\}} = (w \in (\{z\} \cup \{z^{P - 2} \mod P\}) ⟼ w)$
170	169	oveq2i	$⊢ \sum_{T} ({I ↾}_{\{z, z^{P - 2} \mod P\}}) = \underset{w \in \{z\} \cup \{z^{P - 2} \mod P\}}{\sum_{T}} w$
171	65	a1i	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to T \in CMnd$
172		snfi	$⊢ \{z\} \in Fin$
173	172	a1i	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to \{z\} \in Fin$
174		elsni	$⊢ w \in \{z\} \to w = z$
175	174	adantl	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land w \in \{z\}) \to w = z$
176	144	adantr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land w \in \{z\}) \to z \in ℂ$
177	175 176	eqeltrd	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land w \in \{z\}) \to w \in ℂ$
178	177	adantlr	$⊢ (((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \land w \in \{z\}) \to w \in ℂ$
179	143 96	sseldd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z^{P - 2} \mod P \in ℂ$
180	179	adantr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to z^{P - 2} \mod P \in ℂ$
181		simprr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg z \in \{P - 1\}$
182		velsn	$⊢ z \in \{P - 1\} \leftrightarrow z = P - 1$
183	181 182	sylnib	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg z = P - 1$
184		biorf	$⊢ \neg z = P - 1 \to (z = 1 \leftrightarrow (z = P - 1 \lor z = 1))$
185	183 184	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (z = 1 \leftrightarrow (z = P - 1 \lor z = 1))$
186		ovex	$⊢ z^{P - 2} \mod P \in V$
187	186	elsn	$⊢ z^{P - 2} \mod P \in \{z\} \leftrightarrow z^{P - 2} \mod P = z$
188		eqcom	$⊢ z^{P - 2} \mod P = z \leftrightarrow z = z^{P - 2} \mod P$
189	187 188	bitri	$⊢ z^{P - 2} \mod P \in \{z\} \leftrightarrow z = z^{P - 2} \mod P$
190		orcom	$⊢ (z = P - 1 \lor z = 1) \leftrightarrow (z = 1 \lor z = P - 1)$
191	155 189 190	3bitr4g	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (z^{P - 2} \mod P \in \{z\} \leftrightarrow (z = P - 1 \lor z = 1))$
192	185 191	bitr4d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (z = 1 \leftrightarrow z^{P - 2} \mod P \in \{z\})$
193	192	necon3abid	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (z \neq 1 \leftrightarrow \neg z^{P - 2} \mod P \in \{z\})$
194	193	biimpa	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to \neg z^{P - 2} \mod P \in \{z\}$
195		id	$⊢ w = z^{P - 2} \mod P \to w = z^{P - 2} \mod P$
196	40 62 171 173 178 180 194 180 195	gsumunsn	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to \underset{w \in \{z\} \cup \{z^{P - 2} \mod P\}}{\sum_{T}} w = (\underset{w \in \{z\}}{\sum_{T}}, w) (z^{P - 2} \mod P)$
197	170 196	syl5eq	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to \sum_{T} ({I ↾}_{\{z, z^{P - 2} \mod P\}}) = (\underset{w \in \{z\}}{\sum_{T}}, w) (z^{P - 2} \mod P)$
198	147	adantr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to \underset{w \in \{z\}}{\sum_{T}} w = z$
199	198	oveq1d	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to (\underset{w \in \{z\}}{\sum_{T}}, w) (z^{P - 2} \mod P) = z (z^{P - 2} \mod P)$
200	197 199	eqtrd	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to \sum_{T} ({I ↾}_{\{z, z^{P - 2} \mod P\}}) = z (z^{P - 2} \mod P)$
201	200	oveq1d	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to (\sum_{T}, ({I ↾}_{\{z, z^{P - 2} \mod P\}})) \mod P = z (z^{P - 2} \mod P) \mod P$
202	153	elfzelzd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z \in ℤ$
203	24	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P \in ℕ$
204		fzm1ndvds	$⊢ (P \in ℕ \land z \in (1 \dots P - 1)) \to \neg P ∥ z$
205	203 153 204	syl2anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg P ∥ z$
206		eqid	$⊢ z^{P - 2} \mod P = z^{P - 2} \mod P$
207	206	prmdiv	$⊢ (P \in ℙ \land z \in ℤ \land \neg P ∥ z) \to (z^{P - 2} \mod P \in (1 \dots P - 1) \land P ∥ (z (z^{P - 2} \mod P) - 1))$
208	152 202 205 207	syl3anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (z^{P - 2} \mod P \in (1 \dots P - 1) \land P ∥ (z (z^{P - 2} \mod P) - 1))$
209	208	simprd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P ∥ (z (z^{P - 2} \mod P) - 1)$
210		elfznn	$⊢ z \in (1 \dots P - 1) \to z \in ℕ$
211	153 210	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z \in ℕ$
212	129 96	sseldd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z^{P - 2} \mod P \in (1 \dots P - 1)$
213		elfznn	$⊢ z^{P - 2} \mod P \in (1 \dots P - 1) \to z^{P - 2} \mod P \in ℕ$
214	212 213	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z^{P - 2} \mod P \in ℕ$
215	211 214	nnmulcld	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z (z^{P - 2} \mod P) \in ℕ$
216	215	nnzd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z (z^{P - 2} \mod P) \in ℤ$
217		1zzd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 \in ℤ$
218		moddvds	$⊢ (P \in ℕ \land z (z^{P - 2} \mod P) \in ℤ \land 1 \in ℤ) \to (z (z^{P - 2} \mod P) \mod P = 1 \mod P \leftrightarrow P ∥ (z (z^{P - 2} \mod P) - 1))$
219	203 216 217 218	syl3anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (z (z^{P - 2} \mod P) \mod P = 1 \mod P \leftrightarrow P ∥ (z (z^{P - 2} \mod P) - 1))$
220	209 219	mpbird	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z (z^{P - 2} \mod P) \mod P = 1 \mod P$
221	220	adantr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to z (z^{P - 2} \mod P) \mod P = 1 \mod P$
222	201 221	eqtrd	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land z \neq 1) \to (\sum_{T}, ({I ↾}_{\{z, z^{P - 2} \mod P\}})) \mod P = 1 \mod P$
223	165 222	pm2.61dane	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (\sum_{T}, ({I ↾}_{\{z, z^{P - 2} \mod P\}})) \mod P = 1 \mod P$
224		modmul1	$⊢ ((\sum_{T} ({I ↾}_{\{z, z^{P - 2} \mod P\}}) \in ℝ \land 1 \in ℝ) \land (\sum_{T} ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) \in ℤ \land P \in ℝ^{+}) \land (\sum_{T}, ({I ↾}_{\{z, z^{P - 2} \mod P\}})) \mod P = 1 \mod P) \to (\sum_{T}, ({I ↾}_{\{z, z^{P - 2} \mod P\}})) (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P = 1 (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P$
225	127 128 140 141 223 224	syl221anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (\sum_{T}, ({I ↾}_{\{z, z^{P - 2} \mod P\}})) (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P = 1 (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P$
226	140	zcnd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \sum_{T} ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) \in ℂ$
227	226	mulid2d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) = \sum_{T} ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})$
228	227	oveq1d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P = (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P$
229		sseqin2	$⊢ \{z, z^{P - 2} \mod P\} \subseteq S \leftrightarrow S \cap \{z, z^{P - 2} \mod P\} = \{z, z^{P - 2} \mod P\}$
230	97 229	sylib	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S \cap \{z, z^{P - 2} \mod P\} = \{z, z^{P - 2} \mod P\}$
231		vex	$⊢ z \in V$
232	231	prnz	$⊢ \{z, z^{P - 2} \mod P\} \neq \emptyset$
233	232	a1i	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \{z, z^{P - 2} \mod P\} \neq \emptyset$
234	230 233	eqnetrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S \cap \{z, z^{P - 2} \mod P\} \neq \emptyset$
235		disj4	$⊢ S \cap \{z, z^{P - 2} \mod P\} = \emptyset \leftrightarrow \neg S ∖ \{z, z^{P - 2} \mod P\} \subset S$
236	235	necon2abii	$⊢ S ∖ \{z, z^{P - 2} \mod P\} \subset S \leftrightarrow S \cap \{z, z^{P - 2} \mod P\} \neq \emptyset$
237	234 236	sylibr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S ∖ \{z, z^{P - 2} \mod P\} \subset S$
238		psseq1	$⊢ s = S ∖ \{z, z^{P - 2} \mod P\} \to (s \subset S \leftrightarrow S ∖ \{z, z^{P - 2} \mod P\} \subset S)$
239		reseq2	$⊢ s = S ∖ \{z, z^{P - 2} \mod P\} \to {I ↾}_{s} = {I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}$
240	239	oveq2d	$⊢ s = S ∖ \{z, z^{P - 2} \mod P\} \to \sum_{T} ({I ↾}_{s}) = \sum_{T} ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})$
241	240	oveq1d	$⊢ s = S ∖ \{z, z^{P - 2} \mod P\} \to (\sum_{T}, ({I ↾}_{s})) \mod P = (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P$
242	241	eqeq1d	$⊢ s = S ∖ \{z, z^{P - 2} \mod P\} \to ((\sum_{T}, ({I ↾}_{s})) \mod P = -1 \mod P \leftrightarrow (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P = -1 \mod P)$
243	238 242	imbi12d	$⊢ s = S ∖ \{z, z^{P - 2} \mod P\} \to ((s \subset S \to (\sum_{T}, ({I ↾}_{s})) \mod P = -1 \mod P) \leftrightarrow (S ∖ \{z, z^{P - 2} \mod P\} \subset S \to (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P = -1 \mod P))$
244	5	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \forall s \in A (s \subset S \to (\sum_{T}, ({I ↾}_{s})) \mod P = -1 \mod P)$
245		ovex	$⊢ (1 \dots P - 1) \in V$
246	245	elpw2	$⊢ S ∖ \{z, z^{P - 2} \mod P\} \in 𝒫 (1 \dots P - 1) \leftrightarrow S ∖ \{z, z^{P - 2} \mod P\} \subseteq (1 \dots P - 1)$
247	130 246	sylibr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S ∖ \{z, z^{P - 2} \mod P\} \in 𝒫 (1 \dots P - 1)$
248	14	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in S$
249		eqcom	$⊢ z = P - 1 \leftrightarrow P - 1 = z$
250	182 249	bitri	$⊢ z \in \{P - 1\} \leftrightarrow P - 1 = z$
251	181 250	sylnib	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg P - 1 = z$
252		oveq1	$⊢ P - 1 = z^{P - 2} \mod P \to {(P - 1)}^{P - 2} = {(z^{P - 2} \mod P)}^{P - 2}$
253	252	oveq1d	$⊢ P - 1 = z^{P - 2} \mod P \to {(P - 1)}^{P - 2} \mod P = {(z^{P - 2} \mod P)}^{P - 2} \mod P$
254	203 36	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in ℕ_{0}$
255		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
256	254 255	eleqtrdi	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in ℤ_{\geq 0}$
257		eluzfz2	$⊢ P - 1 \in ℤ_{\geq 0} \to P - 1 \in (0 \dots P - 1)$
258	256 257	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in (0 \dots P - 1)$
259		prmz	$⊢ P \in ℙ \to P \in ℤ$
260	152 259	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P \in ℤ$
261	120 248	sseldd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in ℤ$
262		1z	$⊢ 1 \in ℤ$
263		zsubcl	$⊢ (P - 1 \in ℤ \land 1 \in ℤ) \to P - 1 - 1 \in ℤ$
264	261 262 263	sylancl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 - 1 \in ℤ$
265		dvdsmul1	$⊢ (P \in ℤ \land P - 1 - 1 \in ℤ) \to P ∥ P (P - 1 - 1)$
266	260 264 265	syl2anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P ∥ P (P - 1 - 1)$
267	203	nncnd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P \in ℂ$
268	264	zcnd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 - 1 \in ℂ$
269	267 268	mulcld	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1 - 1) \in ℂ$
270		1cnd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 \in ℂ$
271	254	nn0cnd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in ℂ$
272	267 270 271	subdird	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (P - 1) (P - 1) = P (P - 1) - 1 (P - 1)$
273	267 271	mulcld	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1) \in ℂ$
274	273 267 270	subsubd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1) - (P - 1) = P (P - 1) - P + 1$
275	271	mulid2d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 (P - 1) = P - 1$
276	275	oveq2d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1) - 1 (P - 1) = P (P - 1) - (P - 1)$
277	267 271	muls1d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1 - 1) = P (P - 1) - P$
278	277	oveq1d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1 - 1) + 1 = P (P - 1) - P + 1$
279	274 276 278	3eqtr4d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1) - 1 (P - 1) = P (P - 1 - 1) + 1$
280	272 279	eqtrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (P - 1) (P - 1) = P (P - 1 - 1) + 1$
281	269 270 280	mvrraddd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (P - 1) (P - 1) - 1 = P (P - 1 - 1)$
282	266 281	breqtrrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P ∥ ((P - 1) (P - 1) - 1)$
283	129 248	sseldd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in (1 \dots P - 1)$
284		fzm1ndvds	$⊢ (P \in ℕ \land P - 1 \in (1 \dots P - 1)) \to \neg P ∥ (P - 1)$
285	203 283 284	syl2anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg P ∥ (P - 1)$
286		eqid	$⊢ {(P - 1)}^{P - 2} \mod P = {(P - 1)}^{P - 2} \mod P$
287	286	prmdiveq	$⊢ (P \in ℙ \land P - 1 \in ℤ \land \neg P ∥ (P - 1)) \to ((P - 1 \in (0 \dots P - 1) \land P ∥ ((P - 1) (P - 1) - 1)) \leftrightarrow P - 1 = {(P - 1)}^{P - 2} \mod P)$
288	152 261 285 287	syl3anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to ((P - 1 \in (0 \dots P - 1) \land P ∥ ((P - 1) (P - 1) - 1)) \leftrightarrow P - 1 = {(P - 1)}^{P - 2} \mod P)$
289	258 282 288	mpbi2and	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 = {(P - 1)}^{P - 2} \mod P$
290	206	prmdivdiv	$⊢ (P \in ℙ \land z \in (1 \dots P - 1)) \to z = {(z^{P - 2} \mod P)}^{P - 2} \mod P$
291	152 153 290	syl2anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z = {(z^{P - 2} \mod P)}^{P - 2} \mod P$
292	289 291	eqeq12d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (P - 1 = z \leftrightarrow {(P - 1)}^{P - 2} \mod P = {(z^{P - 2} \mod P)}^{P - 2} \mod P)$
293	253 292	syl5ibr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (P - 1 = z^{P - 2} \mod P \to P - 1 = z)$
294	251 293	mtod	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg P - 1 = z^{P - 2} \mod P$
295		ioran	$⊢ \neg (P - 1 = z \lor P - 1 = z^{P - 2} \mod P) \leftrightarrow (\neg P - 1 = z \land \neg P - 1 = z^{P - 2} \mod P)$
296	251 294 295	sylanbrc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg (P - 1 = z \lor P - 1 = z^{P - 2} \mod P)$
297		ovex	$⊢ P - 1 \in V$
298	297	elpr	$⊢ P - 1 \in \{z, z^{P - 2} \mod P\} \leftrightarrow (P - 1 = z \lor P - 1 = z^{P - 2} \mod P)$
299	296 298	sylnibr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg P - 1 \in \{z, z^{P - 2} \mod P\}$
300	248 299	eldifd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in (S ∖ \{z, z^{P - 2} \mod P\})$
301		eldifi	$⊢ y \in (S ∖ \{z, z^{P - 2} \mod P\}) \to y \in S$
302	95	r19.21bi	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to y^{P - 2} \mod P \in S$
303	301 302	sylan2	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in (S ∖ \{z, z^{P - 2} \mod P\})) \to y^{P - 2} \mod P \in S$
304		eldif	$⊢ y \in (S ∖ \{z, z^{P - 2} \mod P\}) \leftrightarrow (y \in S \land \neg y \in \{z, z^{P - 2} \mod P\})$
305	152	adantr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to P \in ℙ$
306	129	sselda	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to y \in (1 \dots P - 1)$
307		eqid	$⊢ y^{P - 2} \mod P = y^{P - 2} \mod P$
308	307	prmdivdiv	$⊢ (P \in ℙ \land y \in (1 \dots P - 1)) \to y = {(y^{P - 2} \mod P)}^{P - 2} \mod P$
309	305 306 308	syl2anc	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to y = {(y^{P - 2} \mod P)}^{P - 2} \mod P$
310		oveq1	$⊢ y^{P - 2} \mod P = z \to {(y^{P - 2} \mod P)}^{P - 2} = z^{P - 2}$
311	310	oveq1d	$⊢ y^{P - 2} \mod P = z \to {(y^{P - 2} \mod P)}^{P - 2} \mod P = z^{P - 2} \mod P$
312	311	eqeq2d	$⊢ y^{P - 2} \mod P = z \to (y = {(y^{P - 2} \mod P)}^{P - 2} \mod P \leftrightarrow y = z^{P - 2} \mod P)$
313	309 312	syl5ibcom	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to (y^{P - 2} \mod P = z \to y = z^{P - 2} \mod P)$
314		oveq1	$⊢ y^{P - 2} \mod P = z^{P - 2} \mod P \to {(y^{P - 2} \mod P)}^{P - 2} = {(z^{P - 2} \mod P)}^{P - 2}$
315	314	oveq1d	$⊢ y^{P - 2} \mod P = z^{P - 2} \mod P \to {(y^{P - 2} \mod P)}^{P - 2} \mod P = {(z^{P - 2} \mod P)}^{P - 2} \mod P$
316	291	adantr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to z = {(z^{P - 2} \mod P)}^{P - 2} \mod P$
317	309 316	eqeq12d	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to (y = z \leftrightarrow {(y^{P - 2} \mod P)}^{P - 2} \mod P = {(z^{P - 2} \mod P)}^{P - 2} \mod P)$
318	315 317	syl5ibr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to (y^{P - 2} \mod P = z^{P - 2} \mod P \to y = z)$
319	313 318	orim12d	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to ((y^{P - 2} \mod P = z \lor y^{P - 2} \mod P = z^{P - 2} \mod P) \to (y = z^{P - 2} \mod P \lor y = z))$
320		ovex	$⊢ y^{P - 2} \mod P \in V$
321	320	elpr	$⊢ y^{P - 2} \mod P \in \{z, z^{P - 2} \mod P\} \leftrightarrow (y^{P - 2} \mod P = z \lor y^{P - 2} \mod P = z^{P - 2} \mod P)$
322		vex	$⊢ y \in V$
323	322	elpr	$⊢ y \in \{z, z^{P - 2} \mod P\} \leftrightarrow (y = z \lor y = z^{P - 2} \mod P)$
324		orcom	$⊢ (y = z \lor y = z^{P - 2} \mod P) \leftrightarrow (y = z^{P - 2} \mod P \lor y = z)$
325	323 324	bitri	$⊢ y \in \{z, z^{P - 2} \mod P\} \leftrightarrow (y = z^{P - 2} \mod P \lor y = z)$
326	319 321 325	3imtr4g	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to (y^{P - 2} \mod P \in \{z, z^{P - 2} \mod P\} \to y \in \{z, z^{P - 2} \mod P\})$
327	326	con3d	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to (\neg y \in \{z, z^{P - 2} \mod P\} \to \neg y^{P - 2} \mod P \in \{z, z^{P - 2} \mod P\})$
328	327	impr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land (y \in S \land \neg y \in \{z, z^{P - 2} \mod P\})) \to \neg y^{P - 2} \mod P \in \{z, z^{P - 2} \mod P\}$
329	304 328	sylan2b	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in (S ∖ \{z, z^{P - 2} \mod P\})) \to \neg y^{P - 2} \mod P \in \{z, z^{P - 2} \mod P\}$
330	303 329	eldifd	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in (S ∖ \{z, z^{P - 2} \mod P\})) \to y^{P - 2} \mod P \in (S ∖ \{z, z^{P - 2} \mod P\})$
331	330	ralrimiva	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \forall y \in (S ∖ \{z, z^{P - 2} \mod P\}) y^{P - 2} \mod P \in (S ∖ \{z, z^{P - 2} \mod P\})$
332	300 331	jca	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (P - 1 \in (S ∖ \{z, z^{P - 2} \mod P\}) \land \forall y \in (S ∖ \{z, z^{P - 2} \mod P\}) y^{P - 2} \mod P \in (S ∖ \{z, z^{P - 2} \mod P\}))$
333		eleq2	$⊢ x = S ∖ \{z, z^{P - 2} \mod P\} \to (P - 1 \in x \leftrightarrow P - 1 \in (S ∖ \{z, z^{P - 2} \mod P\}))$
334		eleq2	$⊢ x = S ∖ \{z, z^{P - 2} \mod P\} \to (y^{P - 2} \mod P \in x \leftrightarrow y^{P - 2} \mod P \in (S ∖ \{z, z^{P - 2} \mod P\}))$
335	334	raleqbi1dv	$⊢ x = S ∖ \{z, z^{P - 2} \mod P\} \to (\forall y \in x y^{P - 2} \mod P \in x \leftrightarrow \forall y \in (S ∖ \{z, z^{P - 2} \mod P\}) y^{P - 2} \mod P \in (S ∖ \{z, z^{P - 2} \mod P\}))$
336	333 335	anbi12d	$⊢ x = S ∖ \{z, z^{P - 2} \mod P\} \to ((P - 1 \in x \land \forall y \in x y^{P - 2} \mod P \in x) \leftrightarrow (P - 1 \in (S ∖ \{z, z^{P - 2} \mod P\}) \land \forall y \in (S ∖ \{z, z^{P - 2} \mod P\}) y^{P - 2} \mod P \in (S ∖ \{z, z^{P - 2} \mod P\})))$
337	336 2	elrab2	$⊢ S ∖ \{z, z^{P - 2} \mod P\} \in A \leftrightarrow (S ∖ \{z, z^{P - 2} \mod P\} \in 𝒫 (1 \dots P - 1) \land (P - 1 \in (S ∖ \{z, z^{P - 2} \mod P\}) \land \forall y \in (S ∖ \{z, z^{P - 2} \mod P\}) y^{P - 2} \mod P \in (S ∖ \{z, z^{P - 2} \mod P\})))$
338	247 332 337	sylanbrc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S ∖ \{z, z^{P - 2} \mod P\} \in A$
339	243 244 338	rspcdva	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (S ∖ \{z, z^{P - 2} \mod P\} \subset S \to (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P = -1 \mod P)$
340	237 339	mpd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P = -1 \mod P$
341	228 340	eqtrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 (\sum_{T}, ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})) \mod P = -1 \mod P$
342	111 225 341	3eqtrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P$
343	342	ex	$⊢ φ \to ((z \in S \land \neg z \in \{P - 1\}) \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P)$
344	343	exlimdv	$⊢ φ \to (\exists z (z \in S \land \neg z \in \{P - 1\}) \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P)$
345	58 344	syl5bi	$⊢ φ \to (\neg S \subseteq \{P - 1\} \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P)$
346	57 345	pm2.61d	$⊢ φ \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P$

Metamath Proof Explorer

Theorem wilthlem2

Proof