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	$$⊢\phi \to I\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
	zringlpirlem.n0	$$⊢\phi \to I\ne \left\{0\right\}$$
Assertion	zringlpirlem1	$$⊢\phi \to I\cap \mathbb{N}\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		zringlpirlem.i	$$⊢\phi \to I\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
2		zringlpirlem.n0	$$⊢\phi \to I\ne \left\{0\right\}$$
3		simplr	$$⊢\left(\left(\phi \wedge a\in I\right)\wedge a\ne 0\right)\to a\in I$$
4		eleq1	$$⊢\left|a\right|=a\to \left(\left|a\right|\in I\leftrightarrow a\in I\right)$$
5	3 4	syl5ibrcom	$$⊢\left(\left(\phi \wedge a\in I\right)\wedge a\ne 0\right)\to \left(\left|a\right|=a\to \left|a\right|\in I\right)$$
6		zsubrg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
7		subrgsubg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\to \mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
8	6 7	ax-mp	$$⊢\mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)$$
9		zringbas	$$⊢\mathbb{Z}={\mathrm{Base}}_{{\mathbb{Z}}_{\mathrm{ring}}}$$
10		eqid	$$⊢\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)=\mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
11	9 10	lidlss	$$⊢I\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\to I\subseteq \mathbb{Z}$$
12	1 11	syl	$$⊢\phi \to I\subseteq \mathbb{Z}$$
13	12	sselda	$$⊢\left(\phi \wedge a\in I\right)\to a\in \mathbb{Z}$$
14		df-zring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Z}$$
15		eqid	$$⊢{inv}_g\left({ℂ}_{\mathrm{fld}}\right)={inv}_g\left({ℂ}_{\mathrm{fld}}\right)$$
16		eqid	$$⊢{inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
17	14 15 16	subginv	$$⊢\left(\mathbb{Z}\in \mathrm{SubGrp}\left({ℂ}_{\mathrm{fld}}\right)\wedge a\in \mathbb{Z}\right)\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(a\right)={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(a\right)$$
18	8 13 17	sylancr	$$⊢\left(\phi \wedge a\in I\right)\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(a\right)={inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(a\right)$$
19	13	zcnd	$$⊢\left(\phi \wedge a\in I\right)\to a\in ℂ$$
20		cnfldneg	$$⊢a\in ℂ\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(a\right)=-a$$
21	19 20	syl	$$⊢\left(\phi \wedge a\in I\right)\to {inv}_g\left({ℂ}_{\mathrm{fld}}\right)\left(a\right)=-a$$
22	18 21	eqtr3d	$$⊢\left(\phi \wedge a\in I\right)\to {inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(a\right)=-a$$
23		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
24	1	adantr	$$⊢\left(\phi \wedge a\in I\right)\to I\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)$$
25		simpr	$$⊢\left(\phi \wedge a\in I\right)\to a\in I$$
26	10 16	lidlnegcl	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge I\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge a\in I\right)\to {inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(a\right)\in I$$
27	23 24 25 26	mp3an2i	$$⊢\left(\phi \wedge a\in I\right)\to {inv}_g\left({\mathbb{Z}}_{\mathrm{ring}}\right)\left(a\right)\in I$$
28	22 27	eqeltrrd	$$⊢\left(\phi \wedge a\in I\right)\to -a\in I$$
29	28	adantr	$$⊢\left(\left(\phi \wedge a\in I\right)\wedge a\ne 0\right)\to -a\in I$$
30		eleq1	$$⊢\left|a\right|=-a\to \left(\left|a\right|\in I\leftrightarrow -a\in I\right)$$
31	29 30	syl5ibrcom	$$⊢\left(\left(\phi \wedge a\in I\right)\wedge a\ne 0\right)\to \left(\left|a\right|=-a\to \left|a\right|\in I\right)$$
32	13	zred	$$⊢\left(\phi \wedge a\in I\right)\to a\in ℝ$$
33	32	absord	$$⊢\left(\phi \wedge a\in I\right)\to \left(\left|a\right|=a\vee \left|a\right|=-a\right)$$
34	33	adantr	$$⊢\left(\left(\phi \wedge a\in I\right)\wedge a\ne 0\right)\to \left(\left|a\right|=a\vee \left|a\right|=-a\right)$$
35	5 31 34	mpjaod	$$⊢\left(\left(\phi \wedge a\in I\right)\wedge a\ne 0\right)\to \left|a\right|\in I$$
36		nnabscl	$$⊢\left(a\in \mathbb{Z}\wedge a\ne 0\right)\to \left|a\right|\in \mathbb{N}$$
37	13 36	sylan	$$⊢\left(\left(\phi \wedge a\in I\right)\wedge a\ne 0\right)\to \left|a\right|\in \mathbb{N}$$
38	35 37	elind	$$⊢\left(\left(\phi \wedge a\in I\right)\wedge a\ne 0\right)\to \left|a\right|\in \left(I\cap \mathbb{N}\right)$$
39	38	ne0d	$$⊢\left(\left(\phi \wedge a\in I\right)\wedge a\ne 0\right)\to I\cap \mathbb{N}\ne \varnothing$$
40		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
41	10 40	lidlnz	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge I\in \mathrm{LIdeal}\left({\mathbb{Z}}_{\mathrm{ring}}\right)\wedge I\ne \left\{0\right\}\right)\to \exists a\in Ia\ne 0$$
42	23 1 2 41	mp3an2i	$$⊢\phi \to \exists a\in Ia\ne 0$$
43	39 42	r19.29a	$$⊢\phi \to I\cap \mathbb{N}\ne \varnothing$$