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 biimtrdi ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑃 ∈ ( ℙ ∖ { 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 ) − 𝐴 ) ) ) )