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 
|- ( ph -> I e. ( LIdeal ` ZZring ) )
zringlpirlem.n0 
|- ( ph -> I =/= { 0 } )
zringlpirlem.g 
|- G = inf ( ( I i^i NN ) , RR , < )
Assertion zringlpirlem2 
|- ( ph -> G e. I )

Proof

Step Hyp Ref Expression
1 zringlpirlem.i 
 |-  ( ph -> I e. ( LIdeal ` ZZring ) )
2 zringlpirlem.n0 
 |-  ( ph -> I =/= { 0 } )
3 zringlpirlem.g 
 |-  G = inf ( ( I i^i NN ) , RR , < )
4 inss2 
 |-  ( I i^i NN ) C_ NN
5 nnuz 
 |-  NN = ( ZZ>= ` 1 )
6 4 5 sseqtri 
 |-  ( I i^i NN ) C_ ( ZZ>= ` 1 )
7 1 2 zringlpirlem1 
 |-  ( ph -> ( I i^i NN ) =/= (/) )
8 infssuzcl 
 |-  ( ( ( I i^i NN ) C_ ( ZZ>= ` 1 ) /\ ( I i^i NN ) =/= (/) ) -> inf ( ( I i^i NN ) , RR , < ) e. ( I i^i NN ) )
9 6 7 8 sylancr 
 |-  ( ph -> inf ( ( I i^i NN ) , RR , < ) e. ( I i^i NN ) )
10 9 elin1d 
 |-  ( ph -> inf ( ( I i^i NN ) , RR , < ) e. I )
11 3 10 eqeltrid 
 |-  ( ph -> G e. I )