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 )