wilthlem3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > wilthlem3		Structured version Visualization version GIF version

Theorem wilthlem3 27100

Description: Lemma for wilth 27101. Here we round out the argument of wilthlem2 27099 with the final step of the induction. The induction argument shows that every subset of 1...(𝑃 − 1) that is closed under inverse and contains 𝑃 − 1 multiplies to -1 mod 𝑃, and clearly 1...(𝑃 − 1) itself is such a set. Thus, the product of all the elements is -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.)

**Hypotheses**
Ref	Expression
wilthlem.t	⊢ 𝑇 = (mulGrp‘ℂ_fld)
wilthlem.a	⊢ 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)}

**Assertion**
Ref	Expression
wilthlem3	⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((!‘(𝑃 − 1)) + 1))

Distinct variable groups: 𝑥,𝑦,𝐴 𝑥,𝑃,𝑦 𝑥,𝑇,𝑦

Proof of Theorem wilthlem3 Dummy variables 𝑡 𝑠 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmuz2 16702	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
2		uz2m1nn 12910	. . . . . . . 8 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
3	1, 2	syl 17	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ)
4		nnuz 12864	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
5	3, 4	eleqtrdi 2862	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ (ℤ_≥‘1))
6		eluzfz2 13523	. . . . . 6 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘1) → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
7	5, 6	syl 17	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
8		simpl 485	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℙ)
9		elfzelz 13515	. . . . . . . . 9 ⊢ (𝑦 ∈ (1...(𝑃 − 1)) → 𝑦 ∈ ℤ)
10	9	adantl 484	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑦 ∈ ℤ)
11		prmnn 16680	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
12		fzm1ndvds 16328	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑦)
13	11, 12	sylan 588	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑦)
14		eqid 2752	. . . . . . . . 9 ⊢ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑦↑(𝑃 − 2)) mod 𝑃)
15	14	prmdiv 16792	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑦) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑦 · ((𝑦↑(𝑃 − 2)) mod 𝑃)) − 1)))
16	8, 10, 13, 15	syl3anc 1382	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑦 · ((𝑦↑(𝑃 − 2)) mod 𝑃)) − 1)))
17	16	simpld 497	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
18	17	ralrimiva 3144	. . . . 5 ⊢ (𝑃 ∈ ℙ → ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
19		ovex 7414	. . . . . . 7 ⊢ (1...(𝑃 − 1)) ∈ V
20	19	pwid 4568	. . . . . 6 ⊢ (1...(𝑃 − 1)) ∈ 𝒫 (1...(𝑃 − 1))
21		eleq2 2841	. . . . . . . 8 ⊢ (𝑥 = (1...(𝑃 − 1)) → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ (1...(𝑃 − 1))))
22		eleq2 2841	. . . . . . . . 9 ⊢ (𝑥 = (1...(𝑃 − 1)) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
23	22	raleqbi1dv 3320	. . . . . . . 8 ⊢ (𝑥 = (1...(𝑃 − 1)) → (∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
24	21, 23	anbi12d 640	. . . . . . 7 ⊢ (𝑥 = (1...(𝑃 − 1)) → (((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥) ↔ ((𝑃 − 1) ∈ (1...(𝑃 − 1)) ∧ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))))
25		wilthlem.a	. . . . . . 7 ⊢ 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)}
26	24, 25	elrab2 3644	. . . . . 6 ⊢ ((1...(𝑃 − 1)) ∈ 𝐴 ↔ ((1...(𝑃 − 1)) ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ (1...(𝑃 − 1)) ∧ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))))
27	20, 26	mpbiran 717	. . . . 5 ⊢ ((1...(𝑃 − 1)) ∈ 𝐴 ↔ ((𝑃 − 1) ∈ (1...(𝑃 − 1)) ∧ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
28	7, 18, 27	sylanbrc 591	. . . 4 ⊢ (𝑃 ∈ ℙ → (1...(𝑃 − 1)) ∈ 𝐴)
29		fzfi 13971	. . . . 5 ⊢ (1...(𝑃 − 1)) ∈ Fin
30		eleq1 2840	. . . . . . . 8 ⊢ (𝑠 = 𝑡 → (𝑠 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))
31		reseq2 5949	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → ( I ↾ 𝑠) = ( I ↾ 𝑡))
32	31	oveq2d 7397	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (𝑇 Σ_g ( I ↾ 𝑠)) = (𝑇 Σ_g ( I ↾ 𝑡)))
33	32	oveq1d 7396	. . . . . . . . 9 ⊢ (𝑠 = 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃))
34	33	eqeq1d 2754	. . . . . . . 8 ⊢ (𝑠 = 𝑡 → (((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃)))
35	30, 34	imbi12d 346	. . . . . . 7 ⊢ (𝑠 = 𝑡 → ((𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ (𝑡 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))))
36	35	imbi2d 342	. . . . . 6 ⊢ (𝑠 = 𝑡 → ((𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ↔ (𝑃 ∈ ℙ → (𝑡 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃)))))
37		eleq1 2840	. . . . . . . 8 ⊢ (𝑠 = (1...(𝑃 − 1)) → (𝑠 ∈ 𝐴 ↔ (1...(𝑃 − 1)) ∈ 𝐴))
38		reseq2 5949	. . . . . . . . . . 11 ⊢ (𝑠 = (1...(𝑃 − 1)) → ( I ↾ 𝑠) = ( I ↾ (1...(𝑃 − 1))))
39	38	oveq2d 7397	. . . . . . . . . 10 ⊢ (𝑠 = (1...(𝑃 − 1)) → (𝑇 Σ_g ( I ↾ 𝑠)) = (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))))
40	39	oveq1d 7396	. . . . . . . . 9 ⊢ (𝑠 = (1...(𝑃 − 1)) → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃))
41	40	eqeq1d 2754	. . . . . . . 8 ⊢ (𝑠 = (1...(𝑃 − 1)) → (((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃)))
42	37, 41	imbi12d 346	. . . . . . 7 ⊢ (𝑠 = (1...(𝑃 − 1)) → ((𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((1...(𝑃 − 1)) ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃))))
43	42	imbi2d 342	. . . . . 6 ⊢ (𝑠 = (1...(𝑃 − 1)) → ((𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ↔ (𝑃 ∈ ℙ → ((1...(𝑃 − 1)) ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃)))))
44		bi2.04 390	. . . . . . . . . . 11 ⊢ ((𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) ↔ (𝑃 ∈ ℙ → (𝑠 ⊊ 𝑡 → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
45		pm2.27 42	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ ℙ → ((𝑃 ∈ ℙ → (𝑠 ⊊ 𝑡 → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → (𝑠 ⊊ 𝑡 → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
46	45	com34 91	. . . . . . . . . . 11 ⊢ (𝑃 ∈ ℙ → ((𝑃 ∈ ℙ → (𝑠 ⊊ 𝑡 → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → (𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
47	44, 46	biimtrid 244	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → ((𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → (𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
48	47	alimdv 1926	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → (∀𝑠(𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → ∀𝑠(𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
49		df-ral 3067	. . . . . . . . 9 ⊢ (∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ∀𝑠(𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))))
50	48, 49	imbitrrdi 254	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → (∀𝑠(𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))))
51		wilthlem.t	. . . . . . . . . 10 ⊢ 𝑇 = (mulGrp‘ℂ_fld)
52		simp1 1145	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → 𝑃 ∈ ℙ)
53		simp3 1147	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ 𝐴)
54		simp2 1146	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
55	51, 25, 52, 53, 54	wilthlem2 27099	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))
56	55	3exp 1128	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → (∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) → (𝑡 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))))
57	50, 56	syldc 48	. . . . . . 7 ⊢ (∀𝑠(𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → (𝑃 ∈ ℙ → (𝑡 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))))
58	57	a1i 11	. . . . . 6 ⊢ (𝑡 ∈ Fin → (∀𝑠(𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → (𝑃 ∈ ℙ → (𝑡 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃)))))
59	36, 43, 58	findcard3 9212	. . . . 5 ⊢ ((1...(𝑃 − 1)) ∈ Fin → (𝑃 ∈ ℙ → ((1...(𝑃 − 1)) ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃))))
60	29, 59	ax-mp 5	. . . 4 ⊢ (𝑃 ∈ ℙ → ((1...(𝑃 − 1)) ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃)))
61	28, 60	mpd 15	. . 3 ⊢ (𝑃 ∈ ℙ → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃))
62		cnfld1 21418	. . . . . 6 ⊢ 1 = (1_r‘ℂ_fld)
63	51, 62	ringidval 20201	. . . . 5 ⊢ 1 = (0_g‘𝑇)
64		cncrng 21414	. . . . . 6 ⊢ ℂ_fld ∈ CRing
65	51	crngmgp 20259	. . . . . 6 ⊢ (ℂ_fld ∈ CRing → 𝑇 ∈ CMnd)
66	64, 65	mp1i 13	. . . . 5 ⊢ (𝑃 ∈ ℙ → 𝑇 ∈ CMnd)
67	29	a1i 11	. . . . 5 ⊢ (𝑃 ∈ ℙ → (1...(𝑃 − 1)) ∈ Fin)
68		zsubrg 21441	. . . . . 6 ⊢ ℤ ∈ (SubRing‘ℂ_fld)
69	51	subrgsubm 20603	. . . . . 6 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubMnd‘𝑇))
70	68, 69	mp1i 13	. . . . 5 ⊢ (𝑃 ∈ ℙ → ℤ ∈ (SubMnd‘𝑇))
71		f1oi 6830	. . . . . . . 8 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))–1-1-onto→(1...(𝑃 − 1))
72		f1of 6791	. . . . . . . 8 ⊢ (( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))–1-1-onto→(1...(𝑃 − 1)) → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶(1...(𝑃 − 1)))
73	71, 72	ax-mp 5	. . . . . . 7 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶(1...(𝑃 − 1))
74		fzssz 13517	. . . . . . 7 ⊢ (1...(𝑃 − 1)) ⊆ ℤ
75		fss 6693	. . . . . . 7 ⊢ ((( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶(1...(𝑃 − 1)) ∧ (1...(𝑃 − 1)) ⊆ ℤ) → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ)
76	73, 74, 75	mp2an 700	. . . . . 6 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ
77	76	a1i 11	. . . . 5 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ)
78		1ex 11162	. . . . . . 7 ⊢ 1 ∈ V
79	78	a1i 11	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 1 ∈ V)
80	77, 67, 79	fdmfifsupp 9307	. . . . 5 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))) finSupp 1)
81	63, 66, 67, 70, 77, 80	gsumsubmcl 19931	. . . 4 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) ∈ ℤ)
82		1z 12587	. . . . 5 ⊢ 1 ∈ ℤ
83		znegcl 12592	. . . . 5 ⊢ (1 ∈ ℤ → -1 ∈ ℤ)
84	82, 83	mp1i 13	. . . 4 ⊢ (𝑃 ∈ ℙ → -1 ∈ ℤ)
85		moddvds 16269	. . . 4 ⊢ ((𝑃 ∈ ℕ ∧ (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) ∈ ℤ ∧ -1 ∈ ℤ) → (((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1)))
86	11, 81, 84, 85	syl3anc 1382	. . 3 ⊢ (𝑃 ∈ ℙ → (((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1)))
87	61, 86	mpbid 234	. 2 ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1))
88		fcoi1 6723	. . . . . . . . . 10 ⊢ (( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶(1...(𝑃 − 1)) → (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))) = ( I ↾ (1...(𝑃 − 1))))
89	73, 88	ax-mp 5	. . . . . . . . 9 ⊢ (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))) = ( I ↾ (1...(𝑃 − 1)))
90	89	fveq1i 6853	. . . . . . . 8 ⊢ ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = (( I ↾ (1...(𝑃 − 1)))‘𝑘)
91		fvres 6871	. . . . . . . 8 ⊢ (𝑘 ∈ (1...(𝑃 − 1)) → (( I ↾ (1...(𝑃 − 1)))‘𝑘) = ( I ‘𝑘))
92	90, 91	eqtrid 2799	. . . . . . 7 ⊢ (𝑘 ∈ (1...(𝑃 − 1)) → ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = ( I ‘𝑘))
93	92	adantl 484	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑃 − 1))) → ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = ( I ‘𝑘))
94	5, 93	seqfveq 14025	. . . . 5 ⊢ (𝑃 ∈ ℙ → (seq1( · , (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))))‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
95		cnfldbas 21397	. . . . . . 7 ⊢ ℂ = (Base‘ℂ_fld)
96	51, 95	mgpbas 20163	. . . . . 6 ⊢ ℂ = (Base‘𝑇)
97		cnfldmul 21401	. . . . . . 7 ⊢ · = (._r‘ℂ_fld)
98	51, 97	mgpplusg 20162	. . . . . 6 ⊢ · = (+_g‘𝑇)
99		eqid 2752	. . . . . 6 ⊢ (Cntz‘𝑇) = (Cntz‘𝑇)
100		cnring 21415	. . . . . . 7 ⊢ ℂ_fld ∈ Ring
101	51	ringmgp 20257	. . . . . . 7 ⊢ (ℂ_fld ∈ Ring → 𝑇 ∈ Mnd)
102	100, 101	mp1i 13	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑇 ∈ Mnd)
103		zsscn 12562	. . . . . . . 8 ⊢ ℤ ⊆ ℂ
104		fss 6693	. . . . . . . 8 ⊢ ((( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ ∧ ℤ ⊆ ℂ) → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ)
105	76, 103, 104	mp2an 700	. . . . . . 7 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ
106	105	a1i 11	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ)
107	96, 99, 66, 106	cntzcmnf 19857	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ran ( I ↾ (1...(𝑃 − 1))) ⊆ ((Cntz‘𝑇)‘ran ( I ↾ (1...(𝑃 − 1)))))
108		f1of1 6790	. . . . . . 7 ⊢ (( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))–1-1-onto→(1...(𝑃 − 1)) → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))–1-1→(1...(𝑃 − 1)))
109	71, 108	mp1i 13	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))–1-1→(1...(𝑃 − 1)))
110		suppssdm 8141	. . . . . . . . 9 ⊢ (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ dom ( I ↾ (1...(𝑃 − 1)))
111		dmresi 6027	. . . . . . . . 9 ⊢ dom ( I ↾ (1...(𝑃 − 1))) = (1...(𝑃 − 1))
112	110, 111	sseqtri 3975	. . . . . . . 8 ⊢ (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ (1...(𝑃 − 1))
113		rnresi 6050	. . . . . . . 8 ⊢ ran ( I ↾ (1...(𝑃 − 1))) = (1...(𝑃 − 1))
114	112, 113	sseqtrri 3976	. . . . . . 7 ⊢ (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ ran ( I ↾ (1...(𝑃 − 1)))
115	114	a1i 11	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ ran ( I ↾ (1...(𝑃 − 1))))
116		eqid 2752	. . . . . 6 ⊢ ((( 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, 3, 109, 115, 116	gsumval3 19919	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) = (seq1( · , (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))))‘(𝑃 − 1)))
118		facnn 14274	. . . . . 6 ⊢ ((𝑃 − 1) ∈ ℕ → (!‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
119	3, 118	syl 17	. . . . 5 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
120	94, 117, 119	3eqtr4d 2797	. . . 4 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) = (!‘(𝑃 − 1)))
121	120	oveq1d 7396	. . 3 ⊢ (𝑃 ∈ ℙ → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1) = ((!‘(𝑃 − 1)) − -1))
122		nnm1nn0 12508	. . . . . . 7 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
123	11, 122	syl 17	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ₀)
124	123	faccld 14283	. . . . 5 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) ∈ ℕ)
125	124	nncnd 12212	. . . 4 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) ∈ ℂ)
126		ax-1cn 11117	. . . 4 ⊢ 1 ∈ ℂ
127		subneg 11466	. . . 4 ⊢ (((!‘(𝑃 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((!‘(𝑃 − 1)) − -1) = ((!‘(𝑃 − 1)) + 1))
128	125, 126, 127	sylancl 594	. . 3 ⊢ (𝑃 ∈ ℙ → ((!‘(𝑃 − 1)) − -1) = ((!‘(𝑃 − 1)) + 1))
129	121, 128	eqtrd 2787	. 2 ⊢ (𝑃 ∈ ℙ → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1) = ((!‘(𝑃 − 1)) + 1))
130	87, 129	breqtrd 5116	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((!‘(𝑃 − 1)) + 1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1095 ∀wal 1548 = wceq 1550 ∈ wcel 2132 ∀wral 3066 {crab 3404 Vcvv 3444 ⊆ wss 3895 ⊊ wpss 3896 𝒫 cpw 4545 class class class wbr 5090 I cid 5530 dom cdm 5636 ran crn 5637 ↾ cres 5638 ∘ ccom 5640 ⟶wf 6502 –1-1→wf1 6503 –1-1-onto→wf1o 6505 ‘cfv 6506 (class class class)co 7381 supp csupp 8124 Fincfn 8912 ℂcc 11057 1c1 11060 + caddc 11062 · cmul 11064 − cmin 11400 -cneg 11401 ℕcn 12196 2c2 12258 ℕ₀cn0 12467 ℤcz 12554 ℤ_≥cuz 12825 ...cfz 13498 mod cmo 13865 seqcseq 14000 ↑cexp 14060 !cfa 14272 ∥ cdvds 16258 ℙcprime 16677 Σ_g cgsu 17441 Mndcmnd 18740 SubMndcsubmnd 18788 Cntzccntz 19327 CMndccmn 19792 mulGrpcmgp 20158 Ringcrg 20251 CRingccrg 20252 SubRingcsubrg 20587 ℂ_fldccnfld 21393

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1805 ax-4 1819 ax-5 1920 ax-6 1977 ax-7 2018 ax-8 2134 ax-9 2142 ax-10 2165 ax-11 2181 ax-12 2202 ax-ext 2724 ax-rep 5217 ax-sep 5236 ax-nul 5246 ax-pow 5312 ax-pr 5380 ax-un 7703 ax-cnex 11115 ax-resscn 11116 ax-1cn 11117 ax-icn 11118 ax-addcl 11119 ax-addrcl 11120 ax-mulcl 11121 ax-mulrcl 11122 ax-mulcom 11123 ax-addass 11124 ax-mulass 11125 ax-distr 11126 ax-i2m1 11127 ax-1ne0 11128 ax-1rid 11129 ax-rnegex 11130 ax-rrecex 11131 ax-cnre 11132 ax-pre-lttri 11133 ax-pre-lttrn 11134 ax-pre-ltadd 11135 ax-pre-mulgt0 11136 ax-pre-sup 11137 ax-addf 11138 ax-mulf 11139

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3or 1096 df-3an 1097 df-tru 1553 df-fal 1563 df-ex 1790 df-nf 1794 df-sb 2081 df-mo 2556 df-eu 2586 df-clab 2731 df-cleq 2744 df-clel 2827 df-nfc 2901 df-ne 2948 df-nel 3052 df-ral 3067 df-rex 3077 df-rmo 3357 df-reu 3358 df-rab 3405 df-v 3446 df-sbc 3736 df-csb 3844 df-dif 3898 df-un 3900 df-in 3902 df-ss 3912 df-pss 3915 df-nul 4277 df-if 4471 df-pw 4547 df-sn 4573 df-pr 4575 df-tp 4577 df-op 4579 df-uni 4856 df-int 4896 df-iun 4941 df-iin 4942 df-br 5091 df-opab 5153 df-mpt 5172 df-tr 5198 df-id 5531 df-eprel 5536 df-po 5544 df-so 5545 df-fr 5589 df-se 5590 df-we 5591 df-xp 5642 df-rel 5643 df-cnv 5644 df-co 5645 df-dm 5646 df-rn 5647 df-res 5648 df-ima 5649 df-pred 6273 df-ord 6334 df-on 6335 df-lim 6336 df-suc 6337 df-iota 6462 df-fun 6508 df-fn 6509 df-f 6510 df-f1 6511 df-fo 6512 df-f1o 6513 df-fv 6514 df-isom 6515 df-riota 7338 df-ov 7384 df-oprab 7385 df-mpo 7386 df-of 7645 df-om 7832 df-1st 7955 df-2nd 7956 df-supp 8125 df-frecs 8246 df-wrecs 8277 df-recs 8326 df-rdg 8365 df-1o 8421 df-2o 8422 df-oadd 8425 df-er 8662 df-en 8913 df-dom 8914 df-sdom 8915 df-fin 8916 df-fsupp 9294 df-sup 9374 df-inf 9375 df-oi 9444 df-dju 9845 df-card 9883 df-pnf 11204 df-mnf 11205 df-xr 11206 df-ltxr 11207 df-le 11208 df-sub 11402 df-neg 11403 df-div 11831 df-nn 12197 df-2 12266 df-3 12267 df-4 12268 df-5 12269 df-6 12270 df-7 12271 df-8 12272 df-9 12273 df-n0 12468 df-xnn0 12541 df-z 12555 df-dec 12675 df-uz 12826 df-rp 12980 df-fz 13499 df-fzo 13646 df-fl 13788 df-mod 13866 df-seq 14001 df-exp 14061 df-fac 14273 df-hash 14330 df-cj 15098 df-re 15099 df-im 15100 df-sqrt 15234 df-abs 15235 df-dvds 16259 df-gcd 16501 df-prm 16678 df-phi 16773 df-struct 17155 df-sets 17172 df-slot 17190 df-ndx 17202 df-base 17218 df-ress 17239 df-plusg 17271 df-mulr 17272 df-starv 17273 df-tset 17277 df-ple 17278 df-ds 17280 df-unif 17281 df-0g 17442 df-gsum 17443 df-mre 17586 df-mrc 17587 df-acs 17589 df-mgm 18646 df-sgrp 18725 df-mnd 18741 df-submnd 18790 df-grp 18950 df-minusg 18951 df-mulg 19082 df-subg 19137 df-cntz 19329 df-cmn 19794 df-abl 19795 df-mgp 20159 df-rng 20171 df-ur 20200 df-ring 20253 df-cring 20254 df-subrng 20564 df-subrg 20588 df-cnfld 21394

This theorem is referenced by: wilth 27101

W3C validator