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 φ M
nzss.n φ N V
Assertion nzss φ M N N M

Proof

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