Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } = { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } |
2 |
1
|
lgscl2 |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐴 /L 𝑁 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } ) |
3 |
|
fveq2 |
⊢ ( 𝑥 = ( 𝐴 /L 𝑁 ) → ( abs ‘ 𝑥 ) = ( abs ‘ ( 𝐴 /L 𝑁 ) ) ) |
4 |
3
|
breq1d |
⊢ ( 𝑥 = ( 𝐴 /L 𝑁 ) → ( ( abs ‘ 𝑥 ) ≤ 1 ↔ ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 ) ) |
5 |
4
|
elrab |
⊢ ( ( 𝐴 /L 𝑁 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } ↔ ( ( 𝐴 /L 𝑁 ) ∈ ℤ ∧ ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 ) ) |
6 |
5
|
simprbi |
⊢ ( ( 𝐴 /L 𝑁 ) ∈ { 𝑥 ∈ ℤ ∣ ( abs ‘ 𝑥 ) ≤ 1 } → ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 ) |
7 |
2 6
|
syl |
⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝐴 /L 𝑁 ) ) ≤ 1 ) |