Step | Hyp | Ref
| Expression |
1 | | snfi 7923 |
. . . 4
⊢ {0}
∈ Fin |
2 | | cnex 9896 |
. . . . . . . . 9
⊢ ℂ
∈ V |
3 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ℂ
∈ V) |
4 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝑧↑(ϕ‘𝑁)) ∈ V |
5 | 4 | a1i 11 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ) → (𝑧↑(ϕ‘𝑁)) ∈ V) |
6 | | 1cnd 9935 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ) → 1 ∈
ℂ) |
7 | | eqidd 2611 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) = (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁)))) |
8 | | fconstmpt 5085 |
. . . . . . . . 9
⊢ (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1) |
9 | 8 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1)) |
10 | 3, 5, 6, 7, 9 | offval2 6812 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘𝑓
− (ℂ × {1})) = (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))) |
11 | | ssid 3587 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
12 | 11 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ℂ
⊆ ℂ) |
13 | | 1cnd 9935 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
14 | | phicl 15312 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) ∈
ℕ) |
15 | 14 | nnnn0d 11228 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) ∈
ℕ0) |
16 | | plypow 23765 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ ∧ (ϕ‘𝑁) ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈
(Poly‘ℂ)) |
17 | 12, 13, 15, 16 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈
(Poly‘ℂ)) |
18 | | ax-1cn 9873 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
19 | | plyconst 23766 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ) → (ℂ × {1}) ∈
(Poly‘ℂ)) |
20 | 11, 18, 19 | mp2an 704 |
. . . . . . . 8
⊢ (ℂ
× {1}) ∈ (Poly‘ℂ) |
21 | | plysubcl 23782 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈ (Poly‘ℂ)
∧ (ℂ × {1}) ∈ (Poly‘ℂ)) → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘𝑓
− (ℂ × {1})) ∈ (Poly‘ℂ)) |
22 | 17, 20, 21 | sylancl 693 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘𝑓
− (ℂ × {1})) ∈ (Poly‘ℂ)) |
23 | 10, 22 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ∈
(Poly‘ℂ)) |
24 | | 0cn 9911 |
. . . . . . 7
⊢ 0 ∈
ℂ |
25 | | neg1ne0 11003 |
. . . . . . . 8
⊢ -1 ≠
0 |
26 | 14 | 0expd 12886 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(0↑(ϕ‘𝑁)) =
0) |
27 | 26 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
((0↑(ϕ‘𝑁))
− 1) = (0 − 1)) |
28 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 0 → (𝑧↑(ϕ‘𝑁)) = (0↑(ϕ‘𝑁))) |
29 | 28 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝑧 = 0 → ((𝑧↑(ϕ‘𝑁)) − 1) = ((0↑(ϕ‘𝑁)) − 1)) |
30 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) = (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) |
31 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
((0↑(ϕ‘𝑁)) − 1) ∈ V |
32 | 29, 30, 31 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (0 ∈
ℂ → ((𝑧 ∈
ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
((0↑(ϕ‘𝑁))
− 1)) |
33 | 24, 32 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
((0↑(ϕ‘𝑁))
− 1) |
34 | | df-neg 10148 |
. . . . . . . . . 10
⊢ -1 = (0
− 1) |
35 | 27, 33, 34 | 3eqtr4g 2669 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
-1) |
36 | 35 | neeq1d 2841 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0
↔ -1 ≠ 0)) |
37 | 25, 36 | mpbiri 247 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠
0) |
38 | | ne0p 23767 |
. . . . . . 7
⊢ ((0
∈ ℂ ∧ ((𝑧
∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0) →
(𝑧 ∈ ℂ ↦
((𝑧↑(ϕ‘𝑁)) − 1)) ≠
0𝑝) |
39 | 24, 37, 38 | sylancr 694 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠
0𝑝) |
40 | 30 | mptiniseg 5546 |
. . . . . . . . 9
⊢ (0 ∈
ℂ → (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) = {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}) |
41 | 24, 40 | ax-mp 5 |
. . . . . . . 8
⊢ (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) = {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0} |
42 | 41 | eqcomi 2619 |
. . . . . . 7
⊢ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} = (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) |
43 | 42 | fta1 23867 |
. . . . . 6
⊢ (((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ∈
(Poly‘ℂ) ∧ (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠ 0𝑝)
→ ({𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin ∧
(#‘{𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ≤ (deg‘(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) −
1))))) |
44 | 23, 39, 43 | syl2anc 691 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ({𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin
∧ (#‘{𝑧 ∈
ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ≤ (deg‘(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) −
1))))) |
45 | 44 | simpld 474 |
. . . 4
⊢ (𝑁 ∈ ℕ → {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈
Fin) |
46 | | unfi 8112 |
. . . 4
⊢ (({0}
∈ Fin ∧ {𝑧 ∈
ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin) → ({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈
Fin) |
47 | 1, 45, 46 | sylancr 694 |
. . 3
⊢ (𝑁 ∈ ℕ → ({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈
Fin) |
48 | | eqid 2610 |
. . . 4
⊢
(ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁) |
49 | | eqid 2610 |
. . . 4
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(ℤ/nℤ‘𝑁)) |
50 | 48, 49 | znfi 19727 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Base‘(ℤ/nℤ‘𝑁)) ∈ Fin) |
51 | | mapfi 8145 |
. . 3
⊢ ((({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈ Fin ∧
(Base‘(ℤ/nℤ‘𝑁)) ∈ Fin) → (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin) |
52 | 47, 50, 51 | syl2anc 691 |
. 2
⊢ (𝑁 ∈ ℕ → (({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin) |
53 | | dchrabl.g |
. . . . . . . 8
⊢ 𝐺 = (DChr‘𝑁) |
54 | | dchrfi.b |
. . . . . . . 8
⊢ 𝐷 = (Base‘𝐺) |
55 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ 𝐷) |
56 | 53, 48, 54, 49, 55 | dchrf 24767 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
57 | | ffn 5958 |
. . . . . . 7
⊢ (𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ → 𝑓 Fn
(Base‘(ℤ/nℤ‘𝑁))) |
58 | 56, 57 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓 Fn
(Base‘(ℤ/nℤ‘𝑁))) |
59 | | df-ne 2782 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑥) ≠ 0 ↔ ¬ (𝑓‘𝑥) = 0) |
60 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝑓‘𝑥) ∈ V |
61 | 60 | elsn 4140 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑥) ∈ {0} ↔ (𝑓‘𝑥) = 0) |
62 | 59, 61 | xchbinxr 324 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑥) ≠ 0 ↔ ¬ (𝑓‘𝑥) ∈ {0}) |
63 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) |
64 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘𝑥) ∈ ℂ) |
65 | 56, 63, 64 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ∈ ℂ) |
66 | 53, 48, 54 | dchrmhm 24766 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 ⊆
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) |
67 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑓 ∈ 𝐷) |
68 | 66, 67 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld))) |
69 | 15 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℕ0) |
70 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) |
71 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . 19
⊢
(mulGrp‘(ℤ/nℤ‘𝑁)) =
(mulGrp‘(ℤ/nℤ‘𝑁)) |
72 | 71, 49 | mgpbas 18318 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(mulGrp‘(ℤ/nℤ‘𝑁))) |
73 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(.g‘(mulGrp‘(ℤ/nℤ‘𝑁))) =
(.g‘(mulGrp‘(ℤ/nℤ‘𝑁))) |
74 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
75 | 72, 73, 74 | mhmmulg 17406 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) ∧ (ϕ‘𝑁) ∈ ℕ0 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥))) |
76 | 68, 69, 70, 75 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥))) |
77 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
78 | 48 | zncrng 19712 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ (ℤ/nℤ‘𝑁) ∈ CRing) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ →
(ℤ/nℤ‘𝑁) ∈ CRing) |
80 | | crngring 18381 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((ℤ/nℤ‘𝑁) ∈ CRing →
(ℤ/nℤ‘𝑁) ∈ Ring) |
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(ℤ/nℤ‘𝑁) ∈ Ring) |
82 | 81 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(ℤ/nℤ‘𝑁) ∈ Ring) |
83 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Unit‘(ℤ/nℤ‘𝑁)) |
84 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) =
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) |
85 | 83, 84 | unitgrp 18490 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp) |
86 | 82, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp) |
87 | 48, 83 | znunithash 19732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ →
(#‘(Unit‘(ℤ/nℤ‘𝑁))) = (ϕ‘𝑁)) |
88 | 87, 15 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(#‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0) |
89 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(Unit‘(ℤ/nℤ‘𝑁)) ∈ V |
90 | | hashclb 13011 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈ V →
((Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ↔
(#‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0)) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ↔
(#‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0) |
92 | 88, 91 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ →
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin) |
93 | 92 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin) |
94 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ≠ 0) |
95 | 53, 48, 54, 49, 83, 67, 70 | dchrn0 24775 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((𝑓‘𝑥) ≠ 0 ↔ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) |
96 | 94, 95 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) |
97 | 83, 84 | unitgrpbas 18489 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Base‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
98 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
99 | 97, 98 | oddvds2 17806 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp ∧
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥
(#‘(Unit‘(ℤ/nℤ‘𝑁)))) |
100 | 86, 93, 96, 99 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥
(#‘(Unit‘(ℤ/nℤ‘𝑁)))) |
101 | 87 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(#‘(Unit‘(ℤ/nℤ‘𝑁))) = (ϕ‘𝑁)) |
102 | 100, 101 | breqtrd 4609 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (ϕ‘𝑁)) |
103 | 14 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℕ) |
104 | 103 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℤ) |
105 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
106 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
107 | 97, 98, 105, 106 | oddvds 17789 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)) ∧ (ϕ‘𝑁) ∈ ℤ) →
(((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (ϕ‘𝑁) ↔ ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))))) |
108 | 86, 96, 104, 107 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (ϕ‘𝑁) ↔ ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))))) |
109 | 102, 108 | mpbid 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))) |
110 | 83, 71 | unitsubm 18493 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
(Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁)))) |
111 | 82, 110 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁)))) |
112 | 73, 84, 105 | submmulg 17409 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))) ∧ (ϕ‘𝑁) ∈ ℕ0 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥)) |
113 | 111, 69, 96, 112 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥)) |
114 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1r‘(ℤ/nℤ‘𝑁)) =
(1r‘(ℤ/nℤ‘𝑁)) |
115 | 71, 114 | ringidval 18326 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘(mulGrp‘(ℤ/nℤ‘𝑁))) |
116 | 84, 115 | subm0 17179 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))) →
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))) |
117 | 111, 116 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))) |
118 | 109, 113,
117 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
(1r‘(ℤ/nℤ‘𝑁))) |
119 | 118 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
(𝑓‘(1r‘(ℤ/nℤ‘𝑁)))) |
120 | 76, 119 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = (𝑓‘(1r‘(ℤ/nℤ‘𝑁)))) |
121 | | cnfldexp 19598 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓‘𝑥) ∈ ℂ ∧ (ϕ‘𝑁) ∈ ℕ0)
→ ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) |
122 | 65, 69, 121 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) |
123 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
124 | | cnfld1 19590 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 =
(1r‘ℂfld) |
125 | 123, 124 | ringidval 18326 |
. . . . . . . . . . . . . . . . 17
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
126 | 115, 125 | mhm0 17166 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) → (𝑓‘(1r‘(ℤ/nℤ‘𝑁))) = 1) |
127 | 68, 126 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘(1r‘(ℤ/nℤ‘𝑁))) = 1) |
128 | 120, 122,
127 | 3eqtr3d 2652 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((𝑓‘𝑥)↑(ϕ‘𝑁)) = 1) |
129 | 128 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = (1 −
1)) |
130 | | 1m1e0 10966 |
. . . . . . . . . . . . 13
⊢ (1
− 1) = 0 |
131 | 129, 130 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = 0) |
132 | | oveq1 6556 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑓‘𝑥) → (𝑧↑(ϕ‘𝑁)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) |
133 | 132 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑓‘𝑥) → ((𝑧↑(ϕ‘𝑁)) − 1) = (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1)) |
134 | 133 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑓‘𝑥) → (((𝑧↑(ϕ‘𝑁)) − 1) = 0 ↔ (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = 0)) |
135 | 134 | elrab 3331 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ↔ ((𝑓‘𝑥) ∈ ℂ ∧ (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = 0)) |
136 | 65, 131, 135 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) |
137 | 136 | expr 641 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((𝑓‘𝑥) ≠ 0 → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
138 | 62, 137 | syl5bir 232 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (¬ (𝑓‘𝑥) ∈ {0} → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
139 | 138 | orrd 392 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((𝑓‘𝑥) ∈ {0} ∨ (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
140 | | elun 3715 |
. . . . . . . 8
⊢ ((𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↔ ((𝑓‘𝑥) ∈ {0} ∨ (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
141 | 139, 140 | sylibr 223 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
142 | 141 | ralrimiva 2949 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))(𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
143 | | ffnfv 6295 |
. . . . . 6
⊢ (𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↔ (𝑓 Fn
(Base‘(ℤ/nℤ‘𝑁)) ∧ ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))(𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))) |
144 | 58, 142, 143 | sylanbrc 695 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0})) |
145 | 144 | ex 449 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ 𝐷 → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}))) |
146 | 47, 50 | elmapd 7758 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ↔ 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}))) |
147 | 145, 146 | sylibrd 248 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ 𝐷 → 𝑓 ∈ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁))))) |
148 | 147 | ssrdv 3574 |
. 2
⊢ (𝑁 ∈ ℕ → 𝐷 ⊆ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁)))) |
149 | | ssfi 8065 |
. 2
⊢ (((({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin ∧ 𝐷 ⊆ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁)))) → 𝐷 ∈ Fin) |
150 | 52, 148, 149 | syl2anc 691 |
1
⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) |