Theorem zringlpirlem2

Description: Lemma for zringlpir . A nonzero ideal of integers contains the least positive element. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by AV, 9-Jun-2019) (Revised by AV, 27-Sep-2020)

	Ref	Expression
Hypotheses	zringlpirlem.i	$$⊢\phi \to I\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	zringlpirlem.n0	$$⊢\phi \to I\ne \left\{0\right\}$$
	zringlpirlem.g	$$⊢G=inf\left(I\cap \mathbb{N},ℝ,<\right)$$
Assertion	zringlpirlem2	$$⊢\phi \to G\in I$$

Proof

Step	Hyp	Ref	Expression
1		zringlpirlem.i	$$⊢\phi \to I\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		zringlpirlem.n0	$$⊢\phi \to I\ne \left\{0\right\}$$
3		zringlpirlem.g	$$⊢G=inf\left(I\cap \mathbb{N},ℝ,<\right)$$
4		inss2	$$⊢I\cap \mathbb{N}\subseteq \mathbb{N}$$
5		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
6	4 5	sseqtri	$$⊢I\cap \mathbb{N}\subseteq {\mathbb{Z}}_{\ge 1}$$
7	1 2	zringlpirlem1	$$⊢\phi \to I\cap \mathbb{N}\ne \varnothing$$
8		infssuzcl	$$⊢\left(I\cap \mathbb{N}\subseteq {\mathbb{Z}}_{\ge 1}\wedge I\cap \mathbb{N}\ne \varnothing \right)\to inf\left(I\cap \mathbb{N},ℝ,<\right)\in \left(I\cap \mathbb{N}\right)$$
9	6 7 8	sylancr	$$⊢\phi \to inf\left(I\cap \mathbb{N},ℝ,<\right)\in \left(I\cap \mathbb{N}\right)$$
10	9	elin1d	$$⊢\phi \to inf\left(I\cap \mathbb{N},ℝ,<\right)\in I$$
11	3 10	eqeltrid	$$⊢\phi \to G\in I$$