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 = ( DChr ` N )
	dchrabs2.d	|- D = ( Base ` G )
	dchrabs2.z	|- Z = ( Z/nZ ` N )
	dchrabs2.b	|- B = ( Base ` Z )
	dchrabs2.x	|- ( ph -> X e. D )
	dchrabs2.a	|- ( ph -> A e. B )
Assertion	dchrabs2	|- ( ph -> ( abs ` ( X ` A ) ) <_ 1 )

Proof

Step	Hyp	Ref	Expression
1		dchrabs2.g	|- G = ( DChr ` N )
2		dchrabs2.d	|- D = ( Base ` G )
3		dchrabs2.z	|- Z = ( Z/nZ ` N )
4		dchrabs2.b	|- B = ( Base ` Z )
5		dchrabs2.x	|- ( ph -> X e. D )
6		dchrabs2.a	|- ( ph -> A e. B )
7		simpr	|- ( ( ph /\ ( X ` A ) = 0 ) -> ( X ` A ) = 0 )
8	7	abs00bd	|- ( ( ph /\ ( X ` A ) = 0 ) -> ( abs ` ( X ` A ) ) = 0 )
9		0le1	|- 0 <_ 1
10	8 9	eqbrtrdi	|- ( ( ph /\ ( X ` A ) = 0 ) -> ( abs ` ( X ` A ) ) <_ 1 )
11	5	adantr	|- ( ( ph /\ ( X ` A ) =/= 0 ) -> X e. D )
12		eqid	|- ( Unit ` Z ) = ( Unit ` Z )
13	1 3 2 4 12 5 6	dchrn0	|- ( ph -> ( ( X ` A ) =/= 0 <-> A e. ( Unit ` Z ) ) )
14	13	biimpa	|- ( ( ph /\ ( X ` A ) =/= 0 ) -> A e. ( Unit ` Z ) )
15	1 2 11 3 12 14	dchrabs	|- ( ( ph /\ ( X ` A ) =/= 0 ) -> ( abs ` ( X ` A ) ) = 1 )
16		1le1	|- 1 <_ 1
17	15 16	eqbrtrdi	|- ( ( ph /\ ( X ` A ) =/= 0 ) -> ( abs ` ( X ` A ) ) <_ 1 )
18	10 17	pm2.61dane	|- ( ph -> ( abs ` ( X ` A ) ) <_ 1 )