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 = ℤ/Nℤ
dchrabs2.b ⊢ B = Base Z
dchrabs2.x ⊢ φ → X ∈ D
dchrabs2.a ⊢ φ → A ∈ B
Assertion dchrabs2 ⊢ φ → X ⁡ A ≤ 1

Proof

Step Hyp Ref Expression
1 dchrabs2.g ⊢ G = DChr ⁡ N
2 dchrabs2.d ⊢ D = Base G
3 dchrabs2.z ⊢ Z = ℤ/Nℤ
4 dchrabs2.b ⊢ B = Base Z
5 dchrabs2.x ⊢ φ → X ∈ D
6 dchrabs2.a ⊢ φ → A ∈ B
7 simpr ⊢ φ ∧ X ⁡ A = 0 → X ⁡ A = 0
8 7 abs00bd ⊢ φ ∧ X ⁡ A = 0 → X ⁡ A = 0
9 0le1 ⊢ 0 ≤ 1
10 8 9 eqbrtrdi ⊢ φ ∧ X ⁡ A = 0 → X ⁡ A ≤ 1
11 5 adantr ⊢ φ ∧ X ⁡ A ≠ 0 → X ∈ D
12 eqid ⊢ Unit ⁡ Z = Unit ⁡ Z
13 1 3 2 4 12 5 6 dchrn0 ⊢ φ → X ⁡ A ≠ 0 ↔ A ∈ Unit ⁡ Z
14 13 biimpa ⊢ φ ∧ X ⁡ A ≠ 0 → A ∈ Unit ⁡ Z
15 1 2 11 3 12 14 dchrabs ⊢ φ ∧ X ⁡ A ≠ 0 → X ⁡ A = 1
16 1le1 ⊢ 1 ≤ 1
17 15 16 eqbrtrdi ⊢ φ ∧ X ⁡ A ≠ 0 → X ⁡ A ≤ 1
18 10 17 pm2.61dane ⊢ φ → X ⁡ A ≤ 1