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 )