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 )