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 imbitrid ⊢ 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 imbitrrdi ⊢ 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