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

Proof

Step Hyp Ref Expression
1 zringlpirlem.i 
 |-  ( ph -> I e. ( LIdeal ` ZZring ) )
2 zringlpirlem.n0 
 |-  ( ph -> I =/= { 0 } )
3 simplr 
 |-  ( ( ( ph /\ a e. I ) /\ a =/= 0 ) -> a e. I )
4 eleq1 
 |-  ( ( abs ` a ) = a -> ( ( abs ` a ) e. I <-> a e. I ) )
5 3 4 syl5ibrcom 
 |-  ( ( ( ph /\ a e. I ) /\ a =/= 0 ) -> ( ( abs ` a ) = a -> ( abs ` a ) e. I ) )
6 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
7 subrgsubg 
 |-  ( ZZ e. ( SubRing ` CCfld ) -> ZZ e. ( SubGrp ` CCfld ) )
8 6 7 ax-mp 
 |-  ZZ e. ( SubGrp ` CCfld )
9 zringbas 
 |-  ZZ = ( Base ` ZZring )
10 eqid 
 |-  ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
11 9 10 lidlss 
 |-  ( I e. ( LIdeal ` ZZring ) -> I C_ ZZ )
12 1 11 syl 
 |-  ( ph -> I C_ ZZ )
13 12 sselda 
 |-  ( ( ph /\ a e. I ) -> a e. ZZ )
14 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
15 eqid 
 |-  ( invg ` CCfld ) = ( invg ` CCfld )
16 eqid 
 |-  ( invg ` ZZring ) = ( invg ` ZZring )
17 14 15 16 subginv 
 |-  ( ( ZZ e. ( SubGrp ` CCfld ) /\ a e. ZZ ) -> ( ( invg ` CCfld ) ` a ) = ( ( invg ` ZZring ) ` a ) )
18 8 13 17 sylancr 
 |-  ( ( ph /\ a e. I ) -> ( ( invg ` CCfld ) ` a ) = ( ( invg ` ZZring ) ` a ) )
19 13 zcnd 
 |-  ( ( ph /\ a e. I ) -> a e. CC )
20 cnfldneg 
 |-  ( a e. CC -> ( ( invg ` CCfld ) ` a ) = -u a )
21 19 20 syl 
 |-  ( ( ph /\ a e. I ) -> ( ( invg ` CCfld ) ` a ) = -u a )
22 18 21 eqtr3d 
 |-  ( ( ph /\ a e. I ) -> ( ( invg ` ZZring ) ` a ) = -u a )
23 zringring 
 |-  ZZring e. Ring
24 1 adantr 
 |-  ( ( ph /\ a e. I ) -> I e. ( LIdeal ` ZZring ) )
25 simpr 
 |-  ( ( ph /\ a e. I ) -> a e. I )
26 10 16 lidlnegcl 
 |-  ( ( ZZring e. Ring /\ I e. ( LIdeal ` ZZring ) /\ a e. I ) -> ( ( invg ` ZZring ) ` a ) e. I )
27 23 24 25 26 mp3an2i 
 |-  ( ( ph /\ a e. I ) -> ( ( invg ` ZZring ) ` a ) e. I )
28 22 27 eqeltrrd 
 |-  ( ( ph /\ a e. I ) -> -u a e. I )
29 28 adantr 
 |-  ( ( ( ph /\ a e. I ) /\ a =/= 0 ) -> -u a e. I )
30 eleq1 
 |-  ( ( abs ` a ) = -u a -> ( ( abs ` a ) e. I <-> -u a e. I ) )
31 29 30 syl5ibrcom 
 |-  ( ( ( ph /\ a e. I ) /\ a =/= 0 ) -> ( ( abs ` a ) = -u a -> ( abs ` a ) e. I ) )
32 13 zred 
 |-  ( ( ph /\ a e. I ) -> a e. RR )
33 32 absord 
 |-  ( ( ph /\ a e. I ) -> ( ( abs ` a ) = a \/ ( abs ` a ) = -u a ) )
34 33 adantr 
 |-  ( ( ( ph /\ a e. I ) /\ a =/= 0 ) -> ( ( abs ` a ) = a \/ ( abs ` a ) = -u a ) )
35 5 31 34 mpjaod 
 |-  ( ( ( ph /\ a e. I ) /\ a =/= 0 ) -> ( abs ` a ) e. I )
36 nnabscl 
 |-  ( ( a e. ZZ /\ a =/= 0 ) -> ( abs ` a ) e. NN )
37 13 36 sylan 
 |-  ( ( ( ph /\ a e. I ) /\ a =/= 0 ) -> ( abs ` a ) e. NN )
38 35 37 elind 
 |-  ( ( ( ph /\ a e. I ) /\ a =/= 0 ) -> ( abs ` a ) e. ( I i^i NN ) )
39 38 ne0d 
 |-  ( ( ( ph /\ a e. I ) /\ a =/= 0 ) -> ( I i^i NN ) =/= (/) )
40 zring0 
 |-  0 = ( 0g ` ZZring )
41 10 40 lidlnz 
 |-  ( ( ZZring e. Ring /\ I e. ( LIdeal ` ZZring ) /\ I =/= { 0 } ) -> E. a e. I a =/= 0 )
42 23 1 2 41 mp3an2i 
 |-  ( ph -> E. a e. I a =/= 0 )
43 39 42 r19.29a 
 |-  ( ph -> ( I i^i NN ) =/= (/) )