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 17 22 modcld ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ∈ ℝ )
24 23 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ∈ ℂ )
25 ax-1cn ⊢ 1 ∈ ℂ
26 25 a1i ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 1 ∈ ℂ )
27 lgsval3 ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝐴 /L 𝑃 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) − 1 ) )
28 24 26 27 mvrrsubd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) + 1 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) )
29 28 oveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 /L 𝑃 ) + 1 ) mod 𝑃 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) mod 𝑃 ) )
30 modabs2 ⊢ ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) )
31 17 22 30 syl2anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) )
32 29 31 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 /L 𝑃 ) + 1 ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) )
33 modadd1 ⊢ ( ( ( ( ( 𝐴 /L 𝑃 ) + 1 ) ∈ ℝ ∧ ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∈ ℝ ) ∧ ( - 1 ∈ ℝ ∧ 𝑃 ∈ ℝ+ ) ∧ ( ( ( 𝐴 /L 𝑃 ) + 1 ) mod 𝑃 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) mod 𝑃 ) ) → ( ( ( ( 𝐴 /L 𝑃 ) + 1 ) + - 1 ) mod 𝑃 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) + - 1 ) mod 𝑃 ) )
34 9 17 19 22 32 33 syl221anc ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 𝐴 /L 𝑃 ) + 1 ) + - 1 ) mod 𝑃 ) = ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) + - 1 ) mod 𝑃 ) )
35 9 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) + 1 ) ∈ ℂ )
36 negsub ⊢ ( ( ( ( 𝐴 /L 𝑃 ) + 1 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐴 /L 𝑃 ) + 1 ) + - 1 ) = ( ( ( 𝐴 /L 𝑃 ) + 1 ) − 1 ) )
37 35 25 36 sylancl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 /L 𝑃 ) + 1 ) + - 1 ) = ( ( ( 𝐴 /L 𝑃 ) + 1 ) − 1 ) )
38 7 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝐴 /L 𝑃 ) ∈ ℂ )
39 pncan ⊢ ( ( ( 𝐴 /L 𝑃 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐴 /L 𝑃 ) + 1 ) − 1 ) = ( 𝐴 /L 𝑃 ) )
40 38 25 39 sylancl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 /L 𝑃 ) + 1 ) − 1 ) = ( 𝐴 /L 𝑃 ) )
41 37 40 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 /L 𝑃 ) + 1 ) + - 1 ) = ( 𝐴 /L 𝑃 ) )
42 41 oveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 𝐴 /L 𝑃 ) + 1 ) + - 1 ) mod 𝑃 ) = ( ( 𝐴 /L 𝑃 ) mod 𝑃 ) )
43 17 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∈ ℂ )
44 negsub ⊢ ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) + - 1 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − 1 ) )
45 43 25 44 sylancl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) + - 1 ) = ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − 1 ) )
46 15 recnd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℂ )
47 pncan ⊢ ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − 1 ) = ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) )
48 46 25 47 sylancl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) − 1 ) = ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) )
49 45 48 eqtrd ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) + - 1 ) = ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) )
50 49 oveq1d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) + 1 ) + - 1 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )
51 34 42 50 3eqtr3d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) mod 𝑃 ) = ( ( 𝐴 ↑ ( ( 𝑃 − 1 ) / 2 ) ) mod 𝑃 ) )