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 27005

Description: Lemma for wilth 27006. Here we round out the argument of wilthlem2 27004 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 16604	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ_≥‘2))
2		uz2m1nn 12818	. . . . . . . 8 ⊢ (𝑃 ∈ (ℤ_≥‘2) → (𝑃 − 1) ∈ ℕ)
3	1, 2	syl 17	. . . . . . 7 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ)
4		nnuz 12772	. . . . . . 7 ⊢ ℕ = (ℤ_≥‘1)
5	3, 4	eleqtrdi 2841	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ (ℤ_≥‘1))
6		eluzfz2 13429	. . . . . 6 ⊢ ((𝑃 − 1) ∈ (ℤ_≥‘1) → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
7	5, 6	syl 17	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ (1...(𝑃 − 1)))
8		simpl 482	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑃 ∈ ℙ)
9		elfzelz 13421	. . . . . . . . 9 ⊢ (𝑦 ∈ (1...(𝑃 − 1)) → 𝑦 ∈ ℤ)
10	9	adantl 481	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑦 ∈ ℤ)
11		prmnn 16582	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
12		fzm1ndvds 16230	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℕ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑦)
13	11, 12	sylan 580	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑦)
14		eqid 2731	. . . . . . . . 9 ⊢ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑦↑(𝑃 − 2)) mod 𝑃)
15	14	prmdiv 16693	. . . . . . . 8 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑦) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑦 · ((𝑦↑(𝑃 − 2)) mod 𝑃)) − 1)))
16	8, 10, 13, 15	syl3anc 1373	. . . . . . 7 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑦 · ((𝑦↑(𝑃 − 2)) mod 𝑃)) − 1)))
17	16	simpld 494	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
18	17	ralrimiva 3124	. . . . 5 ⊢ (𝑃 ∈ ℙ → ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))
19		ovex 7379	. . . . . . 7 ⊢ (1...(𝑃 − 1)) ∈ V
20	19	pwid 4572	. . . . . 6 ⊢ (1...(𝑃 − 1)) ∈ 𝒫 (1...(𝑃 − 1))
21		eleq2 2820	. . . . . . . 8 ⊢ (𝑥 = (1...(𝑃 − 1)) → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ (1...(𝑃 − 1))))
22		eleq2 2820	. . . . . . . . 9 ⊢ (𝑥 = (1...(𝑃 − 1)) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
23	22	raleqbi1dv 3304	. . . . . . . 8 ⊢ (𝑥 = (1...(𝑃 − 1)) → (∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
24	21, 23	anbi12d 632	. . . . . . 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 3650	. . . . . 6 ⊢ ((1...(𝑃 − 1)) ∈ 𝐴 ↔ ((1...(𝑃 − 1)) ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ (1...(𝑃 − 1)) ∧ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)))))
27	20, 26	mpbiran 709	. . . . 5 ⊢ ((1...(𝑃 − 1)) ∈ 𝐴 ↔ ((𝑃 − 1) ∈ (1...(𝑃 − 1)) ∧ ∀𝑦 ∈ (1...(𝑃 − 1))((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))))
28	7, 18, 27	sylanbrc 583	. . . 4 ⊢ (𝑃 ∈ ℙ → (1...(𝑃 − 1)) ∈ 𝐴)
29		fzfi 13876	. . . . 5 ⊢ (1...(𝑃 − 1)) ∈ Fin
30		eleq1 2819	. . . . . . . 8 ⊢ (𝑠 = 𝑡 → (𝑠 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴))
31		reseq2 5923	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑡 → ( I ↾ 𝑠) = ( I ↾ 𝑡))
32	31	oveq2d 7362	. . . . . . . . . 10 ⊢ (𝑠 = 𝑡 → (𝑇 Σ_g ( I ↾ 𝑠)) = (𝑇 Σ_g ( I ↾ 𝑡)))
33	32	oveq1d 7361	. . . . . . . . 9 ⊢ (𝑠 = 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃))
34	33	eqeq1d 2733	. . . . . . . 8 ⊢ (𝑠 = 𝑡 → (((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃)))
35	30, 34	imbi12d 344	. . . . . . 7 ⊢ (𝑠 = 𝑡 → ((𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ (𝑡 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))))
36	35	imbi2d 340	. . . . . 6 ⊢ (𝑠 = 𝑡 → ((𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ↔ (𝑃 ∈ ℙ → (𝑡 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃)))))
37		eleq1 2819	. . . . . . . 8 ⊢ (𝑠 = (1...(𝑃 − 1)) → (𝑠 ∈ 𝐴 ↔ (1...(𝑃 − 1)) ∈ 𝐴))
38		reseq2 5923	. . . . . . . . . . 11 ⊢ (𝑠 = (1...(𝑃 − 1)) → ( I ↾ 𝑠) = ( I ↾ (1...(𝑃 − 1))))
39	38	oveq2d 7362	. . . . . . . . . 10 ⊢ (𝑠 = (1...(𝑃 − 1)) → (𝑇 Σ_g ( I ↾ 𝑠)) = (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))))
40	39	oveq1d 7361	. . . . . . . . 9 ⊢ (𝑠 = (1...(𝑃 − 1)) → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃))
41	40	eqeq1d 2733	. . . . . . . 8 ⊢ (𝑠 = (1...(𝑃 − 1)) → (((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃)))
42	37, 41	imbi12d 344	. . . . . . 7 ⊢ (𝑠 = (1...(𝑃 − 1)) → ((𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((1...(𝑃 − 1)) ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃))))
43	42	imbi2d 340	. . . . . 6 ⊢ (𝑠 = (1...(𝑃 − 1)) → ((𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))) ↔ (𝑃 ∈ ℙ → ((1...(𝑃 − 1)) ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃)))))
44		bi2.04 387	. . . . . . . . . . 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 242	. . . . . . . . . 10 ⊢ (𝑃 ∈ ℙ → ((𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → (𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
48	47	alimdv 1917	. . . . . . . . 9 ⊢ (𝑃 ∈ ℙ → (∀𝑠(𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → ∀𝑠(𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))))
49		df-ral 3048	. . . . . . . . 9 ⊢ (∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ∀𝑠(𝑠 ∈ 𝐴 → (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))))
50	48, 49	imbitrrdi 252	. . . . . . . 8 ⊢ (𝑃 ∈ ℙ → (∀𝑠(𝑠 ⊊ 𝑡 → (𝑃 ∈ ℙ → (𝑠 ∈ 𝐴 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))) → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃))))
51		wilthlem.t	. . . . . . . . . 10 ⊢ 𝑇 = (mulGrp‘ℂ_fld)
52		simp1 1136	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → 𝑃 ∈ ℙ)
53		simp3 1138	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → 𝑡 ∈ 𝐴)
54		simp2 1137	. . . . . . . . . 10 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)))
55	51, 25, 52, 53, 54	wilthlem2 27004	. . . . . . . . 9 ⊢ ((𝑃 ∈ ℙ ∧ ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑡 → ((𝑇 Σ_g ( I ↾ 𝑠)) mod 𝑃) = (-1 mod 𝑃)) ∧ 𝑡 ∈ 𝐴) → ((𝑇 Σ_g ( I ↾ 𝑡)) mod 𝑃) = (-1 mod 𝑃))
56	55	3exp 1119	. . . . . . . 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 9167	. . . . 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 21328	. . . . . 6 ⊢ 1 = (1_r‘ℂ_fld)
63	51, 62	ringidval 20099	. . . . 5 ⊢ 1 = (0_g‘𝑇)
64		cncrng 21323	. . . . . 6 ⊢ ℂ_fld ∈ CRing
65	51	crngmgp 20157	. . . . . 6 ⊢ (ℂ_fld ∈ CRing → 𝑇 ∈ CMnd)
66	64, 65	mp1i 13	. . . . 5 ⊢ (𝑃 ∈ ℙ → 𝑇 ∈ CMnd)
67	29	a1i 11	. . . . 5 ⊢ (𝑃 ∈ ℙ → (1...(𝑃 − 1)) ∈ Fin)
68		zsubrg 21355	. . . . . 6 ⊢ ℤ ∈ (SubRing‘ℂ_fld)
69	51	subrgsubm 20498	. . . . . 6 ⊢ (ℤ ∈ (SubRing‘ℂ_fld) → ℤ ∈ (SubMnd‘𝑇))
70	68, 69	mp1i 13	. . . . 5 ⊢ (𝑃 ∈ ℙ → ℤ ∈ (SubMnd‘𝑇))
71		f1oi 6801	. . . . . . . 8 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))–1-1-onto→(1...(𝑃 − 1))
72		f1of 6763	. . . . . . . 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 13423	. . . . . . 7 ⊢ (1...(𝑃 − 1)) ⊆ ℤ
75		fss 6667	. . . . . . 7 ⊢ ((( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶(1...(𝑃 − 1)) ∧ (1...(𝑃 − 1)) ⊆ ℤ) → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ)
76	73, 74, 75	mp2an 692	. . . . . 6 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ
77	76	a1i 11	. . . . 5 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ)
78		1ex 11105	. . . . . . 7 ⊢ 1 ∈ V
79	78	a1i 11	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 1 ∈ V)
80	77, 67, 79	fdmfifsupp 9259	. . . . 5 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))) finSupp 1)
81	63, 66, 67, 70, 77, 80	gsumsubmcl 19829	. . . 4 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) ∈ ℤ)
82		1z 12499	. . . . 5 ⊢ 1 ∈ ℤ
83		znegcl 12504	. . . . 5 ⊢ (1 ∈ ℤ → -1 ∈ ℤ)
84	82, 83	mp1i 13	. . . 4 ⊢ (𝑃 ∈ ℙ → -1 ∈ ℤ)
85		moddvds 16171	. . . 4 ⊢ ((𝑃 ∈ ℕ ∧ (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) ∈ ℤ ∧ -1 ∈ ℤ) → (((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1)))
86	11, 81, 84, 85	syl3anc 1373	. . 3 ⊢ (𝑃 ∈ ℙ → (((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) mod 𝑃) = (-1 mod 𝑃) ↔ 𝑃 ∥ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1)))
87	61, 86	mpbid 232	. 2 ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1))
88		fcoi1 6697	. . . . . . . . . 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 6823	. . . . . . . 8 ⊢ ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = (( I ↾ (1...(𝑃 − 1)))‘𝑘)
91		fvres 6841	. . . . . . . 8 ⊢ (𝑘 ∈ (1...(𝑃 − 1)) → (( I ↾ (1...(𝑃 − 1)))‘𝑘) = ( I ‘𝑘))
92	90, 91	eqtrid 2778	. . . . . . 7 ⊢ (𝑘 ∈ (1...(𝑃 − 1)) → ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = ( I ‘𝑘))
93	92	adantl 481	. . . . . 6 ⊢ ((𝑃 ∈ ℙ ∧ 𝑘 ∈ (1...(𝑃 − 1))) → ((( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1))))‘𝑘) = ( I ‘𝑘))
94	5, 93	seqfveq 13930	. . . . 5 ⊢ (𝑃 ∈ ℙ → (seq1( · , (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))))‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
95		cnfldbas 21293	. . . . . . 7 ⊢ ℂ = (Base‘ℂ_fld)
96	51, 95	mgpbas 20061	. . . . . 6 ⊢ ℂ = (Base‘𝑇)
97		cnfldmul 21297	. . . . . . 7 ⊢ · = (._r‘ℂ_fld)
98	51, 97	mgpplusg 20060	. . . . . 6 ⊢ · = (+_g‘𝑇)
99		eqid 2731	. . . . . 6 ⊢ (Cntz‘𝑇) = (Cntz‘𝑇)
100		cnring 21325	. . . . . . 7 ⊢ ℂ_fld ∈ Ring
101	51	ringmgp 20155	. . . . . . 7 ⊢ (ℂ_fld ∈ Ring → 𝑇 ∈ Mnd)
102	100, 101	mp1i 13	. . . . . 6 ⊢ (𝑃 ∈ ℙ → 𝑇 ∈ Mnd)
103		zsscn 12473	. . . . . . . 8 ⊢ ℤ ⊆ ℂ
104		fss 6667	. . . . . . . 8 ⊢ ((( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℤ ∧ ℤ ⊆ ℂ) → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ)
105	76, 103, 104	mp2an 692	. . . . . . 7 ⊢ ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ
106	105	a1i 11	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ( I ↾ (1...(𝑃 − 1))):(1...(𝑃 − 1))⟶ℂ)
107	96, 99, 66, 106	cntzcmnf 19755	. . . . . 6 ⊢ (𝑃 ∈ ℙ → ran ( I ↾ (1...(𝑃 − 1))) ⊆ ((Cntz‘𝑇)‘ran ( I ↾ (1...(𝑃 − 1)))))
108		f1of1 6762	. . . . . . 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 8107	. . . . . . . . 9 ⊢ (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ dom ( I ↾ (1...(𝑃 − 1)))
111		dmresi 6001	. . . . . . . . 9 ⊢ dom ( I ↾ (1...(𝑃 − 1))) = (1...(𝑃 − 1))
112	110, 111	sseqtri 3983	. . . . . . . 8 ⊢ (( I ↾ (1...(𝑃 − 1))) supp 1) ⊆ (1...(𝑃 − 1))
113		rnresi 6024	. . . . . . . 8 ⊢ ran ( I ↾ (1...(𝑃 − 1))) = (1...(𝑃 − 1))
114	112, 113	sseqtrri 3984	. . . . . . 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 2731	. . . . . 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 19817	. . . . 5 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) = (seq1( · , (( I ↾ (1...(𝑃 − 1))) ∘ ( I ↾ (1...(𝑃 − 1)))))‘(𝑃 − 1)))
118		facnn 14179	. . . . . 6 ⊢ ((𝑃 − 1) ∈ ℕ → (!‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
119	3, 118	syl 17	. . . . 5 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) = (seq1( · , I )‘(𝑃 − 1)))
120	94, 117, 119	3eqtr4d 2776	. . . 4 ⊢ (𝑃 ∈ ℙ → (𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) = (!‘(𝑃 − 1)))
121	120	oveq1d 7361	. . 3 ⊢ (𝑃 ∈ ℙ → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1) = ((!‘(𝑃 − 1)) − -1))
122		nnm1nn0 12419	. . . . . . 7 ⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈ ℕ₀)
123	11, 122	syl 17	. . . . . 6 ⊢ (𝑃 ∈ ℙ → (𝑃 − 1) ∈ ℕ₀)
124	123	faccld 14188	. . . . 5 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) ∈ ℕ)
125	124	nncnd 12138	. . . 4 ⊢ (𝑃 ∈ ℙ → (!‘(𝑃 − 1)) ∈ ℂ)
126		ax-1cn 11061	. . . 4 ⊢ 1 ∈ ℂ
127		subneg 11407	. . . 4 ⊢ (((!‘(𝑃 − 1)) ∈ ℂ ∧ 1 ∈ ℂ) → ((!‘(𝑃 − 1)) − -1) = ((!‘(𝑃 − 1)) + 1))
128	125, 126, 127	sylancl 586	. . 3 ⊢ (𝑃 ∈ ℙ → ((!‘(𝑃 − 1)) − -1) = ((!‘(𝑃 − 1)) + 1))
129	121, 128	eqtrd 2766	. 2 ⊢ (𝑃 ∈ ℙ → ((𝑇 Σ_g ( I ↾ (1...(𝑃 − 1)))) − -1) = ((!‘(𝑃 − 1)) + 1))
130	87, 129	breqtrd 5117	1 ⊢ (𝑃 ∈ ℙ → 𝑃 ∥ ((!‘(𝑃 − 1)) + 1))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 ∀wal 1539 = wceq 1541 ∈ wcel 2111 ∀wral 3047 {crab 3395 Vcvv 3436 ⊆ wss 3902 ⊊ wpss 3903 𝒫 cpw 4550 class class class wbr 5091 I cid 5510 dom cdm 5616 ran crn 5617 ↾ cres 5618 ∘ ccom 5620 ⟶wf 6477 –1-1→wf1 6478 –1-1-onto→wf1o 6480 ‘cfv 6481 (class class class)co 7346 supp csupp 8090 Fincfn 8869 ℂcc 11001 1c1 11004 + caddc 11006 · cmul 11008 − cmin 11341 -cneg 11342 ℕcn 12122 2c2 12177 ℕ₀cn0 12378 ℤcz 12465 ℤ_≥cuz 12729 ...cfz 13404 mod cmo 13770 seqcseq 13905 ↑cexp 13965 !cfa 14177 ∥ cdvds 16160 ℙcprime 16579 Σ_g cgsu 17341 Mndcmnd 18639 SubMndcsubmnd 18687 Cntzccntz 19225 CMndccmn 19690 mulGrpcmgp 20056 Ringcrg 20149 CRingccrg 20150 SubRingcsubrg 20482 ℂ_fldccnfld 21289

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5217 ax-sep 5234 ax-nul 5244 ax-pow 5303 ax-pr 5370 ax-un 7668 ax-cnex 11059 ax-resscn 11060 ax-1cn 11061 ax-icn 11062 ax-addcl 11063 ax-addrcl 11064 ax-mulcl 11065 ax-mulrcl 11066 ax-mulcom 11067 ax-addass 11068 ax-mulass 11069 ax-distr 11070 ax-i2m1 11071 ax-1ne0 11072 ax-1rid 11073 ax-rnegex 11074 ax-rrecex 11075 ax-cnre 11076 ax-pre-lttri 11077 ax-pre-lttrn 11078 ax-pre-ltadd 11079 ax-pre-mulgt0 11080 ax-pre-sup 11081 ax-addf 11082 ax-mulf 11083

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3742 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4476 df-pw 4552 df-sn 4577 df-pr 4579 df-tp 4581 df-op 4583 df-uni 4860 df-int 4898 df-iun 4943 df-iin 4944 df-br 5092 df-opab 5154 df-mpt 5173 df-tr 5199 df-id 5511 df-eprel 5516 df-po 5524 df-so 5525 df-fr 5569 df-se 5570 df-we 5571 df-xp 5622 df-rel 5623 df-cnv 5624 df-co 5625 df-dm 5626 df-rn 5627 df-res 5628 df-ima 5629 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-of 7610 df-om 7797 df-1st 7921 df-2nd 7922 df-supp 8091 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-2o 8386 df-oadd 8389 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-fsupp 9246 df-sup 9326 df-inf 9327 df-oi 9396 df-dju 9791 df-card 9829 df-pnf 11145 df-mnf 11146 df-xr 11147 df-ltxr 11148 df-le 11149 df-sub 11343 df-neg 11344 df-div 11772 df-nn 12123 df-2 12185 df-3 12186 df-4 12187 df-5 12188 df-6 12189 df-7 12190 df-8 12191 df-9 12192 df-n0 12379 df-xnn0 12452 df-z 12466 df-dec 12586 df-uz 12730 df-rp 12888 df-fz 13405 df-fzo 13552 df-fl 13693 df-mod 13771 df-seq 13906 df-exp 13966 df-fac 14178 df-hash 14235 df-cj 15003 df-re 15004 df-im 15005 df-sqrt 15139 df-abs 15140 df-dvds 16161 df-gcd 16403 df-prm 16580 df-phi 16674 df-struct 17055 df-sets 17072 df-slot 17090 df-ndx 17102 df-base 17118 df-ress 17139 df-plusg 17171 df-mulr 17172 df-starv 17173 df-tset 17177 df-ple 17178 df-ds 17180 df-unif 17181 df-0g 17342 df-gsum 17343 df-mre 17485 df-mrc 17486 df-acs 17488 df-mgm 18545 df-sgrp 18624 df-mnd 18640 df-submnd 18689 df-grp 18846 df-minusg 18847 df-mulg 18978 df-subg 19033 df-cntz 19227 df-cmn 19692 df-abl 19693 df-mgp 20057 df-rng 20069 df-ur 20098 df-ring 20151 df-cring 20152 df-subrng 20459 df-subrg 20483 df-cnfld 21290

This theorem is referenced by: wilth 27006

W3C validator