Metamath Proof Explorer

Theorem zringlpirlem3

Description: Lemma for zringlpir . All elements of a nonzero ideal of integers are divided by the least one. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by AV, 9-Jun-2019) (Proof shortened 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 , < )
zringlpirlem.x 
|- ( ph -> X e. I )
Assertion zringlpirlem3 
|- ( ph -> G || X )

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 zringlpirlem.x 
 |-  ( ph -> X e. I )
5 zringbas 
 |-  ZZ = ( Base ` ZZring )
6 eqid 
 |-  ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
7 5 6 lidlss 
 |-  ( I e. ( LIdeal ` ZZring ) -> I C_ ZZ )
8 1 7 syl 
 |-  ( ph -> I C_ ZZ )
9 8 4 sseldd 
 |-  ( ph -> X e. ZZ )
10 9 zred 
 |-  ( ph -> X e. RR )
11 inss2 
 |-  ( I i^i NN ) C_ NN
12 nnuz 
 |-  NN = ( ZZ>= ` 1 )
13 11 12 sseqtri 
 |-  ( I i^i NN ) C_ ( ZZ>= ` 1 )
14 1 2 zringlpirlem1 
 |-  ( ph -> ( I i^i NN ) =/= (/) )
15 infssuzcl 
 |-  ( ( ( I i^i NN ) C_ ( ZZ>= ` 1 ) /\ ( I i^i NN ) =/= (/) ) -> inf ( ( I i^i NN ) , RR , < ) e. ( I i^i NN ) )
16 13 14 15 sylancr 
 |-  ( ph -> inf ( ( I i^i NN ) , RR , < ) e. ( I i^i NN ) )
17 3 16 eqeltrid 
 |-  ( ph -> G e. ( I i^i NN ) )
18 17 elin2d 
 |-  ( ph -> G e. NN )
19 18 nnrpd 
 |-  ( ph -> G e. RR+ )
20 modlt 
 |-  ( ( X e. RR /\ G e. RR+ ) -> ( X mod G ) < G )
21 10 19 20 syl2anc 
 |-  ( ph -> ( X mod G ) < G )
22 9 18 zmodcld 
 |-  ( ph -> ( X mod G ) e. NN0 )
23 22 nn0red 
 |-  ( ph -> ( X mod G ) e. RR )
24 18 nnred 
 |-  ( ph -> G e. RR )
25 23 24 ltnled 
 |-  ( ph -> ( ( X mod G ) < G <-> -. G <_ ( X mod G ) ) )
26 21 25 mpbid 
 |-  ( ph -> -. G <_ ( X mod G ) )
27 9 zcnd 
 |-  ( ph -> X e. CC )
28 18 nncnd 
 |-  ( ph -> G e. CC )
29 10 18 nndivred 
 |-  ( ph -> ( X / G ) e. RR )
30 29 flcld 
 |-  ( ph -> ( |_ ` ( X / G ) ) e. ZZ )
31 30 zcnd 
 |-  ( ph -> ( |_ ` ( X / G ) ) e. CC )
32 28 31 mulcld 
 |-  ( ph -> ( G x. ( |_ ` ( X / G ) ) ) e. CC )
33 27 32 negsubd 
 |-  ( ph -> ( X + -u ( G x. ( |_ ` ( X / G ) ) ) ) = ( X - ( G x. ( |_ ` ( X / G ) ) ) ) )
34 30 znegcld 
 |-  ( ph -> -u ( |_ ` ( X / G ) ) e. ZZ )
35 34 zcnd 
 |-  ( ph -> -u ( |_ ` ( X / G ) ) e. CC )
36 35 28 mulcomd 
 |-  ( ph -> ( -u ( |_ ` ( X / G ) ) x. G ) = ( G x. -u ( |_ ` ( X / G ) ) ) )
37 28 31 mulneg2d 
 |-  ( ph -> ( G x. -u ( |_ ` ( X / G ) ) ) = -u ( G x. ( |_ ` ( X / G ) ) ) )
38 36 37 eqtrd 
 |-  ( ph -> ( -u ( |_ ` ( X / G ) ) x. G ) = -u ( G x. ( |_ ` ( X / G ) ) ) )
