This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lcmflefac

Description: The least common multiple of all positive integers less than or equal to an integer is less than or equal to the factorial of the integer. (Contributed by AV, 16-Aug-2020) (Revised by AV, 27-Aug-2020)

		Ref	Expression
	Assertion	lcmflefac	$⊢ N \in ℕ \to \underline{lcm} ((1 \dots N)) \leq N!$

Proof

Step	Hyp	Ref	Expression
1		fzssz	$⊢ (1 \dots N) \subseteq ℤ$
2	1	a1i	$⊢ N \in ℕ \to (1 \dots N) \subseteq ℤ$
3		fzfid	$⊢ N \in ℕ \to (1 \dots N) \in Fin$
4		0nelfz1	$⊢ 0 \notin (1 \dots N)$
5	4	a1i	$⊢ N \in ℕ \to 0 \notin (1 \dots N)$
6	2 3 5	3jca	$⊢ N \in ℕ \to ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin \land 0 \notin (1 \dots N))$
7		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
8	7	faccld	$⊢ N \in ℕ \to N! \in ℕ$
9		elfznn	$⊢ m \in (1 \dots N) \to m \in ℕ$
10		elfzuz3	$⊢ m \in (1 \dots N) \to N \in ℤ_{\geq m}$
11	10	adantl	$⊢ (N \in ℕ \land m \in (1 \dots N)) \to N \in ℤ_{\geq m}$
12		dvdsfac	$⊢ (m \in ℕ \land N \in ℤ_{\geq m}) \to m ∥ N!$
13	9 11 12	syl2an2	$⊢ (N \in ℕ \land m \in (1 \dots N)) \to m ∥ N!$
14	13	ralrimiva	$⊢ N \in ℕ \to \forall m \in (1 \dots N) m ∥ N!$
15	8 14	jca	$⊢ N \in ℕ \to (N! \in ℕ \land \forall m \in (1 \dots N) m ∥ N!)$
16		lcmfledvds	$⊢ ((1 \dots N) \subseteq ℤ \land (1 \dots N) \in Fin \land 0 \notin (1 \dots N)) \to ((N! \in ℕ \land \forall m \in (1 \dots N) m ∥ N!) \to \underline{lcm} ((1 \dots N)) \leq N!)$
17	6 15 16	sylc	$⊢ N \in ℕ \to \underline{lcm} ((1 \dots N)) \leq N!$