Metamath Proof Explorer

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 )