Metamath Proof Explorer


Theorem lgsdchr

Description: The Legendre symbol function X ( m ) = ( m /L N ) , where N is an odd positive number, is a real Dirichlet character modulo N . (Contributed by Mario Carneiro, 28-Apr-2016)

Ref Expression
Hypotheses lgsdchr.g
|- G = ( DChr ` N )
lgsdchr.z
|- Z = ( Z/nZ ` N )
lgsdchr.d
|- D = ( Base ` G )
lgsdchr.b
|- B = ( Base ` Z )
lgsdchr.l
|- L = ( ZRHom ` Z )
lgsdchr.x
|- X = ( y e. B |-> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) )
Assertion lgsdchr
|- ( ( N e. NN /\ -. 2 || N ) -> ( X e. D /\ X : B --> RR ) )

Proof

Step Hyp Ref Expression
1 lgsdchr.g
 |-  G = ( DChr ` N )
2 lgsdchr.z
 |-  Z = ( Z/nZ ` N )
3 lgsdchr.d
 |-  D = ( Base ` G )
4 lgsdchr.b
 |-  B = ( Base ` Z )
5 lgsdchr.l
 |-  L = ( ZRHom ` Z )
6 lgsdchr.x
 |-  X = ( y e. B |-> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) )
7 iotaex
 |-  ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) e. _V
8 7 a1i
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ y e. B ) -> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) e. _V )
9 6 a1i
 |-  ( ( N e. NN /\ -. 2 || N ) -> X = ( y e. B |-> ( iota h E. m e. ZZ ( y = ( L ` m ) /\ h = ( m /L N ) ) ) ) )
10 nnnn0
 |-  ( N e. NN -> N e. NN0 )
11 10 adantr
 |-  ( ( N e. NN /\ -. 2 || N ) -> N e. NN0 )
12 2 4 5 znzrhfo
 |-  ( N e. NN0 -> L : ZZ -onto-> B )
13 11 12 syl
 |-  ( ( N e. NN /\ -. 2 || N ) -> L : ZZ -onto-> B )
14 foelrn
 |-  ( ( L : ZZ -onto-> B /\ x e. B ) -> E. a e. ZZ x = ( L ` a ) )
15 13 14 sylan
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ x e. B ) -> E. a e. ZZ x = ( L ` a ) )
16 1 2 3 4 5 6 lgsdchrval
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( X ` ( L ` a ) ) = ( a /L N ) )
17 simpr
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> a e. ZZ )
18 nnz
 |-  ( N e. NN -> N e. ZZ )
19 18 ad2antrr
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> N e. ZZ )
20 lgscl
 |-  ( ( a e. ZZ /\ N e. ZZ ) -> ( a /L N ) e. ZZ )
21 17 19 20 syl2anc
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( a /L N ) e. ZZ )
22 21 zred
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( a /L N ) e. RR )
23 16 22 eqeltrd
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( X ` ( L ` a ) ) e. RR )
24 fveq2
 |-  ( x = ( L ` a ) -> ( X ` x ) = ( X ` ( L ` a ) ) )
25 24 eleq1d
 |-  ( x = ( L ` a ) -> ( ( X ` x ) e. RR <-> ( X ` ( L ` a ) ) e. RR ) )
26 23 25 syl5ibrcom
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( x = ( L ` a ) -> ( X ` x ) e. RR ) )
27 26 rexlimdva
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( E. a e. ZZ x = ( L ` a ) -> ( X ` x ) e. RR ) )
28 27 imp
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ E. a e. ZZ x = ( L ` a ) ) -> ( X ` x ) e. RR )
29 15 28 syldan
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ x e. B ) -> ( X ` x ) e. RR )
30 8 9 29 fmpt2d
 |-  ( ( N e. NN /\ -. 2 || N ) -> X : B --> RR )
31 ax-resscn
 |-  RR C_ CC
32 fss
 |-  ( ( X : B --> RR /\ RR C_ CC ) -> X : B --> CC )
33 30 31 32 sylancl
 |-  ( ( N e. NN /\ -. 2 || N ) -> X : B --> CC )
34 eqid
 |-  ( Unit ` Z ) = ( Unit ` Z )
35 4 34 unitss
 |-  ( Unit ` Z ) C_ B
36 foelrn
 |-  ( ( L : ZZ -onto-> B /\ y e. B ) -> E. b e. ZZ y = ( L ` b ) )
37 13 36 sylan
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ y e. B ) -> E. b e. ZZ y = ( L ` b ) )
38 15 37 anim12dan
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( x e. B /\ y e. B ) ) -> ( E. a e. ZZ x = ( L ` a ) /\ E. b e. ZZ y = ( L ` b ) ) )
39 reeanv
 |-  ( E. a e. ZZ E. b e. ZZ ( x = ( L ` a ) /\ y = ( L ` b ) ) <-> ( E. a e. ZZ x = ( L ` a ) /\ E. b e. ZZ y = ( L ` b ) ) )
40 17 adantrr
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> a e. ZZ )
41 simprr
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> b e. ZZ )
42 11 adantr
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> N e. NN0 )
43 lgsdirnn0
 |-  ( ( a e. ZZ /\ b e. ZZ /\ N e. NN0 ) -> ( ( a x. b ) /L N ) = ( ( a /L N ) x. ( b /L N ) ) )
44 40 41 42 43 syl3anc
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a x. b ) /L N ) = ( ( a /L N ) x. ( b /L N ) ) )
45 2 zncrng
 |-  ( N e. NN0 -> Z e. CRing )
46 11 45 syl
 |-  ( ( N e. NN /\ -. 2 || N ) -> Z e. CRing )
47 crngring
 |-  ( Z e. CRing -> Z e. Ring )
48 46 47 syl
 |-  ( ( N e. NN /\ -. 2 || N ) -> Z e. Ring )
49 48 adantr
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> Z e. Ring )
50 5 zrhrhm
 |-  ( Z e. Ring -> L e. ( ZZring RingHom Z ) )
51 49 50 syl
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> L e. ( ZZring RingHom Z ) )
52 zringbas
 |-  ZZ = ( Base ` ZZring )
53 zringmulr
 |-  x. = ( .r ` ZZring )
54 eqid
 |-  ( .r ` Z ) = ( .r ` Z )
55 52 53 54 rhmmul
 |-  ( ( L e. ( ZZring RingHom Z ) /\ a e. ZZ /\ b e. ZZ ) -> ( L ` ( a x. b ) ) = ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) )
56 51 40 41 55 syl3anc
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( L ` ( a x. b ) ) = ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) )
57 56 fveq2d
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( L ` ( a x. b ) ) ) = ( X ` ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) )
58 zmulcl
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> ( a x. b ) e. ZZ )
59 1 2 3 4 5 6 lgsdchrval
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a x. b ) e. ZZ ) -> ( X ` ( L ` ( a x. b ) ) ) = ( ( a x. b ) /L N ) )
60 58 59 sylan2
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( L ` ( a x. b ) ) ) = ( ( a x. b ) /L N ) )
61 57 60 eqtr3d
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) = ( ( a x. b ) /L N ) )
62 16 adantrr
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( L ` a ) ) = ( a /L N ) )
63 1 2 3 4 5 6 lgsdchrval
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ b e. ZZ ) -> ( X ` ( L ` b ) ) = ( b /L N ) )
64 63 adantrl
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( L ` b ) ) = ( b /L N ) )
65 62 64 oveq12d
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( X ` ( L ` a ) ) x. ( X ` ( L ` b ) ) ) = ( ( a /L N ) x. ( b /L N ) ) )
66 44 61 65 3eqtr4d
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( X ` ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) = ( ( X ` ( L ` a ) ) x. ( X ` ( L ` b ) ) ) )
67 oveq12
 |-  ( ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( x ( .r ` Z ) y ) = ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) )
