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 27111

Description: Lemma for wilth 27112. Here we round out the argument of wilthlem2 27110 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 16713	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
2		uz2m1nn 12921	. . . . . . . 8 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
3	1, 2	syl 17	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ)
4		nnuz 12875	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
5	3, 4	eleqtrdi 2871	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ (ℤ_≥‘1))
6		eluzfz2 13534	. . . . . 6 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘1) → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
7	5, 6	syl 17	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
8		simpl 486	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℙ)
9		elfzelz 13526	. . . . . . . . 9 ⊢ (𝑦 ∈ (1...(𝑃 − 1)) → 𝑦 ∈ ℤ)
10	9	adantl 485	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑦 ∈ ℤ)
11		prmnn 16691	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
12		fzm1ndvds 16339	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑦)
13	11, 12	sylan 589	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑦)
14		eqid 2761	. . . . . . . . 9 ⊢ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑦↑(𝑃 − 2)) mod 𝑃)
15	14	prmdiv 16803	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑦) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑦 · ((𝑦↑(𝑃 − 2)) mod 𝑃)) − 1)))
16	8, 10, 13, 15	syl3anc 1389	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑦 · ((𝑦↑(𝑃 − 2)) mod 𝑃)) − 1)))
17	16	simpld 498	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
18	17	ralrimiva 3153	. . . . 5 ⊢ (𝑃 ∈ ℙ → ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
19		ovex 7425	. . . . . . 7 ⊢ (1...(𝑃 − 1)) ∈ V
20	19	pwid 4577	. . . . . 6 ⊢ (1...(𝑃 − 1)) ∈ 𝒫 (1...(𝑃 − 1))
21		eleq2 2850	. . . . . . . 8 ⊢ (𝑥 = (1...(𝑃 − 1)) → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ (1...(𝑃 − 1))))
22		eleq2 2850	. . . . . . . . 9 ⊢ (𝑥 = (1...(𝑃 − 1)) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
23	22	raleqbi1dv 3329	. . . . . . . 8 ⊢ (𝑥 = (1...(𝑃 − 1)) → (∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
24	21, 23	anbi12d 641	. . . . . . 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 3653	. . . . . 6 ⊢ ((1...(𝑃 − 1)) ∈ 𝐴 ↔ ((1...(𝑃 − 1)) ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ (1...(𝑃 − 1)) ∧ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))))
27	20, 26	mpbiran 719	. . . . 5 ⊢ ((1...(𝑃 − 1)) ∈ 𝐴 ↔ ((𝑃 − 1) ∈ (1...(𝑃 − 1)) ∧ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
28	7, 18, 27	sylanbrc 592	. . . 4 ⊢ (𝑃 ∈ ℙ → (1...(𝑃 − 1)) ∈ 𝐴)
29		fzfi 13982	. . . . 5 ⊢ (1...(𝑃 − 1)) ∈ Fin
30		eleq1 2849	. . . . . . . 8 ⊢ (𝑠 = 𝑡 → (𝑠 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))
31		reseq2 5958	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → ( I ↾ 𝑠) = ( I ↾ 𝑡))
32	31	oveq2d 7408	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (𝑇 Σ_g ( I ↾ 𝑠)) = (𝑇 Σ_g ( I ↾ 𝑡)))
33	32	oveq1d 7407	. . . . . . . . 9 ⊢ (𝑠 = 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃))
34	33	eqeq1d 2763	. . . . . . . 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 2849	. . . . . . . 8 ⊢ (𝑠 = (1...(𝑃 − 1)) → (𝑠 ∈ 𝐴 ↔ (1...(𝑃 − 1)) ∈ 𝐴))
38		reseq2 5958	. . . . . . . . . . 11 ⊢ (𝑠 = (1...(𝑃 − 1)) → ( I ↾ 𝑠) = ( I ↾ (1...(𝑃 − 1))))
39	38	oveq2d 7408	. . . . . . . . . 10 ⊢ (𝑠 = (1...(𝑃 − 1)) → (𝑇 Σ_g ( I ↾ 𝑠)) = (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))))
40	39	oveq1d 7407	. . . . . . . . 9 ⊢ (𝑠 = (1...(𝑃 − 1)) → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃))
41	40	eqeq1d 2763	. . . . . . . 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 1935	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → (∀𝑠(𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → ∀𝑠(𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
49		df-ral 3076	. . . . . . . . 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 1148	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → 𝑃 ∈ ℙ)
53		simp3 1150	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ 𝐴)
54		simp2 1149	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
55	51, 25, 52, 53, 54	wilthlem2 27110	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))
56	55	3exp 1131	. . . . . . . 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 9223	. . . . 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 21429	. . . . . 6 ⊢ 1 = (1_r‘ℂ_fld)
63	51, 62	ringidval 20212	. . . . 5 ⊢ 1 = (0_g‘𝑇)
64		cncrng 21425	. . . . . 6 ⊢ ℂ_fld ∈ CRing
65	51	crngmgp 20270	. . . . . 6 ⊢ (ℂ_fld ∈ CRing → 𝑇 ∈ CMnd)
66	64, 65	mp1i 13	. . . . 5 ⊢ (𝑃 ∈ ℙ → 𝑇 ∈ CMnd)
67	29	a1i 11	. . . . 5 ⊢ (𝑃 ∈ ℙ → (1...(𝑃 − 1)) ∈ Fin)
68		zsubrg 21452	. . . . . 6 ⊢ ℤ ∈ (SubRing‘ℂ_fld)
69	51	subrgsubm 20614	. . . . . 6 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubMnd‘𝑇))
70	68, 69	mp1i 13	. . . . 5 ⊢ (𝑃 ∈ ℙ → ℤ ∈ (SubMnd‘𝑇))
71		f1oi 6841	. . . . . . . 8 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))–1-1-onto→(1...(𝑃 − 1))
72		f1of 6802	. . . . . . . 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 13528	. . . . . . 7 ⊢ (1...(𝑃 − 1)) ⊆ ℤ
75		fss 6704	. . . . . . 7 ⊢ ((( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶(1...(𝑃 − 1)) ∧ (1...(𝑃 − 1)) ⊆ ℤ) → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ)
76	73, 74, 75	mp2an 702	. . . . . 6 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ
77	76	a1i 11	. . . . 5 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ)
78		1ex 11173	. . . . . . 7 ⊢ 1 ∈ V
79	78	a1i 11	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 1 ∈ V)
80	77, 67, 79	fdmfifsupp 9318	. . . . 5 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))) finSupp 1)
81	63, 66, 67, 70, 77, 80	gsumsubmcl 19942	. . . 4 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) ∈ ℤ)
82		1z 12598	. . . . 5 ⊢ 1 ∈ ℤ
83		znegcl 12603	. . . . 5 ⊢ (1 ∈ ℤ → -1 ∈ ℤ)
84	82, 83	mp1i 13	. . . 4 ⊢ (𝑃 ∈ ℙ → -1 ∈ ℤ)
85		moddvds 16280	. . . 4 ⊢ ((𝑃 ∈ ℕ ∧ (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) ∈ ℤ ∧ -1 ∈ ℤ) → (((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1)))
86	11, 81, 84, 85	syl3anc 1389	. . 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 6734	. . . . . . . . . 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 6864	. . . . . . . 8 ⊢ ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = (( I ↾ (1...(𝑃 − 1)))‘𝑘)
91		fvres 6882	. . . . . . . 8 ⊢ (𝑘 ∈ (1...(𝑃 − 1)) → (( I ↾ (1...(𝑃 − 1)))‘𝑘) = ( I ‘𝑘))
92	90, 91	eqtrid 2808	. . . . . . 7 ⊢ (𝑘 ∈ (1...(𝑃 − 1)) → ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = ( I ‘𝑘))
93	92	adantl 485	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑃 − 1))) → ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = ( I ‘𝑘))
94	5, 93	seqfveq 14036	. . . . 5 ⊢ (𝑃 ∈ ℙ → (seq1( · , (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))))‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
95		cnfldbas 21408	. . . . . . 7 ⊢ ℂ = (Base‘ℂ_fld)
96	51, 95	mgpbas 20174	. . . . . 6 ⊢ ℂ = (Base‘𝑇)
97		cnfldmul 21412	. . . . . . 7 ⊢ · = (._r‘ℂ_fld)
98	51, 97	mgpplusg 20173	. . . . . 6 ⊢ · = (+_g‘𝑇)
99		eqid 2761	. . . . . 6 ⊢ (Cntz‘𝑇) = (Cntz‘𝑇)
100		cnring 21426	. . . . . . 7 ⊢ ℂ_fld ∈ Ring
101	51	ringmgp 20268	. . . . . . 7 ⊢ (ℂ_fld ∈ Ring → 𝑇 ∈ Mnd)
102	100, 101	mp1i 13	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑇 ∈ Mnd)
103		zsscn 12573	. . . . . . . 8 ⊢ ℤ ⊆ ℂ
104		fss 6704	. . . . . . . 8 ⊢ ((( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ ∧ ℤ ⊆ ℂ) → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ)
105	76, 103, 104	mp2an 702	. . . . . . 7 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ
106	105	a1i 11	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ)
107	96, 99, 66, 106	cntzcmnf 19868	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ran ( I ↾ (1...(𝑃 − 1))) ⊆ ((Cntz‘𝑇)‘ran ( I ↾ (1...(𝑃 − 1)))))
108		f1of1 6801	. . . . . . 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 8152	. . . . . . . . 9 ⊢ (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ dom ( I ↾ (1...(𝑃 − 1)))
111		dmresi 6038	. . . . . . . . 9 ⊢ dom ( I ↾ (1...(𝑃 − 1))) = (1...(𝑃 − 1))
112	110, 111	sseqtri 3984	. . . . . . . 8 ⊢ (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ (1...(𝑃 − 1))
113		rnresi 6061	. . . . . . . 8 ⊢ ran ( I ↾ (1...(𝑃 − 1))) = (1...(𝑃 − 1))
114	112, 113	sseqtrri 3985	. . . . . . 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 2761	. . . . . 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 19930	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) = (seq1( · , (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))))‘(𝑃 − 1)))
118		facnn 14285	. . . . . 6 ⊢ ((𝑃 − 1) ∈ ℕ → (!‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
119	3, 118	syl 17	. . . . 5 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
120	94, 117, 119	3eqtr4d 2806	. . . 4 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) = (!‘(𝑃 − 1)))
121	120	oveq1d 7407	. . 3 ⊢ (𝑃 ∈ ℙ → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1) = ((!‘(𝑃 − 1)) − -1))
122		nnm1nn0 12519	. . . . . . 7 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
123	11, 122	syl 17	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ₀)
124	123	faccld 14294	. . . . 5 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) ∈ ℕ)
125	124	nncnd 12223	. . . 4 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) ∈ ℂ)
126		ax-1cn 11128	. . . 4 ⊢ 1 ∈ ℂ
127		subneg 11477	. . . 4 ⊢ (((!‘(𝑃 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((!‘(𝑃 − 1)) − -1) = ((!‘(𝑃 − 1)) + 1))
128	125, 126, 127	sylancl 595	. . 3 ⊢ (𝑃 ∈ ℙ → ((!‘(𝑃 − 1)) − -1) = ((!‘(𝑃 − 1)) + 1))
129	121, 128	eqtrd 2796	. 2 ⊢ (𝑃 ∈ ℙ → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1) = ((!‘(𝑃 − 1)) + 1))
130	87, 129	breqtrd 5125	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((!‘(𝑃 − 1)) + 1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 ∀wal 1557 = wceq 1559 ∈ wcel 2141 ∀wral 3075 {crab 3413 Vcvv 3453 ⊆ wss 3904 ⊊ wpss 3905 𝒫 cpw 4554 class class class wbr 5099 I cid 5539 dom cdm 5645 ran crn 5646 ↾ cres 5647 ∘ ccom 5649 ⟶wf 6513 –1-1→wf1 6514 –1-1-onto→wf1o 6516 ‘cfv 6517 (class class class)co 7392 supp csupp 8135 Fincfn 8923 ℂcc 11068 1c1 11071 + caddc 11073 · cmul 11075 − cmin 11411 -cneg 11412 ℕcn 12207 2c2 12269 ℕ₀cn0 12478 ℤcz 12565 ℤ_≥cuz 12836 ...cfz 13509 mod cmo 13876 seqcseq 14011 ↑cexp 14071 !cfa 14283 ∥ cdvds 16269 ℙcprime 16688 Σ_g cgsu 17452 Mndcmnd 18751 SubMndcsubmnd 18799 Cntzccntz 19338 CMndccmn 19803 mulGrpcmgp 20169 Ringcrg 20262 CRingccrg 20263 SubRingcsubrg 20598 ℂ_fldccnfld 21404

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5226 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147 ax-pre-sup 11148 ax-addf 11149 ax-mulf 11150

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-tp 4586 df-op 4588 df-uni 4865 df-int 4905 df-iun 4950 df-iin 4951 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-se 5599 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-isom 6526 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-of 7656 df-om 7843 df-1st 7966 df-2nd 7967 df-supp 8136 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-1o 8432 df-2o 8433 df-oadd 8436 df-er 8673 df-en 8924 df-dom 8925 df-sdom 8926 df-fin 8927 df-fsupp 9305 df-sup 9385 df-inf 9386 df-oi 9455 df-dju 9856 df-card 9894 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-div 11842 df-nn 12208 df-2 12277 df-3 12278 df-4 12279 df-5 12280 df-6 12281 df-7 12282 df-8 12283 df-9 12284 df-n0 12479 df-xnn0 12552 df-z 12566 df-dec 12686 df-uz 12837 df-rp 12991 df-fz 13510 df-fzo 13657 df-fl 13799 df-mod 13877 df-seq 14012 df-exp 14072 df-fac 14284 df-hash 14341 df-cj 15109 df-re 15110 df-im 15111 df-sqrt 15245 df-abs 15246 df-dvds 16270 df-gcd 16512 df-prm 16689 df-phi 16784 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17250 df-plusg 17282 df-mulr 17283 df-starv 17284 df-tset 17288 df-ple 17289 df-ds 17291 df-unif 17292 df-0g 17453 df-gsum 17454 df-mre 17597 df-mrc 17598 df-acs 17600 df-mgm 18657 df-sgrp 18736 df-mnd 18752 df-submnd 18801 df-grp 18961 df-minusg 18962 df-mulg 19093 df-subg 19148 df-cntz 19340 df-cmn 19805 df-abl 19806 df-mgp 20170 df-rng 20182 df-ur 20211 df-ring 20264 df-cring 20265 df-subrng 20575 df-subrg 20599 df-cnfld 21405

This theorem is referenced by: wilth 27112

W3C validator