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	|- S = ( RSpan ` ZZring )
Assertion	znlidl	|- ( N e. ZZ -> ( S ` { N } ) e. ( LIdeal ` ZZring ) )

Proof

Step	Hyp	Ref	Expression
1		znval.s	|- S = ( RSpan ` ZZring )
2		zringring	|- ZZring e. Ring
3		snssi	|- ( N e. ZZ -> { N } C_ ZZ )
4		zringbas	|- ZZ = ( Base ` ZZring )
5		eqid	|- ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
6	1 4 5	rspcl	|- ( ( ZZring e. Ring /\ { N } C_ ZZ ) -> ( S ` { N } ) e. ( LIdeal ` ZZring ) )
7	2 3 6	sylancr	|- ( N e. ZZ -> ( S ` { N } ) e. ( LIdeal ` ZZring ) )