Description: The Legendre symbol at 1 . See definition in ApostolNT p. 188. (Contributed by Mario Carneiro, 28-Apr-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | lgs1 | ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L 1 ) = 1 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sq1 | ⊢ ( 1 ↑ 2 ) = 1 | |
2 | 1 | oveq2i | ⊢ ( 𝐴 /L ( 1 ↑ 2 ) ) = ( 𝐴 /L 1 ) |
3 | gcd1 | ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 gcd 1 ) = 1 ) | |
4 | 1nn | ⊢ 1 ∈ ℕ | |
5 | lgssq2 | ⊢ ( ( 𝐴 ∈ ℤ ∧ 1 ∈ ℕ ∧ ( 𝐴 gcd 1 ) = 1 ) → ( 𝐴 /L ( 1 ↑ 2 ) ) = 1 ) | |
6 | 4 5 | mp3an2 | ⊢ ( ( 𝐴 ∈ ℤ ∧ ( 𝐴 gcd 1 ) = 1 ) → ( 𝐴 /L ( 1 ↑ 2 ) ) = 1 ) |
7 | 3 6 | mpdan | ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L ( 1 ↑ 2 ) ) = 1 ) |
8 | 2 7 | syl5eqr | ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 /L 1 ) = 1 ) |