Metamath Proof Explorer

Theorem 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 ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )

Proof

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