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

Metamath Proof Explorer

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	$⊢ φ \to I \in LIdeal (ℤ_{ring})$
		zringlpirlem.n0	$⊢ φ \to I \neq \{0\}$
		zringlpirlem.g	$⊢ G = inf (I \cap ℕ ℝ <)$
	Assertion	zringlpirlem2	$⊢ φ \to G \in I$

Proof

Step	Hyp	Ref	Expression
1		zringlpirlem.i	$⊢ φ \to I \in LIdeal (ℤ_{ring})$
2		zringlpirlem.n0	$⊢ φ \to I \neq \{0\}$
3		zringlpirlem.g	$⊢ G = inf (I \cap ℕ ℝ <)$
4		inss2	$⊢ I \cap ℕ \subseteq ℕ$
5		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
6	4 5	sseqtri	$⊢ I \cap ℕ \subseteq ℤ_{\geq 1}$
7	1 2	zringlpirlem1	$⊢ φ \to I \cap ℕ \neq \emptyset$
8		infssuzcl	$⊢ (I \cap ℕ \subseteq ℤ_{\geq 1} \land I \cap ℕ \neq \emptyset) \to inf (I \cap ℕ ℝ <) \in (I \cap ℕ)$
9	6 7 8	sylancr	$⊢ φ \to inf (I \cap ℕ ℝ <) \in (I \cap ℕ)$
10	9	elin1d	$⊢ φ \to inf (I \cap ℕ ℝ <) \in I$
11	3 10	eqeltrid	$⊢ φ \to G \in I$