Theorem dchr1re

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

	Ref	Expression
Hypotheses	dchr1re.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
	dchr1re.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
	dchr1re.o	$$⊢\underset{\dot{}}{1}=0_G$$
	dchr1re.b	$$⊢B={\mathrm{Base}}_Z$$
	dchr1re.n	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	dchr1re	$$⊢\phi \to \underset{\dot{}}{1}:B⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		dchr1re.g	$$⊢G=\mathrm{DChr}\left(N\right)$$
2		dchr1re.z	$$⊢Z=\mathbb{Z}/N\mathbb{Z}$$
3		dchr1re.o	$$⊢\underset{\dot{}}{1}=0_G$$
4		dchr1re.b	$$⊢B={\mathrm{Base}}_Z$$
5		dchr1re.n	$$⊢\phi \to N\in \mathbb{N}$$
6		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
7	1	dchrabl	$$⊢N\in \mathbb{N}\to G\in \mathrm{Abel}$$
8		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
9	6 3	grpidcl	$$⊢G\in \mathrm{Grp}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_G$$
10	5 7 8 9	4syl	$$⊢\phi \to \underset{\dot{}}{1}\in {\mathrm{Base}}_G$$
11	1 2 6 4 10	dchrf	$$⊢\phi \to \underset{\dot{}}{1}:B⟶ℂ$$
12	11	ffnd	$$⊢\phi \to \underset{\dot{}}{1}FnB$$
13		simpr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge \underset{\dot{}}{1}\left(x\right)=0\right)\to \underset{\dot{}}{1}\left(x\right)=0$$
14		0re	$$⊢0\in ℝ$$
15	13 14	eqeltrdi	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge \underset{\dot{}}{1}\left(x\right)=0\right)\to \underset{\dot{}}{1}\left(x\right)\in ℝ$$
16		eqid	$$⊢\mathrm{Unit}\left(Z\right)=\mathrm{Unit}\left(Z\right)$$
17	5	ad2antrr	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge \underset{\dot{}}{1}\left(x\right)\ne 0\right)\to N\in \mathbb{N}$$
18	10	adantr	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_G$$
19		simpr	$$⊢\left(\phi \wedge x\in B\right)\to x\in B$$
20	1 2 6 4 16 18 19	dchrn0	$$⊢\left(\phi \wedge x\in B\right)\to \left(\underset{\dot{}}{1}\left(x\right)\ne 0\leftrightarrow x\in \mathrm{Unit}\left(Z\right)\right)$$
21	20	biimpa	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge \underset{\dot{}}{1}\left(x\right)\ne 0\right)\to x\in \mathrm{Unit}\left(Z\right)$$
22	1 2 3 16 17 21	dchr1	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge \underset{\dot{}}{1}\left(x\right)\ne 0\right)\to \underset{\dot{}}{1}\left(x\right)=1$$
23		1re	$$⊢1\in ℝ$$
24	22 23	eqeltrdi	$$⊢\left(\left(\phi \wedge x\in B\right)\wedge \underset{\dot{}}{1}\left(x\right)\ne 0\right)\to \underset{\dot{}}{1}\left(x\right)\in ℝ$$
25	15 24	pm2.61dane	$$⊢\left(\phi \wedge x\in B\right)\to \underset{\dot{}}{1}\left(x\right)\in ℝ$$
26	25	ralrimiva	$$⊢\phi \to \forall x\in B\underset{\dot{}}{1}\left(x\right)\in ℝ$$
27		ffnfv	$$⊢\underset{\dot{}}{1}:B⟶ℝ\leftrightarrow \left(\underset{\dot{}}{1}FnB\wedge \forall x\in B\underset{\dot{}}{1}\left(x\right)\in ℝ\right)$$
28	12 26 27	sylanbrc	$$⊢\phi \to \underset{\dot{}}{1}:B⟶ℝ$$