lgsmod

Description: The Legendre (Jacobi) symbol is preserved under reduction mod n when n is odd. (Contributed by Mario Carneiro, 4-Feb-2015)

		Ref	Expression
	Assertion	lgsmod	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to (A \mod N) /_{L} N = A /_{L} N$

Proof

Step	Hyp	Ref	Expression
1		zmodcl	$⊢ (A \in ℤ \land N \in ℕ) \to A \mod N \in ℕ_{0}$
2	1	3adant3	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to A \mod N \in ℕ_{0}$
3	2	nn0zd	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to A \mod N \in ℤ$
4	3	ad2antrr	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to A \mod N \in ℤ$
5		simpr	$⊢ ((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \to n \in ℙ$
6	5	adantr	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to n \in ℙ$
7		simpl3	$⊢ ((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \to \neg 2 ∥ N$
8		breq1	$⊢ n = 2 \to (n ∥ N \leftrightarrow 2 ∥ N)$
9	8	notbid	$⊢ n = 2 \to (\neg n ∥ N \leftrightarrow \neg 2 ∥ N)$
10	7 9	syl5ibrcom	$⊢ ((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \to (n = 2 \to \neg n ∥ N)$
11	10	necon2ad	$⊢ ((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \to (n ∥ N \to n \neq 2)$
12	11	imp	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to n \neq 2$
13		eldifsn	$⊢ n \in (ℙ ∖ \{2\}) \leftrightarrow (n \in ℙ \land n \neq 2)$
14	6 12 13	sylanbrc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to n \in (ℙ ∖ \{2\})$
15		oddprm	$⊢ n \in (ℙ ∖ \{2\}) \to \frac{n - 1}{2} \in ℕ$
16	14 15	syl	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to \frac{n - 1}{2} \in ℕ$
17	16	nnnn0d	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to \frac{n - 1}{2} \in ℕ_{0}$
18		zexpcl	$⊢ (A \mod N \in ℤ \land \frac{n - 1}{2} \in ℕ_{0}) \to {(A \mod N)}^{\frac{n - 1}{2}} \in ℤ$
19	4 17 18	syl2anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to {(A \mod N)}^{\frac{n - 1}{2}} \in ℤ$
20	19	zred	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to {(A \mod N)}^{\frac{n - 1}{2}} \in ℝ$
21		simpll1	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to A \in ℤ$
22		zexpcl	$⊢ (A \in ℤ \land \frac{n - 1}{2} \in ℕ_{0}) \to A^{\frac{n - 1}{2}} \in ℤ$
23	21 17 22	syl2anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to A^{\frac{n - 1}{2}} \in ℤ$
24	23	zred	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to A^{\frac{n - 1}{2}} \in ℝ$
25		1red	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to 1 \in ℝ$
26		prmnn	$⊢ n \in ℙ \to n \in ℕ$
27	26	ad2antlr	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to n \in ℕ$
28	27	nnrpd	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to n \in ℝ^{+}$
29		prmz	$⊢ n \in ℙ \to n \in ℤ$
30	29	ad2antlr	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to n \in ℤ$
31		simp2	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to N \in ℕ$
32	31	ad2antrr	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to N \in ℕ$
33	32	nnzd	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to N \in ℤ$
34	4 21	zsubcld	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to (A \mod N) - A \in ℤ$
35		simpr	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to n ∥ N$
36	21	zred	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to A \in ℝ$
37	32	nnrpd	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to N \in ℝ^{+}$
38		modabs2	$⊢ (A \in ℝ \land N \in ℝ^{+}) \to (A \mod N) \mod N = A \mod N$
39	36 37 38	syl2anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to (A \mod N) \mod N = A \mod N$
40		moddvds	$⊢ (N \in ℕ \land A \mod N \in ℤ \land A \in ℤ) \to ((A \mod N) \mod N = A \mod N \leftrightarrow N ∥ ((A \mod N) - A))$
41	32 4 21 40	syl3anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to ((A \mod N) \mod N = A \mod N \leftrightarrow N ∥ ((A \mod N) - A))$
42	39 41	mpbid	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to N ∥ ((A \mod N) - A)$
43	30 33 34 35 42	dvdstrd	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to n ∥ ((A \mod N) - A)$
44		moddvds	$⊢ (n \in ℕ \land A \mod N \in ℤ \land A \in ℤ) \to ((A \mod N) \mod n = A \mod n \leftrightarrow n ∥ ((A \mod N) - A))$
45	27 4 21 44	syl3anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to ((A \mod N) \mod n = A \mod n \leftrightarrow n ∥ ((A \mod N) - A))$
46	43 45	mpbird	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to (A \mod N) \mod n = A \mod n$
47		modexp	$⊢ ((A \mod N \in ℤ \land A \in ℤ) \land (\frac{n - 1}{2} \in ℕ_{0} \land n \in ℝ^{+}) \land (A \mod N) \mod n = A \mod n) \to {(A \mod N)}^{\frac{n - 1}{2}} \mod n = A^{\frac{n - 1}{2}} \mod n$
48	4 21 17 28 46 47	syl221anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to {(A \mod N)}^{\frac{n - 1}{2}} \mod n = A^{\frac{n - 1}{2}} \mod n$
49		modadd1	$⊢ (({(A \mod N)}^{\frac{n - 1}{2}} \in ℝ \land A^{\frac{n - 1}{2}} \in ℝ) \land (1 \in ℝ \land n \in ℝ^{+}) \land {(A \mod N)}^{\frac{n - 1}{2}} \mod n = A^{\frac{n - 1}{2}} \mod n) \to ({(A \mod N)}^{\frac{n - 1}{2}} + 1) \mod n = (A^{\frac{n - 1}{2}} + 1) \mod n$
50	20 24 25 28 48 49	syl221anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to ({(A \mod N)}^{\frac{n - 1}{2}} + 1) \mod n = (A^{\frac{n - 1}{2}} + 1) \mod n$
51	50	oveq1d	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to (({(A \mod N)}^{\frac{n - 1}{2}} + 1) \mod n) - 1 = ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1$
52		lgsval3	$⊢ (A \mod N \in ℤ \land n \in (ℙ ∖ \{2\})) \to (A \mod N) /_{L} n = (({(A \mod N)}^{\frac{n - 1}{2}} + 1) \mod n) - 1$
53	4 14 52	syl2anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to (A \mod N) /_{L} n = (({(A \mod N)}^{\frac{n - 1}{2}} + 1) \mod n) - 1$
54		lgsval3	$⊢ (A \in ℤ \land n \in (ℙ ∖ \{2\})) \to A /_{L} n = ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1$
55	21 14 54	syl2anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to A /_{L} n = ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1$
56	51 53 55	3eqtr4d	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to (A \mod N) /_{L} n = A /_{L} n$
57	56	oveq1d	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land n ∥ N) \to {((A \mod N) /_{L} n)}^{n pCnt N} = {(A /_{L} n)}^{n pCnt N}$
58	3	ad2antrr	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to A \mod N \in ℤ$
59	29	ad2antlr	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to n \in ℤ$
60		lgscl	$⊢ (A \mod N \in ℤ \land n \in ℤ) \to (A \mod N) /_{L} n \in ℤ$
61	58 59 60	syl2anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to (A \mod N) /_{L} n \in ℤ$
62	61	zcnd	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to (A \mod N) /_{L} n \in ℂ$
63	62	exp0d	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to {((A \mod N) /_{L} n)}^{0} = 1$
64		simpll1	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to A \in ℤ$
65		lgscl	$⊢ (A \in ℤ \land n \in ℤ) \to A /_{L} n \in ℤ$
66	64 59 65	syl2anc	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to A /_{L} n \in ℤ$
67	66	zcnd	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to A /_{L} n \in ℂ$
68	67	exp0d	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to {(A /_{L} n)}^{0} = 1$
69	63 68	eqtr4d	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to {((A \mod N) /_{L} n)}^{0} = {(A /_{L} n)}^{0}$
70	31	adantr	$⊢ ((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \to N \in ℕ$
71		pceq0	$⊢ (n \in ℙ \land N \in ℕ) \to (n pCnt N = 0 \leftrightarrow \neg n ∥ N)$
72	5 70 71	syl2anc	$⊢ ((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \to (n pCnt N = 0 \leftrightarrow \neg n ∥ N)$
73	72	biimpar	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to n pCnt N = 0$
74	73	oveq2d	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to {((A \mod N) /_{L} n)}^{n pCnt N} = {((A \mod N) /_{L} n)}^{0}$
75	73	oveq2d	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to {(A /_{L} n)}^{n pCnt N} = {(A /_{L} n)}^{0}$
76	69 74 75	3eqtr4d	$⊢ (((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \land \neg n ∥ N) \to {((A \mod N) /_{L} n)}^{n pCnt N} = {(A /_{L} n)}^{n pCnt N}$
77	57 76	pm2.61dan	$⊢ ((A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \land n \in ℙ) \to {((A \mod N) /_{L} n)}^{n pCnt N} = {(A /_{L} n)}^{n pCnt N}$
78	77	ifeq1da	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to if (n \in ℙ, {((A \mod N) /_{L} n)}^{n pCnt N}, 1) = if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)$
79	78	mpteq2dv	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to (n \in ℕ ⟼ if (n \in ℙ, {((A \mod N) /_{L} n)}^{n pCnt N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))$
80	79	seqeq3d	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {((A \mod N) /_{L} n)}^{n pCnt N}, 1))) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)))$
81	80	fveq1d	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {((A \mod N) /_{L} n)}^{n pCnt N}, 1))) (N) = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (N)$
82		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, {((A \mod N) /_{L} n)}^{n pCnt N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {((A \mod N) /_{L} n)}^{n pCnt N}, 1))$
83	82	lgsval4a	$⊢ (A \mod N \in ℤ \land N \in ℕ) \to (A \mod N) /_{L} N = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {((A \mod N) /_{L} n)}^{n pCnt N}, 1))) (N)$
84	3 31 83	syl2anc	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to (A \mod N) /_{L} N = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {((A \mod N) /_{L} n)}^{n pCnt N}, 1))) (N)$
85		eqid	$⊢ (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1)) = (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))$
86	85	lgsval4a	$⊢ (A \in ℤ \land N \in ℕ) \to A /_{L} N = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (N)$
87	86	3adant3	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to A /_{L} N = seq 1 (\times (n \in ℕ ⟼ if (n \in ℙ, {(A /_{L} n)}^{n pCnt N}, 1))) (N)$
88	81 84 87	3eqtr4d	$⊢ (A \in ℤ \land N \in ℕ \land \neg 2 ∥ N) \to (A \mod N) /_{L} N = A /_{L} N$

Metamath Proof Explorer

Theorem lgsmod

Proof