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 ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N 2 = 1

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A ∈ ℤ
2 nnz ⊢ N ∈ ℕ → N ∈ ℤ
3 2 3ad2ant2 ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → N ∈ ℤ
4 nnne0 ⊢ N ∈ ℕ → N ≠ 0
5 4 3ad2ant2 ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → N ≠ 0
6 lgsdi ⊢ A ∈ ℤ ∧ N ∈ ℤ ∧ N ∈ ℤ ∧ N ≠ 0 ∧ N ≠ 0 → A / L N ⋅ N = A / L N ⁢ A / L N
7 1 3 3 5 5 6 syl32anc ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N ⋅ N = A / L N ⁢ A / L N
8 nncn ⊢ N ∈ ℕ → N ∈ ℂ
9 8 3ad2ant2 ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → N ∈ ℂ
10 9 sqvald ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → N 2 = N ⋅ N
11 10 oveq2d ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N 2 = A / L N ⋅ N
12 lgscl ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N ∈ ℤ
13 1 3 12 syl2anc ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N ∈ ℤ
14 13 zred ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N ∈ ℝ
15 absresq ⊢ A / L N ∈ ℝ → A / L N 2 = A / L N 2
16 14 15 syl ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N 2 = A / L N 2
17 lgsabs1 ⊢ A ∈ ℤ ∧ N ∈ ℤ → A / L N = 1 ↔ A gcd N = 1
18 2 17 sylan2 ⊢ A ∈ ℤ ∧ N ∈ ℕ → A / L N = 1 ↔ A gcd N = 1
19 18 biimp3ar ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N = 1
20 19 oveq1d ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N 2 = 1 2
21 sq1 ⊢ 1 2 = 1
22 20 21 eqtrdi ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N 2 = 1
23 13 zcnd ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N ∈ ℂ
24 23 sqvald ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N 2 = A / L N ⁢ A / L N
25 16 22 24 3eqtr3d ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → 1 = A / L N ⁢ A / L N
26 7 11 25 3eqtr4d ⊢ A ∈ ℤ ∧ N ∈ ℕ ∧ A gcd N = 1 → A / L N 2 = 1