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 27058

Description: Lemma for wilth 27059. Here we round out the argument of wilthlem2 27057 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 16663	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
2		uz2m1nn 12871	. . . . . . . 8 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
3	1, 2	syl 17	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ)
4		nnuz 12825	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
5	3, 4	eleqtrdi 2850	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ (ℤ_≥‘1))
6		eluzfz2 13484	. . . . . 6 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘1) → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
7	5, 6	syl 17	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
8		simpl 483	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℙ)
9		elfzelz 13476	. . . . . . . . 9 ⊢ (𝑦 ∈ (1...(𝑃 − 1)) → 𝑦 ∈ ℤ)
10	9	adantl 482	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑦 ∈ ℤ)
11		prmnn 16641	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
12		fzm1ndvds 16289	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑦)
13	11, 12	sylan 586	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑦)
14		eqid 2740	. . . . . . . . 9 ⊢ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑦↑(𝑃 − 2)) mod 𝑃)
15	14	prmdiv 16753	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑦) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑦 · ((𝑦↑(𝑃 − 2)) mod 𝑃)) − 1)))
16	8, 10, 13, 15	syl3anc 1379	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑦 · ((𝑦↑(𝑃 − 2)) mod 𝑃)) − 1)))
17	16	simpld 495	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
18	17	ralrimiva 3132	. . . . 5 ⊢ (𝑃 ∈ ℙ → ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
19		ovex 7396	. . . . . . 7 ⊢ (1...(𝑃 − 1)) ∈ V
20	19	pwid 4558	. . . . . 6 ⊢ (1...(𝑃 − 1)) ∈ 𝒫 (1...(𝑃 − 1))
21		eleq2 2829	. . . . . . . 8 ⊢ (𝑥 = (1...(𝑃 − 1)) → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ (1...(𝑃 − 1))))
22		eleq2 2829	. . . . . . . . 9 ⊢ (𝑥 = (1...(𝑃 − 1)) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
23	22	raleqbi1dv 3308	. . . . . . . 8 ⊢ (𝑥 = (1...(𝑃 − 1)) → (∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
24	21, 23	anbi12d 638	. . . . . . 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 3639	. . . . . 6 ⊢ ((1...(𝑃 − 1)) ∈ 𝐴 ↔ ((1...(𝑃 − 1)) ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ (1...(𝑃 − 1)) ∧ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))))
27	20, 26	mpbiran 715	. . . . 5 ⊢ ((1...(𝑃 − 1)) ∈ 𝐴 ↔ ((𝑃 − 1) ∈ (1...(𝑃 − 1)) ∧ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
28	7, 18, 27	sylanbrc 589	. . . 4 ⊢ (𝑃 ∈ ℙ → (1...(𝑃 − 1)) ∈ 𝐴)
29		fzfi 13932	. . . . 5 ⊢ (1...(𝑃 − 1)) ∈ Fin
30		eleq1 2828	. . . . . . . 8 ⊢ (𝑠 = 𝑡 → (𝑠 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))
31		reseq2 5933	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → ( I ↾ 𝑠) = ( I ↾ 𝑡))
32	31	oveq2d 7379	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (𝑇 Σ_g ( I ↾ 𝑠)) = (𝑇 Σ_g ( I ↾ 𝑡)))
33	32	oveq1d 7378	. . . . . . . . 9 ⊢ (𝑠 = 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃))
34	33	eqeq1d 2742	. . . . . . . 8 ⊢ (𝑠 = 𝑡 → (((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃)))
35	30, 34	imbi12d 345	. . . . . . 7 ⊢ (𝑠 = 𝑡 → ((𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ (𝑡 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))))
36	35	imbi2d 341	. . . . . 6 ⊢ (𝑠 = 𝑡 → ((𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ↔ (𝑃 ∈ ℙ → (𝑡 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃)))))
37		eleq1 2828	. . . . . . . 8 ⊢ (𝑠 = (1...(𝑃 − 1)) → (𝑠 ∈ 𝐴 ↔ (1...(𝑃 − 1)) ∈ 𝐴))
38		reseq2 5933	. . . . . . . . . . 11 ⊢ (𝑠 = (1...(𝑃 − 1)) → ( I ↾ 𝑠) = ( I ↾ (1...(𝑃 − 1))))
39	38	oveq2d 7379	. . . . . . . . . 10 ⊢ (𝑠 = (1...(𝑃 − 1)) → (𝑇 Σ_g ( I ↾ 𝑠)) = (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))))
40	39	oveq1d 7378	. . . . . . . . 9 ⊢ (𝑠 = (1...(𝑃 − 1)) → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃))
41	40	eqeq1d 2742	. . . . . . . 8 ⊢ (𝑠 = (1...(𝑃 − 1)) → (((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃)))
42	37, 41	imbi12d 345	. . . . . . 7 ⊢ (𝑠 = (1...(𝑃 − 1)) → ((𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((1...(𝑃 − 1)) ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃))))
43	42	imbi2d 341	. . . . . 6 ⊢ (𝑠 = (1...(𝑃 − 1)) → ((𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ↔ (𝑃 ∈ ℙ → ((1...(𝑃 − 1)) ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃)))))
44		bi2.04 388	. . . . . . . . . . 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 243	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → ((𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → (𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
48	47	alimdv 1923	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → (∀𝑠(𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → ∀𝑠(𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
49		df-ral 3055	. . . . . . . . 9 ⊢ (∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ∀𝑠(𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))))
50	48, 49	imbitrrdi 253	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → (∀𝑠(𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))))
51		wilthlem.t	. . . . . . . . . 10 ⊢ 𝑇 = (mulGrp‘ℂ_fld)
52		simp1 1142	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → 𝑃 ∈ ℙ)
53		simp3 1144	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ 𝐴)
54		simp2 1143	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
55	51, 25, 52, 53, 54	wilthlem2 27057	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))
56	55	3exp 1125	. . . . . . . 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 9190	. . . . 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 21379	. . . . . 6 ⊢ 1 = (1_r‘ℂ_fld)
63	51, 62	ringidval 20162	. . . . 5 ⊢ 1 = (0_g‘𝑇)
64		cncrng 21375	. . . . . 6 ⊢ ℂ_fld ∈ CRing
65	51	crngmgp 20220	. . . . . 6 ⊢ (ℂ_fld ∈ CRing → 𝑇 ∈ CMnd)
66	64, 65	mp1i 13	. . . . 5 ⊢ (𝑃 ∈ ℙ → 𝑇 ∈ CMnd)
67	29	a1i 11	. . . . 5 ⊢ (𝑃 ∈ ℙ → (1...(𝑃 − 1)) ∈ Fin)
68		zsubrg 21402	. . . . . 6 ⊢ ℤ ∈ (SubRing‘ℂ_fld)
69	51	subrgsubm 20564	. . . . . 6 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubMnd‘𝑇))
70	68, 69	mp1i 13	. . . . 5 ⊢ (𝑃 ∈ ℙ → ℤ ∈ (SubMnd‘𝑇))
71		f1oi 6812	. . . . . . . 8 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))–1-1-onto→(1...(𝑃 − 1))
72		f1of 6774	. . . . . . . 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 13478	. . . . . . 7 ⊢ (1...(𝑃 − 1)) ⊆ ℤ
75		fss 6678	. . . . . . 7 ⊢ ((( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶(1...(𝑃 − 1)) ∧ (1...(𝑃 − 1)) ⊆ ℤ) → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ)
76	73, 74, 75	mp2an 698	. . . . . 6 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ
77	76	a1i 11	. . . . 5 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ)
78		1ex 11138	. . . . . . 7 ⊢ 1 ∈ V
79	78	a1i 11	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 1 ∈ V)
80	77, 67, 79	fdmfifsupp 9285	. . . . 5 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))) finSupp 1)
81	63, 66, 67, 70, 77, 80	gsumsubmcl 19892	. . . 4 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) ∈ ℤ)
82		1z 12555	. . . . 5 ⊢ 1 ∈ ℤ
83		znegcl 12560	. . . . 5 ⊢ (1 ∈ ℤ → -1 ∈ ℤ)
84	82, 83	mp1i 13	. . . 4 ⊢ (𝑃 ∈ ℙ → -1 ∈ ℤ)
85		moddvds 16230	. . . 4 ⊢ ((𝑃 ∈ ℕ ∧ (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) ∈ ℤ ∧ -1 ∈ ℤ) → (((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1)))
86	11, 81, 84, 85	syl3anc 1379	. . 3 ⊢ (𝑃 ∈ ℙ → (((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1)))
87	61, 86	mpbid 233	. 2 ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1))
88		fcoi1 6708	. . . . . . . . . 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 6835	. . . . . . . 8 ⊢ ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = (( I ↾ (1...(𝑃 − 1)))‘𝑘)
91		fvres 6853	. . . . . . . 8 ⊢ (𝑘 ∈ (1...(𝑃 − 1)) → (( I ↾ (1...(𝑃 − 1)))‘𝑘) = ( I ‘𝑘))
92	90, 91	eqtrid 2787	. . . . . . 7 ⊢ (𝑘 ∈ (1...(𝑃 − 1)) → ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = ( I ‘𝑘))
93	92	adantl 482	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑃 − 1))) → ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = ( I ‘𝑘))
94	5, 93	seqfveq 13986	. . . . 5 ⊢ (𝑃 ∈ ℙ → (seq1( · , (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))))‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
95		cnfldbas 21358	. . . . . . 7 ⊢ ℂ = (Base‘ℂ_fld)
96	51, 95	mgpbas 20124	. . . . . 6 ⊢ ℂ = (Base‘𝑇)
97		cnfldmul 21362	. . . . . . 7 ⊢ · = (._r‘ℂ_fld)
98	51, 97	mgpplusg 20123	. . . . . 6 ⊢ · = (+_g‘𝑇)
99		eqid 2740	. . . . . 6 ⊢ (Cntz‘𝑇) = (Cntz‘𝑇)
100		cnring 21376	. . . . . . 7 ⊢ ℂ_fld ∈ Ring
101	51	ringmgp 20218	. . . . . . 7 ⊢ (ℂ_fld ∈ Ring → 𝑇 ∈ Mnd)
102	100, 101	mp1i 13	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑇 ∈ Mnd)
103		zsscn 12530	. . . . . . . 8 ⊢ ℤ ⊆ ℂ
104		fss 6678	. . . . . . . 8 ⊢ ((( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ ∧ ℤ ⊆ ℂ) → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ)
105	76, 103, 104	mp2an 698	. . . . . . 7 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ
106	105	a1i 11	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ)
107	96, 99, 66, 106	cntzcmnf 19818	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ran ( I ↾ (1...(𝑃 − 1))) ⊆ ((Cntz‘𝑇)‘ran ( I ↾ (1...(𝑃 − 1)))))
108		f1of1 6773	. . . . . . 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 8124	. . . . . . . . 9 ⊢ (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ dom ( I ↾ (1...(𝑃 − 1)))
111		dmresi 6011	. . . . . . . . 9 ⊢ dom ( I ↾ (1...(𝑃 − 1))) = (1...(𝑃 − 1))
112	110, 111	sseqtri 3970	. . . . . . . 8 ⊢ (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ (1...(𝑃 − 1))
113		rnresi 6034	. . . . . . . 8 ⊢ ran ( I ↾ (1...(𝑃 − 1))) = (1...(𝑃 − 1))
114	112, 113	sseqtrri 3971	. . . . . . 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 2740	. . . . . 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 19880	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) = (seq1( · , (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))))‘(𝑃 − 1)))
118		facnn 14235	. . . . . 6 ⊢ ((𝑃 − 1) ∈ ℕ → (!‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
119	3, 118	syl 17	. . . . 5 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
120	94, 117, 119	3eqtr4d 2785	. . . 4 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) = (!‘(𝑃 − 1)))
121	120	oveq1d 7378	. . 3 ⊢ (𝑃 ∈ ℙ → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1) = ((!‘(𝑃 − 1)) − -1))
122		nnm1nn0 12476	. . . . . . 7 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
123	11, 122	syl 17	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ₀)
124	123	faccld 14244	. . . . 5 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) ∈ ℕ)
125	124	nncnd 12188	. . . 4 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) ∈ ℂ)
126		ax-1cn 11094	. . . 4 ⊢ 1 ∈ ℂ
127		subneg 11441	. . . 4 ⊢ (((!‘(𝑃 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((!‘(𝑃 − 1)) − -1) = ((!‘(𝑃 − 1)) + 1))
128	125, 126, 127	sylancl 592	. . 3 ⊢ (𝑃 ∈ ℙ → ((!‘(𝑃 − 1)) − -1) = ((!‘(𝑃 − 1)) + 1))
129	121, 128	eqtrd 2775	. 2 ⊢ (𝑃 ∈ ℙ → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1) = ((!‘(𝑃 − 1)) + 1))
130	87, 129	breqtrd 5105	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((!‘(𝑃 − 1)) + 1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 ∀wal 1545 = wceq 1547 ∈ wcel 2119 ∀wral 3054 {crab 3392 Vcvv 3432 ⊆ wss 3890 ⊊ wpss 3891 𝒫 cpw 4536 class class class wbr 5079 I cid 5519 dom cdm 5625 ran crn 5626 ↾ cres 5627 ∘ ccom 5629 ⟶wf 6488 –1-1→wf1 6489 –1-1-onto→wf1o 6491 ‘cfv 6492 (class class class)co 7363 supp csupp 8107 Fincfn 8890 ℂcc 11034 1c1 11037 + caddc 11039 · cmul 11041 − cmin 11375 -cneg 11376 ℕcn 12172 2c2 12234 ℕ₀cn0 12435 ℤcz 12522 ℤ_≥cuz 12786 ...cfz 13459 mod cmo 13826 seqcseq 13961 ↑cexp 14021 !cfa 14233 ∥ cdvds 16219 ℙcprime 16638 Σ_g cgsu 17401 Mndcmnd 18700 SubMndcsubmnd 18748 Cntzccntz 19288 CMndccmn 19753 mulGrpcmgp 20119 Ringcrg 20212 CRingccrg 20213 SubRingcsubrg 20548 ℂ_fldccnfld 21354

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685 ax-cnex 11092 ax-resscn 11093 ax-1cn 11094 ax-icn 11095 ax-addcl 11096 ax-addrcl 11097 ax-mulcl 11098 ax-mulrcl 11099 ax-mulcom 11100 ax-addass 11101 ax-mulass 11102 ax-distr 11103 ax-i2m1 11104 ax-1ne0 11105 ax-1rid 11106 ax-rnegex 11107 ax-rrecex 11108 ax-cnre 11109 ax-pre-lttri 11110 ax-pre-lttrn 11111 ax-pre-ltadd 11112 ax-pre-mulgt0 11113 ax-pre-sup 11114 ax-addf 11115 ax-mulf 11116

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-nel 3040 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4846 df-int 4885 df-iun 4930 df-iin 4931 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-of 7627 df-om 7814 df-1st 7938 df-2nd 7939 df-supp 8108 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-rdg 8346 df-1o 8402 df-2o 8403 df-oadd 8406 df-er 8640 df-en 8891 df-dom 8892 df-sdom 8893 df-fin 8894 df-fsupp 9272 df-sup 9352 df-inf 9353 df-oi 9422 df-dju 9823 df-card 9861 df-pnf 11179 df-mnf 11180 df-xr 11181 df-ltxr 11182 df-le 11183 df-sub 11377 df-neg 11378 df-div 11806 df-nn 12173 df-2 12242 df-3 12243 df-4 12244 df-5 12245 df-6 12246 df-7 12247 df-8 12248 df-9 12249 df-n0 12436 df-xnn0 12509 df-z 12523 df-dec 12643 df-uz 12787 df-rp 12941 df-fz 13460 df-fzo 13607 df-fl 13749 df-mod 13827 df-seq 13962 df-exp 14022 df-fac 14234 df-hash 14291 df-cj 15059 df-re 15060 df-im 15061 df-sqrt 15195 df-abs 15196 df-dvds 16220 df-gcd 16462 df-prm 16639 df-phi 16734 df-struct 17115 df-sets 17132 df-slot 17150 df-ndx 17162 df-base 17178 df-ress 17199 df-plusg 17231 df-mulr 17232 df-starv 17233 df-tset 17237 df-ple 17238 df-ds 17240 df-unif 17241 df-0g 17402 df-gsum 17403 df-mre 17546 df-mrc 17547 df-acs 17549 df-mgm 18606 df-sgrp 18685 df-mnd 18701 df-submnd 18750 df-grp 18910 df-minusg 18911 df-mulg 19042 df-subg 19097 df-cntz 19290 df-cmn 19755 df-abl 19756 df-mgp 20120 df-rng 20132 df-ur 20161 df-ring 20214 df-cring 20215 df-subrng 20525 df-subrg 20549 df-cnfld 21355

This theorem is referenced by: wilth 27059

W3C validator