Theorem lgssq

Description: The Legendre symbol at a square is equal to 1 . Together with lgsmod this implies that the Legendre symbol takes value 1 at every quadratic residue. (Contributed by Mario Carneiro, 5-Feb-2015) (Revised by AV, 20-Jul-2021)

	Ref	Expression
Assertion	lgssq	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝐴 ↑ 2 ) /L 𝑁 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		simp1l	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝐴 ∈ ℤ )
2		simp2	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝑁 ∈ ℤ )
3		simp1r	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝐴 ≠ 0 )
4		lgsdir	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐴 ≠ 0 ∧ 𝐴 ≠ 0 ) ) → ( ( 𝐴 · 𝐴 ) /L 𝑁 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐴 /L 𝑁 ) ) )
5	1 1 2 3 3 4	syl32anc	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝐴 · 𝐴 ) /L 𝑁 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐴 /L 𝑁 ) ) )
6		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
7	6	adantr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℂ )
8	7	3ad2ant1	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 𝐴 ∈ ℂ )
9	8	sqvald	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
10	9	oveq1d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝐴 ↑ 2 ) /L 𝑁 ) = ( ( 𝐴 · 𝐴 ) /L 𝑁 ) )
11		lgscl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ ℤ )
12	1 2 11	syl2anc	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( 𝐴 /L 𝑁 ) ∈ ℤ )
13	12	zred	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( 𝐴 /L 𝑁 ) ∈ ℝ )
14		absresq	⊢ ( ( 𝐴 /L 𝑁 ) ∈ ℝ → ( ( abs ‘ ( 𝐴 /L 𝑁 ) ) ↑ 2 ) = ( ( 𝐴 /L 𝑁 ) ↑ 2 ) )
15	13 14	syl	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( abs ‘ ( 𝐴 /L 𝑁 ) ) ↑ 2 ) = ( ( 𝐴 /L 𝑁 ) ↑ 2 ) )
16		lgsabs1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ ( 𝐴 /L 𝑁 ) ) = 1 ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )
17	16	adantlr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ ( 𝐴 /L 𝑁 ) ) = 1 ↔ ( 𝐴 gcd 𝑁 ) = 1 ) )
18	17	biimp3ar	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( abs ‘ ( 𝐴 /L 𝑁 ) ) = 1 )
19	18	oveq1d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( abs ‘ ( 𝐴 /L 𝑁 ) ) ↑ 2 ) = ( 1 ↑ 2 ) )
20		sq1	⊢ ( 1 ↑ 2 ) = 1
21	19 20	eqtrdi	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( abs ‘ ( 𝐴 /L 𝑁 ) ) ↑ 2 ) = 1 )
22	12	zcnd	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( 𝐴 /L 𝑁 ) ∈ ℂ )
23	22	sqvald	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝐴 /L 𝑁 ) ↑ 2 ) = ( ( 𝐴 /L 𝑁 ) · ( 𝐴 /L 𝑁 ) ) )
24	15 21 23	3eqtr3d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → 1 = ( ( 𝐴 /L 𝑁 ) · ( 𝐴 /L 𝑁 ) ) )
25	5 10 24	3eqtr4d	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐴 ≠ 0 ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐴 gcd 𝑁 ) = 1 ) → ( ( 𝐴 ↑ 2 ) /L 𝑁 ) = 1 )