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 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ ( 𝐴 /L 𝑁 ) ) = 1 ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )

Proof

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