Step | Hyp | Ref
| Expression |
1 | | simpr 479 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → 𝑆 ⊆ {(𝑃 − 1)}) |
2 | | wilthlem2.s |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ 𝐴) |
3 | | eleq2 2848 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑆 → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ 𝑆)) |
4 | | eleq2 2848 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑆 → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)) |
5 | 4 | raleqbi1dv 3328 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑆 → (∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)) |
6 | 3, 5 | anbi12d 624 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑆 → (((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥) ↔ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))) |
7 | | wilthlem.a |
. . . . . . . . . . . . . . 15
⊢ 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)} |
8 | 6, 7 | elrab2 3576 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ 𝐴 ↔ (𝑆 ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))) |
9 | 2, 8 | sylib 210 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))) |
10 | 9 | simprd 491 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)) |
11 | 10 | simpld 490 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 − 1) ∈ 𝑆) |
12 | 11 | snssd 4571 |
. . . . . . . . . 10
⊢ (𝜑 → {(𝑃 − 1)} ⊆ 𝑆) |
13 | 12 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → {(𝑃 − 1)} ⊆ 𝑆) |
14 | 1, 13 | eqssd 3838 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → 𝑆 = {(𝑃 − 1)}) |
15 | 14 | reseq2d 5642 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → ( I ↾ 𝑆) = ( I ↾ {(𝑃 − 1)})) |
16 | | mptresid 5712 |
. . . . . . 7
⊢ (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧) = ( I ↾ {(𝑃 − 1)}) |
17 | 15, 16 | syl6eqr 2832 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → ( I ↾ 𝑆) = (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) |
18 | 17 | oveq2d 6938 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → (𝑇 Σg ( I ↾
𝑆)) = (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧))) |
19 | 18 | oveq1d 6937 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃)) |
20 | | wilthlem2.p |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℙ) |
21 | | prmnn 15793 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℕ) |
23 | 22 | nncnd 11392 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℂ) |
24 | | ax-1cn 10330 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
25 | | negsub 10671 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑃 + -1) =
(𝑃 −
1)) |
26 | 23, 24, 25 | sylancl 580 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 + -1) = (𝑃 − 1)) |
27 | | neg1cn 11496 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
28 | | addcom 10562 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℂ ∧ -1 ∈
ℂ) → (𝑃 + -1) =
(-1 + 𝑃)) |
29 | 23, 27, 28 | sylancl 580 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 + -1) = (-1 + 𝑃)) |
30 | 26, 29 | eqtr3d 2816 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 − 1) = (-1 + 𝑃)) |
31 | | cnring 20164 |
. . . . . . . . . 10
⊢
ℂfld ∈ Ring |
32 | | wilthlem.t |
. . . . . . . . . . 11
⊢ 𝑇 =
(mulGrp‘ℂfld) |
33 | 32 | ringmgp 18940 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → 𝑇 ∈ Mnd) |
34 | 31, 33 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ Mnd) |
35 | | nnm1nn0 11685 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
36 | 22, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
37 | 36 | nn0cnd 11704 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 1) ∈ ℂ) |
38 | | cnfldbas 20146 |
. . . . . . . . . . 11
⊢ ℂ =
(Base‘ℂfld) |
39 | 32, 38 | mgpbas 18882 |
. . . . . . . . . 10
⊢ ℂ =
(Base‘𝑇) |
40 | | id 22 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑃 − 1) → 𝑧 = (𝑃 − 1)) |
41 | 39, 40 | gsumsn 18740 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Mnd ∧ (𝑃 − 1) ∈ ℂ ∧
(𝑃 − 1) ∈
ℂ) → (𝑇
Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (𝑃 − 1)) |
42 | 34, 37, 37, 41 | syl3anc 1439 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (𝑃 − 1)) |
43 | 23 | mulid2d 10395 |
. . . . . . . . 9
⊢ (𝜑 → (1 · 𝑃) = 𝑃) |
44 | 43 | oveq2d 6938 |
. . . . . . . 8
⊢ (𝜑 → (-1 + (1 · 𝑃)) = (-1 + 𝑃)) |
45 | 30, 42, 44 | 3eqtr4d 2824 |
. . . . . . 7
⊢ (𝜑 → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (-1 + (1 · 𝑃))) |
46 | 45 | oveq1d 6937 |
. . . . . 6
⊢ (𝜑 → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = ((-1 + (1 · 𝑃)) mod 𝑃)) |
47 | | neg1rr 11497 |
. . . . . . . 8
⊢ -1 ∈
ℝ |
48 | 47 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → -1 ∈
ℝ) |
49 | 22 | nnrpd 12179 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
50 | | 1zzd 11760 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
51 | | modcyc 13024 |
. . . . . . 7
⊢ ((-1
∈ ℝ ∧ 𝑃
∈ ℝ+ ∧ 1 ∈ ℤ) → ((-1 + (1 ·
𝑃)) mod 𝑃) = (-1 mod 𝑃)) |
52 | 48, 49, 50, 51 | syl3anc 1439 |
. . . . . 6
⊢ (𝜑 → ((-1 + (1 · 𝑃)) mod 𝑃) = (-1 mod 𝑃)) |
53 | 46, 52 | eqtrd 2814 |
. . . . 5
⊢ (𝜑 → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃)) |
54 | 53 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃)) |
55 | 19, 54 | eqtrd 2814 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃)) |
56 | 55 | ex 403 |
. 2
⊢ (𝜑 → (𝑆 ⊆ {(𝑃 − 1)} → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃))) |
57 | | nss 3882 |
. . 3
⊢ (¬
𝑆 ⊆ {(𝑃 − 1)} ↔ ∃𝑧(𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) |
58 | | cnfld1 20167 |
. . . . . . . . . 10
⊢ 1 =
(1r‘ℂfld) |
59 | 32, 58 | ringidval 18890 |
. . . . . . . . 9
⊢ 1 =
(0g‘𝑇) |
60 | | cnfldmul 20148 |
. . . . . . . . . 10
⊢ ·
= (.r‘ℂfld) |
61 | 32, 60 | mgpplusg 18880 |
. . . . . . . . 9
⊢ ·
= (+g‘𝑇) |
62 | | cncrng 20163 |
. . . . . . . . . . 11
⊢
ℂfld ∈ CRing |
63 | 32 | crngmgp 18942 |
. . . . . . . . . . 11
⊢
(ℂfld ∈ CRing → 𝑇 ∈ CMnd) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑇 ∈ CMnd |
65 | 64 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑇 ∈ CMnd) |
66 | 2 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ∈ 𝐴) |
67 | | f1oi 6428 |
. . . . . . . . . . . 12
⊢ ( I
↾ 𝑆):𝑆–1-1-onto→𝑆 |
68 | | f1of 6391 |
. . . . . . . . . . . 12
⊢ (( I
↾ 𝑆):𝑆–1-1-onto→𝑆 → ( I ↾ 𝑆):𝑆⟶𝑆) |
69 | 67, 68 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ( I
↾ 𝑆):𝑆⟶𝑆 |
70 | 9 | simpld 490 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ 𝒫 (1...(𝑃 − 1))) |
71 | 70 | elpwid 4391 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ⊆ (1...(𝑃 − 1))) |
72 | | elfzelz 12659 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (1...(𝑃 − 1)) → 𝑧 ∈ ℤ) |
73 | 72 | ssriv 3825 |
. . . . . . . . . . . . 13
⊢
(1...(𝑃 − 1))
⊆ ℤ |
74 | 71, 73 | syl6ss 3833 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ⊆ ℤ) |
75 | | zsscn 11736 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℂ |
76 | 74, 75 | syl6ss 3833 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
77 | | fss 6304 |
. . . . . . . . . . 11
⊢ ((( I
↾ 𝑆):𝑆⟶𝑆 ∧ 𝑆 ⊆ ℂ) → ( I ↾ 𝑆):𝑆⟶ℂ) |
78 | 69, 76, 77 | sylancr 581 |
. . . . . . . . . 10
⊢ (𝜑 → ( I ↾ 𝑆):𝑆⟶ℂ) |
79 | 78 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ 𝑆):𝑆⟶ℂ) |
80 | | fzfi 13090 |
. . . . . . . . . . . 12
⊢
(1...(𝑃 − 1))
∈ Fin |
81 | | ssfi 8468 |
. . . . . . . . . . . 12
⊢
(((1...(𝑃 −
1)) ∈ Fin ∧ 𝑆
⊆ (1...(𝑃 −
1))) → 𝑆 ∈
Fin) |
82 | 80, 71, 81 | sylancr 581 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ Fin) |
83 | | 1ex 10372 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
84 | 83 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
V) |
85 | 78, 82, 84 | fdmfifsupp 8573 |
. . . . . . . . . 10
⊢ (𝜑 → ( I ↾ 𝑆) finSupp 1) |
86 | 85 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ 𝑆) finSupp 1) |
87 | | disjdif 4264 |
. . . . . . . . . 10
⊢ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∩ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ∅ |
88 | 87 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∩ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ∅) |
89 | | undif2 4268 |
. . . . . . . . . 10
⊢ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) |
90 | | simprl 761 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ 𝑆) |
91 | | oveq1 6929 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → (𝑦↑(𝑃 − 2)) = (𝑧↑(𝑃 − 2))) |
92 | 91 | oveq1d 6937 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
93 | 92 | eleq1d 2844 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆 ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)) |
94 | 10 | simprd 491 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) |
95 | 94 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) |
96 | 93, 95, 90 | rspcdva 3517 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) |
97 | | prssi 4583 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ 𝑆 ∧ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆) |
98 | 90, 96, 97 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆) |
99 | | ssequn1 4006 |
. . . . . . . . . . 11
⊢ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆 ↔ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) = 𝑆) |
100 | 98, 99 | sylib 210 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) = 𝑆) |
101 | 89, 100 | syl5req 2827 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 = ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
102 | 39, 59, 61, 65, 66, 79, 86, 88, 101 | gsumsplit 18714 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
𝑆)) = ((𝑇 Σg (( I ↾
𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg (( I ↾
𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))) |
103 | 98 | resabs1d 5677 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
104 | 103 | oveq2d 6938 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (( I ↾
𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
105 | | difss 3960 |
. . . . . . . . . . . 12
⊢ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ 𝑆 |
106 | | resabs1 5676 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ 𝑆 → (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
107 | 105, 106 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (( I
↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
108 | 107 | oveq2i 6933 |
. . . . . . . . . 10
⊢ (𝑇 Σg (( I
↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) = (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
109 | 108 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (( I ↾
𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) = (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) |
110 | 104, 109 | oveq12d 6940 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg (( I ↾
𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg (( I ↾
𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) = ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))) |
111 | 102, 110 | eqtrd 2814 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
𝑆)) = ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))) |
112 | 111 | oveq1d 6937 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃)) |
113 | | prfi 8523 |
. . . . . . . . . 10
⊢ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∈ Fin |
114 | 113 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∈ Fin) |
115 | | zsubrg 20195 |
. . . . . . . . . 10
⊢ ℤ
∈ (SubRing‘ℂfld) |
116 | 32 | subrgsubm 19185 |
. . . . . . . . . 10
⊢ (ℤ
∈ (SubRing‘ℂfld) → ℤ ∈
(SubMnd‘𝑇)) |
117 | 115, 116 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ℤ ∈
(SubMnd‘𝑇)) |
118 | | f1oi 6428 |
. . . . . . . . . . 11
⊢ ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}–1-1-onto→{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} |
119 | | f1of 6391 |
. . . . . . . . . . 11
⊢ (( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}–1-1-onto→{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
120 | 118, 119 | ax-mp 5 |
. . . . . . . . . 10
⊢ ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} |
121 | 74 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ ℤ) |
122 | 98, 121 | sstrd 3831 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ ℤ) |
123 | | fss 6304 |
. . . . . . . . . 10
⊢ ((( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∧ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ ℤ) → ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶ℤ) |
124 | 120, 122,
123 | sylancr 581 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶ℤ) |
125 | 83 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈
V) |
126 | 124, 114,
125 | fdmfifsupp 8573 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) finSupp 1) |
127 | 59, 65, 114, 117, 124, 126 | gsumsubmcl 18705 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℤ) |
128 | 127 | zred 11834 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℝ) |
129 | | 1red 10377 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈
ℝ) |
130 | 71 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ (1...(𝑃 − 1))) |
131 | 130 | ssdifssd 3971 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1))) |
132 | | ssfi 8468 |
. . . . . . . . 9
⊢
(((1...(𝑃 −
1)) ∈ Fin ∧ (𝑆
∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1))) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ Fin) |
133 | 80, 131, 132 | sylancr 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ Fin) |
134 | | f1oi 6428 |
. . . . . . . . . 10
⊢ ( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})–1-1-onto→(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
135 | | f1of 6391 |
. . . . . . . . . 10
⊢ (( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})–1-1-onto→(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
136 | 134, 135 | ax-mp 5 |
. . . . . . . . 9
⊢ ( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
137 | 121 | ssdifssd 3971 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ ℤ) |
138 | | fss 6304 |
. . . . . . . . 9
⊢ ((( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ ℤ) → ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶ℤ) |
139 | 136, 137,
138 | sylancr 581 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶ℤ) |
140 | 139, 133,
125 | fdmfifsupp 8573 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) finSupp 1) |
141 | 59, 65, 133, 117, 139, 140 | gsumsubmcl 18705 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℤ) |
142 | 49 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈
ℝ+) |
143 | 34 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑇 ∈ Mnd) |
144 | 76 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ ℂ) |
145 | 144, 90 | sseldd 3822 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℂ) |
146 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) |
147 | 39, 146 | gsumsn 18740 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Mnd ∧ 𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑇 Σg
(𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧) |
148 | 143, 145,
145, 147 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧) |
149 | 148 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧) |
150 | | mptresid 5712 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ {𝑧} ↦ 𝑤) = ( I ↾ {𝑧}) |
151 | | dfsn2 4411 |
. . . . . . . . . . . . . 14
⊢ {𝑧} = {𝑧, 𝑧} |
152 | | simpr 479 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → 𝑧 = 1) |
153 | 152 | orcd 862 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))) |
154 | 20 | adantr 474 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℙ) |
155 | 130, 90 | sseldd 3822 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ (1...(𝑃 − 1))) |
156 | | wilthlem1 25246 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → (𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1)))) |
157 | 154, 155,
156 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1)))) |
158 | 157 | biimpar 471 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))) → 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
159 | 153, 158 | syldan 585 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
160 | 159 | preq2d 4507 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → {𝑧, 𝑧} = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
161 | 151, 160 | syl5eq 2826 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → {𝑧} = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
162 | 161 | reseq2d 5642 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → ( I ↾ {𝑧}) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
163 | 150, 162 | syl5eq 2826 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑤 ∈ {𝑧} ↦ 𝑤) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
164 | 163 | oveq2d 6938 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
165 | 149, 164,
152 | 3eqtr3d 2822 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = 1) |
166 | 165 | oveq1d 6937 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃)) |
167 | | df-pr 4401 |
. . . . . . . . . . . . . . 15
⊢ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} = ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
168 | 167 | reseq2i 5639 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ( I ↾ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
169 | | mptresid 5712 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤) = ( I ↾ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
170 | 168, 169 | eqtr4i 2805 |
. . . . . . . . . . . . 13
⊢ ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤) |
171 | 170 | oveq2i 6933 |
. . . . . . . . . . . 12
⊢ (𝑇 Σg ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑇 Σg (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)) |
172 | 64 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → 𝑇 ∈ CMnd) |
173 | | snfi 8326 |
. . . . . . . . . . . . . 14
⊢ {𝑧} ∈ Fin |
174 | 173 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → {𝑧} ∈ Fin) |
175 | | elsni 4415 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑧} → 𝑤 = 𝑧) |
176 | 175 | adantl 475 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑤 = 𝑧) |
177 | 145 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑧 ∈ ℂ) |
178 | 176, 177 | eqeltrd 2859 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑤 ∈ ℂ) |
179 | 178 | adantlr 705 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) ∧ 𝑤 ∈ {𝑧}) → 𝑤 ∈ ℂ) |
180 | 144, 96 | sseldd 3822 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℂ) |
181 | 180 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℂ) |
182 | | simprr 763 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑧 ∈ {(𝑃 − 1)}) |
183 | | velsn 4414 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ {(𝑃 − 1)} ↔ 𝑧 = (𝑃 − 1)) |
184 | 182, 183 | sylnib 320 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑧 = (𝑃 − 1)) |
185 | | biorf 923 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 = (𝑃 − 1) → (𝑧 = 1 ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1))) |
186 | 184, 185 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = 1 ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1))) |
187 | | ovex 6954 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ V |
188 | 187 | elsn 4413 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) = 𝑧) |
189 | | eqcom 2785 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧↑(𝑃 − 2)) mod 𝑃) = 𝑧 ↔ 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
190 | 188, 189 | bitri 267 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
191 | | orcom 859 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 = (𝑃 − 1) ∨ 𝑧 = 1) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))) |
192 | 157, 190,
191 | 3bitr4g 306 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1))) |
193 | 186, 192 | bitr4d 274 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = 1 ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧})) |
194 | 193 | necon3abid 3005 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 ≠ 1 ↔ ¬ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧})) |
195 | 194 | biimpa 470 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ¬ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧}) |
196 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((𝑧↑(𝑃 − 2)) mod 𝑃) → 𝑤 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
197 | 39, 61, 172, 174, 179, 181, 195, 181, 196 | gsumunsn 18745 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)) = ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
198 | 171, 197 | syl5eq 2826 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
199 | 148 | adantr 474 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧) |
200 | 199 | oveq1d 6937 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)) = (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
201 | 198, 200 | eqtrd 2814 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
202 | 201 | oveq1d 6937 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
203 | 155, 72 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℤ) |
204 | 22 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℕ) |
205 | | fzm1ndvds 15451 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℕ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑧) |
206 | 204, 155,
205 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑃 ∥ 𝑧) |
207 | | eqid 2778 |
. . . . . . . . . . . . . 14
⊢ ((𝑧↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) |
208 | 207 | prmdiv 15894 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝑧 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑧) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))) |
209 | 154, 203,
206, 208 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))) |
210 | 209 | simprd 491 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)) |
211 | | elfznn 12687 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (1...(𝑃 − 1)) → 𝑧 ∈ ℕ) |
212 | 155, 211 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℕ) |
213 | 130, 96 | sseldd 3822 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))) |
214 | | elfznn 12687 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℕ) |
215 | 213, 214 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℕ) |
216 | 212, 215 | nnmulcld 11428 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℕ) |
217 | 216 | nnzd 11833 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℤ) |
218 | | 1zzd 11760 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈
ℤ) |
219 | | moddvds 15398 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℤ ∧ 1 ∈ ℤ)
→ (((𝑧 ·
((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))) |
220 | 204, 217,
218, 219 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))) |
221 | 210, 220 | mpbird 249 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃)) |
222 | 221 | adantr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃)) |
223 | 202, 222 | eqtrd 2814 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃)) |
224 | 166, 223 | pm2.61dane 3057 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃)) |
225 | | modmul1 13042 |
. . . . . . 7
⊢ ((((𝑇 Σg ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℝ ∧ 1 ∈ ℝ)
∧ ((𝑇
Σg ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℤ ∧ 𝑃 ∈ ℝ+) ∧ ((𝑇 Σg ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃)) → (((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((1 · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃)) |
226 | 128, 129,
141, 142, 224, 225 | syl221anc 1449 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((1 · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃)) |
227 | 141 | zcnd 11835 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℂ) |
228 | 227 | mulid2d 10395 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (1 · (𝑇 Σg ( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) = (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) |
229 | 228 | oveq1d 6937 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((1 · (𝑇 Σg ( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃)) |
230 | | sseqin2 4040 |
. . . . . . . . . . 11
⊢ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
231 | 98, 230 | sylib 210 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
232 | | vex 3401 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
233 | 232 | prnz 4543 |
. . . . . . . . . . 11
⊢ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ≠ ∅ |
234 | 233 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ≠ ∅) |
235 | 231, 234 | eqnetrd 3036 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ≠ ∅) |
236 | | disj4 4251 |
. . . . . . . . . 10
⊢ ((𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ∅ ↔ ¬ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆) |
237 | 236 | necon2abii 3019 |
. . . . . . . . 9
⊢ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ≠ ∅) |
238 | 235, 237 | sylibr 226 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆) |
239 | | psseq1 3916 |
. . . . . . . . . 10
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (𝑠 ⊊ 𝑆 ↔ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆)) |
240 | | reseq2 5637 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ( I ↾ 𝑠) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
241 | 240 | oveq2d 6938 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (𝑇 Σg ( I ↾
𝑠)) = (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) |
242 | 241 | oveq1d 6937 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑇 Σg ( I ↾
𝑠)) mod 𝑃) = ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃)) |
243 | 242 | eqeq1d 2780 |
. . . . . . . . . 10
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑇 Σg ( I ↾
𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))) |
244 | 239, 243 | imbi12d 336 |
. . . . . . . . 9
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑠 ⊊ 𝑆 → ((𝑇 Σg ( I ↾
𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 → ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)))) |
245 | | wilthlem2.r |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑆 → ((𝑇 Σg ( I ↾
𝑠)) mod 𝑃) = (-1 mod 𝑃))) |
246 | 245 | adantr 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑆 → ((𝑇 Σg ( I ↾
𝑠)) mod 𝑃) = (-1 mod 𝑃))) |
247 | | ovex 6954 |
. . . . . . . . . . . 12
⊢
(1...(𝑃 − 1))
∈ V |
248 | 247 | elpw2 5062 |
. . . . . . . . . . 11
⊢ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)) ↔ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1))) |
249 | 131, 248 | sylibr 226 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1))) |
250 | 11 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ 𝑆) |
251 | | eqcom 2785 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑃 − 1) ↔ (𝑃 − 1) = 𝑧) |
252 | 183, 251 | bitri 267 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {(𝑃 − 1)} ↔ (𝑃 − 1) = 𝑧) |
253 | 182, 252 | sylnib 320 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) = 𝑧) |
254 | | oveq1 6929 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → ((𝑃 − 1)↑(𝑃 − 2)) = (((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2))) |
255 | 254 | oveq1d 6937 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
256 | 204, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈
ℕ0) |
257 | | nn0uz 12028 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℕ0 = (ℤ≥‘0) |
258 | 256, 257 | syl6eleq 2869 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈
(ℤ≥‘0)) |
259 | | eluzfz2 12666 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 − 1) ∈
(ℤ≥‘0) → (𝑃 − 1) ∈ (0...(𝑃 − 1))) |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (0...(𝑃 − 1))) |
261 | | prmz 15794 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
262 | 154, 261 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℤ) |
263 | 121, 250 | sseldd 3822 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℤ) |
264 | | 1z 11759 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℤ |
265 | | zsubcl 11771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 − 1) ∈ ℤ ∧
1 ∈ ℤ) → ((𝑃 − 1) − 1) ∈
ℤ) |
266 | 263, 264,
265 | sylancl 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) − 1) ∈
ℤ) |
267 | | dvdsmul1 15410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℤ ∧ ((𝑃 − 1) − 1) ∈
ℤ) → 𝑃 ∥
(𝑃 · ((𝑃 − 1) −
1))) |
268 | 262, 266,
267 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ (𝑃 · ((𝑃 − 1) − 1))) |
269 | 204 | nncnd 11392 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℂ) |
270 | 24 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈
ℂ) |
271 | 256 | nn0cnd 11704 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℂ) |
272 | 269, 270,
271 | subdird 10832 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) · (𝑃 − 1)) = ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1)))) |
273 | 269, 271 | mulcld 10397 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · (𝑃 − 1)) ∈
ℂ) |
274 | 273, 269,
270 | subsubd 10762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (𝑃 − 1)) = (((𝑃 · (𝑃 − 1)) − 𝑃) + 1)) |
275 | 271 | mulid2d 10395 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (1 · (𝑃 − 1)) = (𝑃 − 1)) |
276 | 275 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))) = ((𝑃 · (𝑃 − 1)) − (𝑃 − 1))) |
277 | 269, 271,
270 | subdid 10831 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) = ((𝑃 · (𝑃 − 1)) − (𝑃 · 1))) |
278 | 269 | mulid1d 10394 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · 1) = 𝑃) |
279 | 278 | oveq2d 6938 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (𝑃 · 1)) = ((𝑃 · (𝑃 − 1)) − 𝑃)) |
280 | 277, 279 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) = ((𝑃 · (𝑃 − 1)) − 𝑃)) |
281 | 280 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · ((𝑃 − 1) − 1)) + 1) = (((𝑃 · (𝑃 − 1)) − 𝑃) + 1)) |
282 | 274, 276,
281 | 3eqtr4d 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))) = ((𝑃 · ((𝑃 − 1) − 1)) +
1)) |
283 | 272, 282 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) · (𝑃 − 1)) = ((𝑃 · ((𝑃 − 1) − 1)) +
1)) |
284 | 283 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) · (𝑃 − 1)) − 1) = (((𝑃 · ((𝑃 − 1) − 1)) + 1) −
1)) |
285 | 266 | zcnd 11835 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) − 1) ∈
ℂ) |
286 | 269, 285 | mulcld 10397 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) ∈
ℂ) |
287 | | pncan 10628 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 · ((𝑃 − 1) − 1)) ∈ ℂ ∧
1 ∈ ℂ) → (((𝑃 · ((𝑃 − 1) − 1)) + 1) − 1) =
(𝑃 · ((𝑃 − 1) −
1))) |
288 | 286, 24, 287 | sylancl 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 · ((𝑃 − 1) − 1)) + 1) − 1) =
(𝑃 · ((𝑃 − 1) −
1))) |
289 | 284, 288 | eqtrd 2814 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) · (𝑃 − 1)) − 1) = (𝑃 · ((𝑃 − 1) − 1))) |
290 | 268, 289 | breqtrrd 4914 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) |
291 | 130, 250 | sseldd 3822 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (1...(𝑃 − 1))) |
292 | | fzm1ndvds 15451 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℕ ∧ (𝑃 − 1) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝑃 − 1)) |
293 | 204, 291,
292 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑃 ∥ (𝑃 − 1)) |
294 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) |
295 | 294 | prmdiveq 15895 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧
¬ 𝑃 ∥ (𝑃 − 1)) → (((𝑃 − 1) ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) ↔ (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃))) |
296 | 154, 263,
293, 295 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) ↔ (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃))) |
297 | 260, 290,
296 | mpbi2and 702 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)) |
298 | 207 | prmdivdiv 15896 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
299 | 154, 155,
298 | syl2anc 579 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
300 | 297, 299 | eqeq12d 2793 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) = 𝑧 ↔ (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))) |
301 | 255, 300 | syl5ibr 238 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (𝑃 − 1) = 𝑧)) |
302 | 253, 301 | mtod 190 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
303 | | ioran 969 |
. . . . . . . . . . . . . 14
⊢ (¬
((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) ↔ (¬ (𝑃 − 1) = 𝑧 ∧ ¬ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
304 | 253, 302,
303 | sylanbrc 578 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
305 | | ovex 6954 |
. . . . . . . . . . . . . 14
⊢ (𝑃 − 1) ∈
V |
306 | 305 | elpr 4421 |
. . . . . . . . . . . . 13
⊢ ((𝑃 − 1) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
307 | 304, 306 | sylnibr 321 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
308 | 250, 307 | eldifd 3803 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
309 | | eldifi 3955 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → 𝑦 ∈ 𝑆) |
310 | 95 | r19.21bi 3114 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) |
311 | 309, 310 | sylan2 586 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) |
312 | | eldif 3802 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↔ (𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
313 | 154 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → 𝑃 ∈ ℙ) |
314 | 130 | sselda 3821 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ (1...(𝑃 − 1))) |
315 | | eqid 2778 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑦↑(𝑃 − 2)) mod 𝑃) |
316 | 315 | prmdivdiv 15896 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
317 | 313, 314,
316 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → 𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
318 | | oveq1 6929 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → (((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) = (𝑧↑(𝑃 − 2))) |
319 | 318 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
320 | 319 | eqeq2d 2788 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → (𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) ↔ 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
321 | 317, 320 | syl5ibcom 237 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
322 | | oveq1 6929 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) = (((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2))) |
323 | 322 | oveq1d 6937 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
324 | 299 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
325 | 317, 324 | eqeq12d 2793 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → (𝑦 = 𝑧 ↔ ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))) |
326 | 323, 325 | syl5ibr 238 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → 𝑦 = 𝑧)) |
327 | 321, 326 | orim12d 950 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → ((((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) → (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧))) |
328 | | ovex 6954 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ V |
329 | 328 | elpr 4421 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
330 | | vex 3401 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑦 ∈ V |
331 | 330 | elpr 4421 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (𝑦 = 𝑧 ∨ 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
332 | | orcom 859 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 = 𝑧 ∨ 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) ↔ (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧)) |
333 | 331, 332 | bitri 267 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧)) |
334 | 327, 329,
333 | 3imtr4g 288 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
335 | 334 | con3d 150 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → (¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
336 | 335 | impr 448 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ (𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
337 | 312, 336 | sylan2b 587 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
338 | 311, 337 | eldifd 3803 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
339 | 338 | ralrimiva 3148 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
340 | 308, 339 | jca 507 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
341 | | eleq2 2848 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
342 | | eleq2 2848 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
343 | 342 | raleqbi1dv 3328 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
344 | 341, 343 | anbi12d 624 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥) ↔ ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) |
345 | 344, 7 | elrab2 3576 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴 ↔ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) |
346 | 249, 340,
345 | sylanbrc 578 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴) |
347 | 244, 246,
346 | rspcdva 3517 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 → ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))) |
348 | 238, 347 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)) |
349 | 229, 348 | eqtrd 2814 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((1 · (𝑇 Σg ( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = (-1 mod 𝑃)) |
350 | 112, 226,
349 | 3eqtrd 2818 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃)) |
351 | 350 | ex 403 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃))) |
352 | 351 | exlimdv 1976 |
. . 3
⊢ (𝜑 → (∃𝑧(𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃))) |
353 | 57, 352 | syl5bi 234 |
. 2
⊢ (𝜑 → (¬ 𝑆 ⊆ {(𝑃 − 1)} → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃))) |
354 | 56, 353 | pm2.61d 172 |
1
⊢ (𝜑 → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃)) |