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 ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( 𝐴 /L ( 𝑁 ↑ 2 ) ) = 1 )

Proof

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