Metamath Proof Explorer

Theorem lgssq

Description: The Legendre symbol at a square is equal to 1 . Together with lgsmod this implies that the Legendre symbol takes value 1 at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015) (Revised by AV, 20-Jul-2021)

Ref Expression
Assertion lgssq 
|- ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ 2 ) /L N ) = 1 )

Proof

Step Hyp Ref Expression
1 simp1l 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> A e. ZZ )
2 simp2 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> N e. ZZ )
3 simp1r 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> A =/= 0 )
4 lgsdir 
 |-  ( ( ( A e. ZZ /\ A e. ZZ /\ N e. ZZ ) /\ ( A =/= 0 /\ A =/= 0 ) ) -> ( ( A x. A ) /L N ) = ( ( A /L N ) x. ( A /L N ) ) )
5 1 1 2 3 3 4 syl32anc 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A x. A ) /L N ) = ( ( A /L N ) x. ( A /L N ) ) )
6 zcn 
 |-  ( A e. ZZ -> A e. CC )
7 6 adantr 
 |-  ( ( A e. ZZ /\ A =/= 0 ) -> A e. CC )
8 7 3ad2ant1 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> A e. CC )
9 8 sqvald 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( A ^ 2 ) = ( A x. A ) )
10 9 oveq1d 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ 2 ) /L N ) = ( ( A x. A ) /L N ) )
11 lgscl 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. ZZ )
12 1 2 11 syl2anc 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( A /L N ) e. ZZ )
13 12 zred 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( A /L N ) e. RR )
14 absresq 
 |-  ( ( A /L N ) e. RR -> ( ( abs ` ( A /L N ) ) ^ 2 ) = ( ( A /L N ) ^ 2 ) )
15 13 14 syl 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( abs ` ( A /L N ) ) ^ 2 ) = ( ( A /L N ) ^ 2 ) )
16 lgsabs1 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) = 1 <-> ( A gcd N ) = 1 ) )
17 16 adantlr 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) = 1 <-> ( A gcd N ) = 1 ) )
18 17 biimp3ar 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( abs ` ( A /L N ) ) = 1 )
19 18 oveq1d 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( abs ` ( A /L N ) ) ^ 2 ) = ( 1 ^ 2 ) )
20 sq1 
 |-  ( 1 ^ 2 ) = 1
21 19 20 eqtrdi 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( abs ` ( A /L N ) ) ^ 2 ) = 1 )
22 12 zcnd 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( A /L N ) e. CC )
23 22 sqvald 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A /L N ) ^ 2 ) = ( ( A /L N ) x. ( A /L N ) ) )
24 15 21 23 3eqtr3d 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> 1 = ( ( A /L N ) x. ( A /L N ) ) )
25 5 10 24 3eqtr4d 
 |-  ( ( ( A e. ZZ /\ A =/= 0 ) /\ N e. ZZ /\ ( A gcd N ) = 1 ) -> ( ( A ^ 2 ) /L N ) = 1 )