Metamath Proof Explorer

Theorem zringlpir

Description: The integers are a principal ideal ring. (Contributed by Stefan O'Rear, 3-Jan-2015) (Revised by AV, 9-Jun-2019) (Proof shortened by AV, 27-Sep-2020)

Ref Expression
Assertion zringlpir 
|- ZZring e. LPIR

Proof

Step Hyp Ref Expression
1 zringring 
 |-  ZZring e. Ring
2 eleq1 
 |-  ( x = { 0 } -> ( x e. ( LPIdeal ` ZZring ) <-> { 0 } e. ( LPIdeal ` ZZring ) ) )
3 simpl 
 |-  ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) -> x e. ( LIdeal ` ZZring ) )
4 simpr 
 |-  ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) -> x =/= { 0 } )
5 eqid 
 |-  inf ( ( x i^i NN ) , RR , < ) = inf ( ( x i^i NN ) , RR , < )
6 3 4 5 zringlpirlem2 
 |-  ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) -> inf ( ( x i^i NN ) , RR , < ) e. x )
7 simpll 
 |-  ( ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) /\ z e. x ) -> x e. ( LIdeal ` ZZring ) )
8 simplr 
 |-  ( ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) /\ z e. x ) -> x =/= { 0 } )
9 simpr 
 |-  ( ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) /\ z e. x ) -> z e. x )
10 7 8 5 9 zringlpirlem3 
 |-  ( ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) /\ z e. x ) -> inf ( ( x i^i NN ) , RR , < ) || z )
11 10 ralrimiva 
 |-  ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) -> A. z e. x inf ( ( x i^i NN ) , RR , < ) || z )
12 breq1 
 |-  ( y = inf ( ( x i^i NN ) , RR , < ) -> ( y || z <-> inf ( ( x i^i NN ) , RR , < ) || z ) )
13 12 ralbidv 
 |-  ( y = inf ( ( x i^i NN ) , RR , < ) -> ( A. z e. x y || z <-> A. z e. x inf ( ( x i^i NN ) , RR , < ) || z ) )
14 13 rspcev 
 |-  ( ( inf ( ( x i^i NN ) , RR , < ) e. x /\ A. z e. x inf ( ( x i^i NN ) , RR , < ) || z ) -> E. y e. x A. z e. x y || z )
15 6 11 14 syl2anc 
 |-  ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) -> E. y e. x A. z e. x y || z )
16 eqid 
 |-  ( LIdeal ` ZZring ) = ( LIdeal ` ZZring )
17 eqid 
 |-  ( LPIdeal ` ZZring ) = ( LPIdeal ` ZZring )
18 dvdsrzring 
 |-  || = ( ||r ` ZZring )
19 16 17 18 lpigen 
 |-  ( ( ZZring e. Ring /\ x e. ( LIdeal ` ZZring ) ) -> ( x e. ( LPIdeal ` ZZring ) <-> E. y e. x A. z e. x y || z ) )
20 1 19 mpan 
 |-  ( x e. ( LIdeal ` ZZring ) -> ( x e. ( LPIdeal ` ZZring ) <-> E. y e. x A. z e. x y || z ) )
21 20 adantr 
 |-  ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) -> ( x e. ( LPIdeal ` ZZring ) <-> E. y e. x A. z e. x y || z ) )
22 15 21 mpbird 
 |-  ( ( x e. ( LIdeal ` ZZring ) /\ x =/= { 0 } ) -> x e. ( LPIdeal ` ZZring ) )
23 zring0 
 |-  0 = ( 0g ` ZZring )
24 17 23 lpi0 
 |-  ( ZZring e. Ring -> { 0 } e. ( LPIdeal ` ZZring ) )
25 1 24 mp1i 
 |-  ( x e. ( LIdeal ` ZZring ) -> { 0 } e. ( LPIdeal ` ZZring ) )
26 2 22 25 pm2.61ne 
 |-  ( x e. ( LIdeal ` ZZring ) -> x e. ( LPIdeal ` ZZring ) )
27 26 ssriv 
 |-  ( LIdeal ` ZZring ) C_ ( LPIdeal ` ZZring )
28 17 16 islpir2 
 |-  ( ZZring e. LPIR <-> ( ZZring e. Ring /\ ( LIdeal ` ZZring ) C_ ( LPIdeal ` ZZring ) ) )
29 1 27 28 mpbir2an 
 |-  ZZring e. LPIR