| Step | Hyp | Ref
| Expression |
| 1 | | dchrmhm.g |
. . . 4
⊢ 𝐺 = (DChr‘𝑁) |
| 2 | | dchrmhm.b |
. . . 4
⊢ 𝐷 = (Base‘𝐺) |
| 3 | 1, 2 | dchrrcl 27284 |
. . 3
⊢ (𝑋 ∈ 𝐷 → 𝑁 ∈ ℕ) |
| 4 | | dchrmhm.z |
. . . . 5
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
| 5 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝑍) =
(Base‘𝑍) |
| 6 | | eqid 2737 |
. . . . 5
⊢
(Unit‘𝑍) =
(Unit‘𝑍) |
| 7 | | id 22 |
. . . . 5
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ) |
| 8 | 1, 4, 5, 6, 7, 2 | dchrelbas2 27281 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑦 ∈ (Base‘𝑍)((𝑋‘𝑦) ≠ 0 → 𝑦 ∈ (Unit‘𝑍))))) |
| 9 | | nnnn0 12533 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℕ0) |
| 10 | 9 | adantr 480 |
. . . . . . 7
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → 𝑁 ∈
ℕ0) |
| 11 | | dchrelbas4.l |
. . . . . . . 8
⊢ 𝐿 = (ℤRHom‘𝑍) |
| 12 | 4, 5, 11 | znzrhfo 21566 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
| 13 | | fveq2 6906 |
. . . . . . . . . 10
⊢ ((𝐿‘𝑥) = 𝑦 → (𝑋‘(𝐿‘𝑥)) = (𝑋‘𝑦)) |
| 14 | 13 | neeq1d 3000 |
. . . . . . . . 9
⊢ ((𝐿‘𝑥) = 𝑦 → ((𝑋‘(𝐿‘𝑥)) ≠ 0 ↔ (𝑋‘𝑦) ≠ 0)) |
| 15 | | eleq1 2829 |
. . . . . . . . 9
⊢ ((𝐿‘𝑥) = 𝑦 → ((𝐿‘𝑥) ∈ (Unit‘𝑍) ↔ 𝑦 ∈ (Unit‘𝑍))) |
| 16 | 14, 15 | imbi12d 344 |
. . . . . . . 8
⊢ ((𝐿‘𝑥) = 𝑦 → (((𝑋‘(𝐿‘𝑥)) ≠ 0 → (𝐿‘𝑥) ∈ (Unit‘𝑍)) ↔ ((𝑋‘𝑦) ≠ 0 → 𝑦 ∈ (Unit‘𝑍)))) |
| 17 | 16 | cbvfo 7309 |
. . . . . . 7
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → (∀𝑥 ∈ ℤ ((𝑋‘(𝐿‘𝑥)) ≠ 0 → (𝐿‘𝑥) ∈ (Unit‘𝑍)) ↔ ∀𝑦 ∈ (Base‘𝑍)((𝑋‘𝑦) ≠ 0 → 𝑦 ∈ (Unit‘𝑍)))) |
| 18 | 10, 12, 17 | 3syl 18 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (∀𝑥 ∈ ℤ ((𝑋‘(𝐿‘𝑥)) ≠ 0 → (𝐿‘𝑥) ∈ (Unit‘𝑍)) ↔ ∀𝑦 ∈ (Base‘𝑍)((𝑋‘𝑦) ≠ 0 → 𝑦 ∈ (Unit‘𝑍)))) |
| 19 | | df-ne 2941 |
. . . . . . . . . 10
⊢ ((𝑋‘(𝐿‘𝑥)) ≠ 0 ↔ ¬ (𝑋‘(𝐿‘𝑥)) = 0) |
| 20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → ((𝑋‘(𝐿‘𝑥)) ≠ 0 ↔ ¬ (𝑋‘(𝐿‘𝑥)) = 0)) |
| 21 | 4, 6, 11 | znunit 21582 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℤ)
→ ((𝐿‘𝑥) ∈ (Unit‘𝑍) ↔ (𝑥 gcd 𝑁) = 1)) |
| 22 | 10, 21 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → ((𝐿‘𝑥) ∈ (Unit‘𝑍) ↔ (𝑥 gcd 𝑁) = 1)) |
| 23 | | 1red 11262 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → 1 ∈
ℝ) |
| 24 | | simpr 484 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → 𝑥 ∈ ℤ) |
| 25 | | simpll 767 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℕ) |
| 26 | 25 | nnzd 12640 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℤ) |
| 27 | | nnne0 12300 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0) |
| 28 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 0 ∧ 𝑁 = 0) → 𝑁 = 0) |
| 29 | 28 | necon3ai 2965 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ≠ 0 → ¬ (𝑥 = 0 ∧ 𝑁 = 0)) |
| 30 | 25, 27, 29 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → ¬ (𝑥 = 0 ∧ 𝑁 = 0)) |
| 31 | | gcdn0cl 16539 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬
(𝑥 = 0 ∧ 𝑁 = 0)) → (𝑥 gcd 𝑁) ∈ ℕ) |
| 32 | 24, 26, 30, 31 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → (𝑥 gcd 𝑁) ∈ ℕ) |
| 33 | 32 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → (𝑥 gcd 𝑁) ∈ ℝ) |
| 34 | 32 | nnge1d 12314 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → 1 ≤ (𝑥 gcd 𝑁)) |
| 35 | 23, 33, 34 | leltned 11414 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → (1 < (𝑥 gcd 𝑁) ↔ (𝑥 gcd 𝑁) ≠ 1)) |
| 36 | 35 | necon2bbid 2984 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → ((𝑥 gcd 𝑁) = 1 ↔ ¬ 1 < (𝑥 gcd 𝑁))) |
| 37 | 22, 36 | bitrd 279 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → ((𝐿‘𝑥) ∈ (Unit‘𝑍) ↔ ¬ 1 < (𝑥 gcd 𝑁))) |
| 38 | 20, 37 | imbi12d 344 |
. . . . . . . 8
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → (((𝑋‘(𝐿‘𝑥)) ≠ 0 → (𝐿‘𝑥) ∈ (Unit‘𝑍)) ↔ (¬ (𝑋‘(𝐿‘𝑥)) = 0 → ¬ 1 < (𝑥 gcd 𝑁)))) |
| 39 | | con34b 316 |
. . . . . . . 8
⊢ ((1 <
(𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0) ↔ (¬ (𝑋‘(𝐿‘𝑥)) = 0 → ¬ 1 < (𝑥 gcd 𝑁))) |
| 40 | 38, 39 | bitr4di 289 |
. . . . . . 7
⊢ (((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) ∧ 𝑥 ∈ ℤ) → (((𝑋‘(𝐿‘𝑥)) ≠ 0 → (𝐿‘𝑥) ∈ (Unit‘𝑍)) ↔ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0))) |
| 41 | 40 | ralbidva 3176 |
. . . . . 6
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (∀𝑥 ∈ ℤ ((𝑋‘(𝐿‘𝑥)) ≠ 0 → (𝐿‘𝑥) ∈ (Unit‘𝑍)) ↔ ∀𝑥 ∈ ℤ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0))) |
| 42 | 18, 41 | bitr3d 281 |
. . . . 5
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) → (∀𝑦 ∈ (Base‘𝑍)((𝑋‘𝑦) ≠ 0 → 𝑦 ∈ (Unit‘𝑍)) ↔ ∀𝑥 ∈ ℤ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0))) |
| 43 | 42 | pm5.32da 579 |
. . . 4
⊢ (𝑁 ∈ ℕ → ((𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑦 ∈ (Base‘𝑍)((𝑋‘𝑦) ≠ 0 → 𝑦 ∈ (Unit‘𝑍))) ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ ℤ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0)))) |
| 44 | 8, 43 | bitrd 279 |
. . 3
⊢ (𝑁 ∈ ℕ → (𝑋 ∈ 𝐷 ↔ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ ℤ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0)))) |
| 45 | 3, 44 | biadanii 822 |
. 2
⊢ (𝑋 ∈ 𝐷 ↔ (𝑁 ∈ ℕ ∧ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ ℤ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0)))) |
| 46 | | 3anass 1095 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ ℤ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0)) ↔ (𝑁 ∈ ℕ ∧ (𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ ℤ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0)))) |
| 47 | 45, 46 | bitr4i 278 |
1
⊢ (𝑋 ∈ 𝐷 ↔ (𝑁 ∈ ℕ ∧ 𝑋 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) ∧ ∀𝑥 ∈ ℤ (1 < (𝑥 gcd 𝑁) → (𝑋‘(𝐿‘𝑥)) = 0))) |