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	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	nzss.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
Assertion	nzss	⊢ ( 𝜑 → ( ( ∥ “ { 𝑀 } ) ⊆ ( ∥ “ { 𝑁 } ) ↔ 𝑁 ∥ 𝑀 ) )

Proof

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