Theorem dchr1re

Description: The principal Dirichlet character is a real character. (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	dchr1re.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	dchr1re.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	dchr1re.o	⊢ 1 = ( 0g ‘ 𝐺 )
	dchr1re.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
	dchr1re.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	dchr1re	⊢ ( 𝜑 → 1 : 𝐵 ⟶ ℝ )

Proof

Step	Hyp	Ref	Expression
1		dchr1re.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
2		dchr1re.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
3		dchr1re.o	⊢ 1 = ( 0g ‘ 𝐺 )
4		dchr1re.b	⊢ 𝐵 = ( Base ‘ 𝑍 )
5		dchr1re.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
6		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7	1	dchrabl	⊢ ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
8		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
9	6 3	grpidcl	⊢ ( 𝐺 ∈ Grp → 1 ∈ ( Base ‘ 𝐺 ) )
10	5 7 8 9	4syl	⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝐺 ) )
11	1 2 6 4 10	dchrf	⊢ ( 𝜑 → 1 : 𝐵 ⟶ ℂ )
12	11	ffnd	⊢ ( 𝜑 → 1 Fn 𝐵 )
13		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1 ‘ 𝑥 ) = 0 ) → ( 1 ‘ 𝑥 ) = 0 )
14		0re	⊢ 0 ∈ ℝ
15	13 14	eqeltrdi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1 ‘ 𝑥 ) = 0 ) → ( 1 ‘ 𝑥 ) ∈ ℝ )
16		eqid	⊢ ( Unit ‘ 𝑍 ) = ( Unit ‘ 𝑍 )
17	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1 ‘ 𝑥 ) ≠ 0 ) → 𝑁 ∈ ℕ )
18	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 1 ∈ ( Base ‘ 𝐺 ) )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
20	1 2 6 4 16 18 19	dchrn0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 1 ‘ 𝑥 ) ≠ 0 ↔ 𝑥 ∈ ( Unit ‘ 𝑍 ) ) )
21	20	biimpa	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1 ‘ 𝑥 ) ≠ 0 ) → 𝑥 ∈ ( Unit ‘ 𝑍 ) )
22	1 2 3 16 17 21	dchr1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1 ‘ 𝑥 ) ≠ 0 ) → ( 1 ‘ 𝑥 ) = 1 )
23		1re	⊢ 1 ∈ ℝ
24	22 23	eqeltrdi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) ∧ ( 1 ‘ 𝑥 ) ≠ 0 ) → ( 1 ‘ 𝑥 ) ∈ ℝ )
25	15 24	pm2.61dane	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 1 ‘ 𝑥 ) ∈ ℝ )
26	25	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ( 1 ‘ 𝑥 ) ∈ ℝ )
27		ffnfv	⊢ ( 1 : 𝐵 ⟶ ℝ ↔ ( 1 Fn 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 1 ‘ 𝑥 ) ∈ ℝ ) )
28	12 26 27	sylanbrc	⊢ ( 𝜑 → 1 : 𝐵 ⟶ ℝ )