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	biimtrrid	|- ( ( 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 ) )