| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → 𝑆 ⊆ {(𝑃 − 1)}) |
| 2 | | wilthlem2.s |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ 𝐴) |
| 3 | | eleq2 2830 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑆 → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ 𝑆)) |
| 4 | | eleq2 2830 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑆 → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)) |
| 5 | 4 | raleqbi1dv 3338 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑆 → (∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)) |
| 6 | 3, 5 | anbi12d 632 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑆 → (((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥) ↔ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))) |
| 7 | | wilthlem.a |
. . . . . . . . . . . . . . 15
⊢ 𝐴 = {𝑥 ∈ 𝒫 (1...(𝑃 − 1)) ∣ ((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥)} |
| 8 | 6, 7 | elrab2 3695 |
. . . . . . . . . . . . . 14
⊢ (𝑆 ∈ 𝐴 ↔ (𝑆 ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))) |
| 9 | 2, 8 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑆 ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆))) |
| 10 | 9 | simprd 495 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 − 1) ∈ 𝑆 ∧ ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)) |
| 11 | 10 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 − 1) ∈ 𝑆) |
| 12 | 11 | snssd 4809 |
. . . . . . . . . 10
⊢ (𝜑 → {(𝑃 − 1)} ⊆ 𝑆) |
| 13 | 12 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → {(𝑃 − 1)} ⊆ 𝑆) |
| 14 | 1, 13 | eqssd 4001 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → 𝑆 = {(𝑃 − 1)}) |
| 15 | 14 | reseq2d 5997 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → ( I ↾ 𝑆) = ( I ↾ {(𝑃 − 1)})) |
| 16 | | mptresid 6069 |
. . . . . . 7
⊢ ( I
↾ {(𝑃 − 1)}) =
(𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧) |
| 17 | 15, 16 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → ( I ↾ 𝑆) = (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) |
| 18 | 17 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → (𝑇 Σg ( I ↾
𝑆)) = (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧))) |
| 19 | 18 | oveq1d 7446 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃)) |
| 20 | | wilthlem2.p |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℙ) |
| 21 | | prmnn 16711 |
. . . . . . . . . . . 12
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
| 22 | 20, 21 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ℕ) |
| 23 | 22 | nncnd 12282 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℂ) |
| 24 | | ax-1cn 11213 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
| 25 | | negsub 11557 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℂ ∧ 1 ∈
ℂ) → (𝑃 + -1) =
(𝑃 −
1)) |
| 26 | 23, 24, 25 | sylancl 586 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 + -1) = (𝑃 − 1)) |
| 27 | | neg1cn 12380 |
. . . . . . . . . 10
⊢ -1 ∈
ℂ |
| 28 | | addcom 11447 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℂ ∧ -1 ∈
ℂ) → (𝑃 + -1) =
(-1 + 𝑃)) |
| 29 | 23, 27, 28 | sylancl 586 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 + -1) = (-1 + 𝑃)) |
| 30 | 26, 29 | eqtr3d 2779 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 − 1) = (-1 + 𝑃)) |
| 31 | | cnring 21403 |
. . . . . . . . . 10
⊢
ℂfld ∈ Ring |
| 32 | | wilthlem.t |
. . . . . . . . . . 11
⊢ 𝑇 =
(mulGrp‘ℂfld) |
| 33 | 32 | ringmgp 20236 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → 𝑇 ∈ Mnd) |
| 34 | 31, 33 | mp1i 13 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ Mnd) |
| 35 | | nnm1nn0 12567 |
. . . . . . . . . . 11
⊢ (𝑃 ∈ ℕ → (𝑃 − 1) ∈
ℕ0) |
| 36 | 22, 35 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 − 1) ∈
ℕ0) |
| 37 | 36 | nn0cnd 12589 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 − 1) ∈ ℂ) |
| 38 | | cnfldbas 21368 |
. . . . . . . . . . 11
⊢ ℂ =
(Base‘ℂfld) |
| 39 | 32, 38 | mgpbas 20142 |
. . . . . . . . . 10
⊢ ℂ =
(Base‘𝑇) |
| 40 | | id 22 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑃 − 1) → 𝑧 = (𝑃 − 1)) |
| 41 | 39, 40 | gsumsn 19972 |
. . . . . . . . 9
⊢ ((𝑇 ∈ Mnd ∧ (𝑃 − 1) ∈ ℂ ∧
(𝑃 − 1) ∈
ℂ) → (𝑇
Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (𝑃 − 1)) |
| 42 | 34, 37, 37, 41 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (𝑃 − 1)) |
| 43 | 23 | mullidd 11279 |
. . . . . . . . 9
⊢ (𝜑 → (1 · 𝑃) = 𝑃) |
| 44 | 43 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝜑 → (-1 + (1 · 𝑃)) = (-1 + 𝑃)) |
| 45 | 30, 42, 44 | 3eqtr4d 2787 |
. . . . . . 7
⊢ (𝜑 → (𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) = (-1 + (1 · 𝑃))) |
| 46 | 45 | oveq1d 7446 |
. . . . . 6
⊢ (𝜑 → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = ((-1 + (1 · 𝑃)) mod 𝑃)) |
| 47 | | neg1rr 12381 |
. . . . . . . 8
⊢ -1 ∈
ℝ |
| 48 | 47 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → -1 ∈
ℝ) |
| 49 | 22 | nnrpd 13075 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈
ℝ+) |
| 50 | | 1zzd 12648 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
| 51 | | modcyc 13946 |
. . . . . . 7
⊢ ((-1
∈ ℝ ∧ 𝑃
∈ ℝ+ ∧ 1 ∈ ℤ) → ((-1 + (1 ·
𝑃)) mod 𝑃) = (-1 mod 𝑃)) |
| 52 | 48, 49, 50, 51 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ((-1 + (1 · 𝑃)) mod 𝑃) = (-1 mod 𝑃)) |
| 53 | 46, 52 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃)) |
| 54 | 53 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg (𝑧 ∈ {(𝑃 − 1)} ↦ 𝑧)) mod 𝑃) = (-1 mod 𝑃)) |
| 55 | 19, 54 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ⊆ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃)) |
| 56 | 55 | ex 412 |
. 2
⊢ (𝜑 → (𝑆 ⊆ {(𝑃 − 1)} → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃))) |
| 57 | | nss 4048 |
. . 3
⊢ (¬
𝑆 ⊆ {(𝑃 − 1)} ↔ ∃𝑧(𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) |
| 58 | | cnfld1 21406 |
. . . . . . . . . 10
⊢ 1 =
(1r‘ℂfld) |
| 59 | 32, 58 | ringidval 20180 |
. . . . . . . . 9
⊢ 1 =
(0g‘𝑇) |
| 60 | | cnfldmul 21372 |
. . . . . . . . . 10
⊢ ·
= (.r‘ℂfld) |
| 61 | 32, 60 | mgpplusg 20141 |
. . . . . . . . 9
⊢ ·
= (+g‘𝑇) |
| 62 | | cncrng 21401 |
. . . . . . . . . . 11
⊢
ℂfld ∈ CRing |
| 63 | 32 | crngmgp 20238 |
. . . . . . . . . . 11
⊢
(ℂfld ∈ CRing → 𝑇 ∈ CMnd) |
| 64 | 62, 63 | ax-mp 5 |
. . . . . . . . . 10
⊢ 𝑇 ∈ CMnd |
| 65 | 64 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑇 ∈ CMnd) |
| 66 | 2 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ∈ 𝐴) |
| 67 | | f1oi 6886 |
. . . . . . . . . . . 12
⊢ ( I
↾ 𝑆):𝑆–1-1-onto→𝑆 |
| 68 | | f1of 6848 |
. . . . . . . . . . . 12
⊢ (( I
↾ 𝑆):𝑆–1-1-onto→𝑆 → ( I ↾ 𝑆):𝑆⟶𝑆) |
| 69 | 67, 68 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ( I
↾ 𝑆):𝑆⟶𝑆 |
| 70 | 9 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ 𝒫 (1...(𝑃 − 1))) |
| 71 | 70 | elpwid 4609 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 ⊆ (1...(𝑃 − 1))) |
| 72 | | fzssz 13566 |
. . . . . . . . . . . . 13
⊢
(1...(𝑃 − 1))
⊆ ℤ |
| 73 | 71, 72 | sstrdi 3996 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ⊆ ℤ) |
| 74 | | zsscn 12621 |
. . . . . . . . . . . 12
⊢ ℤ
⊆ ℂ |
| 75 | 73, 74 | sstrdi 3996 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
| 76 | | fss 6752 |
. . . . . . . . . . 11
⊢ ((( I
↾ 𝑆):𝑆⟶𝑆 ∧ 𝑆 ⊆ ℂ) → ( I ↾ 𝑆):𝑆⟶ℂ) |
| 77 | 69, 75, 76 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → ( I ↾ 𝑆):𝑆⟶ℂ) |
| 78 | 77 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ 𝑆):𝑆⟶ℂ) |
| 79 | | fzfi 14013 |
. . . . . . . . . . . 12
⊢
(1...(𝑃 − 1))
∈ Fin |
| 80 | | ssfi 9213 |
. . . . . . . . . . . 12
⊢
(((1...(𝑃 −
1)) ∈ Fin ∧ 𝑆
⊆ (1...(𝑃 −
1))) → 𝑆 ∈
Fin) |
| 81 | 79, 71, 80 | sylancr 587 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ Fin) |
| 82 | | 1ex 11257 |
. . . . . . . . . . . 12
⊢ 1 ∈
V |
| 83 | 82 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
V) |
| 84 | 77, 81, 83 | fdmfifsupp 9415 |
. . . . . . . . . 10
⊢ (𝜑 → ( I ↾ 𝑆) finSupp 1) |
| 85 | 84 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ 𝑆) finSupp 1) |
| 86 | | disjdif 4472 |
. . . . . . . . . 10
⊢ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∩ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ∅ |
| 87 | 86 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∩ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ∅) |
| 88 | | undif2 4477 |
. . . . . . . . . 10
⊢ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) |
| 89 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ 𝑆) |
| 90 | | oveq1 7438 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑧 → (𝑦↑(𝑃 − 2)) = (𝑧↑(𝑃 − 2))) |
| 91 | 90 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = 𝑧 → ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
| 92 | 91 | eleq1d 2826 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆 ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆)) |
| 93 | 10 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) |
| 94 | 93 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑦 ∈ 𝑆 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) |
| 95 | 92, 94, 89 | rspcdva 3623 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) |
| 96 | 89, 95 | prssd 4822 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆) |
| 97 | | ssequn1 4186 |
. . . . . . . . . . 11
⊢ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆 ↔ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) = 𝑆) |
| 98 | 96, 97 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ 𝑆) = 𝑆) |
| 99 | 88, 98 | eqtr2id 2790 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 = ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∪ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
| 100 | 39, 59, 61, 65, 66, 78, 85, 87, 99 | gsumsplit 19946 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
𝑆)) = ((𝑇 Σg (( I ↾
𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg (( I ↾
𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))) |
| 101 | 96 | resabs1d 6026 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (( I ↾ 𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 102 | 101 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (( I ↾
𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
| 103 | | difss 4136 |
. . . . . . . . . . . 12
⊢ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ 𝑆 |
| 104 | | resabs1 6024 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ 𝑆 → (( I ↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
| 105 | 103, 104 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (( I
↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 106 | 105 | oveq2i 7442 |
. . . . . . . . . 10
⊢ (𝑇 Σg (( I
↾ 𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) = (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
| 107 | 106 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (( I ↾
𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) = (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) |
| 108 | 102, 107 | oveq12d 7449 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg (( I ↾
𝑆) ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg (( I ↾
𝑆) ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) = ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))) |
| 109 | 100, 108 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
𝑆)) = ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))))) |
| 110 | 109 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃)) |
| 111 | | prfi 9363 |
. . . . . . . . . 10
⊢ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∈ Fin |
| 112 | 111 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∈ Fin) |
| 113 | | zsubrg 21438 |
. . . . . . . . . 10
⊢ ℤ
∈ (SubRing‘ℂfld) |
| 114 | 32 | subrgsubm 20585 |
. . . . . . . . . 10
⊢ (ℤ
∈ (SubRing‘ℂfld) → ℤ ∈
(SubMnd‘𝑇)) |
| 115 | 113, 114 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ℤ ∈
(SubMnd‘𝑇)) |
| 116 | | f1oi 6886 |
. . . . . . . . . . 11
⊢ ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}–1-1-onto→{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} |
| 117 | | f1of 6848 |
. . . . . . . . . . 11
⊢ (( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}–1-1-onto→{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 118 | 116, 117 | ax-mp 5 |
. . . . . . . . . 10
⊢ ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} |
| 119 | 73 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ ℤ) |
| 120 | 96, 119 | sstrd 3994 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ ℤ) |
| 121 | | fss 6752 |
. . . . . . . . . 10
⊢ ((( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ∧ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ ℤ) → ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶ℤ) |
| 122 | 118, 120,
121 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}):{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}⟶ℤ) |
| 123 | 82 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈
V) |
| 124 | 122, 112,
123 | fdmfifsupp 9415 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) finSupp 1) |
| 125 | 59, 65, 112, 115, 122, 124 | gsumsubmcl 19937 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℤ) |
| 126 | 125 | zred 12722 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) ∈ ℝ) |
| 127 | | 1red 11262 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈
ℝ) |
| 128 | 71 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ (1...(𝑃 − 1))) |
| 129 | 128 | ssdifssd 4147 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1))) |
| 130 | | ssfi 9213 |
. . . . . . . . 9
⊢
(((1...(𝑃 −
1)) ∈ Fin ∧ (𝑆
∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1))) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ Fin) |
| 131 | 79, 129, 130 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ Fin) |
| 132 | | f1oi 6886 |
. . . . . . . . . 10
⊢ ( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})–1-1-onto→(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 133 | | f1of 6848 |
. . . . . . . . . 10
⊢ (( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})–1-1-onto→(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 134 | 132, 133 | ax-mp 5 |
. . . . . . . . 9
⊢ ( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 135 | 119 | ssdifssd 4147 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ ℤ) |
| 136 | | fss 6752 |
. . . . . . . . 9
⊢ ((( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ ℤ) → ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶ℤ) |
| 137 | 134, 135,
136 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})):(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})⟶ℤ) |
| 138 | 137, 131,
123 | fdmfifsupp 9415 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) finSupp 1) |
| 139 | 59, 65, 131, 115, 137, 138 | gsumsubmcl 19937 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℤ) |
| 140 | 49 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈
ℝ+) |
| 141 | 34 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑇 ∈ Mnd) |
| 142 | 75 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑆 ⊆ ℂ) |
| 143 | 142, 89 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℂ) |
| 144 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) |
| 145 | 39, 144 | gsumsn 19972 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ Mnd ∧ 𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑇 Σg
(𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧) |
| 146 | 141, 143,
143, 145 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧) |
| 147 | 146 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧) |
| 148 | | mptresid 6069 |
. . . . . . . . . . . 12
⊢ ( I
↾ {𝑧}) = (𝑤 ∈ {𝑧} ↦ 𝑤) |
| 149 | | dfsn2 4639 |
. . . . . . . . . . . . . 14
⊢ {𝑧} = {𝑧, 𝑧} |
| 150 | | animorrl 983 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))) |
| 151 | 20 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℙ) |
| 152 | 128, 89 | sseldd 3984 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ (1...(𝑃 − 1))) |
| 153 | | wilthlem1 27111 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → (𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1)))) |
| 154 | 151, 152,
153 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1)))) |
| 155 | 154 | biimpar 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))) → 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
| 156 | 150, 155 | syldan 591 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
| 157 | 156 | preq2d 4740 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → {𝑧, 𝑧} = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 158 | 149, 157 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → {𝑧} = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 159 | 158 | reseq2d 5997 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → ( I ↾ {𝑧}) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 160 | 148, 159 | eqtr3id 2791 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑤 ∈ {𝑧} ↦ 𝑤) = ( I ↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 161 | 160 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
| 162 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → 𝑧 = 1) |
| 163 | 147, 161,
162 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = 1) |
| 164 | 163 | oveq1d 7446 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 = 1) → ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃)) |
| 165 | | df-pr 4629 |
. . . . . . . . . . . . . . 15
⊢ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} = ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 166 | 165 | reseq2i 5994 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ( I ↾ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 167 | | mptresid 6069 |
. . . . . . . . . . . . . 14
⊢ ( I
↾ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤) |
| 168 | 166, 167 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤) |
| 169 | 168 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ (𝑇 Σg ( I
↾ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑇 Σg (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)) |
| 170 | 64 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → 𝑇 ∈ CMnd) |
| 171 | | snfi 9083 |
. . . . . . . . . . . . . 14
⊢ {𝑧} ∈ Fin |
| 172 | 171 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → {𝑧} ∈ Fin) |
| 173 | | elsni 4643 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 ∈ {𝑧} → 𝑤 = 𝑧) |
| 174 | 173 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑤 = 𝑧) |
| 175 | 143 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑧 ∈ ℂ) |
| 176 | 174, 175 | eqeltrd 2841 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑤 ∈ {𝑧}) → 𝑤 ∈ ℂ) |
| 177 | 176 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) ∧ 𝑤 ∈ {𝑧}) → 𝑤 ∈ ℂ) |
| 178 | 142, 95 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℂ) |
| 179 | 178 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℂ) |
| 180 | | simprr 773 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑧 ∈ {(𝑃 − 1)}) |
| 181 | | velsn 4642 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ {(𝑃 − 1)} ↔ 𝑧 = (𝑃 − 1)) |
| 182 | 180, 181 | sylnib 328 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑧 = (𝑃 − 1)) |
| 183 | | biorf 937 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑧 = (𝑃 − 1) → (𝑧 = 1 ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1))) |
| 184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = 1 ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1))) |
| 185 | | ovex 7464 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ V |
| 186 | 185 | elsn 4641 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) = 𝑧) |
| 187 | | eqcom 2744 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑧↑(𝑃 − 2)) mod 𝑃) = 𝑧 ↔ 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
| 188 | 186, 187 | bitri 275 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ 𝑧 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
| 189 | | orcom 871 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 = (𝑃 − 1) ∨ 𝑧 = 1) ↔ (𝑧 = 1 ∨ 𝑧 = (𝑃 − 1))) |
| 190 | 154, 188,
189 | 3bitr4g 314 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧} ↔ (𝑧 = (𝑃 − 1) ∨ 𝑧 = 1))) |
| 191 | 184, 190 | bitr4d 282 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 = 1 ↔ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧})) |
| 192 | 191 | necon3abid 2977 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 ≠ 1 ↔ ¬ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧})) |
| 193 | 192 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ¬ ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧}) |
| 194 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ((𝑧↑(𝑃 − 2)) mod 𝑃) → 𝑤 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
| 195 | 39, 61, 170, 172, 177, 179, 193, 179, 194 | gsumunsn 19978 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg (𝑤 ∈ ({𝑧} ∪ {((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↦ 𝑤)) = ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 196 | 169, 195 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 197 | 146 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) = 𝑧) |
| 198 | 197 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg (𝑤 ∈ {𝑧} ↦ 𝑤)) · ((𝑧↑(𝑃 − 2)) mod 𝑃)) = (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 199 | 196, 198 | eqtrd 2777 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → (𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) = (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 200 | 199 | oveq1d 7446 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃)) |
| 201 | 152 | elfzelzd 13565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℤ) |
| 202 | 22 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℕ) |
| 203 | | fzm1ndvds 16359 |
. . . . . . . . . . . . . 14
⊢ ((𝑃 ∈ ℕ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ 𝑧) |
| 204 | 202, 152,
203 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑃 ∥ 𝑧) |
| 205 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ ((𝑧↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) |
| 206 | 205 | prmdiv 16822 |
. . . . . . . . . . . . 13
⊢ ((𝑃 ∈ ℙ ∧ 𝑧 ∈ ℤ ∧ ¬
𝑃 ∥ 𝑧) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))) |
| 207 | 151, 201,
204, 206 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))) |
| 208 | 207 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1)) |
| 209 | | elfznn 13593 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (1...(𝑃 − 1)) → 𝑧 ∈ ℕ) |
| 210 | 152, 209 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 ∈ ℕ) |
| 211 | 128, 95 | sseldd 3984 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1))) |
| 212 | | elfznn 13593 |
. . . . . . . . . . . . . . 15
⊢ (((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ (1...(𝑃 − 1)) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℕ) |
| 213 | 211, 212 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧↑(𝑃 − 2)) mod 𝑃) ∈ ℕ) |
| 214 | 210, 213 | nnmulcld 12319 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℕ) |
| 215 | 214 | nnzd 12640 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℤ) |
| 216 | | 1zzd 12648 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈
ℤ) |
| 217 | | moddvds 16301 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∈ ℕ ∧ (𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) ∈ ℤ ∧ 1 ∈ ℤ)
→ (((𝑧 ·
((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))) |
| 218 | 202, 215,
216, 217 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃) ↔ 𝑃 ∥ ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) − 1))) |
| 219 | 208, 218 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃)) |
| 220 | 219 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑧 · ((𝑧↑(𝑃 − 2)) mod 𝑃)) mod 𝑃) = (1 mod 𝑃)) |
| 221 | 200, 220 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑧 ≠ 1) → ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃)) |
| 222 | 164, 221 | pm2.61dane 3029 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) mod 𝑃) = (1 mod 𝑃)) |
| 223 | | modmul1 13965 |
. . . . . . 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 𝑃)) |
| 224 | 126, 127,
139, 140, 222, 223 | syl221anc 1383 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑇 Σg ( I ↾
{𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((1 · (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃)) |
| 225 | 139 | zcnd 12723 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) ∈ ℂ) |
| 226 | 225 | mullidd 11279 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (1 · (𝑇 Σg ( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) = (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) |
| 227 | 226 | oveq1d 7446 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((1 · (𝑇 Σg ( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃)) |
| 228 | | sseqin2 4223 |
. . . . . . . . . . 11
⊢ ({𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ⊆ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 229 | 96, 228 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 230 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
| 231 | 230 | prnz 4777 |
. . . . . . . . . . 11
⊢ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ≠ ∅ |
| 232 | 231 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ≠ ∅) |
| 233 | 229, 232 | eqnetrd 3008 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ≠ ∅) |
| 234 | | disj4 4459 |
. . . . . . . . . 10
⊢ ((𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) = ∅ ↔ ¬ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆) |
| 235 | 234 | necon2abii 2991 |
. . . . . . . . 9
⊢ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 ↔ (𝑆 ∩ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ≠ ∅) |
| 236 | 233, 235 | sylibr 234 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆) |
| 237 | | psseq1 4090 |
. . . . . . . . . 10
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (𝑠 ⊊ 𝑆 ↔ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆)) |
| 238 | | reseq2 5992 |
. . . . . . . . . . . . 13
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ( I ↾ 𝑠) = ( I ↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
| 239 | 238 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (𝑇 Σg ( I ↾
𝑠)) = (𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) |
| 240 | 239 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑇 Σg ( I ↾
𝑠)) mod 𝑃) = ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃)) |
| 241 | 240 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑇 Σg ( I ↾
𝑠)) mod 𝑃) = (-1 mod 𝑃) ↔ ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))) |
| 242 | 237, 241 | imbi12d 344 |
. . . . . . . . 9
⊢ (𝑠 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑠 ⊊ 𝑆 → ((𝑇 Σg ( I ↾
𝑠)) mod 𝑃) = (-1 mod 𝑃)) ↔ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 → ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)))) |
| 243 | | wilthlem2.r |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑆 → ((𝑇 Σg ( I ↾
𝑠)) mod 𝑃) = (-1 mod 𝑃))) |
| 244 | 243 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑠 ∈ 𝐴 (𝑠 ⊊ 𝑆 → ((𝑇 Σg ( I ↾
𝑠)) mod 𝑃) = (-1 mod 𝑃))) |
| 245 | | ovex 7464 |
. . . . . . . . . . . 12
⊢
(1...(𝑃 − 1))
∈ V |
| 246 | 245 | elpw2 5334 |
. . . . . . . . . . 11
⊢ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)) ↔ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊆ (1...(𝑃 − 1))) |
| 247 | 129, 246 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1))) |
| 248 | 11 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ 𝑆) |
| 249 | | eqcom 2744 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑃 − 1) ↔ (𝑃 − 1) = 𝑧) |
| 250 | 181, 249 | bitri 275 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ {(𝑃 − 1)} ↔ (𝑃 − 1) = 𝑧) |
| 251 | 180, 250 | sylnib 328 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) = 𝑧) |
| 252 | | oveq1 7438 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → ((𝑃 − 1)↑(𝑃 − 2)) = (((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2))) |
| 253 | 252 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
| 254 | 202, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈
ℕ0) |
| 255 | | nn0uz 12920 |
. . . . . . . . . . . . . . . . . . . 20
⊢
ℕ0 = (ℤ≥‘0) |
| 256 | 254, 255 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈
(ℤ≥‘0)) |
| 257 | | eluzfz2 13572 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 − 1) ∈
(ℤ≥‘0) → (𝑃 − 1) ∈ (0...(𝑃 − 1))) |
| 258 | 256, 257 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (0...(𝑃 − 1))) |
| 259 | | prmz 16712 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
| 260 | 151, 259 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℤ) |
| 261 | 119, 248 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℤ) |
| 262 | | 1z 12647 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℤ |
| 263 | | zsubcl 12659 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃 − 1) ∈ ℤ ∧
1 ∈ ℤ) → ((𝑃 − 1) − 1) ∈
ℤ) |
| 264 | 261, 262,
263 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) − 1) ∈
ℤ) |
| 265 | | dvdsmul1 16315 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℤ ∧ ((𝑃 − 1) − 1) ∈
ℤ) → 𝑃 ∥
(𝑃 · ((𝑃 − 1) −
1))) |
| 266 | 260, 264,
265 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ (𝑃 · ((𝑃 − 1) − 1))) |
| 267 | 202 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∈ ℂ) |
| 268 | 264 | zcnd 12723 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) − 1) ∈
ℂ) |
| 269 | 267, 268 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) ∈
ℂ) |
| 270 | | 1cnd 11256 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 1 ∈
ℂ) |
| 271 | 254 | nn0cnd 12589 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ ℂ) |
| 272 | 267, 270,
271 | subdird 11720 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) · (𝑃 − 1)) = ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1)))) |
| 273 | 267, 271 | mulcld 11281 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · (𝑃 − 1)) ∈
ℂ) |
| 274 | 273, 267,
270 | subsubd 11648 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (𝑃 − 1)) = (((𝑃 · (𝑃 − 1)) − 𝑃) + 1)) |
| 275 | 271 | mullidd 11279 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (1 · (𝑃 − 1)) = (𝑃 − 1)) |
| 276 | 275 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))) = ((𝑃 · (𝑃 − 1)) − (𝑃 − 1))) |
| 277 | 267, 271 | muls1d 11723 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 · ((𝑃 − 1) − 1)) = ((𝑃 · (𝑃 − 1)) − 𝑃)) |
| 278 | 277 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · ((𝑃 − 1) − 1)) + 1) = (((𝑃 · (𝑃 − 1)) − 𝑃) + 1)) |
| 279 | 274, 276,
278 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 · (𝑃 − 1)) − (1 · (𝑃 − 1))) = ((𝑃 · ((𝑃 − 1) − 1)) +
1)) |
| 280 | 272, 279 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) · (𝑃 − 1)) = ((𝑃 · ((𝑃 − 1) − 1)) +
1)) |
| 281 | 269, 270,
280 | mvrraddd 11675 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) · (𝑃 − 1)) − 1) = (𝑃 · ((𝑃 − 1) − 1))) |
| 282 | 266, 281 | breqtrrd 5171 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) |
| 283 | 128, 248 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (1...(𝑃 − 1))) |
| 284 | | fzm1ndvds 16359 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℕ ∧ (𝑃 − 1) ∈ (1...(𝑃 − 1))) → ¬ 𝑃 ∥ (𝑃 − 1)) |
| 285 | 202, 283,
284 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ 𝑃 ∥ (𝑃 − 1)) |
| 286 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) |
| 287 | 286 | prmdiveq 16823 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 − 1) ∈ ℤ ∧
¬ 𝑃 ∥ (𝑃 − 1)) → (((𝑃 − 1) ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) ↔ (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃))) |
| 288 | 151, 261,
285, 287 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (((𝑃 − 1) ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ (((𝑃 − 1) · (𝑃 − 1)) − 1)) ↔ (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃))) |
| 289 | 258, 282,
288 | mpbi2and 712 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) = (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃)) |
| 290 | 205 | prmdivdiv 16824 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑃 ∈ ℙ ∧ 𝑧 ∈ (1...(𝑃 − 1))) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
| 291 | 151, 152,
290 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
| 292 | 289, 291 | eqeq12d 2753 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) = 𝑧 ↔ (((𝑃 − 1)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))) |
| 293 | 253, 292 | imbitrrid 246 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (𝑃 − 1) = 𝑧)) |
| 294 | 251, 293 | mtod 198 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
| 295 | | ioran 986 |
. . . . . . . . . . . . . 14
⊢ (¬
((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) ↔ (¬ (𝑃 − 1) = 𝑧 ∧ ¬ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 296 | 251, 294,
295 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 297 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢ (𝑃 − 1) ∈
V |
| 298 | 297 | elpr 4650 |
. . . . . . . . . . . . 13
⊢ ((𝑃 − 1) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ ((𝑃 − 1) = 𝑧 ∨ (𝑃 − 1) = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 299 | 296, 298 | sylnibr 329 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ¬ (𝑃 − 1) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 300 | 248, 299 | eldifd 3962 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 301 | | eldifi 4131 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → 𝑦 ∈ 𝑆) |
| 302 | 94 | r19.21bi 3251 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) |
| 303 | 301, 302 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑆) |
| 304 | | eldif 3961 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ↔ (𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 305 | 151 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → 𝑃 ∈ ℙ) |
| 306 | 128 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ (1...(𝑃 − 1))) |
| 307 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑦↑(𝑃 − 2)) mod 𝑃) |
| 308 | 307 | prmdivdiv 16824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑃 ∈ ℙ ∧ 𝑦 ∈ (1...(𝑃 − 1))) → 𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
| 309 | 305, 306,
308 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → 𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
| 310 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → (((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) = (𝑧↑(𝑃 − 2))) |
| 311 | 310 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) |
| 312 | 311 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → (𝑦 = ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) ↔ 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 313 | 309, 312 | syl5ibcom 245 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 → 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 314 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → (((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) = (((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2))) |
| 315 | 314 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
| 316 | 291 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → 𝑧 = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃)) |
| 317 | 309, 316 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → (𝑦 = 𝑧 ↔ ((((𝑦↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃) = ((((𝑧↑(𝑃 − 2)) mod 𝑃)↑(𝑃 − 2)) mod 𝑃))) |
| 318 | 315, 317 | imbitrrid 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃) → 𝑦 = 𝑧)) |
| 319 | 313, 318 | orim12d 967 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → ((((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃)) → (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧))) |
| 320 | | ovex 7464 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ V |
| 321 | 320 | elpr 4650 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (((𝑦↑(𝑃 − 2)) mod 𝑃) = 𝑧 ∨ ((𝑦↑(𝑃 − 2)) mod 𝑃) = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 322 | | vex 3484 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑦 ∈ V |
| 323 | 322 | elpr 4650 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (𝑦 = 𝑧 ∨ 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃))) |
| 324 | | orcom 871 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 = 𝑧 ∨ 𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃)) ↔ (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧)) |
| 325 | 323, 324 | bitri 275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} ↔ (𝑦 = ((𝑧↑(𝑃 − 2)) mod 𝑃) ∨ 𝑦 = 𝑧)) |
| 326 | 319, 321,
325 | 3imtr4g 296 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 327 | 326 | con3d 152 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ 𝑆) → (¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)} → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 328 | 327 | impr 454 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ (𝑦 ∈ 𝑆 ∧ ¬ 𝑦 ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 329 | 304, 328 | sylan2b 594 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ¬ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) |
| 330 | 303, 329 | eldifd 3962 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) ∧ 𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) → ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 331 | 330 | ralrimiva 3146 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})) |
| 332 | 300, 331 | jca 511 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
| 333 | | eleq2 2830 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → ((𝑃 − 1) ∈ 𝑥 ↔ (𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
| 334 | | eleq2 2830 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
| 335 | 334 | raleqbi1dv 3338 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥 ↔ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) |
| 336 | 333, 335 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) → (((𝑃 − 1) ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ 𝑥) ↔ ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) |
| 337 | 336, 7 | elrab2 3695 |
. . . . . . . . . 10
⊢ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴 ↔ ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝒫 (1...(𝑃 − 1)) ∧ ((𝑃 − 1) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∧ ∀𝑦 ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})((𝑦↑(𝑃 − 2)) mod 𝑃) ∈ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) |
| 338 | 247, 332,
337 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ∈ 𝐴) |
| 339 | 242, 244,
338 | rspcdva 3623 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}) ⊊ 𝑆 → ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃))) |
| 340 | 236, 339 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾
(𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)}))) mod 𝑃) = (-1 mod 𝑃)) |
| 341 | 227, 340 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((1 · (𝑇 Σg ( I
↾ (𝑆 ∖ {𝑧, ((𝑧↑(𝑃 − 2)) mod 𝑃)})))) mod 𝑃) = (-1 mod 𝑃)) |
| 342 | 110, 224,
341 | 3eqtrd 2781 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)})) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃)) |
| 343 | 342 | ex 412 |
. . . 4
⊢ (𝜑 → ((𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃))) |
| 344 | 343 | exlimdv 1933 |
. . 3
⊢ (𝜑 → (∃𝑧(𝑧 ∈ 𝑆 ∧ ¬ 𝑧 ∈ {(𝑃 − 1)}) → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃))) |
| 345 | 57, 344 | biimtrid 242 |
. 2
⊢ (𝜑 → (¬ 𝑆 ⊆ {(𝑃 − 1)} → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃))) |
| 346 | 56, 345 | pm2.61d 179 |
1
⊢ (𝜑 → ((𝑇 Σg ( I ↾
𝑆)) mod 𝑃) = (-1 mod 𝑃)) |