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∈ℤ∧N∈ℤ→A/LN=1↔AgcdN=1

Proof

Step Hyp Ref Expression
1 lgscl ⊢A∈ℤ∧N∈ℤ→A/LN∈ℤ
2 1 zcnd ⊢A∈ℤ∧N∈ℤ→A/LN∈ℂ
3 2 abscld ⊢A∈ℤ∧N∈ℤ→A/LN∈ℝ
4 1re ⊢1∈ℝ
5 letri3 ⊢A/LN∈ℝ∧1∈ℝ→A/LN=1↔A/LN≤1∧1≤A/LN
6 3 4 5 sylancl ⊢A∈ℤ∧N∈ℤ→A/LN=1↔A/LN≤1∧1≤A/LN
7 lgsle1 ⊢A∈ℤ∧N∈ℤ→A/LN≤1
8 7 biantrurd ⊢A∈ℤ∧N∈ℤ→1≤A/LN↔A/LN≤1∧1≤A/LN
9 nnne0 ⊢A/LN∈ℕ→A/LN≠0
10 nn0abscl ⊢A/LN∈ℤ→A/LN∈ℕ0
11 1 10 syl ⊢A∈ℤ∧N∈ℤ→A/LN∈ℕ0
12 elnn0 ⊢A/LN∈ℕ0↔A/LN∈ℕ∨A/LN=0
13 11 12 sylib ⊢A∈ℤ∧N∈ℤ→A/LN∈ℕ∨A/LN=0
14 13 ord ⊢A∈ℤ∧N∈ℤ→¬A/LN∈ℕ→A/LN=0
15 14 necon1ad ⊢A∈ℤ∧N∈ℤ→A/LN≠0→A/LN∈ℕ
16 9 15 impbid2 ⊢A∈ℤ∧N∈ℤ→A/LN∈ℕ↔A/LN≠0
17 elnnnn0c ⊢A/LN∈ℕ↔A/LN∈ℕ0∧1≤A/LN
18 17 baib ⊢A/LN∈ℕ0→A/LN∈ℕ↔1≤A/LN
19 11 18 syl ⊢A∈ℤ∧N∈ℤ→A/LN∈ℕ↔1≤A/LN
20 abs00 ⊢A/LN∈ℂ→A/LN=0↔A/LN=0
21 20 necon3bid ⊢A/LN∈ℂ→A/LN≠0↔A/LN≠0
22 2 21 syl ⊢A∈ℤ∧N∈ℤ→A/LN≠0↔A/LN≠0
23 lgsne0 ⊢A∈ℤ∧N∈ℤ→A/LN≠0↔AgcdN=1
24 22 23 bitrd ⊢A∈ℤ∧N∈ℤ→A/LN≠0↔AgcdN=1
25 16 19 24 3bitr3d ⊢A∈ℤ∧N∈ℤ→1≤A/LN↔AgcdN=1
26 6 8 25 3bitr2d ⊢A∈ℤ∧N∈ℤ→A/LN=1↔AgcdN=1