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 )