| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | snfi 9084 | . . . 4
⊢ {0}
∈ Fin | 
| 2 |  | cnex 11237 | . . . . . . . . 9
⊢ ℂ
∈ V | 
| 3 | 2 | a1i 11 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → ℂ
∈ V) | 
| 4 |  | ovexd 7467 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ) → (𝑧↑(ϕ‘𝑁)) ∈ V) | 
| 5 |  | 1cnd 11257 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ) → 1 ∈
ℂ) | 
| 6 |  | eqidd 2737 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) = (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁)))) | 
| 7 |  | fconstmpt 5746 | . . . . . . . . 9
⊢ (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1) | 
| 8 | 7 | a1i 11 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (ℂ
× {1}) = (𝑧 ∈
ℂ ↦ 1)) | 
| 9 | 3, 4, 5, 6, 8 | offval2 7718 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘f −
(ℂ × {1})) = (𝑧
∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))) | 
| 10 |  | ssid 4005 | . . . . . . . . . 10
⊢ ℂ
⊆ ℂ | 
| 11 | 10 | a1i 11 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ℂ
⊆ ℂ) | 
| 12 |  | 1cnd 11257 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → 1 ∈
ℂ) | 
| 13 |  | phicl 16807 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) ∈
ℕ) | 
| 14 | 13 | nnnn0d 12589 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ →
(ϕ‘𝑁) ∈
ℕ0) | 
| 15 |  | plypow 26245 | . . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ ∧ (ϕ‘𝑁) ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈
(Poly‘ℂ)) | 
| 16 | 11, 12, 14, 15 | syl3anc 1372 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈
(Poly‘ℂ)) | 
| 17 |  | ax-1cn 11214 | . . . . . . . . 9
⊢ 1 ∈
ℂ | 
| 18 |  | plyconst 26246 | . . . . . . . . 9
⊢ ((ℂ
⊆ ℂ ∧ 1 ∈ ℂ) → (ℂ × {1}) ∈
(Poly‘ℂ)) | 
| 19 | 10, 17, 18 | mp2an 692 | . . . . . . . 8
⊢ (ℂ
× {1}) ∈ (Poly‘ℂ) | 
| 20 |  | plysubcl 26262 | . . . . . . . 8
⊢ (((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈ (Poly‘ℂ)
∧ (ℂ × {1}) ∈ (Poly‘ℂ)) → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘f −
(ℂ × {1})) ∈ (Poly‘ℂ)) | 
| 21 | 16, 19, 20 | sylancl 586 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘f −
(ℂ × {1})) ∈ (Poly‘ℂ)) | 
| 22 | 9, 21 | eqeltrrd 2841 | . . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ∈
(Poly‘ℂ)) | 
| 23 |  | 0cn 11254 | . . . . . . 7
⊢ 0 ∈
ℂ | 
| 24 |  | neg1ne0 12383 | . . . . . . . 8
⊢ -1 ≠
0 | 
| 25 | 13 | 0expd 14180 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ →
(0↑(ϕ‘𝑁)) =
0) | 
| 26 | 25 | oveq1d 7447 | . . . . . . . . . 10
⊢ (𝑁 ∈ ℕ →
((0↑(ϕ‘𝑁))
− 1) = (0 − 1)) | 
| 27 |  | oveq1 7439 | . . . . . . . . . . . . 13
⊢ (𝑧 = 0 → (𝑧↑(ϕ‘𝑁)) = (0↑(ϕ‘𝑁))) | 
| 28 | 27 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝑧 = 0 → ((𝑧↑(ϕ‘𝑁)) − 1) = ((0↑(ϕ‘𝑁)) − 1)) | 
| 29 |  | eqid 2736 | . . . . . . . . . . . 12
⊢ (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) = (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) | 
| 30 |  | ovex 7465 | . . . . . . . . . . . 12
⊢
((0↑(ϕ‘𝑁)) − 1) ∈ V | 
| 31 | 28, 29, 30 | fvmpt 7015 | . . . . . . . . . . 11
⊢ (0 ∈
ℂ → ((𝑧 ∈
ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
((0↑(ϕ‘𝑁))
− 1)) | 
| 32 | 23, 31 | ax-mp 5 | . . . . . . . . . 10
⊢ ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
((0↑(ϕ‘𝑁))
− 1) | 
| 33 |  | df-neg 11496 | . . . . . . . . . 10
⊢ -1 = (0
− 1) | 
| 34 | 26, 32, 33 | 3eqtr4g 2801 | . . . . . . . . 9
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) =
-1) | 
| 35 | 34 | neeq1d 2999 | . . . . . . . 8
⊢ (𝑁 ∈ ℕ → (((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0
↔ -1 ≠ 0)) | 
| 36 | 24, 35 | mpbiri 258 | . . . . . . 7
⊢ (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠
0) | 
| 37 |  | ne0p 26247 | . . . . . . 7
⊢ ((0
∈ ℂ ∧ ((𝑧
∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0) →
(𝑧 ∈ ℂ ↦
((𝑧↑(ϕ‘𝑁)) − 1)) ≠
0𝑝) | 
| 38 | 23, 36, 37 | sylancr 587 | . . . . . 6
⊢ (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠
0𝑝) | 
| 39 | 29 | mptiniseg 6258 | . . . . . . . . 9
⊢ (0 ∈
ℂ → (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) = {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}) | 
| 40 | 23, 39 | ax-mp 5 | . . . . . . . 8
⊢ (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) = {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0} | 
| 41 | 40 | eqcomi 2745 | . . . . . . 7
⊢ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} = (◡(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) | 
| 42 | 41 | fta1 26351 | . . . . . 6
⊢ (((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ∈
(Poly‘ℂ) ∧ (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠ 0𝑝)
→ ({𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin ∧
(♯‘{𝑧 ∈
ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ≤ (deg‘(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) −
1))))) | 
| 43 | 22, 38, 42 | syl2anc 584 | . . . . 5
⊢ (𝑁 ∈ ℕ → ({𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin
∧ (♯‘{𝑧
∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ≤ (deg‘(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) −
1))))) | 
| 44 | 43 | simpld 494 | . . . 4
⊢ (𝑁 ∈ ℕ → {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈
Fin) | 
| 45 |  | unfi 9212 | . . . 4
⊢ (({0}
∈ Fin ∧ {𝑧 ∈
ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin) → ({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈
Fin) | 
| 46 | 1, 44, 45 | sylancr 587 | . . 3
⊢ (𝑁 ∈ ℕ → ({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈
Fin) | 
| 47 |  | eqid 2736 | . . . 4
⊢
(ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁) | 
| 48 |  | eqid 2736 | . . . 4
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(ℤ/nℤ‘𝑁)) | 
| 49 | 47, 48 | znfi 21579 | . . 3
⊢ (𝑁 ∈ ℕ →
(Base‘(ℤ/nℤ‘𝑁)) ∈ Fin) | 
| 50 |  | mapfi 9389 | . . 3
⊢ ((({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈ Fin ∧
(Base‘(ℤ/nℤ‘𝑁)) ∈ Fin) → (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑m (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin) | 
| 51 | 46, 49, 50 | syl2anc 584 | . 2
⊢ (𝑁 ∈ ℕ → (({0}
∪ {𝑧 ∈ ℂ
∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑m
(Base‘(ℤ/nℤ‘𝑁))) ∈ Fin) | 
| 52 |  | dchrabl.g | . . . . . . . 8
⊢ 𝐺 = (DChr‘𝑁) | 
| 53 |  | dchrfi.b | . . . . . . . 8
⊢ 𝐷 = (Base‘𝐺) | 
| 54 |  | simpr 484 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ 𝐷) | 
| 55 | 52, 47, 53, 48, 54 | dchrf 27287 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) | 
| 56 | 55 | ffnd 6736 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓 Fn
(Base‘(ℤ/nℤ‘𝑁))) | 
| 57 |  | df-ne 2940 | . . . . . . . . . . 11
⊢ ((𝑓‘𝑥) ≠ 0 ↔ ¬ (𝑓‘𝑥) = 0) | 
| 58 |  | fvex 6918 | . . . . . . . . . . . 12
⊢ (𝑓‘𝑥) ∈ V | 
| 59 | 58 | elsn 4640 | . . . . . . . . . . 11
⊢ ((𝑓‘𝑥) ∈ {0} ↔ (𝑓‘𝑥) = 0) | 
| 60 | 57, 59 | xchbinxr 335 | . . . . . . . . . 10
⊢ ((𝑓‘𝑥) ≠ 0 ↔ ¬ (𝑓‘𝑥) ∈ {0}) | 
| 61 |  | oveq1 7439 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑓‘𝑥) → (𝑧↑(ϕ‘𝑁)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) | 
| 62 | 61 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝑧 = (𝑓‘𝑥) → ((𝑧↑(ϕ‘𝑁)) − 1) = (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1)) | 
| 63 | 62 | eqeq1d 2738 | . . . . . . . . . . . 12
⊢ (𝑧 = (𝑓‘𝑥) → (((𝑧↑(ϕ‘𝑁)) − 1) = 0 ↔ (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = 0)) | 
| 64 |  | simpl 482 | . . . . . . . . . . . . 13
⊢ ((𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) | 
| 65 |  | ffvelcdm 7100 | . . . . . . . . . . . . 13
⊢ ((𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘𝑥) ∈ ℂ) | 
| 66 | 55, 64, 65 | syl2an 596 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ∈ ℂ) | 
| 67 | 52, 47, 53 | dchrmhm 27286 | . . . . . . . . . . . . . . . . . 18
⊢ 𝐷 ⊆
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) | 
| 68 |  | simplr 768 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑓 ∈ 𝐷) | 
| 69 | 67, 68 | sselid 3980 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld))) | 
| 70 | 14 | ad2antrr 726 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℕ0) | 
| 71 |  | simprl 770 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) | 
| 72 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . 19
⊢
(mulGrp‘(ℤ/nℤ‘𝑁)) =
(mulGrp‘(ℤ/nℤ‘𝑁)) | 
| 73 | 72, 48 | mgpbas 20143 | . . . . . . . . . . . . . . . . . 18
⊢
(Base‘(ℤ/nℤ‘𝑁)) =
(Base‘(mulGrp‘(ℤ/nℤ‘𝑁))) | 
| 74 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(.g‘(mulGrp‘(ℤ/nℤ‘𝑁))) =
(.g‘(mulGrp‘(ℤ/nℤ‘𝑁))) | 
| 75 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(.g‘(mulGrp‘ℂfld)) =
(.g‘(mulGrp‘ℂfld)) | 
| 76 | 73, 74, 75 | mhmmulg 19134 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) ∧ (ϕ‘𝑁) ∈ ℕ0 ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥))) | 
| 77 | 69, 70, 71, 76 | syl3anc 1372 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥))) | 
| 78 |  | nnnn0 12535 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) | 
| 79 | 47 | zncrng 21564 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑁 ∈ ℕ0
→ (ℤ/nℤ‘𝑁) ∈ CRing) | 
| 80 | 78, 79 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ →
(ℤ/nℤ‘𝑁) ∈ CRing) | 
| 81 |  | crngring 20243 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((ℤ/nℤ‘𝑁) ∈ CRing →
(ℤ/nℤ‘𝑁) ∈ Ring) | 
| 82 | 80, 81 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(ℤ/nℤ‘𝑁) ∈ Ring) | 
| 83 | 82 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(ℤ/nℤ‘𝑁) ∈ Ring) | 
| 84 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Unit‘(ℤ/nℤ‘𝑁)) | 
| 85 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) =
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) | 
| 86 | 84, 85 | unitgrp 20384 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp) | 
| 87 | 83, 86 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp) | 
| 88 | 47, 84 | znunithash 21584 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑁 ∈ ℕ →
(♯‘(Unit‘(ℤ/nℤ‘𝑁))) = (ϕ‘𝑁)) | 
| 89 | 88, 14 | eqeltrd 2840 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑁 ∈ ℕ →
(♯‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0) | 
| 90 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(Unit‘(ℤ/nℤ‘𝑁)) ∈ V | 
| 91 |  | hashclb 14398 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈ V →
((Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ↔
(♯‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0)) | 
| 92 | 90, 91 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ↔
(♯‘(Unit‘(ℤ/nℤ‘𝑁))) ∈
ℕ0) | 
| 93 | 89, 92 | sylibr 234 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑁 ∈ ℕ →
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin) | 
| 94 | 93 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin) | 
| 95 |  | simprr 772 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ≠ 0) | 
| 96 | 52, 47, 53, 48, 84, 68, 71 | dchrn0 27295 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((𝑓‘𝑥) ≠ 0 ↔ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁)))) | 
| 97 | 95, 96 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) | 
| 98 | 84, 85 | unitgrpbas 20383 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(Unit‘(ℤ/nℤ‘𝑁)) =
(Base‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) | 
| 99 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) | 
| 100 | 98, 99 | oddvds2 19585 | . . . . . . . . . . . . . . . . . . . . 21
⊢
((((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp ∧
(Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥
(♯‘(Unit‘(ℤ/nℤ‘𝑁)))) | 
| 101 | 87, 94, 97, 100 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥
(♯‘(Unit‘(ℤ/nℤ‘𝑁)))) | 
| 102 | 88 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(♯‘(Unit‘(ℤ/nℤ‘𝑁))) = (ϕ‘𝑁)) | 
| 103 | 101, 102 | breqtrd 5168 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (ϕ‘𝑁)) | 
| 104 | 13 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℕ) | 
| 105 | 104 | nnzd 12642 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (ϕ‘𝑁) ∈
ℤ) | 
| 106 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) | 
| 107 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁)))) | 
| 108 | 98, 99, 106, 107 | oddvds 19566 | . . . . . . . . . . . . . . . . . . . 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ℤ‘𝑁)))))) | 
| 109 | 87, 97, 105, 108 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (ϕ‘𝑁) ↔ ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))))) | 
| 110 | 103, 109 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))) | 
| 111 | 84, 72 | unitsubm 20387 | . . . . . . . . . . . . . . . . . . . 20
⊢
((ℤ/nℤ‘𝑁) ∈ Ring →
(Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁)))) | 
| 112 | 83, 111 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁)))) | 
| 113 | 74, 85, 106 | submmulg 19137 | . . . . . . . . . . . . . . . . . . 19
⊢
(((Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))) ∧ (ϕ‘𝑁) ∈ ℕ0 ∧ 𝑥 ∈
(Unit‘(ℤ/nℤ‘𝑁))) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥)) | 
| 114 | 112, 70, 97, 113 | syl3anc 1372 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))𝑥)) | 
| 115 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(1r‘(ℤ/nℤ‘𝑁)) =
(1r‘(ℤ/nℤ‘𝑁)) | 
| 116 | 72, 115 | ringidval 20181 | . . . . . . . . . . . . . . . . . . . 20
⊢
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘(mulGrp‘(ℤ/nℤ‘𝑁))) | 
| 117 | 85, 116 | subm0 18829 | . . . . . . . . . . . . . . . . . . 19
⊢
((Unit‘(ℤ/nℤ‘𝑁)) ∈
(SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))) →
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))) | 
| 118 | 112, 117 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) →
(1r‘(ℤ/nℤ‘𝑁)) =
(0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s
(Unit‘(ℤ/nℤ‘𝑁))))) | 
| 119 | 110, 114,
118 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) =
(1r‘(ℤ/nℤ‘𝑁))) | 
| 120 | 119 | fveq2d 6909 | . . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) =
(𝑓‘(1r‘(ℤ/nℤ‘𝑁)))) | 
| 121 | 77, 120 | eqtr3d 2778 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = (𝑓‘(1r‘(ℤ/nℤ‘𝑁)))) | 
| 122 |  | cnfldexp 21418 | . . . . . . . . . . . . . . . 16
⊢ (((𝑓‘𝑥) ∈ ℂ ∧ (ϕ‘𝑁) ∈ ℕ0)
→ ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) | 
| 123 | 66, 70, 122 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓‘𝑥)) = ((𝑓‘𝑥)↑(ϕ‘𝑁))) | 
| 124 |  | eqid 2736 | . . . . . . . . . . . . . . . . . 18
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) | 
| 125 |  | cnfld1 21407 | . . . . . . . . . . . . . . . . . 18
⊢ 1 =
(1r‘ℂfld) | 
| 126 | 124, 125 | ringidval 20181 | . . . . . . . . . . . . . . . . 17
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) | 
| 127 | 116, 126 | mhm0 18808 | . . . . . . . . . . . . . . . 16
⊢ (𝑓 ∈
((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom
(mulGrp‘ℂfld)) → (𝑓‘(1r‘(ℤ/nℤ‘𝑁))) = 1) | 
| 128 | 69, 127 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘(1r‘(ℤ/nℤ‘𝑁))) = 1) | 
| 129 | 121, 123,
128 | 3eqtr3d 2784 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → ((𝑓‘𝑥)↑(ϕ‘𝑁)) = 1) | 
| 130 | 129 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = (1 −
1)) | 
| 131 |  | 1m1e0 12339 | . . . . . . . . . . . . 13
⊢ (1
− 1) = 0 | 
| 132 | 130, 131 | eqtrdi 2792 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (((𝑓‘𝑥)↑(ϕ‘𝑁)) − 1) = 0) | 
| 133 | 63, 66, 132 | elrabd 3693 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ (𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓‘𝑥) ≠ 0)) → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) | 
| 134 | 133 | expr 456 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((𝑓‘𝑥) ≠ 0 → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) | 
| 135 | 60, 134 | biimtrrid 243 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (¬ (𝑓‘𝑥) ∈ {0} → (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) | 
| 136 | 135 | orrd 863 | . . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → ((𝑓‘𝑥) ∈ {0} ∨ (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) | 
| 137 |  | elun 4152 | . . . . . . . 8
⊢ ((𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↔ ((𝑓‘𝑥) ∈ {0} ∨ (𝑓‘𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) | 
| 138 | 136, 137 | sylibr 234 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) | 
| 139 | 138 | ralrimiva 3145 | . . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))(𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})) | 
| 140 |  | ffnfv 7138 | . . . . . 6
⊢ (𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↔ (𝑓 Fn
(Base‘(ℤ/nℤ‘𝑁)) ∧ ∀𝑥 ∈
(Base‘(ℤ/nℤ‘𝑁))(𝑓‘𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))) | 
| 141 | 56, 139, 140 | sylanbrc 583 | . . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0})) | 
| 142 | 141 | ex 412 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ 𝐷 → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}))) | 
| 143 | 46, 49 | elmapd 8881 | . . . 4
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑m (Base‘(ℤ/nℤ‘𝑁))) ↔ 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) =
0}))) | 
| 144 | 142, 143 | sylibrd 259 | . . 3
⊢ (𝑁 ∈ ℕ → (𝑓 ∈ 𝐷 → 𝑓 ∈ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑m
(Base‘(ℤ/nℤ‘𝑁))))) | 
| 145 | 144 | ssrdv 3988 | . 2
⊢ (𝑁 ∈ ℕ → 𝐷 ⊆ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
↑m (Base‘(ℤ/nℤ‘𝑁)))) | 
| 146 | 51, 145 | ssfid 9302 | 1
⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) |