Metamath Proof Explorer

Theorem nzss

Description: The set of multiples ofm, mℤ, is a subset of those ofn, nℤ, iffn dividesm. Lemma 2.1(a) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5, with mℤ and nℤ as images of the divides relation underm andn. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Hypotheses nzss.m 
|- ( ph -> M e. ZZ )
nzss.n 
|- ( ph -> N e. V )
Assertion nzss 
|- ( ph -> ( ( || " { M } ) C_ ( || " { N } ) <-> N || M ) )

Proof

Step Hyp Ref Expression
1 nzss.m 
 |-  ( ph -> M e. ZZ )
2 nzss.n 
 |-  ( ph -> N e. V )
3 iddvds 
 |-  ( M e. ZZ -> M || M )
4 breq2 
 |-  ( x = M -> ( M || x <-> M || M ) )
5 4 elabg 
 |-  ( M e. ZZ -> ( M e. { x | M || x } <-> M || M ) )
6 3 5 mpbird 
 |-  ( M e. ZZ -> M e. { x | M || x } )
7 reldvds 
 |-  Rel ||
8 relimasn 
 |-  ( Rel || -> ( || " { M } ) = { x | M || x } )
9 7 8 ax-mp 
 |-  ( || " { M } ) = { x | M || x }
10 6 9 eleqtrrdi 
 |-  ( M e. ZZ -> M e. ( || " { M } ) )
11 ssel 
 |-  ( ( || " { M } ) C_ ( || " { N } ) -> ( M e. ( || " { M } ) -> M e. ( || " { N } ) ) )
12 10 11 syl5 
 |-  ( ( || " { M } ) C_ ( || " { N } ) -> ( M e. ZZ -> M e. ( || " { N } ) ) )
13 breq2 
 |-  ( x = M -> ( N || x <-> N || M ) )
14 relimasn 
 |-  ( Rel || -> ( || " { N } ) = { x | N || x } )
15 7 14 ax-mp 
 |-  ( || " { N } ) = { x | N || x }
16 13 15 elab2g 
 |-  ( M e. ZZ -> ( M e. ( || " { N } ) <-> N || M ) )
17 12 16 mpbidi 
 |-  ( ( || " { M } ) C_ ( || " { N } ) -> ( M e. ZZ -> N || M ) )
18 17 com12 
 |-  ( M e. ZZ -> ( ( || " { M } ) C_ ( || " { N } ) -> N || M ) )
19 18 adantr 
 |-  ( ( M e. ZZ /\ N e. V ) -> ( ( || " { M } ) C_ ( || " { N } ) -> N || M ) )
20 ssid 
 |-  { 0 } C_ { 0 }
21 simpl 
 |-  ( ( N || M /\ N = 0 ) -> N || M )
22 breq1 
 |-  ( N = 0 -> ( N || M <-> 0 || M ) )
23 dvdszrcl 
 |-  ( N || M -> ( N e. ZZ /\ M e. ZZ ) )
24 23 simprd 
 |-  ( N || M -> M e. ZZ )
25 0dvds 
 |-  ( M e. ZZ -> ( 0 || M <-> M = 0 ) )
26 24 25 syl 
 |-  ( N || M -> ( 0 || M <-> M = 0 ) )
27 22 26 sylan9bbr 
 |-  ( ( N || M /\ N = 0 ) -> ( N || M <-> M = 0 ) )
28 21 27 mpbid 
 |-  ( ( N || M /\ N = 0 ) -> M = 0 )
29 28 breq1d 
 |-  ( ( N || M /\ N = 0 ) -> ( M || x <-> 0 || x ) )
30 0dvds 
 |-  ( x e. ZZ -> ( 0 || x <-> x = 0 ) )
31 29 30 sylan9bb 
 |-  ( ( ( N || M /\ N = 0 ) /\ x e. ZZ ) -> ( M || x <-> x = 0 ) )
32 31 rabbidva 
 |-  ( ( N || M /\ N = 0 ) -> { x e. ZZ | M || x } = { x e. ZZ | x = 0 } )
33 0z 
 |-  0 e. ZZ
34 rabsn 
 |-  ( 0 e. ZZ -> { x e. ZZ | x = 0 } = { 0 } )
35 33 34 ax-mp 
 |-  { x e. ZZ | x = 0 } = { 0 }
36 32 35 eqtrdi 
 |-  ( ( N || M /\ N = 0 ) -> { x e. ZZ | M || x } = { 0 } )
37 breq1 
 |-  ( N = 0 -> ( N || x <-> 0 || x ) )
38 37 rabbidv 
 |-  ( N = 0 -> { x e. ZZ | N || x } = { x e. ZZ | 0 || x } )
39 30 rabbiia 
 |-  { x e. ZZ | 0 || x } = { x e. ZZ | x = 0 }
40 39 35 eqtri 
 |-  { x e. ZZ | 0 || x } = { 0 }
41 38 40 eqtrdi 
 |-  ( N = 0 -> { x e. ZZ | N || x } = { 0 } )
42 41 adantl 
 |-  ( ( N || M /\ N = 0 ) -> { x e. ZZ | N || x } = { 0 } )
43 36 42 sseq12d 
 |-  ( ( N || M /\ N = 0 ) -> ( { x e. ZZ | M || x } C_ { x e. ZZ | N || x } <-> { 0 } C_ { 0 } ) )
44 20 43 mpbiri 
 |-  ( ( N || M /\ N = 0 ) -> { x e. ZZ | M || x } C_ { x e. ZZ | N || x } )
45 24 zcnd 
 |-  ( N || M -> M e. CC )
46 45 ad2antrr 
 |-  ( ( ( N || M /\ N =/= 0 ) /\ n e. ZZ ) -> M e. CC )
47 23 simpld 
 |-  ( N || M -> N e. ZZ )
48 47 zcnd 
 |-  ( N || M -> N e. CC )
49 48 ad2antrr 
 |-  ( ( ( N || M /\ N =/= 0 ) /\ n e. ZZ ) -> N e. CC )
50 simplr 
 |-  ( ( ( N || M /\ N =/= 0 ) /\ n e. ZZ ) -> N =/= 0 )
51 46 49 50 divcan2d 
 |-  ( ( ( N || M /\ N =/= 0 ) /\ n e. ZZ ) -> ( N x. ( M / N ) ) = M )
52 51 breq1d 
 |-  ( ( ( N || M /\ N =/= 0 ) /\ n e. ZZ ) -> ( ( N x. ( M / N ) ) || n <-> M || n ) )
53 47 adantr 
 |-  ( ( N || M /\ N =/= 0 ) -> N e. ZZ )
54 dvdsval2 
 |-  ( ( N e. ZZ /\ N =/= 0 /\ M e. ZZ ) -> ( N || M <-> ( M / N ) e. ZZ ) )
55 54 biimpd 
 |-  ( ( N e. ZZ /\ N =/= 0 /\ M e. ZZ ) -> ( N || M -> ( M / N ) e. ZZ ) )
56 55 3com23 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ N =/= 0 ) -> ( N || M -> ( M / N ) e. ZZ ) )
57 56 3expa 
 |-  ( ( ( N e. ZZ /\ M e. ZZ ) /\ N =/= 0 ) -> ( N || M -> ( M / N ) e. ZZ ) )
58 23 57 sylan 
 |-  ( ( N || M /\ N =/= 0 ) -> ( N || M -> ( M / N ) e. ZZ ) )
59 58 imp 
 |-  ( ( ( N || M /\ N =/= 0 ) /\ N || M ) -> ( M / N ) e. ZZ )
60 59 anabss1 
 |-  ( ( N || M /\ N =/= 0 ) -> ( M / N ) e. ZZ )
61 53 60 jca 
 |-  ( ( N || M /\ N =/= 0 ) -> ( N e. ZZ /\ ( M / N ) e. ZZ ) )
62 muldvds1 
 |-  ( ( N e. ZZ /\ ( M / N ) e. ZZ /\ n e. ZZ ) -> ( ( N x. ( M / N ) ) || n -> N || n ) )
63 62 3expa 
 |-  ( ( ( N e. ZZ /\ ( M / N ) e. ZZ ) /\ n e. ZZ ) -> ( ( N x. ( M / N ) ) || n -> N || n ) )
64 61 63 sylan 
 |-  ( ( ( N || M /\ N =/= 0 ) /\ n e. ZZ ) -> ( ( N x. ( M / N ) ) || n -> N || n ) )
65 52 64 sylbird 
 |-  ( ( ( N || M /\ N =/= 0 ) /\ n e. ZZ ) -> ( M || n -> N || n ) )
66 65 ss2rabdv 
 |-  ( ( N || M /\ N =/= 0 ) -> { n e. ZZ | M || n } C_ { n e. ZZ | N || n } )
67 breq2 
 |-  ( n = x -> ( M || n <-> M || x ) )
68 67 cbvrabv 
 |-  { n e. ZZ | M || n } = { x e. ZZ | M || x }
69 breq2 
 |-  ( n = x -> ( N || n <-> N || x ) )
70 69 cbvrabv 
 |-  { n e. ZZ | N || n } = { x e. ZZ | N || x }
71 66 68 70 3sstr3g 
 |-  ( ( N || M /\ N =/= 0 ) -> { x e. ZZ | M || x } C_ { x e. ZZ | N || x } )
72 44 71 pm2.61dane 
 |-  ( N || M -> { x e. ZZ | M || x } C_ { x e. ZZ | N || x } )
73 breq1 
 |-  ( n = M -> ( n || x <-> M || x ) )
74 73 rabbidv 
 |-  ( n = M -> { x e. ZZ | n || x } = { x e. ZZ | M || x } )
75 73 abbidv 
 |-  ( n = M -> { x | n || x } = { x | M || x } )
76 74 75 eqeq12d 
 |-  ( n = M -> ( { x e. ZZ | n || x } = { x | n || x } <-> { x e. ZZ | M || x } = { x | M || x } ) )
77 simpr 
 |-  ( ( y e. ZZ /\ n || y ) -> n || y )
78 dvdszrcl 
 |-  ( n || y -> ( n e. ZZ /\ y e. ZZ ) )
79 78 simprd 
 |-  ( n || y -> y e. ZZ )
80 79 ancri 
 |-  ( n || y -> ( y e. ZZ /\ n || y ) )
81 77 80 impbii 
 |-  ( ( y e. ZZ /\ n || y ) <-> n || y )
82 breq2 
 |-  ( x = y -> ( n || x <-> n || y ) )
83 82 elrab 
 |-  ( y e. { x e. ZZ | n || x } <-> ( y e. ZZ /\ n || y ) )
84 vex 
 |-  y e. _V
85 84 82 elab 
 |-  ( y e. { x | n || x } <-> n || y )
86 81 83 85 3bitr4i 
 |-  ( y e. { x e. ZZ | n || x } <-> y e. { x | n || x } )
87 86 eqriv 
 |-  { x e. ZZ | n || x } = { x | n || x }
88 76 87 vtoclg 
 |-  ( M e. ZZ -> { x e. ZZ | M || x } = { x | M || x } )
89 88 adantr 
 |-  ( ( M e. ZZ /\ N e. V ) -> { x e. ZZ | M || x } = { x | M || x } )
90 breq1 
 |-  ( n = N -> ( n || x <-> N || x ) )
91 90 rabbidv 
 |-  ( n = N -> { x e. ZZ | n || x } = { x e. ZZ | N || x } )
92 90 abbidv 
 |-  ( n = N -> { x | n || x } = { x | N || x } )
93 91 92 eqeq12d 
 |-  ( n = N -> ( { x e. ZZ | n || x } = { x | n || x } <-> { x e. ZZ | N || x } = { x | N || x } ) )
94 93 87 vtoclg 
 |-  ( N e. V -> { x e. ZZ | N || x } = { x | N || x } )
95 94 adantl 
 |-  ( ( M e. ZZ /\ N e. V ) -> { x e. ZZ | N || x } = { x | N || x } )
96 89 95 sseq12d 
 |-  ( ( M e. ZZ /\ N e. V ) -> ( { x e. ZZ | M || x } C_ { x e. ZZ | N || x } <-> { x | M || x } C_ { x | N || x } ) )
97 72 96 imbitrid 
 |-  ( ( M e. ZZ /\ N e. V ) -> ( N || M -> { x | M || x } C_ { x | N || x } ) )
98 9 15 sseq12i 
 |-  ( ( || " { M } ) C_ ( || " { N } ) <-> { x | M || x } C_ { x | N || x } )
99 97 98 imbitrrdi 
 |-  ( ( M e. ZZ /\ N e. V ) -> ( N || M -> ( || " { M } ) C_ ( || " { N } ) ) )
100 19 99 impbid 
 |-  ( ( M e. ZZ /\ N e. V ) -> ( ( || " { M } ) C_ ( || " { N } ) <-> N || M ) )
101 1 2 100 syl2anc 
 |-  ( ph -> ( ( || " { M } ) C_ ( || " { N } ) <-> N || M ) )