Metamath Proof Explorer

Theorem dchrpt

Description: For any element other than 1, there is a Dirichlet character that is not one at the given element. (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses dchrpt.g ⊢ G = DChr ⁡ N
dchrpt.z ⊢ Z = ℤ/Nℤ
dchrpt.d ⊢ D = Base G
dchrpt.b ⊢ B = Base Z
dchrpt.1 ⊢ 1 ˙ = 1 Z
dchrpt.n ⊢ φ → N ∈ ℕ
dchrpt.n1 ⊢ φ → A ≠ 1 ˙
dchrpt.a ⊢ φ → A ∈ B
Assertion dchrpt ⊢ φ → ∃ x ∈ D x ⁡ A ≠ 1

Proof

Step Hyp Ref Expression
1 dchrpt.g ⊢ G = DChr ⁡ N
2 dchrpt.z ⊢ Z = ℤ/Nℤ
3 dchrpt.d ⊢ D = Base G
4 dchrpt.b ⊢ B = Base Z
5 dchrpt.1 ⊢ 1 ˙ = 1 Z
6 dchrpt.n ⊢ φ → N ∈ ℕ
7 dchrpt.n1 ⊢ φ → A ≠ 1 ˙
8 dchrpt.a ⊢ φ → A ∈ B
9 6 ad3antrrr ⊢ φ ∧ A ∈ Unit ⁡ Z ∧ w ∈ Word Unit ⁡ Z ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z dom ⁡ DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = Unit ⁡ Z → N ∈ ℕ
10 7 ad3antrrr ⊢ φ ∧ A ∈ Unit ⁡ Z ∧ w ∈ Word Unit ⁡ Z ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z dom ⁡ DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = Unit ⁡ Z → A ≠ 1 ˙
11 eqid ⊢ Unit ⁡ Z = Unit ⁡ Z
12 eqid ⊢ mulGrp Z ↾ 𝑠 Unit ⁡ Z = mulGrp Z ↾ 𝑠 Unit ⁡ Z
13 eqid ⊢ ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z = ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z
14 oveq1 ⊢ n = b → n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = b ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k
15 14 cbvmptv ⊢ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = b ∈ ℤ ⟼ b ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k
16 fveq2 ⊢ k = a → w ⁡ k = w ⁡ a
17 16 oveq2d ⊢ k = a → b ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = b ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ a
18 17 mpteq2dv ⊢ k = a → b ∈ ℤ ⟼ b ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = b ∈ ℤ ⟼ b ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ a
19 15 18 eqtrid ⊢ k = a → n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = b ∈ ℤ ⟼ b ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ a
20 19 rneqd ⊢ k = a → ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = ran ⁡ b ∈ ℤ ⟼ b ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ a
21 20 cbvmptv ⊢ k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = a ∈ dom ⁡ w ⟼ ran ⁡ b ∈ ℤ ⟼ b ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ a
22 simpllr ⊢ φ ∧ A ∈ Unit ⁡ Z ∧ w ∈ Word Unit ⁡ Z ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z dom ⁡ DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = Unit ⁡ Z → A ∈ Unit ⁡ Z
23 simplr ⊢ φ ∧ A ∈ Unit ⁡ Z ∧ w ∈ Word Unit ⁡ Z ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z dom ⁡ DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = Unit ⁡ Z → w ∈ Word Unit ⁡ Z
24 simprl ⊢ φ ∧ A ∈ Unit ⁡ Z ∧ w ∈ Word Unit ⁡ Z ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z dom ⁡ DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = Unit ⁡ Z → mulGrp Z ↾ 𝑠 Unit ⁡ Z dom ⁡ DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k
25 simprr ⊢ φ ∧ A ∈ Unit ⁡ Z ∧ w ∈ Word Unit ⁡ Z ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z dom ⁡ DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = Unit ⁡ Z → mulGrp Z ↾ 𝑠 Unit ⁡ Z DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = Unit ⁡ Z
26 1 2 3 4 5 9 10 11 12 13 21 22 23 24 25 dchrptlem3 ⊢ φ ∧ A ∈ Unit ⁡ Z ∧ w ∈ Word Unit ⁡ Z ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z dom ⁡ DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = Unit ⁡ Z → ∃ x ∈ D x ⁡ A ≠ 1
27 26 3adantr1 ⊢ φ ∧ A ∈ Unit ⁡ Z ∧ w ∈ Word Unit ⁡ Z ∧ k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k : dom ⁡ w ⟶ u ∈ SubGrp ⁡ mulGrp Z ↾ 𝑠 Unit ⁡ Z | mulGrp Z ↾ 𝑠 Unit ⁡ Z ↾ 𝑠 u ∈ CycGrp ∩ ran ⁡ pGrp ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z dom ⁡ DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = Unit ⁡ Z → ∃ x ∈ D x ⁡ A ≠ 1
28 11 12 unitgrpbas ⊢ Unit ⁡ Z = Base mulGrp Z ↾ 𝑠 Unit ⁡ Z
29 eqid ⊢ u ∈ SubGrp ⁡ mulGrp Z ↾ 𝑠 Unit ⁡ Z | mulGrp Z ↾ 𝑠 Unit ⁡ Z ↾ 𝑠 u ∈ CycGrp ∩ ran ⁡ pGrp = u ∈ SubGrp ⁡ mulGrp Z ↾ 𝑠 Unit ⁡ Z | mulGrp Z ↾ 𝑠 Unit ⁡ Z ↾ 𝑠 u ∈ CycGrp ∩ ran ⁡ pGrp
30 6 nnnn0d ⊢ φ → N ∈ ℕ 0
31 2 zncrng ⊢ N ∈ ℕ 0 → Z ∈ CRing
32 11 12 unitabl ⊢ Z ∈ CRing → mulGrp Z ↾ 𝑠 Unit ⁡ Z ∈ Abel
33 30 31 32 3syl ⊢ φ → mulGrp Z ↾ 𝑠 Unit ⁡ Z ∈ Abel
34 33 adantr ⊢ φ ∧ A ∈ Unit ⁡ Z → mulGrp Z ↾ 𝑠 Unit ⁡ Z ∈ Abel
35 2 4 znfi ⊢ N ∈ ℕ → B ∈ Fin
36 6 35 syl ⊢ φ → B ∈ Fin
37 4 11 unitss ⊢ Unit ⁡ Z ⊆ B
38 ssfi ⊢ B ∈ Fin ∧ Unit ⁡ Z ⊆ B → Unit ⁡ Z ∈ Fin
39 36 37 38 sylancl ⊢ φ → Unit ⁡ Z ∈ Fin
40 39 adantr ⊢ φ ∧ A ∈ Unit ⁡ Z → Unit ⁡ Z ∈ Fin
41 eqid ⊢ k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k
42 28 29 34 40 13 41 ablfac2 ⊢ φ ∧ A ∈ Unit ⁡ Z → ∃ w ∈ Word Unit ⁡ Z k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k : dom ⁡ w ⟶ u ∈ SubGrp ⁡ mulGrp Z ↾ 𝑠 Unit ⁡ Z | mulGrp Z ↾ 𝑠 Unit ⁡ Z ↾ 𝑠 u ∈ CycGrp ∩ ran ⁡ pGrp ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z dom ⁡ DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k ∧ mulGrp Z ↾ 𝑠 Unit ⁡ Z DProd k ∈ dom ⁡ w ⟼ ran ⁡ n ∈ ℤ ⟼ n ⋅ mulGrp Z ↾ 𝑠 Unit ⁡ Z w ⁡ k = Unit ⁡ Z
43 27 42 r19.29a ⊢ φ ∧ A ∈ Unit ⁡ Z → ∃ x ∈ D x ⁡ A ≠ 1
44 1 dchrabl ⊢ N ∈ ℕ → G ∈ Abel
45 ablgrp ⊢ G ∈ Abel → G ∈ Grp
46 eqid ⊢ 0 G = 0 G
47 3 46 grpidcl ⊢ G ∈ Grp → 0 G ∈ D
48 6 44 45 47 4syl ⊢ φ → 0 G ∈ D
49 0ne1 ⊢ 0 ≠ 1
50 1 2 3 4 11 48 8 dchrn0 ⊢ φ → 0 G ⁡ A ≠ 0 ↔ A ∈ Unit ⁡ Z
51 50 necon1bbid ⊢ φ → ¬ A ∈ Unit ⁡ Z ↔ 0 G ⁡ A = 0
52 51 biimpa ⊢ φ ∧ ¬ A ∈ Unit ⁡ Z → 0 G ⁡ A = 0
53 52 neeq1d ⊢ φ ∧ ¬ A ∈ Unit ⁡ Z → 0 G ⁡ A ≠ 1 ↔ 0 ≠ 1
54 49 53 mpbiri ⊢ φ ∧ ¬ A ∈ Unit ⁡ Z → 0 G ⁡ A ≠ 1
55 fveq1 ⊢ x = 0 G → x ⁡ A = 0 G ⁡ A
56 55 neeq1d ⊢ x = 0 G → x ⁡ A ≠ 1 ↔ 0 G ⁡ A ≠ 1
57 56 rspcev ⊢ 0 G ∈ D ∧ 0 G ⁡ A ≠ 1 → ∃ x ∈ D x ⁡ A ≠ 1
58 48 54 57 syl2an2r ⊢ φ ∧ ¬ A ∈ Unit ⁡ Z → ∃ x ∈ D x ⁡ A ≠ 1
59 43 58 pm2.61dan ⊢ φ → ∃ x ∈ D x ⁡ A ≠ 1