# Metamath Proof Explorer

## Theorem dchrn0

Description: A Dirichlet character is nonzero on the units of Z/nZ . (Contributed by Mario Carneiro, 18-Apr-2016)

Ref Expression
Hypotheses dchrmhm.g ${⊢}{G}=\mathrm{DChr}\left({N}\right)$
dchrmhm.z ${⊢}{Z}=ℤ/{N}ℤ$
dchrmhm.b ${⊢}{D}={\mathrm{Base}}_{{G}}$
dchrn0.b ${⊢}{B}={\mathrm{Base}}_{{Z}}$
dchrn0.u ${⊢}{U}=\mathrm{Unit}\left({Z}\right)$
dchrn0.x ${⊢}{\phi }\to {X}\in {D}$
dchrn0.a ${⊢}{\phi }\to {A}\in {B}$
Assertion dchrn0 ${⊢}{\phi }\to \left({X}\left({A}\right)\ne 0↔{A}\in {U}\right)$

### Proof

Step Hyp Ref Expression
1 dchrmhm.g ${⊢}{G}=\mathrm{DChr}\left({N}\right)$
2 dchrmhm.z ${⊢}{Z}=ℤ/{N}ℤ$
3 dchrmhm.b ${⊢}{D}={\mathrm{Base}}_{{G}}$
4 dchrn0.b ${⊢}{B}={\mathrm{Base}}_{{Z}}$
5 dchrn0.u ${⊢}{U}=\mathrm{Unit}\left({Z}\right)$
6 dchrn0.x ${⊢}{\phi }\to {X}\in {D}$
7 dchrn0.a ${⊢}{\phi }\to {A}\in {B}$
8 fveq2 ${⊢}{x}={A}\to {X}\left({x}\right)={X}\left({A}\right)$
9 8 neeq1d ${⊢}{x}={A}\to \left({X}\left({x}\right)\ne 0↔{X}\left({A}\right)\ne 0\right)$
10 eleq1 ${⊢}{x}={A}\to \left({x}\in {U}↔{A}\in {U}\right)$
11 9 10 imbi12d ${⊢}{x}={A}\to \left(\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)↔\left({X}\left({A}\right)\ne 0\to {A}\in {U}\right)\right)$
12 1 3 dchrrcl ${⊢}{X}\in {D}\to {N}\in ℕ$
13 6 12 syl ${⊢}{\phi }\to {N}\in ℕ$
14 1 2 4 5 13 3 dchrelbas2 ${⊢}{\phi }\to \left({X}\in {D}↔\left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)\right)$
15 6 14 mpbid ${⊢}{\phi }\to \left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)\right)$
16 15 simprd ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}\left({X}\left({x}\right)\ne 0\to {x}\in {U}\right)$
17 11 16 7 rspcdva ${⊢}{\phi }\to \left({X}\left({A}\right)\ne 0\to {A}\in {U}\right)$
18 17 imp ${⊢}\left({\phi }\wedge {X}\left({A}\right)\ne 0\right)\to {A}\in {U}$
19 ax-1ne0 ${⊢}1\ne 0$
20 19 a1i ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to 1\ne 0$
21 13 nnnn0d ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
22 2 zncrng ${⊢}{N}\in {ℕ}_{0}\to {Z}\in \mathrm{CRing}$
23 crngring ${⊢}{Z}\in \mathrm{CRing}\to {Z}\in \mathrm{Ring}$
24 21 22 23 3syl ${⊢}{\phi }\to {Z}\in \mathrm{Ring}$
25 eqid ${⊢}{inv}_{r}\left({Z}\right)={inv}_{r}\left({Z}\right)$
26 eqid ${⊢}{\cdot }_{{Z}}={\cdot }_{{Z}}$
27 eqid ${⊢}{1}_{{Z}}={1}_{{Z}}$
28 5 25 26 27 unitrinv ${⊢}\left({Z}\in \mathrm{Ring}\wedge {A}\in {U}\right)\to {A}{\cdot }_{{Z}}{inv}_{r}\left({Z}\right)\left({A}\right)={1}_{{Z}}$
29 24 28 sylan ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {A}{\cdot }_{{Z}}{inv}_{r}\left({Z}\right)\left({A}\right)={1}_{{Z}}$
30 29 fveq2d ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {X}\left({A}{\cdot }_{{Z}}{inv}_{r}\left({Z}\right)\left({A}\right)\right)={X}\left({1}_{{Z}}\right)$
31 15 simpld ${⊢}{\phi }\to {X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$
32 31 adantr ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)$
33 7 adantr ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {A}\in {B}$
34 5 25 4 ringinvcl ${⊢}\left({Z}\in \mathrm{Ring}\wedge {A}\in {U}\right)\to {inv}_{r}\left({Z}\right)\left({A}\right)\in {B}$
35 24 34 sylan ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {inv}_{r}\left({Z}\right)\left({A}\right)\in {B}$
36 eqid ${⊢}{\mathrm{mulGrp}}_{{Z}}={\mathrm{mulGrp}}_{{Z}}$
37 36 4 mgpbas ${⊢}{B}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Z}}}$
38 36 26 mgpplusg ${⊢}{\cdot }_{{Z}}={+}_{{\mathrm{mulGrp}}_{{Z}}}$
39 eqid ${⊢}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}={\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}$
40 cnfldmul ${⊢}×={\cdot }_{{ℂ}_{\mathrm{fld}}}$
41 39 40 mgpplusg ${⊢}×={+}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$
42 37 38 41 mhmlin ${⊢}\left({X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge {A}\in {B}\wedge {inv}_{r}\left({Z}\right)\left({A}\right)\in {B}\right)\to {X}\left({A}{\cdot }_{{Z}}{inv}_{r}\left({Z}\right)\left({A}\right)\right)={X}\left({A}\right){X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)$
43 32 33 35 42 syl3anc ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {X}\left({A}{\cdot }_{{Z}}{inv}_{r}\left({Z}\right)\left({A}\right)\right)={X}\left({A}\right){X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)$
44 36 27 ringidval ${⊢}{1}_{{Z}}={0}_{{\mathrm{mulGrp}}_{{Z}}}$
45 cnfld1 ${⊢}1={1}_{{ℂ}_{\mathrm{fld}}}$
46 39 45 ringidval ${⊢}1={0}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$
47 44 46 mhm0 ${⊢}{X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\to {X}\left({1}_{{Z}}\right)=1$
48 32 47 syl ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {X}\left({1}_{{Z}}\right)=1$
49 30 43 48 3eqtr3d ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {X}\left({A}\right){X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)=1$
50 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
51 39 50 mgpbas ${⊢}ℂ={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$
52 37 51 mhmf ${⊢}{X}\in \left({\mathrm{mulGrp}}_{{Z}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\to {X}:{B}⟶ℂ$
53 32 52 syl ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {X}:{B}⟶ℂ$
54 53 35 ffvelrnd ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)\in ℂ$
55 54 mul02d ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to 0\cdot {X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)=0$
56 20 49 55 3netr4d ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {X}\left({A}\right){X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)\ne 0\cdot {X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)$
57 oveq1 ${⊢}{X}\left({A}\right)=0\to {X}\left({A}\right){X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)=0\cdot {X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)$
58 57 necon3i ${⊢}{X}\left({A}\right){X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)\ne 0\cdot {X}\left({inv}_{r}\left({Z}\right)\left({A}\right)\right)\to {X}\left({A}\right)\ne 0$
59 56 58 syl ${⊢}\left({\phi }\wedge {A}\in {U}\right)\to {X}\left({A}\right)\ne 0$
60 18 59 impbida ${⊢}{\phi }\to \left({X}\left({A}\right)\ne 0↔{A}\in {U}\right)$