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⁢MN=M
52 51 breq1d ⊢N∥M∧N≠0∧n∈ℤ→N⁢MN∥n↔M∥n
53 47 adantr ⊢N∥M∧N≠0→N∈ℤ
54 dvdsval2 ⊢N∈ℤ∧N≠0∧M∈ℤ→N∥M↔MN∈ℤ
55 54 biimpd ⊢N∈ℤ∧N≠0∧M∈ℤ→N∥M→MN∈ℤ
56 55 3com23 ⊢N∈ℤ∧M∈ℤ∧N≠0→N∥M→MN∈ℤ
57 56 3expa ⊢N∈ℤ∧M∈ℤ∧N≠0→N∥M→MN∈ℤ
58 23 57 sylan ⊢N∥M∧N≠0→N∥M→MN∈ℤ
59 58 imp ⊢N∥M∧N≠0∧N∥M→MN∈ℤ
60 59 anabss1 ⊢N∥M∧N≠0→MN∈ℤ
61 53 60 jca ⊢N∥M∧N≠0→N∈ℤ∧MN∈ℤ
62 muldvds1 ⊢N∈ℤ∧MN∈ℤ∧n∈ℤ→N⁢MN∥n→N∥n
63 62 3expa ⊢N∈ℤ∧MN∈ℤ∧n∈ℤ→N⁢MN∥n→N∥n
64 61 63 sylan ⊢N∥M∧N≠0∧n∈ℤ→N⁢MN∥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 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