68 67 fveq2d
 |-  ( ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( X ` ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) )
69 fveq2
 |-  ( y = ( L ` b ) -> ( X ` y ) = ( X ` ( L ` b ) ) )
70 24 69 oveqan12d
 |-  ( ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( ( X ` x ) x. ( X ` y ) ) = ( ( X ` ( L ` a ) ) x. ( X ` ( L ` b ) ) ) )
71 68 70 eqeq12d
 |-  ( ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) <-> ( X ` ( ( L ` a ) ( .r ` Z ) ( L ` b ) ) ) = ( ( X ` ( L ` a ) ) x. ( X ` ( L ` b ) ) ) ) )
72 66 71 syl5ibrcom
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
73 72 rexlimdvva
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( E. a e. ZZ E. b e. ZZ ( x = ( L ` a ) /\ y = ( L ` b ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
74 39 73 syl5bir
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( ( E. a e. ZZ x = ( L ` a ) /\ E. b e. ZZ y = ( L ` b ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
75 74 imp
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( E. a e. ZZ x = ( L ` a ) /\ E. b e. ZZ y = ( L ` b ) ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
76 38 75 syldan
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ ( x e. B /\ y e. B ) ) -> ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
77 76 ralrimivva
 |-  ( ( N e. NN /\ -. 2 || N ) -> A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
78 ss2ralv
 |-  ( ( Unit ` Z ) C_ B -> ( A. x e. B A. y e. B ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) -> A. x e. ( Unit ` Z ) A. y e. ( Unit ` Z ) ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) ) )
79 35 77 78 mpsyl
 |-  ( ( N e. NN /\ -. 2 || N ) -> A. x e. ( Unit ` Z ) A. y e. ( Unit ` Z ) ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) )
80 1z
 |-  1 e. ZZ
81 1 2 3 4 5 6 lgsdchrval
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ 1 e. ZZ ) -> ( X ` ( L ` 1 ) ) = ( 1 /L N ) )
82 80 81 mpan2
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( X ` ( L ` 1 ) ) = ( 1 /L N ) )
83 eqid
 |-  ( 1r ` Z ) = ( 1r ` Z )
