Metamath Proof Explorer

Theorem lgsabs1

Description: The Legendre symbol is nonzero (and hence equal to 1 or -u 1 ) precisely when the arguments are coprime. (Contributed by Mario Carneiro, 5-Feb-2015)

Ref Expression
Assertion lgsabs1 
|- ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) = 1 <-> ( A gcd N ) = 1 ) )

Proof

Step Hyp Ref Expression
1 lgscl 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. ZZ )
2 1 zcnd 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( A /L N ) e. CC )
3 2 abscld 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( abs ` ( A /L N ) ) e. RR )
4 1re 
 |-  1 e. RR
5 letri3 
 |-  ( ( ( abs ` ( A /L N ) ) e. RR /\ 1 e. RR ) -> ( ( abs ` ( A /L N ) ) = 1 <-> ( ( abs ` ( A /L N ) ) <_ 1 /\ 1 <_ ( abs ` ( A /L N ) ) ) ) )
6 3 4 5 sylancl 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) = 1 <-> ( ( abs ` ( A /L N ) ) <_ 1 /\ 1 <_ ( abs ` ( A /L N ) ) ) ) )
7 lgsle1 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( abs ` ( A /L N ) ) <_ 1 )
8 7 biantrurd 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( 1 <_ ( abs ` ( A /L N ) ) <-> ( ( abs ` ( A /L N ) ) <_ 1 /\ 1 <_ ( abs ` ( A /L N ) ) ) ) )
9 nnne0 
 |-  ( ( abs ` ( A /L N ) ) e. NN -> ( abs ` ( A /L N ) ) =/= 0 )
10 nn0abscl 
 |-  ( ( A /L N ) e. ZZ -> ( abs ` ( A /L N ) ) e. NN0 )
11 1 10 syl 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( abs ` ( A /L N ) ) e. NN0 )
12 elnn0 
 |-  ( ( abs ` ( A /L N ) ) e. NN0 <-> ( ( abs ` ( A /L N ) ) e. NN \/ ( abs ` ( A /L N ) ) = 0 ) )
13 11 12 sylib 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) e. NN \/ ( abs ` ( A /L N ) ) = 0 ) )
14 13 ord 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( -. ( abs ` ( A /L N ) ) e. NN -> ( abs ` ( A /L N ) ) = 0 ) )
15 14 necon1ad 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) =/= 0 -> ( abs ` ( A /L N ) ) e. NN ) )
16 9 15 impbid2 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) e. NN <-> ( abs ` ( A /L N ) ) =/= 0 ) )
17 elnnnn0c 
 |-  ( ( abs ` ( A /L N ) ) e. NN <-> ( ( abs ` ( A /L N ) ) e. NN0 /\ 1 <_ ( abs ` ( A /L N ) ) ) )
18 17 baib 
 |-  ( ( abs ` ( A /L N ) ) e. NN0 -> ( ( abs ` ( A /L N ) ) e. NN <-> 1 <_ ( abs ` ( A /L N ) ) ) )
19 11 18 syl 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) e. NN <-> 1 <_ ( abs ` ( A /L N ) ) ) )
20 abs00 
 |-  ( ( A /L N ) e. CC -> ( ( abs ` ( A /L N ) ) = 0 <-> ( A /L N ) = 0 ) )
21 20 necon3bid 
 |-  ( ( A /L N ) e. CC -> ( ( abs ` ( A /L N ) ) =/= 0 <-> ( A /L N ) =/= 0 ) )
22 2 21 syl 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) =/= 0 <-> ( A /L N ) =/= 0 ) )
23 lgsne0 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( A /L N ) =/= 0 <-> ( A gcd N ) = 1 ) )
24 22 23 bitrd 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) =/= 0 <-> ( A gcd N ) = 1 ) )
25 16 19 24 3bitr3d 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( 1 <_ ( abs ` ( A /L N ) ) <-> ( A gcd N ) = 1 ) )
26 6 8 25 3bitr2d 
 |-  ( ( A e. ZZ /\ N e. ZZ ) -> ( ( abs ` ( A /L N ) ) = 1 <-> ( A gcd N ) = 1 ) )