Theorem dchrabs2

Description: A Dirichlet character takes values inside the unit circle. (Contributed by Mario Carneiro, 3-May-2016)

	Ref	Expression
Hypotheses	dchrabs2.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchrabs2.d	$$⊢D={\mathrm{Base}}_G$$
	dchrabs2.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchrabs2.b	$$⊢B={\mathrm{Base}}_Z$$
	dchrabs2.x	$$⊢\phi \to X\in D$$
	dchrabs2.a	$$⊢\phi \to A\in B$$
Assertion	dchrabs2	$$⊢\phi \to \left|X\left(A\right)\right|\le 1$$

Proof

Step	Hyp	Ref	Expression
1		dchrabs2.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchrabs2.d	$$⊢D={\mathrm{Base}}_G$$
3		dchrabs2.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
4		dchrabs2.b	$$⊢B={\mathrm{Base}}_Z$$
5		dchrabs2.x	$$⊢\phi \to X\in D$$
6		dchrabs2.a	$$⊢\phi \to A\in B$$
7		simpr	$$⊢\left(\phi \wedge X\left(A\right)=0\right)\to X\left(A\right)=0$$
8	7	abs00bd	$$⊢\left(\phi \wedge X\left(A\right)=0\right)\to \left|X\left(A\right)\right|=0$$
9		0le1	$$⊢0\le 1$$
10	8 9	eqbrtrdi	$$⊢\left(\phi \wedge X\left(A\right)=0\right)\to \left|X\left(A\right)\right|\le 1$$
11	5	adantr	$$⊢\left(\phi \wedge X\left(A\right)\ne 0\right)\to X\in D$$
12		eqid	$$⊢\mathrm{Unit}\left(Z\right)=\mathrm{Unit}\left(Z\right)$$
13	1 3 2 4 12 5 6	dchrn0	$$⊢\phi \to \left(X\left(A\right)\ne 0\leftrightarrow A\in \mathrm{Unit}\left(Z\right)\right)$$
14	13	biimpa	$$⊢\left(\phi \wedge X\left(A\right)\ne 0\right)\to A\in \mathrm{Unit}\left(Z\right)$$
15	1 2 11 3 12 14	dchrabs	$$⊢\left(\phi \wedge X\left(A\right)\ne 0\right)\to \left|X\left(A\right)\right|=1$$
16		1le1	$$⊢1\le 1$$
17	15 16	eqbrtrdi	$$⊢\left(\phi \wedge X\left(A\right)\ne 0\right)\to \left|X\left(A\right)\right|\le 1$$
18	10 17	pm2.61dane	$$⊢\phi \to \left|X\left(A\right)\right|\le 1$$