84 5 83 zrh1
 |-  ( Z e. Ring -> ( L ` 1 ) = ( 1r ` Z ) )
85 48 84 syl
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( L ` 1 ) = ( 1r ` Z ) )
86 85 fveq2d
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( X ` ( L ` 1 ) ) = ( X ` ( 1r ` Z ) ) )
87 18 adantr
 |-  ( ( N e. NN /\ -. 2 || N ) -> N e. ZZ )
88 1lgs
 |-  ( N e. ZZ -> ( 1 /L N ) = 1 )
89 87 88 syl
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( 1 /L N ) = 1 )
90 82 86 89 3eqtr3d
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( X ` ( 1r ` Z ) ) = 1 )
91 lgsne0
 |-  ( ( a e. ZZ /\ N e. ZZ ) -> ( ( a /L N ) =/= 0 <-> ( a gcd N ) = 1 ) )
92 17 19 91 syl2anc
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( ( a /L N ) =/= 0 <-> ( a gcd N ) = 1 ) )
93 92 biimpd
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( ( a /L N ) =/= 0 -> ( a gcd N ) = 1 ) )
94 16 neeq1d
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( ( X ` ( L ` a ) ) =/= 0 <-> ( a /L N ) =/= 0 ) )
95 2 34 5 znunit
 |-  ( ( N e. NN0 /\ a e. ZZ ) -> ( ( L ` a ) e. ( Unit ` Z ) <-> ( a gcd N ) = 1 ) )
96 11 95 sylan
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( ( L ` a ) e. ( Unit ` Z ) <-> ( a gcd N ) = 1 ) )
97 93 94 96 3imtr4d
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( ( X ` ( L ` a ) ) =/= 0 -> ( L ` a ) e. ( Unit ` Z ) ) )
98 24 neeq1d
 |-  ( x = ( L ` a ) -> ( ( X ` x ) =/= 0 <-> ( X ` ( L ` a ) ) =/= 0 ) )
99 eleq1
 |-  ( x = ( L ` a ) -> ( x e. ( Unit ` Z ) <-> ( L ` a ) e. ( Unit ` Z ) ) )
100 98 99 imbi12d
 |-  ( x = ( L ` a ) -> ( ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) <-> ( ( X ` ( L ` a ) ) =/= 0 -> ( L ` a ) e. ( Unit ` Z ) ) ) )
101 97 100 syl5ibrcom
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ a e. ZZ ) -> ( x = ( L ` a ) -> ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) )
102 101 rexlimdva
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( E. a e. ZZ x = ( L ` a ) -> ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) )
103 102 imp
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ E. a e. ZZ x = ( L ` a ) ) -> ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) )
104 15 103 syldan
 |-  ( ( ( N e. NN /\ -. 2 || N ) /\ x e. B ) -> ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) )
105 104 ralrimiva
 |-  ( ( N e. NN /\ -. 2 || N ) -> A. x e. B ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) )
106 79 90 105 3jca
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( A. x e. ( Unit ` Z ) A. y e. ( Unit ` Z ) ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) )
107 simpl
 |-  ( ( N e. NN /\ -. 2 || N ) -> N e. NN )
108 1 2 4 34 107 3 dchrelbas3
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( X e. D <-> ( X : B --> CC /\ ( A. x e. ( Unit ` Z ) A. y e. ( Unit ` Z ) ( X ` ( x ( .r ` Z ) y ) ) = ( ( X ` x ) x. ( X ` y ) ) /\ ( X ` ( 1r ` Z ) ) = 1 /\ A. x e. B ( ( X ` x ) =/= 0 -> x e. ( Unit ` Z ) ) ) ) ) )
109 33 106 108 mpbir2and
 |-  ( ( N e. NN /\ -. 2 || N ) -> X e. D )
110 109 30 jca
 |-  ( ( N e. NN /\ -. 2 || N ) -> ( X e. D /\ X : B --> RR ) )