Metamath Proof Explorer

Theorem dchr1re

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

Ref Expression
Hypotheses dchr1re.g 
|- G = ( DChr ` N )
dchr1re.z 
|- Z = ( Z/nZ ` N )
dchr1re.o 
|- .1. = ( 0g ` G )
dchr1re.b 
|- B = ( Base ` Z )
dchr1re.n 
|- ( ph -> N e. NN )
Assertion dchr1re 
|- ( ph -> .1. : B --> RR )

Proof

Step Hyp Ref Expression
1 dchr1re.g 
 |-  G = ( DChr ` N )
2 dchr1re.z 
 |-  Z = ( Z/nZ ` N )
3 dchr1re.o 
 |-  .1. = ( 0g ` G )
4 dchr1re.b 
 |-  B = ( Base ` Z )
5 dchr1re.n 
 |-  ( ph -> N e. NN )
6 eqid 
 |-  ( Base ` G ) = ( Base ` G )
7 1 dchrabl 
 |-  ( N e. NN -> G e. Abel )
8 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
9 6 3 grpidcl 
 |-  ( G e. Grp -> .1. e. ( Base ` G ) )
10 5 7 8 9 4syl 
 |-  ( ph -> .1. e. ( Base ` G ) )
11 1 2 6 4 10 dchrf 
 |-  ( ph -> .1. : B --> CC )
12 11 ffnd 
 |-  ( ph -> .1. Fn B )
13 simpr 
 |-  ( ( ( ph /\ x e. B ) /\ ( .1. ` x ) = 0 ) -> ( .1. ` x ) = 0 )
14 0re 
 |-  0 e. RR
15 13 14 eqeltrdi 
 |-  ( ( ( ph /\ x e. B ) /\ ( .1. ` x ) = 0 ) -> ( .1. ` x ) e. RR )
16 eqid 
 |-  ( Unit ` Z ) = ( Unit ` Z )
17 5 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ ( .1. ` x ) =/= 0 ) -> N e. NN )
18 10 adantr 
 |-  ( ( ph /\ x e. B ) -> .1. e. ( Base ` G ) )
19 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
20 1 2 6 4 16 18 19 dchrn0 
 |-  ( ( ph /\ x e. B ) -> ( ( .1. ` x ) =/= 0 <-> x e. ( Unit ` Z ) ) )
21 20 biimpa 
 |-  ( ( ( ph /\ x e. B ) /\ ( .1. ` x ) =/= 0 ) -> x e. ( Unit ` Z ) )
22 1 2 3 16 17 21 dchr1 
 |-  ( ( ( ph /\ x e. B ) /\ ( .1. ` x ) =/= 0 ) -> ( .1. ` x ) = 1 )
23 1re 
 |-  1 e. RR
24 22 23 eqeltrdi 
 |-  ( ( ( ph /\ x e. B ) /\ ( .1. ` x ) =/= 0 ) -> ( .1. ` x ) e. RR )
25 15 24 pm2.61dane 
 |-  ( ( ph /\ x e. B ) -> ( .1. ` x ) e. RR )
26 25 ralrimiva 
 |-  ( ph -> A. x e. B ( .1. ` x ) e. RR )
27 ffnfv 
 |-  ( .1. : B --> RR <-> ( .1. Fn B /\ A. x e. B ( .1. ` x ) e. RR ) )
28 12 26 27 sylanbrc 
 |-  ( ph -> .1. : B --> RR )