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 / L N = 1 ↔ A gcd N = 1

Proof

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