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 ⊢ 𝐺 = ( DChr ‘ 𝑁 )
dchrabs2.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
dchrabs2.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
dchrabs2.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
dchrabs2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrabs2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
Assertion dchrabs2 ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ≤ 1 )

Proof

Step Hyp Ref Expression
1 dchrabs2.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
2 dchrabs2.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
3 dchrabs2.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
4 dchrabs2.b ⊢ 𝐵 = ( Base ‘ 𝑍 )
5 dchrabs2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
6 dchrabs2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7 simpr ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 𝐴 ) = 0 ) → ( 𝑋 ‘ 𝐴 ) = 0 )
8 7 abs00bd ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 𝐴 ) = 0 ) → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) = 0 )
9 0le1 ⊢ 0 ≤ 1
10 8 9 eqbrtrdi ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 𝐴 ) = 0 ) → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ≤ 1 )
11 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 𝐴 ) ≠ 0 ) → 𝑋 ∈ 𝐷 )
12 eqid ⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
13 1 3 2 4 12 5 6 dchrn0 ⊢ ( 𝜑 → ( ( 𝑋 ‘ 𝐴 ) ≠ 0 ↔ 𝐴 ∈ ( Unit ‘ 𝑍 ) ) )
14 13 biimpa ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ ( Unit ‘ 𝑍 ) )
15 1 2 11 3 12 14 dchrabs ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 𝐴 ) ≠ 0 ) → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) = 1 )
16 1le1 ⊢ 1 ≤ 1
17 15 16 eqbrtrdi ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 𝐴 ) ≠ 0 ) → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ≤ 1 )
18 10 17 pm2.61dane ⊢ ( 𝜑 → ( abs ‘ ( 𝑋 ‘ 𝐴 ) ) ≤ 1 )