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=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
Assertion	znlidl	$$⊢N\in \mathbb{Z}\to S\left(\left\{N\right\}\right)\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$

Proof

Step	Hyp	Ref	Expression
1		znval.s	$$⊢S=\mathrm{RSpan}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
3		snssi	$$⊢N\in \mathbb{Z}\to \left\{N\right\}\subseteq \mathbb{Z}$$
4		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
5		eqid	$$⊢\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
6	1 4 5	rspcl	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge \left\{N\right\}\subseteq \mathbb{Z}\right)\to S\left(\left\{N\right\}\right)\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
7	2 3 6	sylancr	$$⊢N\in \mathbb{Z}\to S\left(\left\{N\right\}\right)\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$