Metamath Proof Explorer


Theorem lgsqr

Description: The Legendre symbol for odd primes is 1 iff the number is not a multiple of the prime (in which case it is 0 , see lgsne0 ) and the number is a quadratic residue mod P (it is -u 1 for nonresidues by the process of elimination from lgsabs1 ). Given our definition of the Legendre symbol, this theorem is equivalent to Euler's criterion. (Contributed by Mario Carneiro, 15-Jun-2015)

Ref Expression
Assertion lgsqr ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 ↔ ( ¬ 𝑃𝐴 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 eldifi ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ℙ )
2 1 adantl ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑃 ∈ ℙ )
3 prmz ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
4 2 3 syl ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝑃 ∈ ℤ )
5 simpl ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → 𝐴 ∈ ℤ )
6 4 5 gcdcomd ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃 gcd 𝐴 ) = ( 𝐴 gcd 𝑃 ) )
7 6 eqeq1d ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝑃 gcd 𝐴 ) = 1 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) )
8 coprm ( ( 𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( ¬ 𝑃𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) )
9 2 5 8 syl2anc ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ¬ 𝑃𝐴 ↔ ( 𝑃 gcd 𝐴 ) = 1 ) )
10 lgsne0 ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 𝐴 /L 𝑃 ) ≠ 0 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) )
11 5 4 10 syl2anc ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) ≠ 0 ↔ ( 𝐴 gcd 𝑃 ) = 1 ) )
12 7 9 11 3bitr4d ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ¬ 𝑃𝐴 ↔ ( 𝐴 /L 𝑃 ) ≠ 0 ) )
13 12 necon4bbid ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃𝐴 ↔ ( 𝐴 /L 𝑃 ) = 0 ) )
14 0ne1 0 ≠ 1
15 neeq1 ( ( 𝐴 /L 𝑃 ) = 0 → ( ( 𝐴 /L 𝑃 ) ≠ 1 ↔ 0 ≠ 1 ) )
16 14 15 mpbiri ( ( 𝐴 /L 𝑃 ) = 0 → ( 𝐴 /L 𝑃 ) ≠ 1 )
17 13 16 syl6bi ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( 𝑃𝐴 → ( 𝐴 /L 𝑃 ) ≠ 1 ) )
18 17 necon2bd ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ¬ 𝑃𝐴 ) )
19 lgsqrlem5 ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝐴 /L 𝑃 ) = 1 ) → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) )
20 19 3expia ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) )
21 18 20 jcad ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 → ( ¬ 𝑃𝐴 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) )
22 simprl ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑥 ∈ ℤ )
23 22 zred ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑥 ∈ ℝ )
24 absresq ( 𝑥 ∈ ℝ → ( ( abs ‘ 𝑥 ) ↑ 2 ) = ( 𝑥 ↑ 2 ) )
25 23 24 syl ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( abs ‘ 𝑥 ) ↑ 2 ) = ( 𝑥 ↑ 2 ) )
26 25 oveq1d ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) /L 𝑃 ) = ( ( 𝑥 ↑ 2 ) /L 𝑃 ) )
27 simplr ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ¬ 𝑃𝐴 )
28 1 ad3antlr ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ∈ ℙ )
29 28 3 syl ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ∈ ℤ )
30 zsqcl ( 𝑥 ∈ ℤ → ( 𝑥 ↑ 2 ) ∈ ℤ )
31 22 30 syl ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℤ )
32 simplll ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝐴 ∈ ℤ )
33 simprr ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) )
34 dvdssub2 ( ( ( 𝑃 ∈ ℤ ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃𝐴 ) )
35 29 31 32 33 34 syl31anc ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃𝐴 ) )
36 27 35 mtbird ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ¬ 𝑃 ∥ ( 𝑥 ↑ 2 ) )
37 2nn 2 ∈ ℕ
38 37 a1i ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 2 ∈ ℕ )
39 prmdvdsexp ( ( 𝑃 ∈ ℙ ∧ 𝑥 ∈ ℤ ∧ 2 ∈ ℕ ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃𝑥 ) )
40 28 22 38 39 syl3anc ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑃 ∥ ( 𝑥 ↑ 2 ) ↔ 𝑃𝑥 ) )
41 36 40 mtbid ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ¬ 𝑃𝑥 )
42 dvds0 ( 𝑃 ∈ ℤ → 𝑃 ∥ 0 )
43 29 42 syl ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ∥ 0 )
44 breq2 ( 𝑥 = 0 → ( 𝑃𝑥𝑃 ∥ 0 ) )
45 43 44 syl5ibrcom ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑥 = 0 → 𝑃𝑥 ) )
46 45 necon3bd ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ¬ 𝑃𝑥𝑥 ≠ 0 ) )
47 41 46 mpd ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑥 ≠ 0 )
48 nnabscl ( ( 𝑥 ∈ ℤ ∧ 𝑥 ≠ 0 ) → ( abs ‘ 𝑥 ) ∈ ℕ )
49 22 47 48 syl2anc ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℕ )
50 49 nnzd ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℤ )
51 49 nnne0d ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( abs ‘ 𝑥 ) ≠ 0 )
52 50 29 gcdcomd ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( abs ‘ 𝑥 ) gcd 𝑃 ) = ( 𝑃 gcd ( abs ‘ 𝑥 ) ) )
53 dvdsabsb ( ( 𝑃 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑃𝑥𝑃 ∥ ( abs ‘ 𝑥 ) ) )
54 29 22 53 syl2anc ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑃𝑥𝑃 ∥ ( abs ‘ 𝑥 ) ) )
55 41 54 mtbid ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ¬ 𝑃 ∥ ( abs ‘ 𝑥 ) )
56 coprm ( ( 𝑃 ∈ ℙ ∧ ( abs ‘ 𝑥 ) ∈ ℤ ) → ( ¬ 𝑃 ∥ ( abs ‘ 𝑥 ) ↔ ( 𝑃 gcd ( abs ‘ 𝑥 ) ) = 1 ) )
57 28 50 56 syl2anc ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ¬ 𝑃 ∥ ( abs ‘ 𝑥 ) ↔ ( 𝑃 gcd ( abs ‘ 𝑥 ) ) = 1 ) )
58 55 57 mpbid ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝑃 gcd ( abs ‘ 𝑥 ) ) = 1 )
59 52 58 eqtrd ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( abs ‘ 𝑥 ) gcd 𝑃 ) = 1 )
60 lgssq ( ( ( ( abs ‘ 𝑥 ) ∈ ℤ ∧ ( abs ‘ 𝑥 ) ≠ 0 ) ∧ 𝑃 ∈ ℤ ∧ ( ( abs ‘ 𝑥 ) gcd 𝑃 ) = 1 ) → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) /L 𝑃 ) = 1 )
61 50 51 29 59 60 syl211anc ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( ( abs ‘ 𝑥 ) ↑ 2 ) /L 𝑃 ) = 1 )
62 prmnn ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
63 28 62 syl ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ∈ ℕ )
64 moddvds ( ( 𝑃 ∈ ℕ ∧ ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) )
65 63 31 32 64 syl3anc ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) ↔ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) )
66 33 65 mpbird ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( 𝑥 ↑ 2 ) mod 𝑃 ) = ( 𝐴 mod 𝑃 ) )
67 66 oveq1d ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) /L 𝑃 ) = ( ( 𝐴 mod 𝑃 ) /L 𝑃 ) )
68 eldifsni ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ≠ 2 )
69 68 ad3antlr ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 𝑃 ≠ 2 )
70 69 necomd ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → 2 ≠ 𝑃 )
71 2z 2 ∈ ℤ
72 uzid ( 2 ∈ ℤ → 2 ∈ ( ℤ ‘ 2 ) )
73 71 72 ax-mp 2 ∈ ( ℤ ‘ 2 )
74 dvdsprm ( ( 2 ∈ ( ℤ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( 2 ∥ 𝑃 ↔ 2 = 𝑃 ) )
75 74 necon3bbid ( ( 2 ∈ ( ℤ ‘ 2 ) ∧ 𝑃 ∈ ℙ ) → ( ¬ 2 ∥ 𝑃 ↔ 2 ≠ 𝑃 ) )
76 73 28 75 sylancr ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ¬ 2 ∥ 𝑃 ↔ 2 ≠ 𝑃 ) )
77 70 76 mpbird ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ¬ 2 ∥ 𝑃 )
78 lgsmod ( ( ( 𝑥 ↑ 2 ) ∈ ℤ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) /L 𝑃 ) = ( ( 𝑥 ↑ 2 ) /L 𝑃 ) )
79 31 63 77 78 syl3anc ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( ( 𝑥 ↑ 2 ) mod 𝑃 ) /L 𝑃 ) = ( ( 𝑥 ↑ 2 ) /L 𝑃 ) )
80 lgsmod ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ℕ ∧ ¬ 2 ∥ 𝑃 ) → ( ( 𝐴 mod 𝑃 ) /L 𝑃 ) = ( 𝐴 /L 𝑃 ) )
81 32 63 77 80 syl3anc ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( 𝐴 mod 𝑃 ) /L 𝑃 ) = ( 𝐴 /L 𝑃 ) )
82 67 79 81 3eqtr3d ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( ( 𝑥 ↑ 2 ) /L 𝑃 ) = ( 𝐴 /L 𝑃 ) )
83 26 61 82 3eqtr3rd ( ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) → ( 𝐴 /L 𝑃 ) = 1 )
84 83 rexlimdvaa ( ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) ∧ ¬ 𝑃𝐴 ) → ( ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) → ( 𝐴 /L 𝑃 ) = 1 ) )
85 84 expimpd ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( ¬ 𝑃𝐴 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) → ( 𝐴 /L 𝑃 ) = 1 ) )
86 21 85 impbid ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 2 } ) ) → ( ( 𝐴 /L 𝑃 ) = 1 ↔ ( ¬ 𝑃𝐴 ∧ ∃ 𝑥 ∈ ℤ 𝑃 ∥ ( ( 𝑥 ↑ 2 ) − 𝐴 ) ) ) )