MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrfi Structured version   Visualization version   GIF version

Theorem dchrfi 25193
Description: The group of Dirichlet characters is a finite group. (Contributed by Mario Carneiro, 19-Apr-2016.)
Hypotheses
Ref Expression
dchrabl.g 𝐺 = (DChr‘𝑁)
dchrfi.b 𝐷 = (Base‘𝐺)
Assertion
Ref Expression
dchrfi (𝑁 ∈ ℕ → 𝐷 ∈ Fin)

Proof of Theorem dchrfi
Dummy variables 𝑥 𝑓 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 snfi 8273 . . . 4 {0} ∈ Fin
2 cnex 10298 . . . . . . . . 9 ℂ ∈ V
32a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → ℂ ∈ V)
4 ovexd 6904 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ) → (𝑧↑(ϕ‘𝑁)) ∈ V)
5 1cnd 10316 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑧 ∈ ℂ) → 1 ∈ ℂ)
6 eqidd 2807 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) = (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))))
7 fconstmpt 5363 . . . . . . . . 9 (ℂ × {1}) = (𝑧 ∈ ℂ ↦ 1)
87a1i 11 . . . . . . . 8 (𝑁 ∈ ℕ → (ℂ × {1}) = (𝑧 ∈ ℂ ↦ 1))
93, 4, 5, 6, 8offval2 7140 . . . . . . 7 (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘𝑓 − (ℂ × {1})) = (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)))
10 ssid 3820 . . . . . . . . . 10 ℂ ⊆ ℂ
1110a1i 11 . . . . . . . . 9 (𝑁 ∈ ℕ → ℂ ⊆ ℂ)
12 1cnd 10316 . . . . . . . . 9 (𝑁 ∈ ℕ → 1 ∈ ℂ)
13 phicl 15687 . . . . . . . . . 10 (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ ℕ)
1413nnnn0d 11613 . . . . . . . . 9 (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ ℕ0)
15 plypow 24174 . . . . . . . . 9 ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ ∧ (ϕ‘𝑁) ∈ ℕ0) → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈ (Poly‘ℂ))
1611, 12, 14, 15syl3anc 1483 . . . . . . . 8 (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈ (Poly‘ℂ))
17 ax-1cn 10275 . . . . . . . . 9 1 ∈ ℂ
18 plyconst 24175 . . . . . . . . 9 ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → (ℂ × {1}) ∈ (Poly‘ℂ))
1910, 17, 18mp2an 675 . . . . . . . 8 (ℂ × {1}) ∈ (Poly‘ℂ)
20 plysubcl 24191 . . . . . . . 8 (((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∈ (Poly‘ℂ) ∧ (ℂ × {1}) ∈ (Poly‘ℂ)) → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘𝑓 − (ℂ × {1})) ∈ (Poly‘ℂ))
2116, 19, 20sylancl 576 . . . . . . 7 (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ (𝑧↑(ϕ‘𝑁))) ∘𝑓 − (ℂ × {1})) ∈ (Poly‘ℂ))
229, 21eqeltrrd 2886 . . . . . 6 (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ∈ (Poly‘ℂ))
23 0cn 10313 . . . . . . 7 0 ∈ ℂ
24 neg1ne0 11404 . . . . . . . 8 -1 ≠ 0
25130expd 13243 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (0↑(ϕ‘𝑁)) = 0)
2625oveq1d 6885 . . . . . . . . . 10 (𝑁 ∈ ℕ → ((0↑(ϕ‘𝑁)) − 1) = (0 − 1))
27 oveq1 6877 . . . . . . . . . . . . 13 (𝑧 = 0 → (𝑧↑(ϕ‘𝑁)) = (0↑(ϕ‘𝑁)))
2827oveq1d 6885 . . . . . . . . . . . 12 (𝑧 = 0 → ((𝑧↑(ϕ‘𝑁)) − 1) = ((0↑(ϕ‘𝑁)) − 1))
29 eqid 2806 . . . . . . . . . . . 12 (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) = (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))
30 ovex 6902 . . . . . . . . . . . 12 ((0↑(ϕ‘𝑁)) − 1) ∈ V
3128, 29, 30fvmpt 6499 . . . . . . . . . . 11 (0 ∈ ℂ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) = ((0↑(ϕ‘𝑁)) − 1))
3223, 31ax-mp 5 . . . . . . . . . 10 ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) = ((0↑(ϕ‘𝑁)) − 1)
33 df-neg 10550 . . . . . . . . . 10 -1 = (0 − 1)
3426, 32, 333eqtr4g 2865 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) = -1)
3534neeq1d 3037 . . . . . . . 8 (𝑁 ∈ ℕ → (((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0 ↔ -1 ≠ 0))
3624, 35mpbiri 249 . . . . . . 7 (𝑁 ∈ ℕ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0)
37 ne0p 24176 . . . . . . 7 ((0 ∈ ℂ ∧ ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1))‘0) ≠ 0) → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠ 0𝑝)
3823, 36, 37sylancr 577 . . . . . 6 (𝑁 ∈ ℕ → (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠ 0𝑝)
3929mptiniseg 5843 . . . . . . . . 9 (0 ∈ ℂ → ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) = {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
4023, 39ax-mp 5 . . . . . . . 8 ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0}) = {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}
4140eqcomi 2815 . . . . . . 7 {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} = ((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) “ {0})
4241fta1 24276 . . . . . 6 (((𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ∈ (Poly‘ℂ) ∧ (𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)) ≠ 0𝑝) → ({𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin ∧ (♯‘{𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ≤ (deg‘(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)))))
4322, 38, 42syl2anc 575 . . . . 5 (𝑁 ∈ ℕ → ({𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin ∧ (♯‘{𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ≤ (deg‘(𝑧 ∈ ℂ ↦ ((𝑧↑(ϕ‘𝑁)) − 1)))))
4443simpld 484 . . . 4 (𝑁 ∈ ℕ → {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin)
45 unfi 8462 . . . 4 (({0} ∈ Fin ∧ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ∈ Fin) → ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈ Fin)
461, 44, 45sylancr 577 . . 3 (𝑁 ∈ ℕ → ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈ Fin)
47 eqid 2806 . . . 4 (ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁)
48 eqid 2806 . . . 4 (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(ℤ/nℤ‘𝑁))
4947, 48znfi 20111 . . 3 (𝑁 ∈ ℕ → (Base‘(ℤ/nℤ‘𝑁)) ∈ Fin)
50 mapfi 8497 . . 3 ((({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ∈ Fin ∧ (Base‘(ℤ/nℤ‘𝑁)) ∈ Fin) → (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin)
5146, 49, 50syl2anc 575 . 2 (𝑁 ∈ ℕ → (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin)
52 dchrabl.g . . . . . . . 8 𝐺 = (DChr‘𝑁)
53 dchrfi.b . . . . . . . 8 𝐷 = (Base‘𝐺)
54 simpr 473 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑓𝐷) → 𝑓𝐷)
5552, 47, 53, 48, 54dchrf 25180 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑓𝐷) → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ)
5655ffnd 6253 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑓𝐷) → 𝑓 Fn (Base‘(ℤ/nℤ‘𝑁)))
57 df-ne 2979 . . . . . . . . . . 11 ((𝑓𝑥) ≠ 0 ↔ ¬ (𝑓𝑥) = 0)
58 fvex 6417 . . . . . . . . . . . 12 (𝑓𝑥) ∈ V
5958elsn 4385 . . . . . . . . . . 11 ((𝑓𝑥) ∈ {0} ↔ (𝑓𝑥) = 0)
6057, 59xchbinxr 326 . . . . . . . . . 10 ((𝑓𝑥) ≠ 0 ↔ ¬ (𝑓𝑥) ∈ {0})
61 simpl 470 . . . . . . . . . . . . 13 ((𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0) → 𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)))
62 ffvelrn 6575 . . . . . . . . . . . . 13 ((𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ ∧ 𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))) → (𝑓𝑥) ∈ ℂ)
6355, 61, 62syl2an 585 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (𝑓𝑥) ∈ ℂ)
6452, 47, 53dchrmhm 25179 . . . . . . . . . . . . . . . . . 18 𝐷 ⊆ ((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom (mulGrp‘ℂfld))
65 simplr 776 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → 𝑓𝐷)
6664, 65sseldi 3796 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → 𝑓 ∈ ((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom (mulGrp‘ℂfld)))
6714ad2antrr 708 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (ϕ‘𝑁) ∈ ℕ0)
68 simprl 778 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → 𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)))
69 eqid 2806 . . . . . . . . . . . . . . . . . . 19 (mulGrp‘(ℤ/nℤ‘𝑁)) = (mulGrp‘(ℤ/nℤ‘𝑁))
7069, 48mgpbas 18693 . . . . . . . . . . . . . . . . . 18 (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(mulGrp‘(ℤ/nℤ‘𝑁)))
71 eqid 2806 . . . . . . . . . . . . . . . . . 18 (.g‘(mulGrp‘(ℤ/nℤ‘𝑁))) = (.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))
72 eqid 2806 . . . . . . . . . . . . . . . . . 18 (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
7370, 71, 72mhmmulg 17781 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ ((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom (mulGrp‘ℂfld)) ∧ (ϕ‘𝑁) ∈ ℕ0𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) = ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓𝑥)))
7466, 67, 68, 73syl3anc 1483 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) = ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓𝑥)))
75 nnnn0 11562 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
7647zncrng 20096 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑁 ∈ ℕ0 → (ℤ/nℤ‘𝑁) ∈ CRing)
7775, 76syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → (ℤ/nℤ‘𝑁) ∈ CRing)
78 crngring 18756 . . . . . . . . . . . . . . . . . . . . . . . 24 ((ℤ/nℤ‘𝑁) ∈ CRing → (ℤ/nℤ‘𝑁) ∈ Ring)
7977, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → (ℤ/nℤ‘𝑁) ∈ Ring)
8079ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (ℤ/nℤ‘𝑁) ∈ Ring)
81 eqid 2806 . . . . . . . . . . . . . . . . . . . . . . 23 (Unit‘(ℤ/nℤ‘𝑁)) = (Unit‘(ℤ/nℤ‘𝑁))
82 eqid 2806 . . . . . . . . . . . . . . . . . . . . . . 23 ((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))) = ((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))
8381, 82unitgrp 18865 . . . . . . . . . . . . . . . . . . . . . 22 ((ℤ/nℤ‘𝑁) ∈ Ring → ((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp)
8480, 83syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → ((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp)
8547, 81znunithash 20116 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑁 ∈ ℕ → (♯‘(Unit‘(ℤ/nℤ‘𝑁))) = (ϕ‘𝑁))
8685, 14eqeltrd 2885 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑁 ∈ ℕ → (♯‘(Unit‘(ℤ/nℤ‘𝑁))) ∈ ℕ0)
87 fvex 6417 . . . . . . . . . . . . . . . . . . . . . . . 24 (Unit‘(ℤ/nℤ‘𝑁)) ∈ V
88 hashclb 13363 . . . . . . . . . . . . . . . . . . . . . . . 24 ((Unit‘(ℤ/nℤ‘𝑁)) ∈ V → ((Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ↔ (♯‘(Unit‘(ℤ/nℤ‘𝑁))) ∈ ℕ0))
8987, 88ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 ((Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ↔ (♯‘(Unit‘(ℤ/nℤ‘𝑁))) ∈ ℕ0)
9086, 89sylibr 225 . . . . . . . . . . . . . . . . . . . . . 22 (𝑁 ∈ ℕ → (Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin)
9190ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin)
92 simprr 780 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (𝑓𝑥) ≠ 0)
9352, 47, 53, 48, 81, 65, 68dchrn0 25188 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → ((𝑓𝑥) ≠ 0 ↔ 𝑥 ∈ (Unit‘(ℤ/nℤ‘𝑁))))
9492, 93mpbid 223 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → 𝑥 ∈ (Unit‘(ℤ/nℤ‘𝑁)))
9581, 82unitgrpbas 18864 . . . . . . . . . . . . . . . . . . . . . 22 (Unit‘(ℤ/nℤ‘𝑁)) = (Base‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))
96 eqid 2806 . . . . . . . . . . . . . . . . . . . . . 22 (od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))) = (od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))
9795, 96oddvds2 18180 . . . . . . . . . . . . . . . . . . . . 21 ((((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))) ∈ Grp ∧ (Unit‘(ℤ/nℤ‘𝑁)) ∈ Fin ∧ 𝑥 ∈ (Unit‘(ℤ/nℤ‘𝑁))) → ((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (♯‘(Unit‘(ℤ/nℤ‘𝑁))))
9884, 91, 94, 97syl3anc 1483 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → ((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (♯‘(Unit‘(ℤ/nℤ‘𝑁))))
9985ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (♯‘(Unit‘(ℤ/nℤ‘𝑁))) = (ϕ‘𝑁))
10098, 99breqtrd 4870 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → ((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (ϕ‘𝑁))
10113ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (ϕ‘𝑁) ∈ ℕ)
102101nnzd 11743 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (ϕ‘𝑁) ∈ ℤ)
103 eqid 2806 . . . . . . . . . . . . . . . . . . . . 21 (.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))) = (.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))
104 eqid 2806 . . . . . . . . . . . . . . . . . . . . 21 (0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))) = (0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))
10595, 96, 103, 104oddvds 18163 . . . . . . . . . . . . . . . . . . . 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ℤ‘𝑁))))))
10684, 94, 102, 105syl3anc 1483 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (((od‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))‘𝑥) ∥ (ϕ‘𝑁) ↔ ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))𝑥) = (0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))))
107100, 106mpbid 223 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))𝑥) = (0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))))
10881, 69unitsubm 18868 . . . . . . . . . . . . . . . . . . . 20 ((ℤ/nℤ‘𝑁) ∈ Ring → (Unit‘(ℤ/nℤ‘𝑁)) ∈ (SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))))
10980, 108syl 17 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (Unit‘(ℤ/nℤ‘𝑁)) ∈ (SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))))
11071, 82, 103submmulg 17784 . . . . . . . . . . . . . . . . . . 19 (((Unit‘(ℤ/nℤ‘𝑁)) ∈ (SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))) ∧ (ϕ‘𝑁) ∈ ℕ0𝑥 ∈ (Unit‘(ℤ/nℤ‘𝑁))) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) = ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))𝑥))
111109, 67, 94, 110syl3anc 1483 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) = ((ϕ‘𝑁)(.g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁))))𝑥))
112 eqid 2806 . . . . . . . . . . . . . . . . . . . . 21 (1r‘(ℤ/nℤ‘𝑁)) = (1r‘(ℤ/nℤ‘𝑁))
11369, 112ringidval 18701 . . . . . . . . . . . . . . . . . . . 20 (1r‘(ℤ/nℤ‘𝑁)) = (0g‘(mulGrp‘(ℤ/nℤ‘𝑁)))
11482, 113subm0 17557 . . . . . . . . . . . . . . . . . . 19 ((Unit‘(ℤ/nℤ‘𝑁)) ∈ (SubMnd‘(mulGrp‘(ℤ/nℤ‘𝑁))) → (1r‘(ℤ/nℤ‘𝑁)) = (0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))))
115109, 114syl 17 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (1r‘(ℤ/nℤ‘𝑁)) = (0g‘((mulGrp‘(ℤ/nℤ‘𝑁)) ↾s (Unit‘(ℤ/nℤ‘𝑁)))))
116107, 111, 1153eqtr4d 2850 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥) = (1r‘(ℤ/nℤ‘𝑁)))
117116fveq2d 6408 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (𝑓‘((ϕ‘𝑁)(.g‘(mulGrp‘(ℤ/nℤ‘𝑁)))𝑥)) = (𝑓‘(1r‘(ℤ/nℤ‘𝑁))))
11874, 117eqtr3d 2842 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓𝑥)) = (𝑓‘(1r‘(ℤ/nℤ‘𝑁))))
119 cnfldexp 19983 . . . . . . . . . . . . . . . 16 (((𝑓𝑥) ∈ ℂ ∧ (ϕ‘𝑁) ∈ ℕ0) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓𝑥)) = ((𝑓𝑥)↑(ϕ‘𝑁)))
12063, 67, 119syl2anc 575 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → ((ϕ‘𝑁)(.g‘(mulGrp‘ℂfld))(𝑓𝑥)) = ((𝑓𝑥)↑(ϕ‘𝑁)))
121 eqid 2806 . . . . . . . . . . . . . . . . . 18 (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
122 cnfld1 19975 . . . . . . . . . . . . . . . . . 18 1 = (1r‘ℂfld)
123121, 122ringidval 18701 . . . . . . . . . . . . . . . . 17 1 = (0g‘(mulGrp‘ℂfld))
124113, 123mhm0 17544 . . . . . . . . . . . . . . . 16 (𝑓 ∈ ((mulGrp‘(ℤ/nℤ‘𝑁)) MndHom (mulGrp‘ℂfld)) → (𝑓‘(1r‘(ℤ/nℤ‘𝑁))) = 1)
12566, 124syl 17 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (𝑓‘(1r‘(ℤ/nℤ‘𝑁))) = 1)
126118, 120, 1253eqtr3d 2848 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → ((𝑓𝑥)↑(ϕ‘𝑁)) = 1)
127126oveq1d 6885 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (((𝑓𝑥)↑(ϕ‘𝑁)) − 1) = (1 − 1))
128 1m1e0 11369 . . . . . . . . . . . . 13 (1 − 1) = 0
129127, 128syl6eq 2856 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (((𝑓𝑥)↑(ϕ‘𝑁)) − 1) = 0)
130 oveq1 6877 . . . . . . . . . . . . . . 15 (𝑧 = (𝑓𝑥) → (𝑧↑(ϕ‘𝑁)) = ((𝑓𝑥)↑(ϕ‘𝑁)))
131130oveq1d 6885 . . . . . . . . . . . . . 14 (𝑧 = (𝑓𝑥) → ((𝑧↑(ϕ‘𝑁)) − 1) = (((𝑓𝑥)↑(ϕ‘𝑁)) − 1))
132131eqeq1d 2808 . . . . . . . . . . . . 13 (𝑧 = (𝑓𝑥) → (((𝑧↑(ϕ‘𝑁)) − 1) = 0 ↔ (((𝑓𝑥)↑(ϕ‘𝑁)) − 1) = 0))
133132elrab 3559 . . . . . . . . . . . 12 ((𝑓𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0} ↔ ((𝑓𝑥) ∈ ℂ ∧ (((𝑓𝑥)↑(ϕ‘𝑁)) − 1) = 0))
13463, 129, 133sylanbrc 574 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ (𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (𝑓𝑥) ≠ 0)) → (𝑓𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})
135134expr 446 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ 𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))) → ((𝑓𝑥) ≠ 0 → (𝑓𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))
13660, 135syl5bir 234 . . . . . . . . 9 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ 𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))) → (¬ (𝑓𝑥) ∈ {0} → (𝑓𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))
137136orrd 881 . . . . . . . 8 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ 𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))) → ((𝑓𝑥) ∈ {0} ∨ (𝑓𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))
138 elun 3952 . . . . . . . 8 ((𝑓𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↔ ((𝑓𝑥) ∈ {0} ∨ (𝑓𝑥) ∈ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))
139137, 138sylibr 225 . . . . . . 7 (((𝑁 ∈ ℕ ∧ 𝑓𝐷) ∧ 𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))) → (𝑓𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))
140139ralrimiva 3154 . . . . . 6 ((𝑁 ∈ ℕ ∧ 𝑓𝐷) → ∀𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))(𝑓𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))
141 ffnfv 6606 . . . . . 6 (𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↔ (𝑓 Fn (Base‘(ℤ/nℤ‘𝑁)) ∧ ∀𝑥 ∈ (Base‘(ℤ/nℤ‘𝑁))(𝑓𝑥) ∈ ({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})))
14256, 140, 141sylanbrc 574 . . . . 5 ((𝑁 ∈ ℕ ∧ 𝑓𝐷) → 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}))
143142ex 399 . . . 4 (𝑁 ∈ ℕ → (𝑓𝐷𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})))
14446, 49elmapd 8102 . . . 4 (𝑁 ∈ ℕ → (𝑓 ∈ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ↔ 𝑓:(Base‘(ℤ/nℤ‘𝑁))⟶({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0})))
145143, 144sylibrd 250 . . 3 (𝑁 ∈ ℕ → (𝑓𝐷𝑓 ∈ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑𝑚 (Base‘(ℤ/nℤ‘𝑁)))))
146145ssrdv 3804 . 2 (𝑁 ∈ ℕ → 𝐷 ⊆ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑𝑚 (Base‘(ℤ/nℤ‘𝑁))))
147 ssfi 8415 . 2 (((({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑𝑚 (Base‘(ℤ/nℤ‘𝑁))) ∈ Fin ∧ 𝐷 ⊆ (({0} ∪ {𝑧 ∈ ℂ ∣ ((𝑧↑(ϕ‘𝑁)) − 1) = 0}) ↑𝑚 (Base‘(ℤ/nℤ‘𝑁)))) → 𝐷 ∈ Fin)
14851, 146, 147syl2anc 575 1 (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865   = wceq 1637  wcel 2156  wne 2978  wral 3096  {crab 3100  Vcvv 3391  cun 3767  wss 3769  {csn 4370   class class class wbr 4844  cmpt 4923   × cxp 5309  ccnv 5310  cima 5314   Fn wfn 6092  wf 6093  cfv 6097  (class class class)co 6870  𝑓 cof 7121  𝑚 cmap 8088  Fincfn 8188  cc 10215  0cc0 10217  1c1 10218  cle 10356  cmin 10547  -cneg 10548  cn 11301  0cn0 11555  cz 11639  cexp 13079  chash 13333  cdvds 15199  ϕcphi 15682  Basecbs 16064  s cress 16065  0gc0g 16301   MndHom cmhm 17534  SubMndcsubmnd 17535  Grpcgrp 17623  .gcmg 17741  odcod 18141  mulGrpcmgp 18687  1rcur 18699  Ringcrg 18745  CRingccrg 18746  Unitcui 18837  fldccnfld 19950  ℤ/nczn 20055  0𝑝c0p 23649  Polycply 24153  degcdgr 24156  DChrcdchr 25170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-inf2 8781  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295  ax-addf 10296  ax-mulf 10297
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-disj 4813  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-of 7123  df-om 7292  df-1st 7394  df-2nd 7395  df-tpos 7583  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-2o 7793  df-oadd 7796  df-omul 7797  df-er 7975  df-ec 7977  df-qs 7981  df-map 8090  df-pm 8091  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-sup 8583  df-inf 8584  df-oi 8650  df-card 9044  df-acn 9047  df-cda 9271  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-xnn0 11626  df-z 11640  df-dec 11756  df-uz 11901  df-rp 12043  df-fz 12546  df-fzo 12686  df-fl 12813  df-mod 12889  df-seq 13021  df-exp 13080  df-hash 13334  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-clim 14438  df-rlim 14439  df-sum 14636  df-dvds 15200  df-gcd 15432  df-phi 15684  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16171  df-unif 16172  df-0g 16303  df-imas 16369  df-qus 16370  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-subg 17789  df-nsg 17790  df-eqg 17791  df-ghm 17856  df-od 18145  df-cmn 18392  df-abl 18393  df-mgp 18688  df-ur 18700  df-ring 18747  df-cring 18748  df-oppr 18821  df-dvdsr 18839  df-unit 18840  df-invr 18870  df-rnghom 18915  df-subrg 18978  df-lmod 19065  df-lss 19133  df-lsp 19175  df-sra 19377  df-rgmod 19378  df-lidl 19379  df-rsp 19380  df-2idl 19437  df-cnfld 19951  df-zring 20023  df-zrh 20056  df-zn 20059  df-0p 23650  df-ply 24157  df-idp 24158  df-coe 24159  df-dgr 24160  df-quot 24259  df-dchr 25171
This theorem is referenced by:  sumdchr2  25208  dchrhash  25209  rpvmasum2  25414  dchrisum0re  25415
  Copyright terms: Public domain W3C validator