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	17 22	modcld	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A^{\frac{P - 1}{2}} + 1) \mod P \in ℝ$
24	23	recnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A^{\frac{P - 1}{2}} + 1) \mod P \in ℂ$
25		ax-1cn	$⊢ 1 \in ℂ$
26	25	a1i	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to 1 \in ℂ$
27		lgsval3	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A /_{L} P = ((A^{\frac{P - 1}{2}} + 1) \mod P) - 1$
28	24 26 27	mvrrsubd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 = (A^{\frac{P - 1}{2}} + 1) \mod P$
29	28	oveq1d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A /_{L} P) + 1) \mod P = ((A^{\frac{P - 1}{2}} + 1) \mod P) \mod P$
30		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$
31	17 22 30	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$
32	29 31	eqtrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A /_{L} P) + 1) \mod P = (A^{\frac{P - 1}{2}} + 1) \mod P$
33		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$
34	9 17 19 22 32 33	syl221anc	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A /_{L} P) + 1 + -1) \mod P = (A^{\frac{P - 1}{2}} + 1 + -1) \mod P$
35	9	recnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 \in ℂ$
36		negsub	$⊢ ((A /_{L} P) + 1 \in ℂ \land 1 \in ℂ) \to (A /_{L} P) + 1 + -1 = (A /_{L} P) + 1 - 1$
37	35 25 36	sylancl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 + -1 = (A /_{L} P) + 1 - 1$
38	7	recnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A /_{L} P \in ℂ$
39		pncan	$⊢ (A /_{L} P \in ℂ \land 1 \in ℂ) \to (A /_{L} P) + 1 - 1 = A /_{L} P$
40	38 25 39	sylancl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 - 1 = A /_{L} P$
41	37 40	eqtrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A /_{L} P) + 1 + -1 = A /_{L} P$
42	41	oveq1d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to ((A /_{L} P) + 1 + -1) \mod P = (A /_{L} P) \mod P$
43	17	recnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} + 1 \in ℂ$
44		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$
45	43 25 44	sylancl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} + 1 + -1 = A^{\frac{P - 1}{2}} + 1 - 1$
46	15	recnd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} \in ℂ$
47		pncan	$⊢ (A^{\frac{P - 1}{2}} \in ℂ \land 1 \in ℂ) \to A^{\frac{P - 1}{2}} + 1 - 1 = A^{\frac{P - 1}{2}}$
48	46 25 47	sylancl	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} + 1 - 1 = A^{\frac{P - 1}{2}}$
49	45 48	eqtrd	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to A^{\frac{P - 1}{2}} + 1 + -1 = A^{\frac{P - 1}{2}}$
50	49	oveq1d	$⊢ (A \in ℤ \land P \in (ℙ ∖ \{2\})) \to (A^{\frac{P - 1}{2}} + 1 + -1) \mod P = A^{\frac{P - 1}{2}} \mod P$
51	34 42 50	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