nzin

	Ref	Expression
Hypotheses	nzin.m	$⊢ φ \to M \in ℤ$
	nzin.n	$⊢ φ \to N \in ℤ$
Assertion	nzin	$⊢ φ \to ∥ [\{M\}] \cap ∥ [\{N\}] = ∥ [\{M lcm N\}]$

Proof

Step	Hyp	Ref	Expression
1		nzin.m	$⊢ φ \to M \in ℤ$
2		nzin.n	$⊢ φ \to N \in ℤ$
3		dvdszrcl	$⊢ M ∥ n \to (M \in ℤ \land n \in ℤ)$
4		dvdszrcl	$⊢ N ∥ n \to (N \in ℤ \land n \in ℤ)$
5	3 4	anim12i	$⊢ (M ∥ n \land N ∥ n) \to ((M \in ℤ \land n \in ℤ) \land (N \in ℤ \land n \in ℤ))$
6		anandir	$⊢ ((M \in ℤ \land N \in ℤ) \land n \in ℤ) \leftrightarrow ((M \in ℤ \land n \in ℤ) \land (N \in ℤ \land n \in ℤ))$
7	5 6	sylibr	$⊢ (M ∥ n \land N ∥ n) \to ((M \in ℤ \land N \in ℤ) \land n \in ℤ)$
8	7	ancomd	$⊢ (M ∥ n \land N ∥ n) \to (n \in ℤ \land (M \in ℤ \land N \in ℤ))$
9		lcmdvds	$⊢ (n \in ℤ \land M \in ℤ \land N \in ℤ) \to ((M ∥ n \land N ∥ n) \to (M lcm N) ∥ n)$
10	9	3expb	$⊢ (n \in ℤ \land (M \in ℤ \land N \in ℤ)) \to ((M ∥ n \land N ∥ n) \to (M lcm N) ∥ n)$
11	8 10	mpcom	$⊢ (M ∥ n \land N ∥ n) \to (M lcm N) ∥ n$
12		elin	$⊢ n \in (∥ [\{M\}] \cap ∥ [\{N\}]) \leftrightarrow (n \in ∥ [\{M\}] \land n \in ∥ [\{N\}])$
13		reldvds	$⊢ Rel ∥$
14		elrelimasn	$⊢ Rel ∥ \to (n \in ∥ [\{M\}] \leftrightarrow M ∥ n)$
15	13 14	ax-mp	$⊢ n \in ∥ [\{M\}] \leftrightarrow M ∥ n$
16		elrelimasn	$⊢ Rel ∥ \to (n \in ∥ [\{N\}] \leftrightarrow N ∥ n)$
17	13 16	ax-mp	$⊢ n \in ∥ [\{N\}] \leftrightarrow N ∥ n$
18	15 17	anbi12i	$⊢ (n \in ∥ [\{M\}] \land n \in ∥ [\{N\}]) \leftrightarrow (M ∥ n \land N ∥ n)$
19	12 18	bitri	$⊢ n \in (∥ [\{M\}] \cap ∥ [\{N\}]) \leftrightarrow (M ∥ n \land N ∥ n)$
20		elrelimasn	$⊢ Rel ∥ \to (n \in ∥ [\{M lcm N\}] \leftrightarrow (M lcm N) ∥ n)$
21	13 20	ax-mp	$⊢ n \in ∥ [\{M lcm N\}] \leftrightarrow (M lcm N) ∥ n$
22	11 19 21	3imtr4i	$⊢ n \in (∥ [\{M\}] \cap ∥ [\{N\}]) \to n \in ∥ [\{M lcm N\}]$
23	22	ssriv	$⊢ ∥ [\{M\}] \cap ∥ [\{N\}] \subseteq ∥ [\{M lcm N\}]$
24	23	a1i	$⊢ φ \to ∥ [\{M\}] \cap ∥ [\{N\}] \subseteq ∥ [\{M lcm N\}]$
25		dvdslcm	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ (M lcm N) \land N ∥ (M lcm N))$
26	1 2 25	syl2anc	$⊢ φ \to (M ∥ (M lcm N) \land N ∥ (M lcm N))$
27	26	simpld	$⊢ φ \to M ∥ (M lcm N)$
28		lcmcl	$⊢ (M \in ℤ \land N \in ℤ) \to M lcm N \in ℕ_{0}$
29	1 2 28	syl2anc	$⊢ φ \to M lcm N \in ℕ_{0}$
30	29	nn0zd	$⊢ φ \to M lcm N \in ℤ$
31	30 1	nzss	$⊢ φ \to (∥ [\{M lcm N\}] \subseteq ∥ [\{M\}] \leftrightarrow M ∥ (M lcm N))$
32	27 31	mpbird	$⊢ φ \to ∥ [\{M lcm N\}] \subseteq ∥ [\{M\}]$
33	26	simprd	$⊢ φ \to N ∥ (M lcm N)$
34	30 2	nzss	$⊢ φ \to (∥ [\{M lcm N\}] \subseteq ∥ [\{N\}] \leftrightarrow N ∥ (M lcm N))$
35	33 34	mpbird	$⊢ φ \to ∥ [\{M lcm N\}] \subseteq ∥ [\{N\}]$
36	32 35	ssind	$⊢ φ \to ∥ [\{M lcm N\}] \subseteq ∥ [\{M\}] \cap ∥ [\{N\}]$
37	24 36	eqssd	$⊢ φ \to ∥ [\{M\}] \cap ∥ [\{N\}] = ∥ [\{M lcm N\}]$

Metamath Proof Explorer

Theorem nzin

Proof