This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐼 ∩ ℕ ) ≠ ∅ )