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	syl6eq	$⊢ (φ \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	syl5req	$⊢ (φ \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	syl5eqr	$⊢ ((φ \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		elfzelz	$⊢ z \in (1 \dots P - 1) \to z \in ℤ$
203	153 202	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z \in ℤ$
204	24	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P \in ℕ$
205		fzm1ndvds	$⊢ (P \in ℕ \land z \in (1 \dots P - 1)) \to \neg P ∥ z$
206	204 153 205	syl2anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg P ∥ z$
207		eqid	$⊢ z^{P - 2} \mod P = z^{P - 2} \mod P$
208	207	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))$
209	152 203 206 208	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))$
210	209	simprd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P ∥ (z (z^{P - 2} \mod P) - 1)$
211		elfznn	$⊢ z \in (1 \dots P - 1) \to z \in ℕ$
212	153 211	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z \in ℕ$
213	129 96	sseldd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z^{P - 2} \mod P \in (1 \dots P - 1)$
214		elfznn	$⊢ z^{P - 2} \mod P \in (1 \dots P - 1) \to z^{P - 2} \mod P \in ℕ$
215	213 214	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z^{P - 2} \mod P \in ℕ$
216	212 215	nnmulcld	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z (z^{P - 2} \mod P) \in ℕ$
217	216	nnzd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z (z^{P - 2} \mod P) \in ℤ$
218		1zzd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 \in ℤ$
219		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))$
220	204 217 218 219	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))$
221	210 220	mpbird	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z (z^{P - 2} \mod P) \mod P = 1 \mod P$
222	221	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$
223	201 222	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$
224	165 223	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$
225		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$
226	127 128 140 141 224 225	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$
227	140	zcnd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \sum_{T} ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}) \in ℂ$
228	227	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\})})$
229	228	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$
230		sseqin2	$⊢ \{z, z^{P - 2} \mod P\} \subseteq S \leftrightarrow S \cap \{z, z^{P - 2} \mod P\} = \{z, z^{P - 2} \mod P\}$
231	97 230	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\}$
232		vex	$⊢ z \in V$
233	232	prnz	$⊢ \{z, z^{P - 2} \mod P\} \neq \emptyset$
234	233	a1i	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \{z, z^{P - 2} \mod P\} \neq \emptyset$
235	231 234	eqnetrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S \cap \{z, z^{P - 2} \mod P\} \neq \emptyset$
236		disj4	$⊢ S \cap \{z, z^{P - 2} \mod P\} = \emptyset \leftrightarrow \neg S ∖ \{z, z^{P - 2} \mod P\} \subset S$
237	236	necon2abii	$⊢ S ∖ \{z, z^{P - 2} \mod P\} \subset S \leftrightarrow S \cap \{z, z^{P - 2} \mod P\} \neq \emptyset$
238	235 237	sylibr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S ∖ \{z, z^{P - 2} \mod P\} \subset S$
239		psseq1	$⊢ s = S ∖ \{z, z^{P - 2} \mod P\} \to (s \subset S \leftrightarrow S ∖ \{z, z^{P - 2} \mod P\} \subset S)$
240		reseq2	$⊢ s = S ∖ \{z, z^{P - 2} \mod P\} \to {I ↾}_{s} = {I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})}$
241	240	oveq2d	$⊢ s = S ∖ \{z, z^{P - 2} \mod P\} \to \sum_{T} ({I ↾}_{s}) = \sum_{T} ({I ↾}_{(S ∖ \{z, z^{P - 2} \mod P\})})$
242	241	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$
243	242	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)$
244	239 243	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))$
245	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)$
246		ovex	$⊢ (1 \dots P - 1) \in V$
247	246	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)$
248	130 247	sylibr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S ∖ \{z, z^{P - 2} \mod P\} \in 𝒫 (1 \dots P - 1)$
249	14	adantr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in S$
250		eqcom	$⊢ z = P - 1 \leftrightarrow P - 1 = z$
251	182 250	bitri	$⊢ z \in \{P - 1\} \leftrightarrow P - 1 = z$
252	181 251	sylnib	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg P - 1 = z$
253		oveq1	$⊢ P - 1 = z^{P - 2} \mod P \to {(P - 1)}^{P - 2} = {(z^{P - 2} \mod P)}^{P - 2}$
254	253	oveq1d	$⊢ P - 1 = z^{P - 2} \mod P \to {(P - 1)}^{P - 2} \mod P = {(z^{P - 2} \mod P)}^{P - 2} \mod P$
255	204 36	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in ℕ_{0}$
256		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
257	255 256	eleqtrdi	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in ℤ_{\geq 0}$
258		eluzfz2	$⊢ P - 1 \in ℤ_{\geq 0} \to P - 1 \in (0 \dots P - 1)$
259	257 258	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in (0 \dots P - 1)$
260		prmz	$⊢ P \in ℙ \to P \in ℤ$
261	152 260	syl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P \in ℤ$
262	120 249	sseldd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in ℤ$
263		1z	$⊢ 1 \in ℤ$
264		zsubcl	$⊢ (P - 1 \in ℤ \land 1 \in ℤ) \to P - 1 - 1 \in ℤ$
265	262 263 264	sylancl	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 - 1 \in ℤ$
266		dvdsmul1	$⊢ (P \in ℤ \land P - 1 - 1 \in ℤ) \to P ∥ P (P - 1 - 1)$
267	261 265 266	syl2anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P ∥ P (P - 1 - 1)$
268	204	nncnd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P \in ℂ$
269	265	zcnd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 - 1 \in ℂ$
270	268 269	mulcld	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1 - 1) \in ℂ$
271		1cnd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 \in ℂ$
272	255	nn0cnd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in ℂ$
273	268 271 272	subdird	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (P - 1) (P - 1) = P (P - 1) - 1 (P - 1)$
274	268 272	mulcld	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1) \in ℂ$
275	274 268 271	subsubd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1) - (P - 1) = P (P - 1) - P + 1$
276	272	mulid2d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to 1 (P - 1) = P - 1$
277	276	oveq2d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1) - 1 (P - 1) = P (P - 1) - (P - 1)$
278	268 272	muls1d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1 - 1) = P (P - 1) - P$
279	278	oveq1d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1 - 1) + 1 = P (P - 1) - P + 1$
280	275 277 279	3eqtr4d	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P (P - 1) - 1 (P - 1) = P (P - 1 - 1) + 1$
281	273 280	eqtrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (P - 1) (P - 1) = P (P - 1 - 1) + 1$
282	270 271 281	mvrraddd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (P - 1) (P - 1) - 1 = P (P - 1 - 1)$
283	267 282	breqtrrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P ∥ ((P - 1) (P - 1) - 1)$
284	129 249	sseldd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in (1 \dots P - 1)$
285		fzm1ndvds	$⊢ (P \in ℕ \land P - 1 \in (1 \dots P - 1)) \to \neg P ∥ (P - 1)$
286	204 284 285	syl2anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg P ∥ (P - 1)$
287		eqid	$⊢ {(P - 1)}^{P - 2} \mod P = {(P - 1)}^{P - 2} \mod P$
288	287	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)$
289	152 262 286 288	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)$
290	259 283 289	mpbi2and	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 = {(P - 1)}^{P - 2} \mod P$
291	207	prmdivdiv	$⊢ (P \in ℙ \land z \in (1 \dots P - 1)) \to z = {(z^{P - 2} \mod P)}^{P - 2} \mod P$
292	152 153 291	syl2anc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to z = {(z^{P - 2} \mod P)}^{P - 2} \mod P$
293	290 292	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)$
294	254 293	syl5ibr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (P - 1 = z^{P - 2} \mod P \to P - 1 = z)$
295	252 294	mtod	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg P - 1 = z^{P - 2} \mod P$
296		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)$
297	252 295 296	sylanbrc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg (P - 1 = z \lor P - 1 = z^{P - 2} \mod P)$
298		ovex	$⊢ P - 1 \in V$
299	298	elpr	$⊢ P - 1 \in \{z, z^{P - 2} \mod P\} \leftrightarrow (P - 1 = z \lor P - 1 = z^{P - 2} \mod P)$
300	297 299	sylnibr	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to \neg P - 1 \in \{z, z^{P - 2} \mod P\}$
301	249 300	eldifd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to P - 1 \in (S ∖ \{z, z^{P - 2} \mod P\})$
302		eldifi	$⊢ y \in (S ∖ \{z, z^{P - 2} \mod P\}) \to y \in S$
303	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$
304	302 303	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$
305		eldif	$⊢ y \in (S ∖ \{z, z^{P - 2} \mod P\}) \leftrightarrow (y \in S \land \neg y \in \{z, z^{P - 2} \mod P\})$
306	152	adantr	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to P \in ℙ$
307	129	sselda	$⊢ ((φ \land (z \in S \land \neg z \in \{P - 1\})) \land y \in S) \to y \in (1 \dots P - 1)$
308		eqid	$⊢ y^{P - 2} \mod P = y^{P - 2} \mod P$
309	308	prmdivdiv	$⊢ (P \in ℙ \land y \in (1 \dots P - 1)) \to y = {(y^{P - 2} \mod P)}^{P - 2} \mod P$
310	306 307 309	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$
311		oveq1	$⊢ y^{P - 2} \mod P = z \to {(y^{P - 2} \mod P)}^{P - 2} = z^{P - 2}$
312	311	oveq1d	$⊢ y^{P - 2} \mod P = z \to {(y^{P - 2} \mod P)}^{P - 2} \mod P = z^{P - 2} \mod P$
313	312	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)$
314	310 313	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)$
315		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}$
316	315	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$
317	292	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$
318	310 317	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)$
319	316 318	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)$
320	314 319	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))$
321		ovex	$⊢ y^{P - 2} \mod P \in V$
322	321	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)$
323		vex	$⊢ y \in V$
324	323	elpr	$⊢ y \in \{z, z^{P - 2} \mod P\} \leftrightarrow (y = z \lor y = z^{P - 2} \mod P)$
325		orcom	$⊢ (y = z \lor y = z^{P - 2} \mod P) \leftrightarrow (y = z^{P - 2} \mod P \lor y = z)$
326	324 325	bitri	$⊢ y \in \{z, z^{P - 2} \mod P\} \leftrightarrow (y = z^{P - 2} \mod P \lor y = z)$
327	320 322 326	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\})$
328	327	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\})$
329	328	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\}$
330	305 329	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\}$
331	304 330	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\})$
332	331	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\})$
333	301 332	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\}))$
334		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\}))$
335		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\}))$
336	335	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\}))$
337	334 336	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\})))$
338	337 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\})))$
339	248 333 338	sylanbrc	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to S ∖ \{z, z^{P - 2} \mod P\} \in A$
340	244 245 339	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)$
341	238 340	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$
342	229 341	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$
343	111 226 342	3eqtrd	$⊢ (φ \land (z \in S \land \neg z \in \{P - 1\})) \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P$
344	343	ex	$⊢ φ \to ((z \in S \land \neg z \in \{P - 1\}) \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P)$
345	344	exlimdv	$⊢ φ \to (\exists z (z \in S \land \neg z \in \{P - 1\}) \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P)$
346	58 345	syl5bi	$⊢ φ \to (\neg S \subseteq \{P - 1\} \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P)$
347	57 346	pm2.61d	$⊢ φ \to (\sum_{T}, ({I ↾}_{S})) \mod P = -1 \mod P$

Metamath Proof Explorer

Theorem wilthlem2

Proof