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 )