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 \in B ⟼ (ι h \| \exists m \in ℤ (y = L (m) \land h = m /_{L} N)))$
Assertion	lgsdchrval	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \to 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 \in B ⟼ (ι h \| \exists m \in ℤ (y = L (m) \land h = m /_{L} N)))$
7		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
8	7	adantr	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to N \in ℕ_{0}$
9	2 4 5	znzrhfo	$⊢ N \in ℕ_{0} \to L : ℤ \underset{onto}{⟶} B$
10		fof	$⊢ L : ℤ \underset{onto}{⟶} B \to L : ℤ ⟶ B$
11	8 9 10	3syl	$⊢ (N \in ℕ \land \neg 2 ∥ N) \to L : ℤ ⟶ B$
12	11	ffvelcdmda	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \to L (A) \in B$
13		eqeq1	$⊢ y = L (A) \to (y = L (m) \leftrightarrow L (A) = L (m))$
14	13	anbi1d	$⊢ y = L (A) \to ((y = L (m) \land h = m /_{L} N) \leftrightarrow (L (A) = L (m) \land h = m /_{L} N))$
15	14	rexbidv	$⊢ y = L (A) \to (\exists m \in ℤ (y = L (m) \land h = m /_{L} N) \leftrightarrow \exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N))$
16	15	iotabidv	$⊢ y = L (A) \to (ι h \| \exists m \in ℤ (y = L (m) \land h = m /_{L} N)) = (ι h \| \exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N))$
17		iotaex	$⊢ (ι h \| \exists m \in ℤ (y = L (m) \land h = m /_{L} N)) \in V$
18	16 6 17	fvmpt3i	$⊢ L (A) \in B \to X (L (A)) = (ι h \| \exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N))$
19	12 18	syl	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \to X (L (A)) = (ι h \| \exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N))$
20		ovex	$⊢ A /_{L} N \in V$
21		simprr	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to L (A) = L (m)$
22		simplll	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to N \in ℕ$
23	22 7	syl	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to N \in ℕ_{0}$
24		simplr	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to A \in ℤ$
25		simprl	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to m \in ℤ$
26	2 5	zndvds	$⊢ (N \in ℕ_{0} \land A \in ℤ \land m \in ℤ) \to (L (A) = L (m) \leftrightarrow N ∥ (A - m))$
27	23 24 25 26	syl3anc	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to (L (A) = L (m) \leftrightarrow N ∥ (A - m))$
28	21 27	mpbid	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to N ∥ (A - m)$
29		moddvds	$⊢ (N \in ℕ \land A \in ℤ \land m \in ℤ) \to (A \mod N = m \mod N \leftrightarrow N ∥ (A - m))$
30	22 24 25 29	syl3anc	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to (A \mod N = m \mod N \leftrightarrow N ∥ (A - m))$
31	28 30	mpbird	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to A \mod N = m \mod N$
32	31	oveq1d	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to (A \mod N) /_{L} N = (m \mod N) /_{L} N$
33		simpllr	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to \neg 2 ∥ N$
34		lgsmod	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to (A \mod N) /_{L} N = A /_{L} N$
35	24 22 33 34	syl3anc	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to (A \mod N) /_{L} N = A /_{L} N$
36		lgsmod	$⊢ (m \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to (m \mod N) /_{L} N = m /_{L} N$
37	25 22 33 36	syl3anc	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to (m \mod N) /_{L} N = m /_{L} N$
38	32 35 37	3eqtr3d	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to A /_{L} N = m /_{L} N$
39	38	eqeq2d	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to (h = A /_{L} N \leftrightarrow h = m /_{L} N)$
40	39	biimprd	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land (m \in ℤ \land L (A) = L (m))) \to (h = m /_{L} N \to h = A /_{L} N)$
41	40	anassrs	$⊢ ((((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land m \in ℤ) \land L (A) = L (m)) \to (h = m /_{L} N \to h = A /_{L} N)$
42	41	expimpd	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land m \in ℤ) \to ((L (A) = L (m) \land h = m /_{L} N) \to h = A /_{L} N)$
43	42	rexlimdva	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \to (\exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N) \to h = A /_{L} N)$
44		fveq2	$⊢ m = A \to L (m) = L (A)$
45	44	eqcomd	$⊢ m = A \to L (A) = L (m)$
46	45	biantrurd	$⊢ m = A \to (h = m /_{L} N \leftrightarrow (L (A) = L (m) \land h = m /_{L} N))$
47		oveq1	$⊢ m = A \to m /_{L} N = A /_{L} N$
48	47	eqeq2d	$⊢ m = A \to (h = m /_{L} N \leftrightarrow h = A /_{L} N)$
49	46 48	bitr3d	$⊢ m = A \to ((L (A) = L (m) \land h = m /_{L} N) \leftrightarrow h = A /_{L} N)$
50	49	rspcev	$⊢ (A \in ℤ \land h = A /_{L} N) \to \exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N)$
51	50	ex	$⊢ A \in ℤ \to (h = A /_{L} N \to \exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N))$
52	51	adantl	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \to (h = A /_{L} N \to \exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N))$
53	43 52	impbid	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \to (\exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N) \leftrightarrow h = A /_{L} N)$
54	53	adantr	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land A /_{L} N \in V) \to (\exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N) \leftrightarrow h = A /_{L} N)$
55	54	iota5	$⊢ (((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \land A /_{L} N \in V) \to (ι h \| \exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N)) = A /_{L} N$
56	20 55	mpan2	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \to (ι h \| \exists m \in ℤ (L (A) = L (m) \land h = m /_{L} N)) = A /_{L} N$
57	19 56	eqtrd	$⊢ ((N \in ℕ \land \neg 2 ∥ N) \land A \in ℤ) \to X (L (A)) = A /_{L} N$

Metamath Proof Explorer

Theorem lgsdchrval

Proof