Theorem zringlpirlem1

Description: Lemma for zringlpir . A nonzero ideal of integers contains some positive integers. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by AV, 9-Jun-2019)

	Ref	Expression
Hypotheses	zringlpirlem.i	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ ℤring ) )
	zringlpirlem.n0	⊢ ( 𝜑 → 𝐼 ≠ { 0 } )
Assertion	zringlpirlem1	⊢ ( 𝜑 → ( 𝐼 ∩ ℕ ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		zringlpirlem.i	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ ℤring ) )
2		zringlpirlem.n0	⊢ ( 𝜑 → 𝐼 ≠ { 0 } )
3		simplr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑎 ≠ 0 ) → 𝑎 ∈ 𝐼 )
4		eleq1	⊢ ( ( abs ‘ 𝑎 ) = 𝑎 → ( ( abs ‘ 𝑎 ) ∈ 𝐼 ↔ 𝑎 ∈ 𝐼 ) )
5	3 4	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑎 ≠ 0 ) → ( ( abs ‘ 𝑎 ) = 𝑎 → ( abs ‘ 𝑎 ) ∈ 𝐼 ) )
6		zsubrg	⊢ ℤ ∈ ( SubRing ‘ ℂfld )
7		subrgsubg	⊢ ( ℤ ∈ ( SubRing ‘ ℂfld ) → ℤ ∈ ( SubGrp ‘ ℂfld ) )
8	6 7	ax-mp	⊢ ℤ ∈ ( SubGrp ‘ ℂfld )
9		zringbas	⊢ ℤ = ( Base ‘ ℤring )
10		eqid	⊢ ( LIdeal ‘ ℤring ) = ( LIdeal ‘ ℤring )
11	9 10	lidlss	⊢ ( 𝐼 ∈ ( LIdeal ‘ ℤring ) → 𝐼 ⊆ ℤ )
12	1 11	syl	⊢ ( 𝜑 → 𝐼 ⊆ ℤ )
13	12	sselda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝑎 ∈ ℤ )
14		df-zring	⊢ ℤring = ( ℂfld ↾s ℤ )
15		eqid	⊢ ( invg ‘ ℂfld ) = ( invg ‘ ℂfld )
16		eqid	⊢ ( invg ‘ ℤring ) = ( invg ‘ ℤring )
17	14 15 16	subginv	⊢ ( ( ℤ ∈ ( SubGrp ‘ ℂfld ) ∧ 𝑎 ∈ ℤ ) → ( ( invg ‘ ℂfld ) ‘ 𝑎 ) = ( ( invg ‘ ℤring ) ‘ 𝑎 ) )
18	8 13 17	sylancr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( invg ‘ ℂfld ) ‘ 𝑎 ) = ( ( invg ‘ ℤring ) ‘ 𝑎 ) )
19	13	zcnd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝑎 ∈ ℂ )
20		cnfldneg	⊢ ( 𝑎 ∈ ℂ → ( ( invg ‘ ℂfld ) ‘ 𝑎 ) = - 𝑎 )
21	19 20	syl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( invg ‘ ℂfld ) ‘ 𝑎 ) = - 𝑎 )
22	18 21	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( invg ‘ ℤring ) ‘ 𝑎 ) = - 𝑎 )
23		zringring	⊢ ℤring ∈ Ring
24	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝐼 ∈ ( LIdeal ‘ ℤring ) )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝑎 ∈ 𝐼 )
26	10 16	lidlnegcl	⊢ ( ( ℤring ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ ℤring ) ∧ 𝑎 ∈ 𝐼 ) → ( ( invg ‘ ℤring ) ‘ 𝑎 ) ∈ 𝐼 )
27	23 24 25 26	mp3an2i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( invg ‘ ℤring ) ‘ 𝑎 ) ∈ 𝐼 )
28	22 27	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → - 𝑎 ∈ 𝐼 )
29	28	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑎 ≠ 0 ) → - 𝑎 ∈ 𝐼 )
30		eleq1	⊢ ( ( abs ‘ 𝑎 ) = - 𝑎 → ( ( abs ‘ 𝑎 ) ∈ 𝐼 ↔ - 𝑎 ∈ 𝐼 ) )
31	29 30	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑎 ≠ 0 ) → ( ( abs ‘ 𝑎 ) = - 𝑎 → ( abs ‘ 𝑎 ) ∈ 𝐼 ) )
32	13	zred	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → 𝑎 ∈ ℝ )
33	32	absord	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) → ( ( abs ‘ 𝑎 ) = 𝑎 ∨ ( abs ‘ 𝑎 ) = - 𝑎 ) )
34	33	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑎 ≠ 0 ) → ( ( abs ‘ 𝑎 ) = 𝑎 ∨ ( abs ‘ 𝑎 ) = - 𝑎 ) )
35	5 31 34	mpjaod	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ 𝑎 ) ∈ 𝐼 )
36		nnabscl	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑎 ≠ 0 ) → ( abs ‘ 𝑎 ) ∈ ℕ )
37	13 36	sylan	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ 𝑎 ) ∈ ℕ )
38	35 37	elind	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑎 ≠ 0 ) → ( abs ‘ 𝑎 ) ∈ ( 𝐼 ∩ ℕ ) )
39	38	ne0d	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐼 ) ∧ 𝑎 ≠ 0 ) → ( 𝐼 ∩ ℕ ) ≠ ∅ )
40		zring0	⊢ 0 = ( 0g ‘ ℤring )
41	10 40	lidlnz	⊢ ( ( ℤring ∈ Ring ∧ 𝐼 ∈ ( LIdeal ‘ ℤring ) ∧ 𝐼 ≠ { 0 } ) → ∃ 𝑎 ∈ 𝐼 𝑎 ≠ 0 )
42	23 1 2 41	mp3an2i	⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐼 𝑎 ≠ 0 )
43	39 42	r19.29a	⊢ ( 𝜑 → ( 𝐼 ∩ ℕ ) ≠ ∅ )