Step | Hyp | Ref
| Expression |
1 | | snfi 8079 |
. . . 4
⊢ {0}
∈ Fin |
2 | | cnex 10055 |
. . . . . . . . 9
⊢ ℂ
∈ V |
3 | 2 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → ℂ
∈ V) |
4 | | ovexd 6720 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ) → (𝑧↑(ϕ‘𝑁)) ∈ V) |
5 | | 1cnd 10094 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ) → 1 ∈
ℂ) |
6 | | eqidd 2652 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) = (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁)))) |
7 | | fconstmpt 5197 |
. . . . . . . . 9
⊢ (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1) |
8 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1)) |
9 | 3, 4, 5, 6, 8 | offval2 6956 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘𝑓
− (ℂ × {1})) = (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))) |
10 | | ssid 3657 |
. . . . . . . . . 10
⊢ ℂ
⊆ ℂ |
11 | 10 | a1i 11 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ℂ
⊆ ℂ) |
12 | | 1cnd 10094 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) |
13 | | phicl 15521 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) ∈
ℕ) |
14 | 13 | nnnn0d 11389 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) ∈
ℕ0) |
15 | | plypow 24006 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ ∧ (ϕ‘𝑁) ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈
(Poly‘ℂ)) |
16 | 11, 12, 14, 15 | syl3anc 1366 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈
(Poly‘ℂ)) |
17 | | ax-1cn 10032 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
18 | | plyconst 24007 |
. . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ) → (ℂ × {1}) ∈
(Poly‘ℂ)) |
19 | 10, 17, 18 | mp2an 708 |
. . . . . . . 8
⊢ (ℂ
× {1}) ∈ (Poly‘ℂ) |
20 | | plysubcl 24023 |
. . . . . . . 8
⊢ (((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈ (Poly‘ℂ)
∧ (ℂ × {1}) ∈ (Poly‘ℂ)) → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘𝑓
− (ℂ × {1})) ∈ (Poly‘ℂ)) |
21 | 16, 19, 20 | sylancl 695 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘𝑓
− (ℂ × {1})) ∈ (Poly‘ℂ)) |
22 | 9, 21 | eqeltrrd 2731 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ∈
(Poly‘ℂ)) |
23 | | 0cn 10070 |
. . . . . . 7
⊢ 0 ∈
ℂ |
24 | | neg1ne0 11164 |
. . . . . . . 8
⊢ -1 ≠
0 |
25 | 13 | 0expd 13064 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(0↑(ϕ‘𝑁)) =
0) |
26 | 25 | oveq1d 6705 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
((0↑(ϕ‘𝑁))
− 1) = (0 − 1)) |
27 | | oveq1 6697 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 0 → (𝑧↑(ϕ‘𝑁)) = (0↑(ϕ‘𝑁))) |
28 | 27 | oveq1d 6705 |
. . . . . . . . . . . 12
⊢ (𝑧 = 0 → ((𝑧↑(ϕ‘𝑁)) − 1) = ((0↑(ϕ‘𝑁)) − 1)) |
29 | | eqid 2651 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) = (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) |
30 | | ovex 6718 |
. . . . . . . . . . . 12
⊢
((0↑(ϕ‘𝑁)) − 1) ∈ V |
31 | 28, 29, 30 | fvmpt 6321 |
. . . . . . . . . . 11
⊢ (0 ∈
ℂ → ((𝑧 ∈
ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
((0↑(ϕ‘𝑁))
− 1)) |
32 | 23, 31 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
((0↑(ϕ‘𝑁))
− 1) |
33 | | df-neg 10307 |
. . . . . . . . . 10
⊢ -1 = (0
− 1) |
34 | 26, 32, 33 | 3eqtr4g 2710 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
-1) |
35 | 34 | neeq1d 2882 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → (((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0
↔ -1 ≠ 0)) |
36 | 24, 35 | mpbiri 248 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠
0) |
37 | | ne0p 24008 |
. . . . . . 7
⊢ ((0
∈ ℂ ∧ ((𝑧
∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0) →
(𝑧 ∈ ℂ ↦
((𝑧↑(ϕ‘𝑁)) − 1)) ≠
0𝑝) |
38 | 23, 36, 37 | sylancr 696 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠
0𝑝) |
39 | 29 | mptiniseg 5667 |
. . . . . . . . 9
⊢ (0 ∈
ℂ → (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) = {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}) |
40 | 23, 39 | ax-mp 5 |
. . . . . . . 8
⊢ (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) = {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0} |
41 | 40 | eqcomi 2660 |
. . . . . . 7
⊢ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} = (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) |
42 | 41 | fta1 24108 |
. . . . . 6
⊢ (((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ∈
(Poly‘ℂ) ∧ (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠ 0𝑝)
→ ({𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin ∧
(#‘{𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ≤ (deg‘(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) −
1))))) |
43 | 22, 38, 42 | syl2anc 694 |
. . . . 5
⊢ (𝑁 ∈ ℕ → ({𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin
∧ (#‘{𝑧 ∈
ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ≤ (deg‘(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) −
1))))) |
44 | 43 | simpld 474 |
. . . 4
⊢ (𝑁 ∈ ℕ → {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈
Fin) |
45 | | unfi 8268 |
. . . 4
⊢ (({0}
∈ Fin ∧ {𝑧 ∈
ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin) → ({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈
Fin) |
46 | 1, 44, 45 | sylancr 696 |
. . 3
⊢ (𝑁 ∈ ℕ → ({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈
Fin) |
47 | | eqid 2651 |
. . . 4
⊢
(ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁) |
48 | | eqid 2651 |
. . . 4
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(ℤ/nℤ‘𝑁)) |
49 | 47, 48 | znfi 19956 |
. . 3
⊢ (𝑁 ∈ ℕ →
(Base‘(ℤ/nℤ‘𝑁)) ∈ Fin) |
50 | | mapfi 8303 |
. . 3
⊢ ((({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈ Fin ∧
(Base‘(ℤ/nℤ‘𝑁)) ∈ Fin) → (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin) |
51 | 46, 49, 50 | syl2anc 694 |
. 2
⊢ (𝑁 ∈ ℕ → (({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin) |
52 | | dchrabl.g |
. . . . . . . 8
⊢ 𝐺 = (DChr‘𝑁) |
53 | | dchrfi.b |
. . . . . . . 8
⊢ 𝐷 = (Base‘𝐺) |
54 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ 𝐷) |
55 | 52, 47, 53, 48, 54 | dchrf 25012 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
56 | | ffn 6083 |
. . . . . . 7
⊢ (𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ → 𝑓 Fn
(Base‘(ℤ/nℤ‘𝑁))) |
57 | 55, 56 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓 Fn
(Base‘(ℤ/nℤ‘𝑁))) |
58 | | df-ne 2824 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑥) ≠ 0 ↔ ¬ (𝑓‘𝑥) = 0) |
59 | | fvex 6239 |
. . . . . . . . . . . 12
⊢ (𝑓‘𝑥) ∈ V |
60 | 59 | elsn 4225 |
. . . . . . . . . . 11
⊢ ((𝑓‘𝑥) ∈ {0} ↔ (𝑓‘𝑥) = 0) |
61 | 58, 60 | xchbinxr 324 |
. . . . . . . . . 10
⊢ ((𝑓‘𝑥) ≠ 0 ↔ ¬ (𝑓‘𝑥) ∈ {0}) |
62 | | simpl 472 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) |
63 | | ffvelrn 6397 |
. . . . . . . . . . . . 13
⊢ ((𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘𝑥) ∈ ℂ) |
64 | 55, 62, 63 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ∈ ℂ) |
65 | 52, 47, 53 | dchrmhm 25011 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝐷 ⊆
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) |
66 | | simplr 807 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑓 ∈ 𝐷) |
67 | 65, 66 | sseldi 3634 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld))) |
68 | 14 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℕ0) |
69 | | simprl 809 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) |
70 | | eqid 2651 |
. . . . . . . . . . . . . . . . . . 19
⊢
(mulGrp‘(ℤ/nℤ‘𝑁)) =
(mulGrp‘(ℤ/nℤ‘𝑁)) |
71 | 70, 48 | mgpbas 18541 |
. . . . . . . . . . . . . . . . . 18
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(mulGrp‘(ℤ/nℤ‘𝑁))) |
72 | | eqid 2651 |
. . . . . . . . . . . . . . . . . 18
⊢
(.g‘(mulGrp‘(ℤ/nℤ‘𝑁))) =
(.g‘(mulGrp‘(ℤ/nℤ‘𝑁))) |
73 | | eqid 2651 |
. . . . . . . . . . . . . . . . . 18
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) |
74 | 71, 72, 73 | mhmmulg 17630 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) ∧ (ϕ‘𝑁) ∈ ℕ0 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥))) |
75 | 67, 68, 69, 74 | syl3anc 1366 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥))) |
76 | | nnnn0 11337 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
77 | 47 | zncrng 19941 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ (ℤ/nℤ‘𝑁) ∈ CRing) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ →
(ℤ/nℤ‘𝑁) ∈ CRing) |
79 | | crngring 18604 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((ℤ/nℤ‘𝑁) ∈ CRing →
(ℤ/nℤ‘𝑁) ∈ Ring) |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(ℤ/nℤ‘𝑁) ∈ Ring) |
81 | 80 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(ℤ/nℤ‘𝑁) ∈ Ring) |
82 | | eqid 2651 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Unit‘(ℤ/nℤ‘𝑁)) |
83 | | eqid 2651 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) =
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) |
84 | 82, 83 | unitgrp 18713 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp) |
85 | 81, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp) |
86 | 47, 82 | znunithash 19961 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ →
(#‘(Unit‘(ℤ/nℤ‘𝑁))) = (ϕ‘𝑁)) |
87 | 86, 14 | eqeltrd 2730 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(#‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0) |
88 | | fvex 6239 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(Unit‘(ℤ/nℤ‘𝑁)) ∈ V |
89 | | hashclb 13187 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈ V →
((Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ↔
(#‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0)) |
90 | 88, 89 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ↔
(#‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0) |
91 | 87, 90 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ →
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin) |
92 | 91 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin) |
93 | | simprr 811 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ≠ 0) |
94 | 52, 47, 53, 48, 82, 66, 69 | dchrn0 25020 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((𝑓‘𝑥) ≠ 0 ↔ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) |
95 | 93, 94 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) |
96 | 82, 83 | unitgrpbas 18712 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Base‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
97 | | eqid 2651 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
98 | 96, 97 | oddvds2 18029 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp ∧
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥
(#‘(Unit‘(ℤ/nℤ‘𝑁)))) |
99 | 85, 92, 95, 98 | syl3anc 1366 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥
(#‘(Unit‘(ℤ/nℤ‘𝑁)))) |
100 | 86 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(#‘(Unit‘(ℤ/nℤ‘𝑁))) = (ϕ‘𝑁)) |
101 | 99, 100 | breqtrd 4711 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (ϕ‘𝑁)) |
102 | 13 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℕ) |
103 | 102 | nnzd 11519 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℤ) |
104 | | eqid 2651 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
105 | | eqid 2651 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) |
106 | 96, 97, 104, 105 | oddvds 18012 |
. . . . . . . . . . . . . . . . . . . 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ℤ‘𝑁)))))) |
107 | 85, 95, 103, 106 | syl3anc 1366 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (ϕ‘𝑁) ↔ ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))))) |
108 | 101, 107 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))) |
109 | 82, 70 | unitsubm 18716 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
(Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁)))) |
110 | 81, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁)))) |
111 | 72, 83, 104 | submmulg 17633 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))) ∧ (ϕ‘𝑁) ∈ ℕ0 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥)) |
112 | 110, 68, 95, 111 | syl3anc 1366 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥)) |
113 | | eqid 2651 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1r‘(ℤ/nℤ‘𝑁)) =
(1r‘(ℤ/nℤ‘𝑁)) |
114 | 70, 113 | ringidval 18549 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘(mulGrp‘(ℤ/nℤ‘𝑁))) |
115 | 83, 114 | subm0 17403 |
. . . . . . . . . . . . . . . . . . 19
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))) →
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))) |
116 | 110, 115 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))) |
117 | 108, 112,
116 | 3eqtr4d 2695 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
(1r‘(ℤ/nℤ‘𝑁))) |
118 | 117 | fveq2d 6233 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
(𝑓‘(1r‘(ℤ/nℤ‘𝑁)))) |
119 | 75, 118 | eqtr3d 2687 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = (𝑓‘(1r‘(ℤ/nℤ‘𝑁)))) |
120 | | cnfldexp 19827 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓‘𝑥) ∈ ℂ ∧ (ϕ‘𝑁) ∈ ℕ0)
→ ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) |
121 | 64, 68, 120 | syl2anc 694 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) |
122 | | eqid 2651 |
. . . . . . . . . . . . . . . . . 18
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
123 | | cnfld1 19819 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 =
(1r‘ℂfld) |
124 | 122, 123 | ringidval 18549 |
. . . . . . . . . . . . . . . . 17
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
125 | 114, 124 | mhm0 17390 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) → (𝑓‘(1r‘(ℤ/nℤ‘𝑁))) = 1) |
126 | 67, 125 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘(1r‘(ℤ/nℤ‘𝑁))) = 1) |
127 | 119, 121,
126 | 3eqtr3d 2693 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((𝑓‘𝑥)↑(ϕ‘𝑁)) = 1) |
128 | 127 | oveq1d 6705 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = (1 −
1)) |
129 | | 1m1e0 11127 |
. . . . . . . . . . . . 13
⊢ (1
− 1) = 0 |
130 | 128, 129 | syl6eq 2701 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = 0) |
131 | | oveq1 6697 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑓‘𝑥) → (𝑧↑(ϕ‘𝑁)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) |
132 | 131 | oveq1d 6705 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑓‘𝑥) → ((𝑧↑(ϕ‘𝑁)) − 1) = (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1)) |
133 | 132 | eqeq1d 2653 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑓‘𝑥) → (((𝑧↑(ϕ‘𝑁)) − 1) = 0 ↔ (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = 0)) |
134 | 133 | elrab 3396 |
. . . . . . . . . . . 12
⊢ ((𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ↔ ((𝑓‘𝑥) ∈ ℂ ∧ (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = 0)) |
135 | 64, 130, 134 | sylanbrc 699 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) |
136 | 135 | expr 642 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((𝑓‘𝑥) ≠ 0 → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
137 | 61, 136 | syl5bir 233 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (¬ (𝑓‘𝑥) ∈ {0} → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
138 | 137 | orrd 392 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((𝑓‘𝑥) ∈ {0} ∨ (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
139 | | elun 3786 |
. . . . . . . 8
⊢ ((𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↔ ((𝑓‘𝑥) ∈ {0} ∨ (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
140 | 138, 139 | sylibr 224 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
141 | 140 | ralrimiva 2995 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))(𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) |
142 | | ffnfv 6428 |
. . . . . 6
⊢ (𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↔ (𝑓 Fn
(Base‘(ℤ/nℤ‘𝑁)) ∧ ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))(𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))) |
143 | 57, 141, 142 | sylanbrc 699 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0})) |
144 | 143 | ex 449 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ 𝐷 → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}))) |
145 | 46, 49 | elmapd 7913 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ↔ 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}))) |
146 | 144, 145 | sylibrd 249 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ 𝐷 → 𝑓 ∈ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁))))) |
147 | 146 | ssrdv 3642 |
. 2
⊢ (𝑁 ∈ ℕ → 𝐷 ⊆ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁)))) |
148 | | ssfi 8221 |
. 2
⊢ (((({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin ∧ 𝐷 ⊆ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑𝑚 (Base‘(ℤ/nℤ‘𝑁)))) → 𝐷 ∈ Fin) |
149 | 51, 147, 148 | syl2anc 694 |
1
⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) |