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 = ℤ / N ℤ$
	lgsdchr.d	$⊢ D = {Base}_{G}$
	lgsdchr.b	$⊢ B = {Base}_{Z}$
	lgsdchr.l	$⊢ L = ℤRHom (Z)$
	lgsdchr.x	$⊢ X = (y \in B ⟼ (ι h \| \exists m \in ℤ (y = L (m) \land h = m /_{L} N)))$
Assertion	lgsdchr	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to (X \in D \land X : B ⟶ ℝ)$

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 \in B ⟼ (ι h \| \exists m \in ℤ (y = L (m) \land h = m /_{L} N)))$
7		iotaex	$⊢ (ι h \| \exists m \in ℤ (y = L (m) \land h = m /_{L} N)) \in V$
8	7	a1i	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land y \in B) \to (ι h \| \exists m \in ℤ (y = L (m) \land h = m /_{L} N)) \in V$
9	6	a1i	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to X = (y \in B ⟼ (ι h \| \exists m \in ℤ (y = L (m) \land h = m /_{L} N)))$
10		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
11	10	adantr	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to N \in ℕ_{0}$
12	2 4 5	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} B$
13	11 12	syl	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to L : ℤ \underset{onto}{⟶} B$
14		foelrn	$⊢ (L : ℤ \underset{onto}{⟶} B \land x \in B) \to \exists a \in ℤ x = L (a)$
15	13 14	sylan	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land x \in B) \to \exists a \in ℤ x = L (a)$
16	1 2 3 4 5 6	lgsdchrval	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to X (L (a)) = a /_{L} N$
17		simpr	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to a \in ℤ$
18		nnz	$⊢ N \in ℕ \to N \in ℤ$
19	18	ad2antrr	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to N \in ℤ$
20		lgscl	$⊢ (a \in ℤ \land N \in ℤ) \to a /_{L} N \in ℤ$
21	17 19 20	syl2anc	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to a /_{L} N \in ℤ$
22	21	zred	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to a /_{L} N \in ℝ$
23	16 22	eqeltrd	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to X (L (a)) \in ℝ$
24		fveq2	$⊢ x = L (a) \to X (x) = X (L (a))$
25	24	eleq1d	$⊢ x = L (a) \to (X (x) \in ℝ \leftrightarrow X (L (a)) \in ℝ)$
26	23 25	syl5ibrcom	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to (x = L (a) \to X (x) \in ℝ)$
27	26	rexlimdva	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to (\exists a \in ℤ x = L (a) \to X (x) \in ℝ)$
28	27	imp	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land \exists a \in ℤ x = L (a)) \to X (x) \in ℝ$
29	15 28	syldan	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land x \in B) \to X (x) \in ℝ$
30	8 9 29	fmpt2d	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to X : B ⟶ ℝ$
31		ax-resscn	$⊢ ℝ \subseteq ℂ$
32		fss	$⊢ (X : B ⟶ ℝ \land ℝ \subseteq ℂ) \to X : B ⟶ ℂ$
33	30 31 32	sylancl	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to X : B ⟶ ℂ$
34		eqid	$⊢ Unit (Z) = Unit (Z)$
35	4 34	unitss	$⊢ Unit (Z) \subseteq B$
36		foelrn	$⊢ (L : ℤ \underset{onto}{⟶} B \land y \in B) \to \exists b \in ℤ y = L (b)$
37	13 36	sylan	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land y \in B) \to \exists b \in ℤ y = L (b)$
38	15 37	anim12dan	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (x \in B \land y \in B)) \to (\exists a \in ℤ x = L (a) \land \exists b \in ℤ y = L (b))$
39		reeanv	$⊢ \exists a \in ℤ \exists b \in ℤ (x = L (a) \land y = L (b)) \leftrightarrow (\exists a \in ℤ x = L (a) \land \exists b \in ℤ y = L (b))$
40	17	adantrr	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to a \in ℤ$
41		simprr	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to b \in ℤ$
42	11	adantr	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to N \in ℕ_{0}$
43		lgsdirnn0	$⊢ (a \in ℤ \land b \in ℤ \land N \in ℕ_{0}) \to a b /_{L} N = (a /_{L} N) (b /_{L} N)$
44	40 41 42 43	syl3anc	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to a b /_{L} N = (a /_{L} N) (b /_{L} N)$
45	2	zncrng	$⊢ N \in ℕ_{0} \to Z \in CRing$
46	11 45	syl	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to Z \in CRing$
47		crngring	$⊢ Z \in CRing \to Z \in Ring$
48	46 47	syl	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to Z \in Ring$
49	48	adantr	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to Z \in Ring$
50	5	zrhrhm	$⊢ Z \in Ring \to L \in (ℤ_{ring} RingHom Z)$
51	49 50	syl	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to L \in (ℤ_{ring} RingHom Z)$
52		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
53		zringmulr	$⊢ \times = \cdot_{ℤ_{ring}}$
54		eqid	$⊢ \cdot_{Z} = \cdot_{Z}$
55	52 53 54	rhmmul	$⊢ (L \in (ℤ_{ring} RingHom Z) \land a \in ℤ \land b \in ℤ) \to L (a b) = L (a) \cdot_{Z} L (b)$
56	51 40 41 55	syl3anc	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to L (a b) = L (a) \cdot_{Z} L (b)$
57	56	fveq2d	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to X (L (a b)) = X (L (a) \cdot_{Z} L (b))$
58		zmulcl	$⊢ (a \in ℤ \land b \in ℤ) \to a b \in ℤ$
59	1 2 3 4 5 6	lgsdchrval	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a b \in ℤ) \to X (L (a b)) = a b /_{L} N$
60	58 59	sylan2	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to X (L (a b)) = a b /_{L} N$
61	57 60	eqtr3d	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to X (L (a) \cdot_{Z} L (b)) = a b /_{L} N$
62	16	adantrr	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to X (L (a)) = a /_{L} N$
63	1 2 3 4 5 6	lgsdchrval	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land b \in ℤ) \to X (L (b)) = b /_{L} N$
64	63	adantrl	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to X (L (b)) = b /_{L} N$
65	62 64	oveq12d	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to X (L (a)) X (L (b)) = (a /_{L} N) (b /_{L} N)$
66	44 61 65	3eqtr4d	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to X (L (a) \cdot_{Z} L (b)) = X (L (a)) X (L (b))$
67		oveq12	$⊢ (x = L (a) \land y = L (b)) \to x \cdot_{Z} y = L (a) \cdot_{Z} L (b)$
68	67	fveq2d	$⊢ (x = L (a) \land y = L (b)) \to X (x \cdot_{Z} y) = X (L (a) \cdot_{Z} L (b))$
69		fveq2	$⊢ y = L (b) \to X (y) = X (L (b))$
70	24 69	oveqan12d	$⊢ (x = L (a) \land y = L (b)) \to X (x) X (y) = X (L (a)) X (L (b))$
71	68 70	eqeq12d	$⊢ (x = L (a) \land y = L (b)) \to (X (x \cdot_{Z} y) = X (x) X (y) \leftrightarrow X (L (a) \cdot_{Z} L (b)) = X (L (a)) X (L (b)))$
72	66 71	syl5ibrcom	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (a \in ℤ \land b \in ℤ)) \to ((x = L (a) \land y = L (b)) \to X (x \cdot_{Z} y) = X (x) X (y))$
73	72	rexlimdvva	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to (\exists a \in ℤ \exists b \in ℤ (x = L (a) \land y = L (b)) \to X (x \cdot_{Z} y) = X (x) X (y))$
74	39 73	syl5bir	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to ((\exists a \in ℤ x = L (a) \land \exists b \in ℤ y = L (b)) \to X (x \cdot_{Z} y) = X (x) X (y))$
75	74	imp	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (\exists a \in ℤ x = L (a) \land \exists b \in ℤ y = L (b))) \to X (x \cdot_{Z} y) = X (x) X (y)$
76	38 75	syldan	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land (x \in B \land y \in B)) \to X (x \cdot_{Z} y) = X (x) X (y)$
77	76	ralrimivva	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to \forall x \in B \forall y \in B X (x \cdot_{Z} y) = X (x) X (y)$
78		ss2ralv	$⊢ Unit (Z) \subseteq B \to (\forall x \in B \forall y \in B X (x \cdot_{Z} y) = X (x) X (y) \to \forall x \in Unit (Z) \forall y \in Unit (Z) X (x \cdot_{Z} y) = X (x) X (y))$
79	35 77 78	mpsyl	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to \forall x \in Unit (Z) \forall y \in Unit (Z) X (x \cdot_{Z} y) = X (x) X (y)$
80		1z	$⊢ 1 \in ℤ$
81	1 2 3 4 5 6	lgsdchrval	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land 1 \in ℤ) \to X (L (1)) = 1 /_{L} N$
82	80 81	mpan2	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to X (L (1)) = 1 /_{L} N$
83		eqid	$⊢ 1_{Z} = 1_{Z}$
84	5 83	zrh1	$⊢ Z \in Ring \to L (1) = 1_{Z}$
85	48 84	syl	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to L (1) = 1_{Z}$
86	85	fveq2d	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to X (L (1)) = X (1_{Z})$
87	18	adantr	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to N \in ℤ$
88		1lgs	$⊢ N \in ℤ \to 1 /_{L} N = 1$
89	87 88	syl	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to 1 /_{L} N = 1$
90	82 86 89	3eqtr3d	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to X (1_{Z}) = 1$
91		lgsne0	$⊢ (a \in ℤ \land N \in ℤ) \to (a /_{L} N \neq 0 \leftrightarrow a \gcd N = 1)$
92	17 19 91	syl2anc	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to (a /_{L} N \neq 0 \leftrightarrow a \gcd N = 1)$
93	92	biimpd	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to (a /_{L} N \neq 0 \to a \gcd N = 1)$
94	16	neeq1d	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to (X (L (a)) \neq 0 \leftrightarrow a /_{L} N \neq 0)$
95	2 34 5	znunit	$⊢ (N \in ℕ_{0} \land a \in ℤ) \to (L (a) \in Unit (Z) \leftrightarrow a \gcd N = 1)$
96	11 95	sylan	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to (L (a) \in Unit (Z) \leftrightarrow a \gcd N = 1)$
97	93 94 96	3imtr4d	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to (X (L (a)) \neq 0 \to L (a) \in Unit (Z))$
98	24	neeq1d	$⊢ x = L (a) \to (X (x) \neq 0 \leftrightarrow X (L (a)) \neq 0)$
99		eleq1	$⊢ x = L (a) \to (x \in Unit (Z) \leftrightarrow L (a) \in Unit (Z))$
100	98 99	imbi12d	$⊢ x = L (a) \to ((X (x) \neq 0 \to x \in Unit (Z)) \leftrightarrow (X (L (a)) \neq 0 \to L (a) \in Unit (Z)))$
101	97 100	syl5ibrcom	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land a \in ℤ) \to (x = L (a) \to (X (x) \neq 0 \to x \in Unit (Z)))$
102	101	rexlimdva	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to (\exists a \in ℤ x = L (a) \to (X (x) \neq 0 \to x \in Unit (Z)))$
103	102	imp	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land \exists a \in ℤ x = L (a)) \to (X (x) \neq 0 \to x \in Unit (Z))$
104	15 103	syldan	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land x \in B) \to (X (x) \neq 0 \to x \in Unit (Z))$
105	104	ralrimiva	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to \forall x \in B (X (x) \neq 0 \to x \in Unit (Z))$
106	79 90 105	3jca	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to (\forall x \in Unit (Z) \forall y \in Unit (Z) X (x \cdot_{Z} y) = X (x) X (y) \land X (1_{Z}) = 1 \land \forall x \in B (X (x) \neq 0 \to x \in Unit (Z)))$
107		simpl	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to N \in ℕ$
108	1 2 4 34 107 3	dchrelbas3	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to (X \in D \leftrightarrow (X : B ⟶ ℂ \land (\forall x \in Unit (Z) \forall y \in Unit (Z) X (x \cdot_{Z} y) = X (x) X (y) \land X (1_{Z}) = 1 \land \forall x \in B (X (x) \neq 0 \to x \in Unit (Z)))))$
109	33 106 108	mpbir2and	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to X \in D$
110	109 30	jca	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to (X \in D \land X : B ⟶ ℝ)$

Metamath Proof Explorer

Theorem lgsdchr

Proof