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 ) )