lcmcllem

Description: Lemma for lcmn0cl and dvdslcm . (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

		Ref	Expression
	Assertion	lcmcllem	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to M lcm N \in \{n \in ℕ \| (M ∥ n \land N ∥ n)\}$

Proof

Step	Hyp	Ref	Expression
1		lcmn0val	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to M lcm N = inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <)$
2		ssrab2	$⊢ \{n \in ℕ \| (M ∥ n \land N ∥ n)\} \subseteq ℕ$
3		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
4	2 3	sseqtri	$⊢ \{n \in ℕ \| (M ∥ n \land N ∥ n)\} \subseteq ℤ_{\geq 1}$
5		zmulcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \cdot N \in ℤ$
6	5	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to M \cdot N \in ℤ$
7		zcn	$⊢ M \in ℤ \to M \in ℂ$
8		zcn	$⊢ N \in ℤ \to N \in ℂ$
9	7 8	anim12i	$⊢ (M \in ℤ \land N \in ℤ) \to (M \in ℂ \land N \in ℂ)$
10		ioran	$⊢ \neg (M = 0 \lor N = 0) \leftrightarrow (\neg M = 0 \land \neg N = 0)$
11		df-ne	$⊢ M \neq 0 \leftrightarrow \neg M = 0$
12		df-ne	$⊢ N \neq 0 \leftrightarrow \neg N = 0$
13	11 12	anbi12i	$⊢ (M \neq 0 \land N \neq 0) \leftrightarrow (\neg M = 0 \land \neg N = 0)$
14	10 13	sylbb2	$⊢ \neg (M = 0 \lor N = 0) \to (M \neq 0 \land N \neq 0)$
15		mulne0	$⊢ ((M \in ℂ \land M \neq 0) \land (N \in ℂ \land N \neq 0)) \to M \cdot N \neq 0$
16	15	an4s	$⊢ ((M \in ℂ \land N \in ℂ) \land (M \neq 0 \land N \neq 0)) \to M \cdot N \neq 0$
17	9 14 16	syl2an	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to M \cdot N \neq 0$
18		nnabscl	$⊢ (M \cdot N \in ℤ \land M \cdot N \neq 0) \to \|M \cdot N\| \in ℕ$
19	6 17 18	syl2anc	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to \|M \cdot N\| \in ℕ$
20		dvdsmul1	$⊢ (M \in ℤ \land N \in ℤ) \to M ∥ M \cdot N$
21		dvdsabsb	$⊢ (M \in ℤ \land M \cdot N \in ℤ) \to (M ∥ M \cdot N \leftrightarrow M ∥ \|M \cdot N\|)$
22	5 21	syldan	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ M \cdot N \leftrightarrow M ∥ \|M \cdot N\|)$
23	20 22	mpbid	$⊢ (M \in ℤ \land N \in ℤ) \to M ∥ \|M \cdot N\|$
24		dvdsmul2	$⊢ (M \in ℤ \land N \in ℤ) \to N ∥ M \cdot N$
25		dvdsabsb	$⊢ (N \in ℤ \land M \cdot N \in ℤ) \to (N ∥ M \cdot N \leftrightarrow N ∥ \|M \cdot N\|)$
26	5 25	sylan2	$⊢ (N \in ℤ \land (M \in ℤ \land N \in ℤ)) \to (N ∥ M \cdot N \leftrightarrow N ∥ \|M \cdot N\|)$
27	26	anabss7	$⊢ (M \in ℤ \land N \in ℤ) \to (N ∥ M \cdot N \leftrightarrow N ∥ \|M \cdot N\|)$
28	24 27	mpbid	$⊢ (M \in ℤ \land N \in ℤ) \to N ∥ \|M \cdot N\|$
29	23 28	jca	$⊢ (M \in ℤ \land N \in ℤ) \to (M ∥ \|M \cdot N\| \land N ∥ \|M \cdot N\|)$
30	29	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to (M ∥ \|M \cdot N\| \land N ∥ \|M \cdot N\|)$
31		breq2	$⊢ n = \|M \cdot N\| \to (M ∥ n \leftrightarrow M ∥ \|M \cdot N\|)$
32		breq2	$⊢ n = \|M \cdot N\| \to (N ∥ n \leftrightarrow N ∥ \|M \cdot N\|)$
33	31 32	anbi12d	$⊢ n = \|M \cdot N\| \to ((M ∥ n \land N ∥ n) \leftrightarrow (M ∥ \|M \cdot N\| \land N ∥ \|M \cdot N\|))$
34	33	rspcev	$⊢ (\|M \cdot N\| \in ℕ \land (M ∥ \|M \cdot N\| \land N ∥ \|M \cdot N\|)) \to \exists n \in ℕ (M ∥ n \land N ∥ n)$
35	19 30 34	syl2anc	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to \exists n \in ℕ (M ∥ n \land N ∥ n)$
36		rabn0	$⊢ \{n \in ℕ \| (M ∥ n \land N ∥ n)\} \neq \emptyset \leftrightarrow \exists n \in ℕ (M ∥ n \land N ∥ n)$
37	35 36	sylibr	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to \{n \in ℕ \| (M ∥ n \land N ∥ n)\} \neq \emptyset$
38		infssuzcl	$⊢ (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} \subseteq ℤ_{\geq 1} \land \{n \in ℕ \| (M ∥ n \land N ∥ n)\} \neq \emptyset) \to inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <) \in \{n \in ℕ \| (M ∥ n \land N ∥ n)\}$
39	4 37 38	sylancr	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to inf (\{n \in ℕ \| (M ∥ n \land N ∥ n)\} ℝ <) \in \{n \in ℕ \| (M ∥ n \land N ∥ n)\}$
40	1 39	eqeltrd	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \lor N = 0)) \to M lcm N \in \{n \in ℕ \| (M ∥ n \land N ∥ n)\}$

Metamath Proof Explorer

Theorem lcmcllem

Proof