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	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ ℤring ) )
	zringlpirlem.n0	⊢ ( 𝜑 → 𝐼 ≠ { 0 } )
	zringlpirlem.g	⊢ 𝐺 = inf ( ( 𝐼 ∩ ℕ ) , ℝ , < )
Assertion	zringlpirlem2	⊢ ( 𝜑 → 𝐺 ∈ 𝐼 )

Proof

Step	Hyp	Ref	Expression
1		zringlpirlem.i	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ ℤring ) )
2		zringlpirlem.n0	⊢ ( 𝜑 → 𝐼 ≠ { 0 } )
3		zringlpirlem.g	⊢ 𝐺 = inf ( ( 𝐼 ∩ ℕ ) , ℝ , < )
4		inss2	⊢ ( 𝐼 ∩ ℕ ) ⊆ ℕ
5		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
6	4 5	sseqtri	⊢ ( 𝐼 ∩ ℕ ) ⊆ ( ℤ≥ ‘ 1 )
7	1 2	zringlpirlem1	⊢ ( 𝜑 → ( 𝐼 ∩ ℕ ) ≠ ∅ )
8		infssuzcl	⊢ ( ( ( 𝐼 ∩ ℕ ) ⊆ ( ℤ≥ ‘ 1 ) ∧ ( 𝐼 ∩ ℕ ) ≠ ∅ ) → inf ( ( 𝐼 ∩ ℕ ) , ℝ , < ) ∈ ( 𝐼 ∩ ℕ ) )
9	6 7 8	sylancr	⊢ ( 𝜑 → inf ( ( 𝐼 ∩ ℕ ) , ℝ , < ) ∈ ( 𝐼 ∩ ℕ ) )
10	9	elin1d	⊢ ( 𝜑 → inf ( ( 𝐼 ∩ ℕ ) , ℝ , < ) ∈ 𝐼 )
11	3 10	eqeltrid	⊢ ( 𝜑 → 𝐺 ∈ 𝐼 )