lcmf

Description: Characterization of the least common multiple of a set of integers (without 0): A positiven integer is the least common multiple of a set of integers iff it divides each of the elements of the set and every integer which divides each of the elements of the set is greater than or equal to this integer. (Contributed by AV, 22-Aug-2020)

		Ref	Expression
	Assertion	lcmf	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (K = \underline{lcm} (Z) \leftrightarrow (\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)))$

Proof

Step	Hyp	Ref	Expression
1		dvdslcmf	$⊢ (Z \subseteq ℤ \land Z \in Fin) \to \forall m \in Z m ∥ \underline{lcm} (Z)$
2	1	3adant3	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \forall m \in Z m ∥ \underline{lcm} (Z)$
3		lcmfledvds	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to ((k \in ℕ \land \forall m \in Z m ∥ k) \to \underline{lcm} (Z) \leq k)$
4	3	expdimp	$⊢ ((Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \land k \in ℕ) \to (\forall m \in Z m ∥ k \to \underline{lcm} (Z) \leq k)$
5	4	ralrimiva	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \forall k \in ℕ (\forall m \in Z m ∥ k \to \underline{lcm} (Z) \leq k)$
6	2 5	jca	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to (\forall m \in Z m ∥ \underline{lcm} (Z) \land \forall k \in ℕ (\forall m \in Z m ∥ k \to \underline{lcm} (Z) \leq k))$
7	6	adantl	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (\forall m \in Z m ∥ \underline{lcm} (Z) \land \forall k \in ℕ (\forall m \in Z m ∥ k \to \underline{lcm} (Z) \leq k))$
8		breq2	$⊢ K = \underline{lcm} (Z) \to (m ∥ K \leftrightarrow m ∥ \underline{lcm} (Z))$
9	8	ralbidv	$⊢ K = \underline{lcm} (Z) \to (\forall m \in Z m ∥ K \leftrightarrow \forall m \in Z m ∥ \underline{lcm} (Z))$
10		breq1	$⊢ K = \underline{lcm} (Z) \to (K \leq k \leftrightarrow \underline{lcm} (Z) \leq k)$
11	10	imbi2d	$⊢ K = \underline{lcm} (Z) \to ((\forall m \in Z m ∥ k \to K \leq k) \leftrightarrow (\forall m \in Z m ∥ k \to \underline{lcm} (Z) \leq k))$
12	11	ralbidv	$⊢ K = \underline{lcm} (Z) \to (\forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k) \leftrightarrow \forall k \in ℕ (\forall m \in Z m ∥ k \to \underline{lcm} (Z) \leq k))$
13	9 12	anbi12d	$⊢ K = \underline{lcm} (Z) \to ((\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \leftrightarrow (\forall m \in Z m ∥ \underline{lcm} (Z) \land \forall k \in ℕ (\forall m \in Z m ∥ k \to \underline{lcm} (Z) \leq k)))$
14	7 13	syl5ibrcom	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (K = \underline{lcm} (Z) \to (\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)))$
15		lcmfn0cl	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \underline{lcm} (Z) \in ℕ$
16	15	adantl	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to \underline{lcm} (Z) \in ℕ$
17		breq2	$⊢ k = \underline{lcm} (Z) \to (m ∥ k \leftrightarrow m ∥ \underline{lcm} (Z))$
18	17	ralbidv	$⊢ k = \underline{lcm} (Z) \to (\forall m \in Z m ∥ k \leftrightarrow \forall m \in Z m ∥ \underline{lcm} (Z))$
19		breq2	$⊢ k = \underline{lcm} (Z) \to (K \leq k \leftrightarrow K \leq \underline{lcm} (Z))$
20	18 19	imbi12d	$⊢ k = \underline{lcm} (Z) \to ((\forall m \in Z m ∥ k \to K \leq k) \leftrightarrow (\forall m \in Z m ∥ \underline{lcm} (Z) \to K \leq \underline{lcm} (Z)))$
21	20	rspcv	$⊢ \underline{lcm} (Z) \in ℕ \to (\forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k) \to (\forall m \in Z m ∥ \underline{lcm} (Z) \to K \leq \underline{lcm} (Z)))$
22	16 21	syl	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (\forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k) \to (\forall m \in Z m ∥ \underline{lcm} (Z) \to K \leq \underline{lcm} (Z)))$
23	22	adantld	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to ((\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \to (\forall m \in Z m ∥ \underline{lcm} (Z) \to K \leq \underline{lcm} (Z)))$
24	2	adantl	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to \forall m \in Z m ∥ \underline{lcm} (Z)$
25		nnre	$⊢ K \in ℕ \to K \in ℝ$
26	15	nnred	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to \underline{lcm} (Z) \in ℝ$
27		leloe	$⊢ (K \in ℝ \land \underline{lcm} (Z) \in ℝ) \to (K \leq \underline{lcm} (Z) \leftrightarrow (K < \underline{lcm} (Z) \lor K = \underline{lcm} (Z)))$
28	25 26 27	syl2an	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (K \leq \underline{lcm} (Z) \leftrightarrow (K < \underline{lcm} (Z) \lor K = \underline{lcm} (Z)))$
29		lcmfledvds	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to ((K \in ℕ \land \forall m \in Z m ∥ K) \to \underline{lcm} (Z) \leq K)$
30	29	expd	$⊢ (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z) \to (K \in ℕ \to (\forall m \in Z m ∥ K \to \underline{lcm} (Z) \leq K))$
31	30	impcom	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (\forall m \in Z m ∥ K \to \underline{lcm} (Z) \leq K)$
32		lenlt	$⊢ (\underline{lcm} (Z) \in ℝ \land K \in ℝ) \to (\underline{lcm} (Z) \leq K \leftrightarrow \neg K < \underline{lcm} (Z))$
33	26 25 32	syl2anr	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (\underline{lcm} (Z) \leq K \leftrightarrow \neg K < \underline{lcm} (Z))$
34		pm2.21	$⊢ \neg K < \underline{lcm} (Z) \to (K < \underline{lcm} (Z) \to K = \underline{lcm} (Z))$
35	33 34	syl6bi	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (\underline{lcm} (Z) \leq K \to (K < \underline{lcm} (Z) \to K = \underline{lcm} (Z)))$
36	31 35	syldc	$⊢ \forall m \in Z m ∥ K \to ((K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (K < \underline{lcm} (Z) \to K = \underline{lcm} (Z)))$
37	36	adantr	$⊢ (\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \to ((K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (K < \underline{lcm} (Z) \to K = \underline{lcm} (Z)))$
38	37	com13	$⊢ K < \underline{lcm} (Z) \to ((K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to ((\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \to K = \underline{lcm} (Z)))$
39		2a1	$⊢ K = \underline{lcm} (Z) \to ((K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to ((\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \to K = \underline{lcm} (Z)))$
40	38 39	jaoi	$⊢ (K < \underline{lcm} (Z) \lor K = \underline{lcm} (Z)) \to ((K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to ((\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \to K = \underline{lcm} (Z)))$
41	40	com12	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to ((K < \underline{lcm} (Z) \lor K = \underline{lcm} (Z)) \to ((\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \to K = \underline{lcm} (Z)))$
42	28 41	sylbid	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (K \leq \underline{lcm} (Z) \to ((\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \to K = \underline{lcm} (Z)))$
43	24 42	embantd	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to ((\forall m \in Z m ∥ \underline{lcm} (Z) \to K \leq \underline{lcm} (Z)) \to ((\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \to K = \underline{lcm} (Z)))$
44	43	com23	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to ((\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \to ((\forall m \in Z m ∥ \underline{lcm} (Z) \to K \leq \underline{lcm} (Z)) \to K = \underline{lcm} (Z)))$
45	23 44	mpdd	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to ((\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)) \to K = \underline{lcm} (Z))$
46	14 45	impbid	$⊢ (K \in ℕ \land (Z \subseteq ℤ \land Z \in Fin \land 0 \notin Z)) \to (K = \underline{lcm} (Z) \leftrightarrow (\forall m \in Z m ∥ K \land \forall k \in ℕ (\forall m \in Z m ∥ k \to K \leq k)))$

Metamath Proof Explorer

Theorem lcmf

Proof