This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem znlidl

Description: The set n ZZ is an ideal in ZZ . (Contributed by Mario Carneiro, 14-Jun-2015) (Revised by AV, 13-Jun-2019)

Ref Expression
Hypothesis znval.s ⊢ 𝑆 = ( RSpan ‘ ℤring )
Assertion znlidl ( 𝑁 ∈ ℤ → ( 𝑆 ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )

Proof

Step Hyp Ref Expression
1 znval.s ⊢ 𝑆 = ( RSpan ‘ ℤring )
2 zringring ⊢ ℤring ∈ Ring
3 snssi ⊢ ( 𝑁 ∈ ℤ → { 𝑁 } ⊆ ℤ )
4 zringbas ⊢ ℤ = ( Base ‘ ℤring )
5 eqid ⊢ ( LIdeal ‘ ℤring ) = ( LIdeal ‘ ℤring )
6 1 4 5 rspcl ⊢ ( ( ℤring ∈ Ring ∧ { 𝑁 } ⊆ ℤ ) → ( 𝑆 ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )
7 2 3 6 sylancr ⊢ ( 𝑁 ∈ ℤ → ( 𝑆 ‘ { 𝑁 } ) ∈ ( LIdeal ‘ ℤring ) )