39 38 oveq2d 
 |-  ( ph -> ( X + ( -u ( |_ ` ( X / G ) ) x. G ) ) = ( X + -u ( G x. ( |_ ` ( X / G ) ) ) ) )
40 modval 
 |-  ( ( X e. RR /\ G e. RR+ ) -> ( X mod G ) = ( X - ( G x. ( |_ ` ( X / G ) ) ) ) )
41 10 19 40 syl2anc 
 |-  ( ph -> ( X mod G ) = ( X - ( G x. ( |_ ` ( X / G ) ) ) ) )
42 33 39 41 3eqtr4rd 
 |-  ( ph -> ( X mod G ) = ( X + ( -u ( |_ ` ( X / G ) ) x. G ) ) )
43 zringring 
 |-  ZZring e. Ring
44 43 a1i 
 |-  ( ph -> ZZring e. Ring )
45 1 2 3 zringlpirlem2 
 |-  ( ph -> G e. I )
46 zringmulr 
 |-  x. = ( .r ` ZZring )
47 6 5 46 lidlmcl 
 |-  ( ( ( ZZring e. Ring /\ I e. ( LIdeal ` ZZring ) ) /\ ( -u ( |_ ` ( X / G ) ) e. ZZ /\ G e. I ) ) -> ( -u ( |_ ` ( X / G ) ) x. G ) e. I )
48 44 1 34 45 47 syl22anc 
 |-  ( ph -> ( -u ( |_ ` ( X / G ) ) x. G ) e. I )
49 zringplusg 
 |-  + = ( +g ` ZZring )
50 6 49 lidlacl 
 |-  ( ( ( ZZring e. Ring /\ I e. ( LIdeal ` ZZring ) ) /\ ( X e. I /\ ( -u ( |_ ` ( X / G ) ) x. G ) e. I ) ) -> ( X + ( -u ( |_ ` ( X / G ) ) x. G ) ) e. I )
51 44 1 4 48 50 syl22anc 
 |-  ( ph -> ( X + ( -u ( |_ ` ( X / G ) ) x. G ) ) e. I )
52 42 51 eqeltrd 
 |-  ( ph -> ( X mod G ) e. I )
53 52 adantr 
 |-  ( ( ph /\ ( X mod G ) e. NN ) -> ( X mod G ) e. I )
54 simpr 
 |-  ( ( ph /\ ( X mod G ) e. NN ) -> ( X mod G ) e. NN )
55 53 54 elind 
 |-  ( ( ph /\ ( X mod G ) e. NN ) -> ( X mod G ) e. ( I i^i NN ) )
56 infssuzle 
 |-  ( ( ( I i^i NN ) C_ ( ZZ>= ` 1 ) /\ ( X mod G ) e. ( I i^i NN ) ) -> inf ( ( I i^i NN ) , RR , < ) <_ ( X mod G ) )
57 13 55 56 sylancr 
 |-  ( ( ph /\ ( X mod G ) e. NN ) -> inf ( ( I i^i NN ) , RR , < ) <_ ( X mod G ) )
58 3 57 eqbrtrid 
 |-  ( ( ph /\ ( X mod G ) e. NN ) -> G <_ ( X mod G ) )
59 26 58 mtand 
 |-  ( ph -> -. ( X mod G ) e. NN )
60 elnn0 
 |-  ( ( X mod G ) e. NN0 <-> ( ( X mod G ) e. NN \/ ( X mod G ) = 0 ) )
61 22 60 sylib 
 |-  ( ph -> ( ( X mod G ) e. NN \/ ( X mod G ) = 0 ) )
62 orel1 
 |-  ( -. ( X mod G ) e. NN -> ( ( ( X mod G ) e. NN \/ ( X mod G ) = 0 ) -> ( X mod G ) = 0 ) )
63 59 61 62 sylc 
 |-  ( ph -> ( X mod G ) = 0 )
64 dvdsval3 
 |-  ( ( G e. NN /\ X e. ZZ ) -> ( G || X <-> ( X mod G ) = 0 ) )
65 18 9 64 syl2anc 
 |-  ( ph -> ( G || X <-> ( X mod G ) = 0 ) )
66 63 65 mpbird 
 |-  ( ph -> G || X )