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 ⊢ ( 𝜑 → 𝐼 ∈ ( 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 ⊢ ( 𝜑 → 𝐺 ∈ 𝐼 )