lgsvalmod

Description: The Legendre symbol is equivalent to a ^ ( ( p - 1 ) / 2 ) , mod p . This theorem is also called "Euler's criterion", see theorem 9.2 in ApostolNT p. 180, or a representation of Euler's criterion using the Legendre symbol, see also lgsqr . (Contributed by Mario Carneiro, 4-Feb-2015)

		Ref	Expression
	Assertion	lgsvalmod	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) \mod P = A^{\frac{P - 1}{2}} \mod P$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
2	1	adantl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to P \in ℙ$
3		prmz	$⊢ P \in ℙ \to P \in ℤ$
4	2 3	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to P \in ℤ$
5		lgscl	$⊢ (A \in ℤ \land P \in ℤ) \to A /_{L} P \in ℤ$
6	4 5	syldan	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A /_{L} P \in ℤ$
7	6	zred	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A /_{L} P \in ℝ$
8		peano2re	$⊢ A /_{L} P \in ℝ \to (A /_{L} P) + 1 \in ℝ$
9	7 8	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 \in ℝ$
10		oddprm	$⊢ P \in (ℙ ∖ \{2\}) \to \frac{P - 1}{2} \in ℕ$
11	10	adantl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to \frac{P - 1}{2} \in ℕ$
12	11	nnnn0d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to \frac{P - 1}{2} \in ℕ_{0}$
13		zexpcl	$⊢ (A \in ℤ \land \frac{P - 1}{2} \in ℕ_{0}) \to A^{\frac{P - 1}{2}} \in ℤ$
14	12 13	syldan	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} \in ℤ$
15	14	zred	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} \in ℝ$
16		peano2re	$⊢ A^{\frac{P - 1}{2}} \in ℝ \to A^{\frac{P - 1}{2}} + 1 \in ℝ$
17	15 16	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} + 1 \in ℝ$
18		neg1rr	$⊢ - 1 \in ℝ$
19	18	a1i	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to - 1 \in ℝ$
20		prmnn	$⊢ P \in ℙ \to P \in ℕ$
21	2 20	syl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to P \in ℕ$
22	21	nnrpd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to P \in ℝ^{+}$
23		lgsval3	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A /_{L} P = ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1$
24	23	eqcomd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 = A /_{L} P$
25	17 22	modcld	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A^{\frac{P - 1}{2}} + 1) \mod P \in ℝ$
26	25	recnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A^{\frac{P - 1}{2}} + 1) \mod P \in ℂ$
27		ax-1cn	$⊢ 1 \in ℂ$
28	27	a1i	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to 1 \in ℂ$
29	7	recnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A /_{L} P \in ℂ$
30	26 28 29	subadd2d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (((A^{\frac{P - 1}{2}} + 1) \mod P) - 1 = A /_{L} P \leftrightarrow (A /_{L} P) + 1 = (A^{\frac{P - 1}{2}} + 1) \mod P)$
31	24 30	mpbid	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 = (A^{\frac{P - 1}{2}} + 1) \mod P$
32	31	oveq1d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A /_{L} P) + 1) \mod P = ((A^{\frac{P - 1}{2}} + 1) \mod P) \mod P$
33		modabs2	$⊢ (A^{\frac{P - 1}{2}} + 1 \in ℝ \land P \in ℝ^{+}) \to ((A^{\frac{P - 1}{2}} + 1) \mod P) \mod P = (A^{\frac{P - 1}{2}} + 1) \mod P$
34	17 22 33	syl2anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A^{\frac{P - 1}{2}} + 1) \mod P) \mod P = (A^{\frac{P - 1}{2}} + 1) \mod P$
35	32 34	eqtrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A /_{L} P) + 1) \mod P = (A^{\frac{P - 1}{2}} + 1) \mod P$
36		modadd1	$⊢ (((A /_{L} P) + 1 \in ℝ \land A^{\frac{P - 1}{2}} + 1 \in ℝ) \land (- 1 \in ℝ \land P \in ℝ^{+}) \land ((A /_{L} P) + 1) \mod P = (A^{\frac{P - 1}{2}} + 1) \mod P) \to ((A /_{L} P) + 1 + -1) \mod P = (A^{\frac{P - 1}{2}} + 1 + -1) \mod P$
37	9 17 19 22 35 36	syl221anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A /_{L} P) + 1 + -1) \mod P = (A^{\frac{P - 1}{2}} + 1 + -1) \mod P$
38	9	recnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 \in ℂ$
39		negsub	$⊢ ((A /_{L} P) + 1 \in ℂ \land 1 \in ℂ) \to (A /_{L} P) + 1 + -1 = (A /_{L} P) + 1 - 1$
40	38 27 39	sylancl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 + -1 = (A /_{L} P) + 1 - 1$
41		pncan	$⊢ (A /_{L} P \in ℂ \land 1 \in ℂ) \to (A /_{L} P) + 1 - 1 = A /_{L} P$
42	29 27 41	sylancl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 - 1 = A /_{L} P$
43	40 42	eqtrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 + -1 = A /_{L} P$
44	43	oveq1d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A /_{L} P) + 1 + -1) \mod P = (A /_{L} P) \mod P$
45	17	recnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} + 1 \in ℂ$
46		negsub	$⊢ (A^{\frac{P - 1}{2}} + 1 \in ℂ \land 1 \in ℂ) \to A^{\frac{P - 1}{2}} + 1 + -1 = A^{\frac{P - 1}{2}} + 1 - 1$
47	45 27 46	sylancl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} + 1 + -1 = A^{\frac{P - 1}{2}} + 1 - 1$
48	15	recnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} \in ℂ$
49		pncan	$⊢ (A^{\frac{P - 1}{2}} \in ℂ \land 1 \in ℂ) \to A^{\frac{P - 1}{2}} + 1 - 1 = A^{\frac{P - 1}{2}}$
50	48 27 49	sylancl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} + 1 - 1 = A^{\frac{P - 1}{2}}$
51	47 50	eqtrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} + 1 + -1 = A^{\frac{P - 1}{2}}$
52	51	oveq1d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A^{\frac{P - 1}{2}} + 1 + -1) \mod P = A^{\frac{P - 1}{2}} \mod P$
53	37 44 52	3eqtr3d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) \mod P = A^{\frac{P - 1}{2}} \mod P$

Metamath Proof Explorer

Theorem lgsvalmod

Proof