Metamath Proof Explorer


Theorem lgsdchrval

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

Ref Expression
Hypotheses lgsdchr.g G = DChr N
lgsdchr.z Z = /N
lgsdchr.d D = Base G
lgsdchr.b B = Base Z
lgsdchr.l L = ℤRHom Z
lgsdchr.x X = y B ι h | m y = L m h = m / L N
Assertion lgsdchrval N ¬ 2 N A X L A = A / L N

Proof

Step Hyp Ref Expression
1 lgsdchr.g G = DChr N
2 lgsdchr.z Z = /N
3 lgsdchr.d D = Base G
4 lgsdchr.b B = Base Z
5 lgsdchr.l L = ℤRHom Z
6 lgsdchr.x X = y B ι h | m y = L m h = m / L N
7 nnnn0 N N 0
8 7 adantr N ¬ 2 N N 0
9 2 4 5 znzrhfo N 0 L : onto B
10 fof L : onto B L : B
11 8 9 10 3syl N ¬ 2 N L : B
12 11 ffvelrnda N ¬ 2 N A L A B
13 eqeq1 y = L A y = L m L A = L m
14 13 anbi1d y = L A y = L m h = m / L N L A = L m h = m / L N
15 14 rexbidv y = L A m y = L m h = m / L N m L A = L m h = m / L N
16 15 iotabidv y = L A ι h | m y = L m h = m / L N = ι h | m L A = L m h = m / L N
17 iotaex ι h | m y = L m h = m / L N V
18 16 6 17 fvmpt3i L A B X L A = ι h | m L A = L m h = m / L N
19 12 18 syl N ¬ 2 N A X L A = ι h | m L A = L m h = m / L N
20 ovex A / L N V
21 simprr N ¬ 2 N A m L A = L m L A = L m
22 simplll N ¬ 2 N A m L A = L m N
23 22 7 syl N ¬ 2 N A m L A = L m N 0
24 simplr N ¬ 2 N A m L A = L m A
25 simprl N ¬ 2 N A m L A = L m m
26 2 5 zndvds N 0 A m L A = L m N A m
27 23 24 25 26 syl3anc N ¬ 2 N A m L A = L m L A = L m N A m
28 21 27 mpbid N ¬ 2 N A m L A = L m N A m
29 moddvds N A m A mod N = m mod N N A m
30 22 24 25 29 syl3anc N ¬ 2 N A m L A = L m A mod N = m mod N N A m
31 28 30 mpbird N ¬ 2 N A m L A = L m A mod N = m mod N
32 31 oveq1d N ¬ 2 N A m L A = L m A mod N / L N = m mod N / L N
33 simpllr N ¬ 2 N A m L A = L m ¬ 2 N
34 lgsmod A N ¬ 2 N A mod N / L N = A / L N
35 24 22 33 34 syl3anc N ¬ 2 N A m L A = L m A mod N / L N = A / L N
36 lgsmod m N ¬ 2 N m mod N / L N = m / L N
37 25 22 33 36 syl3anc N ¬ 2 N A m L A = L m m mod N / L N = m / L N
38 32 35 37 3eqtr3d N ¬ 2 N A m L A = L m A / L N = m / L N
39 38 eqeq2d N ¬ 2 N A m L A = L m h = A / L N h = m / L N
40 39 biimprd N ¬ 2 N A m L A = L m h = m / L N h = A / L N
41 40 anassrs N ¬ 2 N A m L A = L m h = m / L N h = A / L N
42 41 expimpd N ¬ 2 N A m L A = L m h = m / L N h = A / L N
43 42 rexlimdva N ¬ 2 N A m L A = L m h = m / L N h = A / L N
44 fveq2 m = A L m = L A
45 44 eqcomd m = A L A = L m
46 45 biantrurd m = A h = m / L N L A = L m h = m / L N
47 oveq1 m = A m / L N = A / L N
48 47 eqeq2d m = A h = m / L N h = A / L N
49 46 48 bitr3d m = A L A = L m h = m / L N h = A / L N
50 49 rspcev A h = A / L N m L A = L m h = m / L N
51 50 ex A h = A / L N m L A = L m h = m / L N
52 51 adantl N ¬ 2 N A h = A / L N m L A = L m h = m / L N
53 43 52 impbid N ¬ 2 N A m L A = L m h = m / L N h = A / L N
54 53 adantr N ¬ 2 N A A / L N V m L A = L m h = m / L N h = A / L N
55 54 iota5 N ¬ 2 N A A / L N V ι h | m L A = L m h = m / L N = A / L N
56 20 55 mpan2 N ¬ 2 N A ι h | m L A = L m h = m / L N = A / L N
57 19 56 eqtrd N ¬ 2 N A X L A = A / L N