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=\mathbb{Z}/N\mathbb{Z}$$
	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\leftrightarrow A\in U\right)$$

Proof

Step	Hyp	Ref	Expression
1		dchrmhm.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrmhm.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
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\leftrightarrow X\left(A\right)\ne 0\right)$$
10		eleq1	$$⊢x=A\to \left(x\in U\leftrightarrow A\in U\right)$$
11	9 10	imbi12d	$$⊢x=A\to \left(\left(X\left(x\right)\ne 0\to x\in U\right)\leftrightarrow \left(X\left(A\right)\ne 0\to A\in U\right)\right)$$
12	1 3	dchrrcl	$$⊢X\in D\to N\in \mathbb{N}$$
13	6 12	syl	$$⊢\phi \to N\in \mathbb{N}$$
14	1 2 4 5 13 3	dchrelbas2	$$⊢\phi \to \left(X\in D\leftrightarrow \left(X\in \left({\mathrm{mulGrp}}_Z\mathrm{MndHom}{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}\right)\wedge \forall x\in B\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\left(X\left(x\right)\ne 0\to x\in U\right)\right)$$
16	15	simprd	$$⊢\phi \to \forall x\in B\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 {\mathbb{N}}_0$$
22	2	zncrng	$$⊢N\in {\mathbb{N}}_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	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
41	39 40	mgpplusg	$$⊢\times ={+}_{{\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\leftrightarrow A\in U\right)$$