Theorem nzin

Description: The intersection of the set of multiples ofm, mℤ, and those ofn, nℤ, is the set of multiples of their least common multiple. Roughly Lemma 2.1(c) of https://www.mscs.dal.ca/~selinger/3343/handouts/ideals.pdf p. 5 and Problem 1(b) of https://people.math.binghamton.edu/mazur/teach/40107/40107h16sol.pdf p. 1, with mℤ and nℤ as images of the divides relation under m andn. (Contributed by Steve Rodriguez, 20-Jan-2020)

	Ref	Expression
Hypotheses	nzin.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	nzin.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion	nzin	⊢ ( 𝜑 → ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) = ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		nzin.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		nzin.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
3		dvdszrcl	⊢ ( 𝑀 ∥ 𝑛 → ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) )
4		dvdszrcl	⊢ ( 𝑁 ∥ 𝑛 → ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) )
5	3 4	anim12i	⊢ ( ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) )
6		anandir	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) ↔ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) ) )
7	5 6	sylibr	⊢ ( ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑛 ∈ ℤ ) )
8	7	ancomd	⊢ ( ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) → ( 𝑛 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) )
9		lcmdvds	⊢ ( ( 𝑛 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) → ( 𝑀 lcm 𝑁 ) ∥ 𝑛 ) )
10	9	3expb	⊢ ( ( 𝑛 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) → ( 𝑀 lcm 𝑁 ) ∥ 𝑛 ) )
11	8 10	mpcom	⊢ ( ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) → ( 𝑀 lcm 𝑁 ) ∥ 𝑛 )
12		elin	⊢ ( 𝑛 ∈ ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) ↔ ( 𝑛 ∈ ( ∥ “ { 𝑀 } ) ∧ 𝑛 ∈ ( ∥ “ { 𝑁 } ) ) )
13		reldvds	⊢ Rel ∥
14		elrelimasn	⊢ ( Rel ∥ → ( 𝑛 ∈ ( ∥ “ { 𝑀 } ) ↔ 𝑀 ∥ 𝑛 ) )
15	13 14	ax-mp	⊢ ( 𝑛 ∈ ( ∥ “ { 𝑀 } ) ↔ 𝑀 ∥ 𝑛 )
16		elrelimasn	⊢ ( Rel ∥ → ( 𝑛 ∈ ( ∥ “ { 𝑁 } ) ↔ 𝑁 ∥ 𝑛 ) )
17	13 16	ax-mp	⊢ ( 𝑛 ∈ ( ∥ “ { 𝑁 } ) ↔ 𝑁 ∥ 𝑛 )
18	15 17	anbi12i	⊢ ( ( 𝑛 ∈ ( ∥ “ { 𝑀 } ) ∧ 𝑛 ∈ ( ∥ “ { 𝑁 } ) ) ↔ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) )
19	12 18	bitri	⊢ ( 𝑛 ∈ ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) ↔ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) )
20		elrelimasn	⊢ ( Rel ∥ → ( 𝑛 ∈ ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) ↔ ( 𝑀 lcm 𝑁 ) ∥ 𝑛 ) )
21	13 20	ax-mp	⊢ ( 𝑛 ∈ ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) ↔ ( 𝑀 lcm 𝑁 ) ∥ 𝑛 )
22	11 19 21	3imtr4i	⊢ ( 𝑛 ∈ ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) → 𝑛 ∈ ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) )
23	22	ssriv	⊢ ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) ⊆ ( ∥ “ { ( 𝑀 lcm 𝑁 ) } )
24	23	a1i	⊢ ( 𝜑 → ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) ⊆ ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) )
25		dvdslcm	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ∧ 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ) )
26	1 2 25	syl2anc	⊢ ( 𝜑 → ( 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ∧ 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ) )
27	26	simpld	⊢ ( 𝜑 → 𝑀 ∥ ( 𝑀 lcm 𝑁 ) )
28		lcmcl	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 )
29	1 2 28	syl2anc	⊢ ( 𝜑 → ( 𝑀 lcm 𝑁 ) ∈ ℕ0 )
30	29	nn0zd	⊢ ( 𝜑 → ( 𝑀 lcm 𝑁 ) ∈ ℤ )
31	30 1	nzss	⊢ ( 𝜑 → ( ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) ⊆ ( ∥ “ { 𝑀 } ) ↔ 𝑀 ∥ ( 𝑀 lcm 𝑁 ) ) )
32	27 31	mpbird	⊢ ( 𝜑 → ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) ⊆ ( ∥ “ { 𝑀 } ) )
33	26	simprd	⊢ ( 𝜑 → 𝑁 ∥ ( 𝑀 lcm 𝑁 ) )
34	30 2	nzss	⊢ ( 𝜑 → ( ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) ⊆ ( ∥ “ { 𝑁 } ) ↔ 𝑁 ∥ ( 𝑀 lcm 𝑁 ) ) )
35	33 34	mpbird	⊢ ( 𝜑 → ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) ⊆ ( ∥ “ { 𝑁 } ) )
36	32 35	ssind	⊢ ( 𝜑 → ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) ⊆ ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) )
37	24 36	eqssd	⊢ ( 𝜑 → ( ( ∥ “ { 𝑀 } ) ∩ ( ∥ “ { 𝑁 } ) ) = ( ∥ “ { ( 𝑀 lcm 𝑁 ) } ) )