This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )