Metamath Proof Explorer


Theorem lgssq2

Description: The Legendre symbol at a square is equal to 1 . (Contributed by Mario Carneiro, 5-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 simp1
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> A e. ZZ )
2 nnz
 |-  ( N e. NN -> N e. ZZ )
3 2 3ad2ant2
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> N e. ZZ )
4 nnne0
 |-  ( N e. NN -> N =/= 0 )
5 4 3ad2ant2
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> N =/= 0 )
6 lgsdi
 |-  ( ( ( A e. ZZ /\ N e. ZZ /\ N e. ZZ ) /\ ( N =/= 0 /\ N =/= 0 ) ) -> ( A /L ( N x. N ) ) = ( ( A /L N ) x. ( A /L N ) ) )
7 1 3 3 5 5 6 syl32anc
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( A /L ( N x. N ) ) = ( ( A /L N ) x. ( A /L N ) ) )
8 nncn
 |-  ( N e. NN -> N e. CC )
9 8 3ad2ant2
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> N e. CC )
10 9 sqvald
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( N ^ 2 ) = ( N x. N ) )
11 10 oveq2d
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( A /L ( N ^ 2 ) ) = ( A /L ( N x. N ) ) )
12 lgscl
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. ZZ )
13 1 3 12 syl2anc
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( A /L N ) e. ZZ )
14 13 zred
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( A /L N ) e. RR )
15 absresq
 |-  ( ( A /L N ) e. RR -> ( ( abs ` ( A /L N ) ) ^ 2 ) = ( ( A /L N ) ^ 2 ) )
16 14 15 syl
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( ( abs ` ( A /L N ) ) ^ 2 ) = ( ( A /L N ) ^ 2 ) )
17 lgsabs1
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) = 1 <-> ( A gcd N ) = 1 ) )
18 2 17 sylan2
 |-  ( ( A e. ZZ /\ N e. NN ) -> ( ( abs ` ( A /L N ) ) = 1 <-> ( A gcd N ) = 1 ) )
19 18 biimp3ar
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( abs ` ( A /L N ) ) = 1 )
20 19 oveq1d
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( ( abs ` ( A /L N ) ) ^ 2 ) = ( 1 ^ 2 ) )
21 sq1
 |-  ( 1 ^ 2 ) = 1
22 20 21 eqtrdi
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( ( abs ` ( A /L N ) ) ^ 2 ) = 1 )
23 13 zcnd
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( A /L N ) e. CC )
24 23 sqvald
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( ( A /L N ) ^ 2 ) = ( ( A /L N ) x. ( A /L N ) ) )
25 16 22 24 3eqtr3d
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> 1 = ( ( A /L N ) x. ( A /L N ) ) )
26 7 11 25 3eqtr4d
 |-  ( ( A e. ZZ /\ N e. NN /\ ( A gcd N ) = 1 ) -> ( A /L ( N ^ 2 ) ) = 1 )