Step |
Hyp |
Ref |
Expression |
1 |
|
wilthlem.t |
⊢ 𝑇 = ( mulGrp ‘ ℂfld ) |
2 |
|
wilthlem.a |
⊢ 𝐴 = { 𝑥 ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ∣ ( ( 𝑃 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ) } |
3 |
|
prmuz2 |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ( ℤ≥ ‘ 2 ) ) |
4 |
|
uz2m1nn |
⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( 𝑃 − 1 ) ∈ ℕ ) |
5 |
3 4
|
syl |
⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) ∈ ℕ ) |
6 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
7 |
5 6
|
eleqtrdi |
⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) ∈ ( ℤ≥ ‘ 1 ) ) |
8 |
|
eluzfz2 |
⊢ ( ( 𝑃 − 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) |
9 |
7 8
|
syl |
⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) |
10 |
|
simpl |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑃 ∈ ℙ ) |
11 |
|
elfzelz |
⊢ ( 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) → 𝑦 ∈ ℤ ) |
12 |
11
|
adantl |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → 𝑦 ∈ ℤ ) |
13 |
|
prmnn |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ ) |
14 |
|
fzm1ndvds |
⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ 𝑦 ) |
15 |
13 14
|
sylan |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ¬ 𝑃 ∥ 𝑦 ) |
16 |
|
eqid |
⊢ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) = ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) |
17 |
16
|
prmdiv |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑦 ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝑦 · ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) − 1 ) ) ) |
18 |
10 12 15 17
|
syl3anc |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ 𝑃 ∥ ( ( 𝑦 · ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ) − 1 ) ) ) |
19 |
18
|
simpld |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) |
20 |
19
|
ralrimiva |
⊢ ( 𝑃 ∈ ℙ → ∀ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) |
21 |
|
ovex |
⊢ ( 1 ... ( 𝑃 − 1 ) ) ∈ V |
22 |
21
|
pwid |
⊢ ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) |
23 |
|
eleq2 |
⊢ ( 𝑥 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( 𝑃 − 1 ) ∈ 𝑥 ↔ ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) ) |
24 |
|
eleq2 |
⊢ ( 𝑥 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ↔ ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) ) |
25 |
24
|
raleqbi1dv |
⊢ ( 𝑥 = ( 1 ... ( 𝑃 − 1 ) ) → ( ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ↔ ∀ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) ) |
26 |
23 25
|
anbi12d |
⊢ ( 𝑥 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( ( 𝑃 − 1 ) ∈ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ 𝑥 ) ↔ ( ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) ) ) |
27 |
26 2
|
elrab2 |
⊢ ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 ↔ ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝒫 ( 1 ... ( 𝑃 − 1 ) ) ∧ ( ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) ) ) |
28 |
22 27
|
mpbiran |
⊢ ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 ↔ ( ( 𝑃 − 1 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑃 − 1 ) ) ( ( 𝑦 ↑ ( 𝑃 − 2 ) ) mod 𝑃 ) ∈ ( 1 ... ( 𝑃 − 1 ) ) ) ) |
29 |
9 20 28
|
sylanbrc |
⊢ ( 𝑃 ∈ ℙ → ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 ) |
30 |
|
fzfi |
⊢ ( 1 ... ( 𝑃 − 1 ) ) ∈ Fin |
31 |
|
eleq1 |
⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∈ 𝐴 ↔ 𝑡 ∈ 𝐴 ) ) |
32 |
|
reseq2 |
⊢ ( 𝑠 = 𝑡 → ( I ↾ 𝑠 ) = ( I ↾ 𝑡 ) ) |
33 |
32
|
oveq2d |
⊢ ( 𝑠 = 𝑡 → ( 𝑇 Σg ( I ↾ 𝑠 ) ) = ( 𝑇 Σg ( I ↾ 𝑡 ) ) ) |
34 |
33
|
oveq1d |
⊢ ( 𝑠 = 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) ) |
35 |
34
|
eqeq1d |
⊢ ( 𝑠 = 𝑡 → ( ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
36 |
31 35
|
imbi12d |
⊢ ( 𝑠 = 𝑡 → ( ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ↔ ( 𝑡 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) |
37 |
36
|
imbi2d |
⊢ ( 𝑠 = 𝑡 → ( ( 𝑃 ∈ ℙ → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ↔ ( 𝑃 ∈ ℙ → ( 𝑡 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) ) |
38 |
|
eleq1 |
⊢ ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( 𝑠 ∈ 𝐴 ↔ ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 ) ) |
39 |
|
reseq2 |
⊢ ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( I ↾ 𝑠 ) = ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) |
40 |
39
|
oveq2d |
⊢ ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( 𝑇 Σg ( I ↾ 𝑠 ) ) = ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ) |
41 |
40
|
oveq1d |
⊢ ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) ) |
42 |
41
|
eqeq1d |
⊢ ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
43 |
38 42
|
imbi12d |
⊢ ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ↔ ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) |
44 |
43
|
imbi2d |
⊢ ( 𝑠 = ( 1 ... ( 𝑃 − 1 ) ) → ( ( 𝑃 ∈ ℙ → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ↔ ( 𝑃 ∈ ℙ → ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) ) |
45 |
|
bi2.04 |
⊢ ( ( 𝑠 ⊊ 𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) ↔ ( 𝑃 ∈ ℙ → ( 𝑠 ⊊ 𝑡 → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) ) |
46 |
|
pm2.27 |
⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 ∈ ℙ → ( 𝑠 ⊊ 𝑡 → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ( 𝑠 ⊊ 𝑡 → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) ) |
47 |
46
|
com34 |
⊢ ( 𝑃 ∈ ℙ → ( ( 𝑃 ∈ ℙ → ( 𝑠 ⊊ 𝑡 → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ( 𝑠 ∈ 𝐴 → ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) ) |
48 |
45 47
|
syl5bi |
⊢ ( 𝑃 ∈ ℙ → ( ( 𝑠 ⊊ 𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ( 𝑠 ∈ 𝐴 → ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) ) |
49 |
48
|
alimdv |
⊢ ( 𝑃 ∈ ℙ → ( ∀ 𝑠 ( 𝑠 ⊊ 𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ∀ 𝑠 ( 𝑠 ∈ 𝐴 → ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) ) |
50 |
|
df-ral |
⊢ ( ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ↔ ∀ 𝑠 ( 𝑠 ∈ 𝐴 → ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) |
51 |
49 50
|
syl6ibr |
⊢ ( 𝑃 ∈ ℙ → ( ∀ 𝑠 ( 𝑠 ⊊ 𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) |
52 |
|
simp1 |
⊢ ( ( 𝑃 ∈ ℙ ∧ ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ∧ 𝑡 ∈ 𝐴 ) → 𝑃 ∈ ℙ ) |
53 |
|
simp3 |
⊢ ( ( 𝑃 ∈ ℙ ∧ ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ∧ 𝑡 ∈ 𝐴 ) → 𝑡 ∈ 𝐴 ) |
54 |
|
simp2 |
⊢ ( ( 𝑃 ∈ ℙ ∧ ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ∧ 𝑡 ∈ 𝐴 ) → ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
55 |
1 2 52 53 54
|
wilthlem2 |
⊢ ( ( 𝑃 ∈ ℙ ∧ ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ∧ 𝑡 ∈ 𝐴 ) → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |
56 |
55
|
3exp |
⊢ ( 𝑃 ∈ ℙ → ( ∀ 𝑠 ∈ 𝐴 ( 𝑠 ⊊ 𝑡 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) → ( 𝑡 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) |
57 |
51 56
|
syldc |
⊢ ( ∀ 𝑠 ( 𝑠 ⊊ 𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ( 𝑃 ∈ ℙ → ( 𝑡 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) |
58 |
57
|
a1i |
⊢ ( 𝑡 ∈ Fin → ( ∀ 𝑠 ( 𝑠 ⊊ 𝑡 → ( 𝑃 ∈ ℙ → ( 𝑠 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑠 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) → ( 𝑃 ∈ ℙ → ( 𝑡 ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ 𝑡 ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) ) |
59 |
37 44 58
|
findcard3 |
⊢ ( ( 1 ... ( 𝑃 − 1 ) ) ∈ Fin → ( 𝑃 ∈ ℙ → ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) ) |
60 |
30 59
|
ax-mp |
⊢ ( 𝑃 ∈ ℙ → ( ( 1 ... ( 𝑃 − 1 ) ) ∈ 𝐴 → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) ) |
61 |
29 60
|
mpd |
⊢ ( 𝑃 ∈ ℙ → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ) |
62 |
|
cnfld1 |
⊢ 1 = ( 1r ‘ ℂfld ) |
63 |
1 62
|
ringidval |
⊢ 1 = ( 0g ‘ 𝑇 ) |
64 |
|
cncrng |
⊢ ℂfld ∈ CRing |
65 |
1
|
crngmgp |
⊢ ( ℂfld ∈ CRing → 𝑇 ∈ CMnd ) |
66 |
64 65
|
mp1i |
⊢ ( 𝑃 ∈ ℙ → 𝑇 ∈ CMnd ) |
67 |
30
|
a1i |
⊢ ( 𝑃 ∈ ℙ → ( 1 ... ( 𝑃 − 1 ) ) ∈ Fin ) |
68 |
|
zsubrg |
⊢ ℤ ∈ ( SubRing ‘ ℂfld ) |
69 |
1
|
subrgsubm |
⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubMnd ‘ 𝑇 ) ) |
70 |
68 69
|
mp1i |
⊢ ( 𝑃 ∈ ℙ → ℤ ∈ ( SubMnd ‘ 𝑇 ) ) |
71 |
|
f1oi |
⊢ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) –1-1-onto→ ( 1 ... ( 𝑃 − 1 ) ) |
72 |
|
f1of |
⊢ ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) –1-1-onto→ ( 1 ... ( 𝑃 − 1 ) ) → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ( 1 ... ( 𝑃 − 1 ) ) ) |
73 |
71 72
|
ax-mp |
⊢ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ( 1 ... ( 𝑃 − 1 ) ) |
74 |
|
fzssz |
⊢ ( 1 ... ( 𝑃 − 1 ) ) ⊆ ℤ |
75 |
|
fss |
⊢ ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ( 1 ... ( 𝑃 − 1 ) ) ∧ ( 1 ... ( 𝑃 − 1 ) ) ⊆ ℤ ) → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℤ ) |
76 |
73 74 75
|
mp2an |
⊢ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℤ |
77 |
76
|
a1i |
⊢ ( 𝑃 ∈ ℙ → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℤ ) |
78 |
|
1ex |
⊢ 1 ∈ V |
79 |
78
|
a1i |
⊢ ( 𝑃 ∈ ℙ → 1 ∈ V ) |
80 |
77 67 79
|
fdmfifsupp |
⊢ ( 𝑃 ∈ ℙ → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) finSupp 1 ) |
81 |
63 66 67 70 77 80
|
gsumsubmcl |
⊢ ( 𝑃 ∈ ℙ → ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ∈ ℤ ) |
82 |
|
1z |
⊢ 1 ∈ ℤ |
83 |
|
znegcl |
⊢ ( 1 ∈ ℤ → - 1 ∈ ℤ ) |
84 |
82 83
|
mp1i |
⊢ ( 𝑃 ∈ ℙ → - 1 ∈ ℤ ) |
85 |
|
moddvds |
⊢ ( ( 𝑃 ∈ ℕ ∧ ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ∈ ℤ ∧ - 1 ∈ ℤ ) → ( ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) − - 1 ) ) ) |
86 |
13 81 84 85
|
syl3anc |
⊢ ( 𝑃 ∈ ℙ → ( ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) mod 𝑃 ) = ( - 1 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) − - 1 ) ) ) |
87 |
61 86
|
mpbid |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∥ ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) − - 1 ) ) |
88 |
|
fcoi1 |
⊢ ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ( 1 ... ( 𝑃 − 1 ) ) → ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) = ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) |
89 |
73 88
|
ax-mp |
⊢ ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) = ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) |
90 |
89
|
fveq1i |
⊢ ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ‘ 𝑘 ) = ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ‘ 𝑘 ) |
91 |
|
fvres |
⊢ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) → ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ‘ 𝑘 ) = ( I ‘ 𝑘 ) ) |
92 |
90 91
|
syl5eq |
⊢ ( 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) → ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ‘ 𝑘 ) = ( I ‘ 𝑘 ) ) |
93 |
92
|
adantl |
⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑘 ∈ ( 1 ... ( 𝑃 − 1 ) ) ) → ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ‘ 𝑘 ) = ( I ‘ 𝑘 ) ) |
94 |
7 93
|
seqfveq |
⊢ ( 𝑃 ∈ ℙ → ( seq 1 ( · , ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ) ‘ ( 𝑃 − 1 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑃 − 1 ) ) ) |
95 |
|
cnfldbas |
⊢ ℂ = ( Base ‘ ℂfld ) |
96 |
1 95
|
mgpbas |
⊢ ℂ = ( Base ‘ 𝑇 ) |
97 |
|
cnfldmul |
⊢ · = ( .r ‘ ℂfld ) |
98 |
1 97
|
mgpplusg |
⊢ · = ( +g ‘ 𝑇 ) |
99 |
|
eqid |
⊢ ( Cntz ‘ 𝑇 ) = ( Cntz ‘ 𝑇 ) |
100 |
|
cnring |
⊢ ℂfld ∈ Ring |
101 |
1
|
ringmgp |
⊢ ( ℂfld ∈ Ring → 𝑇 ∈ Mnd ) |
102 |
100 101
|
mp1i |
⊢ ( 𝑃 ∈ ℙ → 𝑇 ∈ Mnd ) |
103 |
|
zsscn |
⊢ ℤ ⊆ ℂ |
104 |
|
fss |
⊢ ( ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℤ ∧ ℤ ⊆ ℂ ) → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℂ ) |
105 |
76 103 104
|
mp2an |
⊢ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℂ |
106 |
105
|
a1i |
⊢ ( 𝑃 ∈ ℙ → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) ⟶ ℂ ) |
107 |
96 99 66 106
|
cntzcmnf |
⊢ ( 𝑃 ∈ ℙ → ran ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ⊆ ( ( Cntz ‘ 𝑇 ) ‘ ran ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ) |
108 |
|
f1of1 |
⊢ ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) –1-1-onto→ ( 1 ... ( 𝑃 − 1 ) ) → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) –1-1→ ( 1 ... ( 𝑃 − 1 ) ) ) |
109 |
71 108
|
mp1i |
⊢ ( 𝑃 ∈ ℙ → ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) : ( 1 ... ( 𝑃 − 1 ) ) –1-1→ ( 1 ... ( 𝑃 − 1 ) ) ) |
110 |
|
suppssdm |
⊢ ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) supp 1 ) ⊆ dom ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) |
111 |
|
dmresi |
⊢ dom ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) = ( 1 ... ( 𝑃 − 1 ) ) |
112 |
110 111
|
sseqtri |
⊢ ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) supp 1 ) ⊆ ( 1 ... ( 𝑃 − 1 ) ) |
113 |
|
rnresi |
⊢ ran ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) = ( 1 ... ( 𝑃 − 1 ) ) |
114 |
112 113
|
sseqtrri |
⊢ ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) supp 1 ) ⊆ ran ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) |
115 |
114
|
a1i |
⊢ ( 𝑃 ∈ ℙ → ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) supp 1 ) ⊆ ran ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) |
116 |
|
eqid |
⊢ ( ( ( 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 5 109 115 116
|
gsumval3 |
⊢ ( 𝑃 ∈ ℙ → ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) = ( seq 1 ( · , ( ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ∘ ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) ) ‘ ( 𝑃 − 1 ) ) ) |
118 |
|
facnn |
⊢ ( ( 𝑃 − 1 ) ∈ ℕ → ( ! ‘ ( 𝑃 − 1 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑃 − 1 ) ) ) |
119 |
5 118
|
syl |
⊢ ( 𝑃 ∈ ℙ → ( ! ‘ ( 𝑃 − 1 ) ) = ( seq 1 ( · , I ) ‘ ( 𝑃 − 1 ) ) ) |
120 |
94 117 119
|
3eqtr4d |
⊢ ( 𝑃 ∈ ℙ → ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) = ( ! ‘ ( 𝑃 − 1 ) ) ) |
121 |
120
|
oveq1d |
⊢ ( 𝑃 ∈ ℙ → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) − - 1 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) ) |
122 |
|
nnm1nn0 |
⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 ) |
123 |
13 122
|
syl |
⊢ ( 𝑃 ∈ ℙ → ( 𝑃 − 1 ) ∈ ℕ0 ) |
124 |
123
|
faccld |
⊢ ( 𝑃 ∈ ℙ → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℕ ) |
125 |
124
|
nncnd |
⊢ ( 𝑃 ∈ ℙ → ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ ) |
126 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
127 |
|
subneg |
⊢ ( ( ( ! ‘ ( 𝑃 − 1 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) |
128 |
125 126 127
|
sylancl |
⊢ ( 𝑃 ∈ ℙ → ( ( ! ‘ ( 𝑃 − 1 ) ) − - 1 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) |
129 |
121 128
|
eqtrd |
⊢ ( 𝑃 ∈ ℙ → ( ( 𝑇 Σg ( I ↾ ( 1 ... ( 𝑃 − 1 ) ) ) ) − - 1 ) = ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) |
130 |
87 129
|
breqtrd |
⊢ ( 𝑃 ∈ ℙ → 𝑃 ∥ ( ( ! ‘ ( 𝑃 − 1 ) ) + 1 ) ) |